From 6eee1352ccaf49c10217b8e8d58a47694b2e8b09 Mon Sep 17 00:00:00 2001 From: maxinemuxin Date: Mon, 31 Oct 2022 11:22:32 -0700 Subject: [PATCH] ab inverse proof --- .DS_Store | Bin 0 -> 6148 bytes __pycache__/element.cpython-39.pyc | Bin 2982 -> 2963 bytes __pycache__/group.cpython-39.pyc | Bin 2859 -> 2847 bytes __pycache__/integer.cpython-39.pyc | Bin 1919 -> 1900 bytes __pycache__/logicObjects.cpython-39.pyc | Bin 10916 -> 11051 bytes __pycache__/proof.cpython-39.pyc | Bin 24610 -> 26342 bytes abelian_proof.py | 6 +- element.py | 1 + group.py | 8 +- inverse_of_ab.py | 26 ++++ logicObjects.py | 34 ++++- proof.py | 169 +++++++++++++++-------- unique inverses.py => unique_inverses.py | 5 +- 13 files changed, 175 insertions(+), 74 deletions(-) create mode 100644 .DS_Store create mode 100644 inverse_of_ab.py rename unique inverses.py => unique_inverses.py (96%) diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..c8693d73e3c6d3cee28ba4ab753c69fd96de237e GIT binary patch literal 6148 zcmeHK%}xR_5S}72E5t}Vc`?~1An^@W0tXL9BM*SEEQncH74he`cVETCr}1Gt={M6x zm$JmfgE3}?v|qP7-%R^8-BKblt;O(ws6j*l3S+f~s>Jv`mldnHo^7C!7%}xJrVC1_ zx8kiGs(>o+*A(ErTgPtg(G@*n?|$vy-cg#xgESk!gFg?4D9v{=U5`@nUnIcb$QH9_ZS2(28rTjx0dGT2PpT=Y5AG~<`(e=W-JwGsm5I~jHRPLbbgV;+@htEahDI{G8=b8F_IneLvbe) zS=3q;Pz9D1*szZcKL0!G@BhmreNqKffq$idskXcA7N+FR)|JWeSsS99qp-1GZc!+x i+;J=oK8p8H#PBZU1~77%TSN~`{|JZ-TB!oRs=x>A9nqBl literal 0 HcmV?d00001 diff --git a/__pycache__/element.cpython-39.pyc b/__pycache__/element.cpython-39.pyc index 9dd07870d8bd880c7c5e15c64abdf83c53f375a5..b886ac39a663558fa5c5e6330ce14c846b63cf27 100644 GIT binary patch delta 151 zcmV;I0BHZF7n2taVGRum00000R%%jXXR!@c0xvi(RdZ!>b1!UZb!}mIX>MgNL}hbp zbZ>AkXKZg`VQejBZgy#MZ*Fa6Zged%FSDcqI069!lidV&0VtDI1;qg@lN$zo0V|W4 z2ABaalQIXZ0Sc4e2gw08lc)%(0XdUW32Ff~lf4PE0X>s(3YP&ulL-q$0X&mU3swUw F5C`lOE)oC$ delta 170 zcmV;b09F5!7p4~tVGRum00000{H0Z5oUsj60zykeI$TwAWpZ;|X>(y=V_ZaUcW!KN zVPtb$Q*d%=Zf77eFfuY+Qe|^xVRB<=TxV==Vqt78Wo~w9a&K;JWo~p_vylQg0s#V( z$^>@-CzC=2#Q`gm2nKxtDwBo=m;o-69|x-e36skQ$pJN!l?bT;IFmmKY5_EpstL0J YJd<7umjOSM_6kD*JCiyKRs$*!2g7+bj{pDw diff --git a/__pycache__/group.cpython-39.pyc b/__pycache__/group.cpython-39.pyc index e2a172cb03a186a0003a5ce74412d8008e0eae34..bb4010333cd72e10873b87f2c2b330df4a215dc8 100644 GIT binary patch delta 1023 zcmZuwOHUI~6u$S)vxRDrq+l(Er#fJ%JZuaaHb7*d4GFr@g{jO94oo}s&VY{$aZwZ3 z^|}W(Mq(m6SNa3|363i_?)(F;IA^8`G)^<$J#){!-#OxlA>aNfUVTpB}D_ zwK4;Au{BXF*ov*W#yxVI*t%`JCbrRJ4@}!!C045CE@&2w=y>b!%N-4_F2L*00faOp zk4VS>!P;PZ3ZNQjA!$;F?o&!a#U`7ID8s%EUIq7TvPuqU#WLhqx*#>SJevcqKjqSW zp9{a_I$O2sbEnQri`?G~yhdr=^&VH8Mpfk^X$CtRF5CzUso$PuZo;|G!A^B_t$gxBCAaJVm0$Z-Za z)FjA&TviKRCqsGa%_$vD#L`THfzoV{Z7POw-J>B5816M$B23*36!}w~F;#IE>9cZ3 z%gtd4Q5SbP7Fns*_{lucm#*_?ONn~~zI}{IXqxuRr&^IVE3aaG;ykcQF^z!pAaH6# zKSBZFBEl$wg>V(&8p0I948knJb%f*biLE}|!%4$`m_H0)GL^_bQ dJO*|$mH#1$%v&|j-g5aoMJAk(Jk3&*9Rb^r%g6u# delta 1058 zcmZvb%}*0S6u@U@Kk0`8sU=`RQBez4un;v$2uU@FiGKkOK4YI0PS{dc_CNDLQj#gA*ToONjULe2$T1Np96jGJ6Bte-g zTn$hIZ{Y^E@d3stkStV_*sS=f2^$G?7Am7dyp-3&&$uLO!ds}4#f1w(_`O(qU{rj{ ze8culbJKX_?YWL;TE0=PGuz#|T%0NvjTP!slWlGrTaLG3ItA+P+RSrzsLPG8K}K;d zd{34KQo`dQX8qz|;JuA(n3Bp@lkh$$kSDQ0q;*z8R+PdM z=Qw(e_!*dJ71anE;n)&W#K?X6az^M#fCte&Oqm2kNOB+rat7@yplL}WukXsiC581u zO4k6#8AdXrb(U9Ie;BIc$?iUURmZR%{!|~|g?Wfs^@$@dwI`x?TKytQ{gwWy!`3!O z<55n)#dg)K0O7mC{Lntm#pytHQD3JiU9*9NJ7L)^xPASsi%7R~5Gaq^g^isxSnqi@ z6lVfU#fHv){?fBtje8U40cEl&0IUy#C1V4Ci-2Lk6~GO^IN&y55^x7l1WW@?>Wrl< p==AVaVp4o vo|B)Hn4_DTSC(0npO>4OSE6gEzd4oh6ASAtrX<5#lVjL+Gs;btU{41CRVyCF delta 111 zcmaFE_n(h1k(ZZ?0SK61yC%tSZsZeXbn)5EKW>Jj&aE^&&$bAOeu~D zE-1>(OII*5Ffxh>N-a)JEK1IZNzchoO3cws%`3|+%FoM9%`1u79K`sEg*A#P$uMfN NC);jDnaQl|=>V%2Bv}9e diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc index 74f4fb559e721d9de4496a273a359fe7212a23e7..a913b8e379c0fb9e80bf6017374773cc179a412c 100644 GIT binary patch delta 1025 zcmY*YU1%It6u#g5?Eg-7lWaCgleB4Lx>K8MA{N2YAVgbip$6LoOr*;uJB_=W>~8N) z(>9%?)@b~Rg*HbY`XJOF1eHR{()LABR1gampI5C=6~zZZDX67_=f=Ev;eK<@`ObXz zF!!5xMn4#{ve9Tr@Cw%^rV`t)ShtYglOC-)vYMXBAD_*h%$J<>qfWKxmMiJ$net?I zrq3zOy+Fr52S1T+JrW<%o@{TLC;~q@C;XYqJSk7gz}(ds+bxu|_H6>6Z*odlL}rTI=sIV;l=8hQ2p;cA7HIN6LVLb_FIw z-IuLYoKlXqnL~{&To5o|XcoE0&4SXug6Nm3^OMkRJ4}U>AMje-FE<5Lm?{ z^iSYf4AWw80s~YJu3;aognq{XS_seKNxBmr!CrbS@-@b&B|49Bx)5E(5$ds4Fhy(D z862g7hKDgq#fGaWPk}ft*;xyfB%wdtTO^0!U zt~Gs%=jc@PGL}~p$MG`FB}QZ_~y0ySPrTZMupNX@AFG_?U(}Kf{fhzw0UBCS^B2gKKnS^KE=bm$!V0+jOG) z0)DCmx84u@O1rlGiC?I%=O*sZy`CX_OS|v;3U?{k`!xQp9qm00%@6uvdkQv1QhPKX z=s+rk9y;HfJd@LN#`9v_cu^Q)+&m;~v+mEA=GaWml&)@LW2vh$c&l1>0rxQ7+MxOFWS=i)!FXdetj5l>~vl!-G^)c{Y!DC7l+K^Ss z23xxmoOCKljRWyN5jAWkL+275^pV}xRbf7+I@MPUAQF+PVmHgf{HW6(wu1@{`I1!L c(a~mGEmnioY*|*w3R}rQlhtc=TG3eOU(ja_J^%m! delta 927 zcmXX^O>7fK6y9&`wbzL~aj;E7AS4Ci*r7p?N`<0=_@})jDIp0Y7Gaa!ICh-1Gv0&} zHceZ%sDwj{-vOyDl0oHwdVv~{kT}7is`wESRV8u&DN@T35E38`g<0?$>6`aA?`hum ze((FOmuZ1Ol_Vr~U~KrimP_m*c69IDoaoIPJfBGAHEkrZD|^JuWHmjX=*jVvnQZP@ z-_eoSXXFiykBlXfne4EZX*bO26wjIyhG`|r%jH42At%ZvrCFDbS-0)BBwI?OfN_bB z(NFHircT>s%V}&B8SkQSqQY`ds2J?C*3mZaNp#R{?*(k4X|;$gJfgw}r?6O#tXc~^rtPa=;$Qk? z&0RbrwPhc9>G3qeiS_wwviuA66b2DgsJz1-(S(+=zrFi>6jN~bnq@NvhTaooO&d-o)L z6A!ogApYbR0SPJ?{O`_8u#&WHXeec-tf3*=-qx^UQe>%4er2AH9S`&U;u@f%ZHCyC dM{OT1i?XGxhJ_hpRjiuTsUa3+jZ6(zy#*Zz0iyr_ diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index 9a283a2a32628b7b3e0a2ab7e47e44891d4315c2..e9a55eb113e6e408bc83a48db86545df96de18e3 100644 GIT binary patch delta 8329 zcmcgRYj9N8dH3ACyLzCGGIW&ICrLZZ*!85-=}hXT)3o1r z?%iEUfT!+{YG=Pa=iGD7{oXIVaFgBs8Os}Vx$FY|b$@^V&D^SXcW(rHY^K zfqeeV5_U%l0tFFIz{7+sf?`$V(}jW}r^G;^!gdKh+sA~P|KjyW+2b<}Y=l+qQTCn| z0?o=kr5}HnDgk9b{m_t6pSC$Vq>kt;n?B9 z@X}!Pcu0*!Bf+TV?PwiSW3eMGW2e&cz(6P((gp@x@VBP>!R@s5_2A1B!YF-Nf|UzL zMRiR=kZ`83VYX5bg#pIrq9Ph|F(FKurUfQMWld5{DMo}MC6YhQTHr~^SE&}@t*VDW zA%e6NABmkvo5$2pRD+*Lb&fJzjdP(e_)L0+dEsgE^4%6D2pWn-5znzn#AcLDiJD0< zA#PGioW}PgXvM5ZDVCjC6mxcF)#Q{g&CXw%6pfu0D6ljPKa&ur@-#Ev<4BmwQ3$1i zekSVGpD1$X*;M|tP%0?4%np1mDt66<&)sx3#Y*uFOc+=8BGnRpQm8Odce@b(6@1fD zR);V45W=*Hv&G@>@v(q&Y;ZU@5Iq(-jDmxAEPd8O)l9sBO6v)e7CZ@Ots55A6JIJ2 z2+YokSf26mFgL3Zy=)b8&U|8hja4kc9jcpvi-3;+XLl3au+_4bnZL80VE#5*ZYQve zz;XgB2;4_tB?6yQ&8KlCfjk1AbMqBP1<@(wG%#boo6*OXY*XFq=|M(JC235w2W%292?T& z>SDN_e-1_t9Gf#Nx zB_b4Vc8fc%-KY#)=y`VukQ(aaGy(a0}`as(!gJY0_9i)Wnpiz6ifAUd>(r z)>RB`C5_&1Yc|ECNSZalQbfPm;EA2DTT(NLk_C+Q!Z%8%WP64q>&xnwaDkJII0`GgZr2-eE1D{8|Fvds$4u zd({<9ZpEfg4WHpgpHaYlhKFyq(^JKPNWyn2{?fy>60KkGe=H*0t@gs11?Sp5X=x}% zeoF}k$7p0APS|jEa!zibX(It2Y_9C-?xrEv=q!7$8Dv%AqqH169#VqQp`f}6rvZC- z@I?36SU40^)D}9r7Cx*z#5~YewUXWBbiM*-s%mRJlV;77FeS|8f@VVzysOU?u~fhn zJFURas!D6#)%T1#74#RAmV{;0h2Ok#fz~?(Eg$~7Y6;s3OR67o-LXEpbG$PlDeS0t zfvHi=J&UoV;<|4ZH7Q|Dh@%Dg^`uNWzl?sna31Fik@H0c=jpatoOdsLr!>cT^)M2T zoF^6x!KVw`lL`%k2zc2Bt* zoq&ijLsv%RnId6qG7t8_>6*hfyVv-exm{x=d-(05r8{kRqb_YZ5>p4mVcleNsF7k_ zGwW7D>J)IQ!Ljh*kU?A&m((?&);2OLJXhN~552N`p*NGN+0LN1t`>2M)Gb?eSDXS4 zZ6v4$gC|3AkNDgt?TW0S4~Tzq3h`ep)LC%9ZWdUIXOHLD&A zxI*{`BSEzae%P?Gx(@9>PEkUzxH0-U@sr2OP~c_EE>?rPamg%-VqcIN_21^{Y=1<@e%-FaL{4n_D}IJUQEpxf3SoU$f{2^C-QN ztVT@`c#J@jz}%c5?ap$xH+mcsrr-_|2;~$4Dg-G<3G?Eph*U$ID9MSVfy=`g4@QOveGb!>2gA7n=Pw3Pwdm;|D&wb6k`1adJbiumh z7P^^#T+*I&syzKOkHt;|RSXy>$6`^87UQ*;dX%51arVQiEjW0zk6t|r)6MJbSpTj$6T5!q=BYKZp5OaLs49M2S#T&*4g% z1p|5UP;@vP)MC+%Bf+7gI@(EC-RfnJLZG#`G>hRBp3pEu)EFiqXW@<3n&c|YLir%M z_VMS31#~LXCgEV&q=hobge4_TS`%h;PF7ybtmiI=+!O``!^L1pgl@>LWZaM)U5l~Xvz=M+!-EWTbgWsB z<>a&YG{Z?s!qg|>Oh=8|{B&M=;m%~Pq*VH0Og3te#mo?gDF z*NytHzn+Kb5*RT&l?YemG7Xw)0#)Xe1-9%k7`7x%)A`?@=g z@+X(!B?js#uwb?9H+&}Lx5y&_Lm zI41W>QPe+%8><(x_wnte@agJWxLIt2jcZHUZD?DQs(MkcGkMyy9&HBO5vU1hRhW+3 z;Xl?cY|6;ni8kZn@~+@#usXxCN5&YblR-_m@u}P$eWw?qy z=n$4s7-SP>qi~{9>M1;Ltb7Si^QV}iDkhqh;w|XKUK!t}pVP~)E_GYx5`9}{Q$iZ1 zF4mjaCqie2HPd=DvW$pC>;RFNobX?3%i&+v6fLX3eMa%B*fQ#jf+3e?LYHP&pC{g+ ziRjG}loJHHyoWE-LN9?U1ipy?WAwb@h)aPNN8C=ye;Ji3jiv~2Y31}XC#`9?-Bs=R z1KB3UK5|-iEP^VaXk7<%_Ldh>KZpAl0r^57F=c|~c{NrM(Kb!|5~c%1@YcFtHu!y# zju=<^>>GS0JrS3pn1rX<7Wj2#A$+#pnO}oJJWjz|uu}dFrQK~T09(8LGIbL$e5YWl z`(=!ITQ<~{7|jGCEp6(KDrxaSRoxFyY*^4iG#f9`lRmC*Ij>wsXB=t}buG9(HXIu2 znE9IxJ*@sZuB)#Q;Ox9cqa4cv^*4xYJ;I@T&;v#+getrFB8Hq5tzqs zC-z{~*k-*LA0y@J)wN?`2+%{gcL0mL6@V^`qC2kMhy&B{wh8NC;_9uR#!vuH-N z#e`f=$eWLv)JuGynRY0agn9NpDrwLYU|EC4m>~pP$+&J)tOj8=B+O3!5{*yZC5$%{ z^x0;5wl^{hH@1GzcI;i^m|vW5pH60?3!6tcZgML8=Z@8dT=6(d$j7DGadi`H@h@I< zisFVz}n>*S;kKinOv57pFx*p5nnYS>9bb# z?!(0M@K$dz#2>u4gQ%Erctde-G^Tk&QLi6+Zm;1Y{sZAy*pN$H*Zl7hLEJ&yUG-ju zJ$*H07l{Z`Rl!<>l~FZSNFs^zd|wm1wyPAISReL54kC3*`$cXl$;<7FMJ5-BQ!)UFoxbEw%@!rp|x+I7D1eZ-u4z(f%` z^*Iz_Zl%XsqUiMQ4;*jM%M5}B9&UT+hcwSprM^kiKO->DUhG4I*eVQf$J*#m??g|Y zh2F0oUdqNGZ_fcYHKL6klp+xVi9OfRR2%oM*?dPwn1=|?xVx|mTk6D)oR3MH)RA}^ zUftWkehRf3ZLWj_=77&^Sca3~Ur4r-xT)X0XQ<6u48 z2Kx?HC*@f*T*V`4X;2+*&pG7)%{%UJ&1n|Z^PG8dwGKv=&G^3Gkx(fT2^L-FsK-cw zmj8-Qal*wbUAe_L05y%pNfYjme~JK$1x)35snC2@m_iRf&Eoqs{BN1=AFx6sa8%o^J3IO;z!JMBw^-_44IB9mU3(%QNF5sUP_G;7TlHb$moI5BRjGl zIooLB|I3p7djBBFy;y$6iz&e)_@4r02y>O}AF>s15(Kh;ZqvgU+YaVUGDL&_GvlH- zj-6RYkZf#dexzJ)Kd`&x*nC(et+u1k99d4X8J1fs^-B8gUx+$ZXKz zKq}*2d?ug^w4+K|(52Haxx|VZ3{Iq<6rv_PcXGkk3eusbWHsHrh(IfWRRnk^Xf=&G z39Ki;3EM-Xy#xjc#0ZQN&oa?rTEFmPmNrQbC>MEZz0ahWDo8u;?G=iF~8JT ylon(0v?+cno)*=hDiQ`G1ju2ht*Cv$VeD7Ig@MOPNE_VDDN-ImA18(`xA;GRuKg?k delta 6734 zcmb_g3v650dA{fJlDvFVBrVAjEmM9-rY$>?U{ zD?66yDUFilv88GJyGfhY4wWTpowR5YZCR6bolziJyY=CwKss=3gJwg~pl#3r8#Z)Z zvHw5!l5{+|8;Xh0$Md+n=l{R+zs~vDci0Qpm^b0^I3@gheEaC|frp;34UVRB!-@3TWcEyo z=dzh(Rv(<;x!kFB6X#0m&`>Iy(uaoJ@GHv}c;D?9J&sE2Qb8JL_%9dOVrfQZAM2l% z`Tl~W;H<_*Sr^JVB#XX9lg+-RAQhEaiAh;imo&?aAP*H#Vv`np{|C>^!Y7nyxMU@P zbzXyGJU|dcC@J}|+*x=>S>dU}Zr+U`v49N!rd(vr@R)T&|9{{JzL?Fh3#`D#Sy9$; zaTHjYk!NwS0*zQ{;Y!b@DV3gGS7)SI_SB^dsGxY#3VvJb=%)&D(W_hWJ+6XfG44v8 zWc(%@F=jM-d9LW2mFgr-EkA+tvgXh|IPa(5&agUMfl2odA47Xl@H1mUI{Y0{{wHw7 zR`1m$~frp@#KybMVN{;2MZT@$Tvn;iahHoS2AXrb(Nw9(7c7&*#`>5SO;3c^A zn`xG|g*Ot=rbT65OYJuJiR&e{6dra*SQotHzQ(%Yl;`}`&Gd}5y2(65Pj4llcbGqq zTSoZ=r(HLIl;_>B#QPMBz-uRhaLxOh+EqAMQVvX}^^%H~tWA#SdAGe0ZAmt6};X_U2-29bA1>vh*9=O)L1KwWoA^hvICbY5O^0mjD z3u#cYoyze`dF^W;Q2F_NTIm*=NRflVlO2bc`qzJ5_Y}RFU<^}>QYYz{hQ_TTl^C(hn6E~(`H|Kd^3KUs%cqZ` zpuY)5Qu#&4gr3S}V^@6(k!qO57W@_3cG_fX2eBngMR#2V+muHP$^Jmoti$|0T_9n&eRj8FtA|JkrX|H81R zpyjsVP_6DPx@enpw-GieYCU(`KjJ=|Y46B-xJXde3CbQw?E@3JELx)BY%TaIzJfrw zr|`1{Or@mg=O&U-n_#(QO=Tx0^^yf&CEij}GbrYMG&W4PXxOe{o=luRMCF7dvGXnpx;oG)O(zg#@zI|YN8k@1G*Wl(s z8W-{M6WA(Q^BDSdgP2Mby7k5iip=adQ+d z$R=5x%!VIwEHAvWvAeOt<`tYRv#Bwx&>z0o)$H3QRK^lW5c(Xf>uTKACkRptWr9?L zM9o$uu;{#jFy&)b1CMmQQs!vmrjz3aN2dKeh(c63;(tP2VLDZYgw)D>1_WvL1iIPeclAhAf znbi|1FG5_E>yPjKRnsTPx{XXN+~HHyrEQNpv&pj77gAd+x6#v1KCGAf)x)}5w-#-b*~oB=Vr}X@DBc%> zCA;3+Cv=-yG%$uGhFN9sRj>RO>;0 zTCDc#J~#8t|5slhTRBS<772u)&r_>HbyP7*8yMTOj)mu+-SZe@oex6{bYI>LhV`b-+K8%Z{WcwdCQ+VR56g0Xh%tOjU9MiHg@7QUR|-_%adMiso-vFaEpFiV#2bMQ(8M=>{>CWO}@MHPO0fNGvM zW19kwl8VCUiBvXUJ~;g@wr)d-?Jg-oSBl!Dy|SL{$|?`O;@D-CM4f>lgW713rGKYG7h zz-nTqtbySKPR(v=y+1GQ8SyK~T zRNlV)l%b&5KI1@TY+tQ8Zb7xnHU)=wHtxypW;%0^-svgU9QFCr(?Ci8j20lq+j ziqKOvyoyF;>-!>13^dngNO-bV$sWQgq)B)z?b_9W)%7JDt|TS8ai#*JOcMjRej8B%X-X$KkJry4gL#nH(oW z>}_Z|xgCDg?|{*u*I6;SCt&(yC%XdkCp-6D5iVjD!Dwt0M3k}_q7szq#Fab$DlOBA zFy+I%5+T`BS#g9eS3+wOD^KpG2kOwXvaRBnO^@dFgf33dK{<{4v4f1b<5KB*8@jAov`?=Orxs`DJRp zK=5Y-FA}^&@G`-d30@`m3xYQY{*vHLg0~31Mo>)+qD7HWWJVV@@+31xN0;hUt*TF5 ztk&SSRkf?rR@JWt@l&ft)Mjkgs3H8+V80GOKKwMR%T%xGQC;{S#D1L`5YNz@M=TMG z21+tda&&d`;6m{tZpZAD98L1LJDnR%jT{^vPvRAG$*!NK2`=^yGN(pD6bRiig$5%$ IgfX7~H@Ym(hyVZp diff --git a/abelian_proof.py b/abelian_proof.py index 043d56a..3c3fc50 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -7,13 +7,13 @@ G = group('G','*') abelianG = forall(['x', 'y'], G, Eq(Mult(['x', 'y']), Mult(['y','x']),G)) -p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), G.elements['e'],G)), goal=abelianG) +p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), Mult([G.elements['e']]),G)), goal=abelianG) p.introGroup(G) p.introElement(G,'a') p.introElement(G,'b') p.closure(G,'a','b') -p.accessAssumption() -p.forallElim(4,['a * b']) +p.accessAssumption() # this and below one +p.forallElim(4,['a * b']) # combine two steps p.leftMult('a',5) p.forallElim(4,['a']) p.substituteRHS(6,7) diff --git a/element.py b/element.py index b9bee3d..9401d8d 100644 --- a/element.py +++ b/element.py @@ -34,6 +34,7 @@ def mult(self,other, group): # this is just for representation elif binOp in self.elementName and ')' != self.elementName[-1]: return "(" + self.elementName + ")" + binOp + other.elementName else: + return self.elementName + binOp + other.elementName def addToGroup(self, group): diff --git a/group.py b/group.py index ba15fb6..bbbd279 100644 --- a/group.py +++ b/group.py @@ -1,6 +1,6 @@ exec(compile(source=open('element.py').read(), filename='element.py', mode='exec')) from logicObjects import identity, Mult - +from element import * class group: # TRUTHS for all classes - need to add more here @@ -14,7 +14,7 @@ class group: def __init__(self, name, binOp, additionalGroupProperties = None): self.groupName = name self.binaryOperator = binOp - self.elements.update({self.identity_identifier:Mult([identity(self)])}) + self.elements.update({self.identity_identifier:identity(self)}) if additionalGroupProperties != None: self.groupProperties.update(additionalGroupProperties) @@ -34,7 +34,7 @@ def __mul__(self,other): # group cartesian product. Worry about this later # declare new element in group with elementName def newElement(self,elementName): if elementName not in self.elements: - self.elements.update({elementName:Mult([element(elementName,self)])}) + self.elements.update({elementName:element(elementName,self)}) else: print("Sorry, that element already exists!") @@ -46,7 +46,7 @@ def mulElements(self, elem1, elem2): # should this return an equation? try: gelem1 = self.elements[elem1] gelem2 = self.elements[elem2] - result = gelem1 * gelem2 # need to specify which group we are multiplying in + result = Mult([gelem1 ,gelem2]) # need to specify which group we are multiplying in self.elements.update({repr(result):result}) # is this the right? except: print("Sorry, one or both of these elements are not in the group!") diff --git a/inverse_of_ab.py b/inverse_of_ab.py new file mode 100644 index 0000000..dd865a7 --- /dev/null +++ b/inverse_of_ab.py @@ -0,0 +1,26 @@ +from enum import unique +from telnetlib import GA +from proof import * +from element import * +from group import * +from integer import * +from logicObjects import * + +G = group('G','*') +ab_inverse = forall(['a','b'], G, Eq(Mult([inverse('b',G),inverse('a',G)]),Mult([inverse(Mult(['a','b']),G)]),G)) +p = Proof('Inverse of ab Proof', assumption = None, goal = ab_inverse) +p.introGroup(G) +p.introElement(G,'a') +p.introElement(G,'b') +p.closure(G,'a','b') +p.introInverse(G, Mult(['a','b'])) +p.rightMultInverse('b',4) +p.inverseElimLHS(5) +p.identleft(6) +p.identright(7) +p.rightMultInverse('a',8) +p.inverseElimLHS(9) +p.identleft(10) +p.switchSidesOfEqual(11) +p.forAllIntroduction(12,["a","b"],[1,2]) +p.qed(13) \ No newline at end of file diff --git a/logicObjects.py b/logicObjects.py index d9ab9f9..c993f45 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -31,7 +31,10 @@ def replace(self, var, expr): #print(self.products,var.products,expr.products) while i < len(self.products): if self.products[i:i+len(var.products)] == var.products: - new_products += expr.products + if isinstance(expr,Mult): + new_products += expr.products + else: + new_products.append(expr) i+=len(var.products) else: new_products.append(self.products[i]) @@ -251,6 +254,11 @@ def __init__ (self, prpty, pg): ## Special types of elements/groups +# class element_(element): +# def __init__(self, pg, elementName): +# elementName = elementName +# super().__init__(elementName, pg) + class identity(element): def __init__(self, pg): elementName = pg.identity_identifier @@ -262,12 +270,24 @@ def __init__(self, pg): pg.addElementProperty(idnty,elementName) class inverse(element): - def __init__(self, elementName, pg): - inverseName = elementName + "^(-1)" + def __init__(self, object, pg): + if type(object) == str: + elementName = object + inverseName = elementName + "^(-1)" + # lhs = Mult([inverseName,pg.elements[object]]) + else: + elementName = repr(object) + inverseName = "(" + elementName + ")" + "^(-1)" + # lhs = Mult([inverseName]+object.products) super().__init__(inverseName, pg) - lhs = Mult([inverseName,elementName]) # self or elementName? - rhs = Mult([pg.identity_identifier]) - inverseEq = Eq(lhs,rhs,pg) - pg.addGroupProperty(inverseEq, "Inverse of " + elementName) + self.inverseName = inverseName + self.elementName = elementName + def __repr__(self): + return self.inverseName + # self or elementName? + # rhs = Mult([pg.identity_identifier]) + # inverseEq = Eq(lhs,rhs,pg) + # pg.addGroupProperty(inverseEq, "Inverse of " + elementName) + ## TO DO: class generator(element): diff --git a/proof.py b/proof.py index 5a26adb..02e2228 100644 --- a/proof.py +++ b/proof.py @@ -1,3 +1,4 @@ +import os, sys from re import L from element import * @@ -21,10 +22,8 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = [], self.subproof = None def qed(self, lineNum): - print(self.goal, self.steps[lineNum]) - if self.goal == self.steps[lineNum]: - self.steps+=["□"] + self.steps+=["."] self.justifications += ["QED"] self.show() else: @@ -146,9 +145,9 @@ def substituteRHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.LHS} with {ev2.RHS} on line {lineNum1}'] self.show() else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def substituteLHS(self, lineNum1, lineNum2): """ @@ -165,9 +164,9 @@ def substituteLHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.RHS} with {ev2.LHS} on line {lineNum1}'] self.show() else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may be neccessary (I think) """ @@ -187,9 +186,9 @@ def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] self.show() else: - messagebox.showerror('Proof Error',f"Line {str(lineNum1)} is not an implies statement") + print('Proof Error',f"Line {str(lineNum1)} is not an implies statement") else: - messagebox.showerror('Proof Error',"The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") + print('Proof Error',"The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") def inverseElimRHS(self,lineNum): """ @@ -214,15 +213,15 @@ def inverseElimRHS(self,lineNum): lawApplied=True break if lawApplied==False: - messagebox.showerror('Proof Error',f"Inverse laws can't be applied on line {lineNum}") + print('Proof Error',f"Inverse laws can't be applied on line {lineNum}") else: self.steps += [newProducts] self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") - + def inverseElimLHS(self,lineNum): """ finds the first pair of group element and its inverse and returns the group element @@ -235,30 +234,31 @@ def inverseElimLHS(self,lineNum): for i in range(len(l)-1): if isinstance(l[i],element) and isinstance(l[i+1],inverse) and (l[i].elementName == l[i+1].elementName): group = l[i].parentGroups[0] # how to deal with multiple groups? - l[i] = group.identity_identifier + l[i] = group.elements[group.identity_identifier] newProducts = Mult(l[:i+1]+l[i+2:]) lawApplied=True break elif isinstance(l[i],inverse) and isinstance(l[i+1],element) and (l[i].elementName == l[i+1].elementName): group = l[i+1].parentGroups[0] # how to deal with multiple groups? - l[i] = group.identity_identifier + l[i] = group.elements[group.identity_identifier] newProducts = Mult(l[:i+1]+l[i+2:]) # should we include 'e' in the Mult object? lawApplied=True break if lawApplied==False: - messagebox.showerror('Proof Error',f"Inverse laws can't be applied on line {lineNum}") + print('Proof Error',f"Inverse laws can't be applied on line {lineNum}") else: - self.steps += [newProducts] + self.steps += [Eq(newProducts,evidence.RHS,evidence.group)] self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") ## For all and there exists elimination def forallElim(self, lineNum, replacements): """ - Given an expression forall(a,b,statement), forallElim substitutes a with another input variable to create a new forall statement + Given an expression forall(a,b,statement), forallElim substitutes a with another input + variable to create a new forall statement :param lineNum: The line number of the line that showed the original forall statement :param replacements: the list of elements to replace the existential elements """ @@ -269,7 +269,7 @@ def forallElim(self, lineNum, replacements): self.justifications += [f'For all elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error',f"There is no forall statmenent on line {lineNum}") + print('Proof Error',f"There is no forall statmenent on line {lineNum}") def thereexistsElim(self, lineNum, replacements): # We can only do this once! @@ -285,7 +285,7 @@ def thereexistsElim(self, lineNum, replacements): # We can only do this once! self.justifications += [f'There exists elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error', f"There is no there exists statmenent on line {lineNum}") + print('Proof Error', f"There is no there exists statmenent on line {lineNum}") ## Multiplication manipulation @@ -305,9 +305,9 @@ def leftMult(self, elemName, lineNum): self.justifications += ['Left multiply line {lineNum} by ' +str(elem) ] self.show() else: - messagebox.showerror('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) else: - messagebox.showerror('Proof Error', f"Line {lineNum} is not an equation") + print('Proof Error', f"Line {lineNum} is not an equation") def rightMult (self, elemName, lineNum): """ @@ -325,9 +325,39 @@ def rightMult (self, elemName, lineNum): self.justifications += ['Right multiply line {lineNum} by ' +str(elem) ] self.show() else: - messagebox.showerror('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + else: + print('Proof Error', f"Line {lineNum} is not an equation") + + + def rightMultInverse (self, elemName, lineNum): + eq = copy.deepcopy(self.steps[lineNum]) + if isinstance(eq, Eq): + if elemName in eq.group.elements: + product = self.MultElem(eq.LHS,inverse(elemName,eq.group)) + result = Eq(product, self.MultElem(eq.RHS, inverse(elemName,eq.group)), eq.group) + self.steps += [result] + self.justifications += ['Right multiply line {lineNum} by ' + elemName] + self.show() + else: + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) else: - messagebox.showerror('Proof Error', f"Line {lineNum} is not an equation") + print('Proof Error', f"Line {lineNum} is not an equation") + + def leftMultInverse (self, elemName, lineNum): + eq = copy.deepcopy(self.steps[lineNum]) + if isinstance(eq, Eq): + if elemName in eq.group.elements: + product = self.MultElem(inverse(elemName,eq.group), eq.LHS) + result = Eq(product, self.MultElem(inverse(elemName,eq.group), eq.RHS), eq.group) + self.steps += [result] + self.justifications += ['Right multiply line {lineNum} by ' + elemName] + self.show() + else: + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + else: + print('Proof Error', f"Line {lineNum} is not an equation") + ##power methods def breakPower(self,input): """ @@ -344,7 +374,7 @@ def breakPower(self,input): self.justifications += ['Convert power object to mult object'] self.show() else: - messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") + print('Proof Error',f"Expected a power object but received type {type(input)}") def combinePower(self, mult): """ @@ -366,7 +396,7 @@ def combinePower(self, mult): self.justifications += ['Convert multiplications to equivalent powers'] self.show() else: - messagebox.showerror('Proof Error',f"Expected a Mult object but received type {type(mult)}") + print('Proof Error',f"Expected a Mult object but received type {type(mult)}") def splitPowerAddition(self,input): """ @@ -378,7 +408,7 @@ def splitPowerAddition(self,input): exp=input.exponent l=exp.split("+") if len(l)==1: - messagebox.showerror('Proof Error',"No power addition to be split apart") + print('Proof Error',"No power addition to be split apart") else: multList=[] for i in l: @@ -388,7 +418,7 @@ def splitPowerAddition(self,input): self.justifications += ["Split up power with addition in exponents"] self.show() else: - messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") + print('Proof Error',f"Expected a power object but received type {type(input)}") def splitPowerMult(self,input): @@ -401,7 +431,7 @@ def splitPowerMult(self,input): exp=input.exponent l=exp.split("*") if len(l)==1: - messagebox.showerror('Proof Error',"No power multiplication to be split apart") + print('Proof Error',"No power multiplication to be split apart") else: elem=element for i in l: @@ -411,7 +441,7 @@ def splitPowerMult(self,input): self.justifications += ["Split up power with multiplication in exponents"] self.show() else: - messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") + print('Proof Error',f"Expected a power object but received type {type(input)}") ## Identity and equality elimination def rightSidesEq(self, lineNum1, lineNum2): @@ -427,7 +457,7 @@ def rightSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same right side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - messagebox.showerror('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") + print('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") def leftSidesEq(self, lineNum1, lineNum2): """ @@ -442,7 +472,7 @@ def leftSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same left side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - messagebox.showerror('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") + print('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") def identleft(self, lineNum): """ @@ -466,7 +496,7 @@ def identleft(self, lineNum): break # else we can't apply identity elimination if l1==[]: - messagebox.showerror('Proof Error',"Identity can't be applied") + print('Proof Error',"Identity can't be applied") else: newProduct = Mult(l1) ret = Eq(newProduct,evidence.RHS,evidence.group) @@ -474,7 +504,7 @@ def identleft(self, lineNum): self.justifications += ["identity elimination "] self.show() else: - messagebox.showerror('Proof Error',f"Expected an equation on line {lineNum} but received {type(evidence)}") + print('Proof Error',f"Expected an equation on line {lineNum} but received {type(evidence)}") def identright(self, lineNum): @@ -485,6 +515,7 @@ def identright(self, lineNum): evidence = self.steps[lineNum] if isinstance(evidence,Eq): l = evidence.RHS.products + print(type(l[0]),type(l[1])) l1=[] for i in range(len(l)-1): # deals with the case a*1 @@ -507,23 +538,26 @@ def identright(self, lineNum): self.justifications += ["identity elimination "] self.show() else: - messagebox.showerror('Proof Error', f"Expected an equation on line {lineNum} but received {type(evidence)}") + print('Proof Error', f"Expected an equation on line {lineNum} but received {type(evidence)}") - def introReflexive(self,eq): + def introReflexive(self,name,G): """ Introduce a reflexive equality (like x=x) Necessary to show something equals something else when not given a starting equation :param eq: The equality you want to introduce """ - if eq.LHS == eq.RHS: - self.steps+=[eq] - self.justifications += ["reflexive equality"] - self.show() - else: - messagebox.showerror('Proof Error', "This is not reflexive") + self.steps+=[Eq(name,name,G)] + self.justifications += ["reflexive equality"] + self.show() + # if eq.LHS == eq.RHS: + # self.steps+=[eq] + # self.justifications += ["reflexive equality"] + # self.show() + # else: + # print('Proof Error', "This is not reflexive") def reduceLogic(self, lineNum): """ @@ -536,7 +570,7 @@ def reduceLogic(self, lineNum): self.justifications += ["logic reduction"] self.show() else: - messagebox.showerror('Proof Error', "This is not a logic statement") + print('Proof Error', "This is not a logic statement") def introCases(self, case): """ @@ -589,7 +623,7 @@ def introElement(self,G, name): :param name: the name of the new element """ if G.contains(name): - messagebox.showerror('Proof Error', f"{name} is already in {G}") + print('Proof Error', f"{name} is already in {G}") else: self.env[name] = G.newElement(name) self.steps += [In(name, G)] @@ -610,14 +644,15 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): v = vars[i] l = elemIntroLines[i] if self.steps[l].elem!=vars[i]: - messagebox.showerror('Proof Error', f'Line {l} does not introduce variable {v}') + print('Proof Error', f'Line {l} does not introduce variable {v}') elif self.steps[l].group!=G: - messagebox.showerror('Proof Error', f'Element {v} is not in group {G}') + print('Proof Error', f'Element {v} is not in group {G}') else: #If you make it here, this is a valid for all intro self.steps+=[forall(vars,G,evidence)] self.justifications+=["For all introduction"] self.show() + return def closure(self,G,a,b): ''' @@ -633,9 +668,9 @@ def closure(self,G,a,b): self.show() else: if not G.contains(a): - messagebox.showerror('Proof Error',f"{a} is not in {G}") + print('Proof Error',f"{a} is not in {G}") else: - messagebox.showerror('Proof Error',f"{b} is not in {G}") + print('Proof Error',f"{b} is not in {G}") def cancelRight(self, lineNum, mult): ''' @@ -653,9 +688,9 @@ def cancelRight(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - messagebox.showerror('Proof Error',f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") + print('Proof Error',f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") def cancelLeft(self, lineNum, mult): ''' @@ -673,9 +708,9 @@ def cancelLeft(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - messagebox.showerror('Proof Error',f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") + print('Proof Error',f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") def switchSidesOfEqual(self, lineNum): ''' @@ -690,7 +725,7 @@ def switchSidesOfEqual(self, lineNum): self.justifications += [f"Switched sides of line {lineNum}"] self.show() else: - messagebox.showerror('Proof Error',f"Hmm, it doesn't look like line {lineNum} isn't an equality") + print('Proof Error',f"Hmm, it doesn't look like line {lineNum} isn't an equality") def notElim(self, lineNum1, lineNum2): ''' @@ -705,7 +740,7 @@ def notElim(self, lineNum1, lineNum2): self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}'] self.show() else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum1} isn't a Not statement") + print('Proof Error',f"The statement on line {lineNum1} isn't a Not statement") def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it ''' @@ -737,7 +772,27 @@ def andElim(self, lineNum, n): self.justifications += ["And elimination"] self.show() else: - messagebox.showerror('Proof Error',"You must choose argument 1 or 2") + print('Proof Error',"You must choose argument 1 or 2") + else: + print('Proof Error',f"The statement on line {lineNum} isn't an And statement") + + def introInverse(self, G, name): + if type(name) == "str": + if not G.contains(name): + print('Proof Error', f"{name} is not defined") + return + else: + for x in name.products: + if not G.contains(x): + print('Proof Error', f"{x} is not defined") + return + if type(name) == str: + lhs = self.MultElem(inverse(name,G),G.elements[name]) + else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum} isn't an And statement") - \ No newline at end of file + name_ = Mult([G.elements[x] for x in name.products]) + lhs = self.MultElem(inverse(name_,G),name_) + rhs = Mult([G.elements["e"]]) + self.steps += [Eq(lhs,rhs,G)] + self.justifications += ["Introducing the inverse of an element"] + self.show() \ No newline at end of file diff --git a/unique inverses.py b/unique_inverses.py similarity index 96% rename from unique inverses.py rename to unique_inverses.py index 56e31e2..adc28a4 100644 --- a/unique inverses.py +++ b/unique_inverses.py @@ -5,7 +5,7 @@ from integer import * from logicObjects import * -''' + G = group('G','*') inversePropertyOne = Eq( Mult(['a','c']) , Mult([G.identity_identifier]) , G) inversePropertyTwo = Eq( Mult(['a','d']) , Mult([G.identity_identifier]) , G) @@ -24,5 +24,4 @@ p2.switchSidesOfEqual(8) p.concludeSubproof(9) p.qed(10) -''' -print(dir(Proof)) +