faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksaspec Group =
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa sort s
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa ops 0:s;
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa -__ :s->s;
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa __+__ :s*s->s, assoc
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa forall x,y:s
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . x+(-x) = 0
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . x+0=x %(leftunit)%
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . 0+x=x %(rightunit)% %implied
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . 0+0=0 %(zero_plus)% %implied
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksaend
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksaspec Theorem =
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa sort s
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa ops 0:s
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa forall x,y:s . x = x %implied
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksaend
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksaspec CounterSatisfiable =
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa sort s
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa ops 0:s;
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa 1:s
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa forall x:s . x = 0
90cca9e16195966c60233151ef05c643e21a586dEugen Kuksa . not( 1 = 0 ) %implied
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksaend