diff options
Diffstat (limited to 'Error.txt')
| -rw-r--r-- | Error.txt | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/Error.txt b/Error.txt deleted file mode 100644 index 7aa836a..0000000 --- a/Error.txt +++ /dev/null @@ -1,16 +0,0 @@ -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 |