diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-04-11 13:37:03 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-04-11 13:37:03 +0200 |
| commit | 15deff4df111d86c84d808f1c9cc4e30013287d0 (patch) | |
| tree | bddc6a2389a8fb5b3c8d39898e992d184105e2fa /Error.txt | |
| parent | 4b2076e6016901cf55ba20cf68b344473ca26f56 (diff) | |
Formalisation of groups and monoids
The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time
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 |