diff options
Diffstat (limited to 'Error.txt')
| -rw-r--r-- | Error.txt | 16 |
1 files changed, 16 insertions, 0 deletions
@@ -0,0 +1,16 @@ +stack exec zf -- library/test.tex +Verification failed: prover found countermodel +fof(leftinverse_eq_rightinverse,conjecture,fa=fc). +fof(monoid_right,axiom,![XA]:(monoid(XA)=>![Xa]:(elem(Xa,s__carrier(XA))=>apply(s__mul(XA),pair(Xa,s__neutral(XA)))=Xa))). +fof(leftinverse_eq_rightinverse1,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=fc). +fof(leftinverse_eq_rightinverse2,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(fc,s__neutral(fG)))). +fof(leftinverse_eq_rightinverse3,axiom,fc=apply(s__mul(fG),pair(s__neutral(fG),fc))). +fof(leftinverse_eq_rightinverse4,axiom,fc=apply(s__mul(fG),pair(fc,s__neutral(fG)))). +fof(leftinverse_eq_rightinverse5,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(s__neutral(fG),fc))). +fof(leftinverse_eq_rightinverse6,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(fa,apply(s__mul(fG),pair(fb,fc))))). +fof(leftinverse_eq_rightinverse7,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(s__neutral(fG),fc))). +fof(leftinverse_eq_rightinverse8,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)). +fof(leftinverse_eq_rightinverse9,axiom,apply(s__mul(fG),pair(fb,fc))=s__neutral(fG)&elem(fc,s__carrier(fG))). +fof(leftinverse_eq_rightinverse10,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)&elem(fb,s__carrier(fG))). +fof(leftinverse_eq_rightinverse11,axiom,elem(fa,s__carrier(fG))). +fof(leftinverse_eq_rightinverse12,axiom,group(fG)).
\ No newline at end of file |