spec Group =
sort s
ops 0:s;
-__ :s->s;
__+__ :s*s->s, assoc
forall x,y:s
. x+(-x) = 0
. x+0=x %(leftunit)%
. 0+x=x %(rightunit)% %implied
. 0+0=0 %(zero_plus)% %implied
end
spec Theorem =
sort s
ops 0:s
forall x,y:s . x = x %implied
end
spec CounterSatisfiable =
sort s
ops 0:s;
1:s
forall x:s . x = 0
. not( 1 = 0 ) %implied
end