diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-03-31 18:59:35 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-03-31 18:59:35 +0200 |
| commit | 4b2076e6016901cf55ba20cf68b344473ca26f56 (patch) | |
| tree | 96d7ccaa015543a6416c6f3d380e5368c888f7e0 | |
| parent | 9abb88060e5bb6405e603dcbe499794e3e181040 (diff) | |
Report_in_text_file
Txt File Error.txt has been filled
| -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 |