From 01241769f51589262128d67f402db6c9ac447c04 Mon Sep 17 00:00:00 2001
From: Morris Kyn <morris.kyn@gmail.com>
Date: Tue, 12 Apr 2022 13:01:04 -0700
Subject: [PATCH] Split QED into QED and for all introduction. Made introducing
 elements a proof step (still uses group class).

---
 __pycache__/element.cpython-38.pyc      | Bin 0 -> 2963 bytes
 __pycache__/environment.cpython-38.pyc  | Bin 0 -> 1454 bytes
 __pycache__/group.cpython-38.pyc        | Bin 0 -> 2443 bytes
 __pycache__/integer.cpython-38.pyc      | Bin 0 -> 1896 bytes
 __pycache__/logicObjects.cpython-38.pyc | Bin 0 -> 8096 bytes
 __pycache__/proof.cpython-38.pyc        | Bin 0 -> 16353 bytes
 abelian_proof.py                        |  33 ++++++++-------
 environment.py                          |  34 ---------------
 logicObjects.py                         |  34 +++++++++++----
 proof.py                                |  54 +++++++++++++++++-------
 proofs/proof1.py                        |   0
 11 files changed, 83 insertions(+), 72 deletions(-)
 create mode 100644 __pycache__/element.cpython-38.pyc
 create mode 100644 __pycache__/environment.cpython-38.pyc
 create mode 100644 __pycache__/group.cpython-38.pyc
 create mode 100644 __pycache__/integer.cpython-38.pyc
 create mode 100644 __pycache__/logicObjects.cpython-38.pyc
 create mode 100644 __pycache__/proof.cpython-38.pyc
 delete mode 100644 environment.py
 delete mode 100644 proofs/proof1.py

diff --git a/__pycache__/element.cpython-38.pyc b/__pycache__/element.cpython-38.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..5cc1d56fd16b90ae1742693068bdd78a5eb43236
GIT binary patch
literal 2963
zcmb_eO>^5s7~Yj+MRpuFO$%vY08tpgE%oqGI!wtl1zHLh7jQELO&E=$RU9>nrLJT`
zJnku->6tr+_LzUbZ{R2B#0;nYg<RlyS5jg-(*q3a*;o6e-DjWYeP4NfVWGiLe*a^A
z^S3%<e^F<$80g$YO|QWS=CC_VaG^bBLOakLj-D<I^o)QX=#GYdO_=DLs;`T=9&1~p
zKO5hz-|pS}=5Dulz0vrvV}Bj**&??00$T)LWbcL9wjD&lZZOE~M8-)VvoJ{QY}?Ch
zFG-?(JB!f^?7i(c3hcg&hsm1V+m45kz<8M2n}O{W<JAWH@6T?DkyzTBakjnI_^4xl
zAp>s*+j}yrR#r#Kz}_83S(rp&fCJ)wfWzfl<KvEf-&0_KJ{*XlpM~*Yt>J^6siLEI
z6E*!FCSVQ+cbedi-e-;xGN&faD(1Lj7K}M_Voq3(nPZ8%Xy92F^P-7oLoA3Ep7Y|2
zSj4j_G;q3<&y{@Ttm~6XRiQSW{v~Sq4$PR3najpnpPqcI3$~-ni(~dcd#aE1XPiUV
z9y{dSwvo@5n|8h3Aa8;h2y%zWPV=+n)VIg-<mNCDUKZdzBMqW0Nk`|rFHJlTnIz9T
zy6RuwSWg3)ZtTWVh8wqnbSI0GjeZnwdeN0&@N+2R0SUiR9?(hlbIWzZL72Jj8SIf-
zFpQhr!f&)#EvuIJoTke{ZK~?_gah})?IbaB$Q437XhQ|BF!Sirkupf6>%N3us==_S
z!-`2?P0%C?wdo9X*hMr(Ejn(@AFv(mK91$;_aj24$9_;Wx3%t9asf-*nnID+;EjQt
z1!KBy@X&QHU}1TCjkmzSsC9CCTHw>Ysxqbg2%}@|0eb|E0f_II@|xh(650xRz%@XH
zH!K6(GC_tF==B)ZV+QNDglY*xt>41i7%x`Qd&N6gU+z=&$(!1>?h$|QIUzgZ?dN}^
zv^A%-84f(Te;48HW$*?9+%^g|7SYaYDzKdz*4<5JIWZ_AU&pev2}AyHq4;T|X2l9E
zIVBNsq$Hv<fR;T450&35&wv;;%;hF>O)wCpHu7bR&7x>{Lfng0OuUQf%2Ado1Siu|
zeo3xERpFpZ6j_we++qj(k>Zy4AA@1=XLL`!PS@z6rb{q=T;!()UW2dwsy#H|;uLOe
zp4SzJ6u@mQ*E%0ar1jIcSdGFo^W)v*#%0=)lrRBsbh*06)-Z|?tG)~qN^zalDE7T5
zy@5vc=4c)%u*kWoT~b(RTKKkODk#w`g=c2=zEmM#e36fqUw~lB)rkwLip~}ql;jY3
z+Nz4OLR792QClwp%__eu`%bfJ5lOS)<{@C2;`TcPj8sD=I9I`%m~SIzE>PkaU?bPf
z8?L(>i(y3Vrt3Z&dQmZ>SWzyfAW3pyNvTbqC9_Osh0JSY-XKG2P8dp2k`fz@r{`fT
zZqQF_n3istRvp$*D|}2&6(WjC`Zi4UEqcPXxbi{E(Ti`mV?1F7zDyLo_z?U8nUR%4
zFFM71m1vYFX6!%()L46_6`ztK*=l($9U{`zWe*Dx6c3J;^bg^u$X=0`rbxT$uIh$F
z%qIl3Wc~aEjLr)a{;?;#f>%|VVn|aOf(fZf=qvctl|eOH`dn^?nM4+<KKb@h{n(A=
zIcxx|biqO{+EJ2&&1ykPeTrHkeRUG)jDsJV(xxrmBy*9Basb*QUnpttgD9$~P<&8!
zk&2YJ(7KAMqSWF|UDAk;I#q}TD*s02x>wQhpG21AQIh^-NCkIV$W;PU3b}NA(ElRi
z`P(P%c`T%C6A+S6ULx}%+14g-t(@SR5lvEJoKXElk1Lq?jP@WmQF_n_{e7BqT@m|`
gks?*8Bx!15mt%%<YqiJ~H)w52e<O@~>(b)fKb{_AUH||9

literal 0
HcmV?d00001

diff --git a/__pycache__/environment.cpython-38.pyc b/__pycache__/environment.cpython-38.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..5567b138a9ae22f6de7986df245a2abd3e57b4c3
GIT binary patch
literal 1454
zcmbtU!EO^V5VgI|W}8h~pjF$z0f}1<^n^r(5UK=KB@Pi%)XOT;DvjL`NOl)*Qq(G(
z=!Yc79QYAF!B<ZG1uigeHw#P32`qU$JD%8Y-aO~D(Wo&RU%sB6eR3H4hL7@~7(1ew
z-Y27&;v*KY6Q+c6u9<Q^i-0TMVJ&$>`>frEEe}B-M>NydWHh5}7KkAm@W2_cKq?+o
z^0NY0NmaRKK~=e`N~@<lwL$BKswtn=nyRY?t-ji%`?joq99;}e9F27}F`Q2C<E~=B
z$9zdM-61n$?=X3jYG|?<%??|NcHkY4G>%A@!a6#-uob0~$=jB&GS#DVD>dyenc1K-
zz906Vbx%`m((X7mX4rkD)Ay4&=?+HmS#R{1eqJEzmi&X{(pCq0f}6m0ngQik+ocK)
zR{MQP3B`bq24qD%BIkAyGtp#oF>@B2Q+qnhAb;tY3N6MZW8Geo=t#AssUqefCMTDP
zwlXnsk`<O4V6%QtDFA&#dkqTYV8zv58Eh%%-&l7~Ogv3eg9=+BLuM-j#Mbe6L`;^v
z{R<4g+9`u668@XIyL5x81JR1BdkAd8Y{5VRC8p}cLWT@f?b2RB)qWXWIq4QxC_iiN
z6LQepIfsQp=VHOoRQh%(%5z_`cT$O`B<)b5-7Tkm^Ml3>9zd&-w;gS>vLBP|YP~d_
zj+4nSjxsf@xDMPbuGdTQBmJ>6JtJMj=Xmfb6vX&0uk$|zP|EA$>SDmZrPw)NFcd=I
zh2n<*FY>Y$C_%Ih*dx**TI(bvO5AJq5#_mT*SPmd(FM?ll(qs|<C|+hOL^^9-Fjgd
z^~O33Z7mGPv6_zH*Te9`v^UCkat?8Kj>3m`2L=i>_%AU{m<KSwab+H!kiqi?2`TjB
jahFRjrRR7qP3cv#eQLyBk^8qptoJ;J_X3n=%JRfdnvW$T

literal 0
HcmV?d00001

diff --git a/__pycache__/group.cpython-38.pyc b/__pycache__/group.cpython-38.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..f1d2c5805480c67d1c21bcade6bb52d74fbc8a85
GIT binary patch
literal 2443
zcmZuz-EP}96eg)3D~_EwZQAq?g|ZH7wROW*6dP6qLx655FktC`tk@<55EPSfl*p1x
z(pzmPSMKfJA-(Lw>;-tctGz<6b`B*wZdMvRJR%Qyc)s&Pzvy<`1llKmzc}Q;{evIN
z&4-U&=xPUuAc6|U$&8*mZwM!xa`u-qqm*!mySY2`VsGfjJ|)ix_qhL>aDT?)7H{p7
zD44cIE{3AeUyLTk6|Y1;a*VIavFr;I9A&vE(xEW!u;k)j&_*I=f{eq4Ov8qs#<}j}
z^m23HV;8zQ0wPFEIf)skv6GS5h3-N3IbMOq0pH{<_g>R@h5Nkqn#64$@D&(Wd7H1o
z*x?=Cg|W-m_&SVhyvH|ST<2H#RTz8R0Yk1CZy?L@$WUR(Uf%`H^M*Vk_7u9>1ya$9
zB&1?MfjeR64p3Kn+OGh`0iDr|z5)Cyhm%uB?!ambWE`C1WS_jHdr@FktiC-&XYDX6
zQaO1(5;E1LG(m%@GX8kPQ!UKZIb=!A9A!ev7TiVR&CI$z>t|WQ2|5!ha*eA*eq>yW
zz6a+&AH_FQ&NH2rMVdcDTQB6_5_t{IdH1OQ<lu!8QXLFSDYJv`g*w&c=wOhShiU$~
zDE`P~S)jWQtVVQtkR(}==_FZ$6O;`+>cj624d`^O7MqLoDagzl@(jAg6*qH4lWY;r
zwg9Eb*_--y`-68hdP`*oL?SA$z+i7%lk4z_caUNvlVl6N6dp>Jbk|FLJB>@wkYDJ=
zgHdxuPsl0TCvp`g<V_$Ev+9gj>SF*LF<R2<Cy98OBq%u7*_qpm3-4*fD8g>7#k@m}
zoNigITjY#ssv)9IAoF0PIPO9;ojKaYNIUUh&Kt1GnPIrHJwsnbzQx42d8V{+l+bZ|
zw1@#2fD+jS61g>Kw}Fpah4>SLF75(z5doKNYbD8WoF@tHQ5a){_UH{d?amFftM6He
zcw$Ie3m*f6c>;*G<O3YfX$6*P2WMyOB1?)uyBu<+&JD0^dT$?sZ}KqI$EgmRR0z{t
zij+@6@d}Jp+mR<RWaK&$)M{Fdr13^FEA-rTtIagpeA&o0K=4CdzV5*hjh$_JmrZ-M
zofiUq2PEbV0a=uU96lOTncB3@f-sVIHLcAmew;oA0Klm?$r+XkRx#k*%BkE<a^~U8
zIl9@K(aNh!$FHQ=qy&F(3PW&yCk6Y>mJdvfZyJce3pyL+ldKqohZ8_dg!4)f@=~bc
zzJ@VOi-|r4neFM5W@A~1u$18;1a?>+;YKCqSgSCVA}mTBW`#Y{Vu6tNz*PAWk_Gt2
z#q@$u#Jr3>MEk3Hcoh4C`m-J%8D9zo7ryL<Rj{IQgZdOsQFs)go3zasZNo2s$n)uR
zqxQ*?^m|T02Vs8-UE%#|r&Mgm!e+A?>c<AGL{6R8L6a^M)0uN0ijy7`&Sy&%bMiH+
zz<7r;bG^RRWs(0~ZIS$6!nP(#{3c!~#7k(e3$d|7ijH=m7}AQ(oQt%${mXJb%)M*#
zVH;B1dITM0HV}2F(M#ElK5LAY4}h2VkX))~SHOnG56#xew;<M}#U|~r>5YZ4mjokt
z(>AaU<AakVrVaI@<l`LqPLjMFr+K|n$B?}&dP07N1gn&-WfBXxyoKZrk`T$qNbV!S
z=#USQTwL99_zKv9=K-T|YrtH(__6j%z~C1It)LS)RubM|iBFJe^~>Q1{-_uip3ef~
pIpwC4mxHYT{P0BdwX%<F{oLB3`T^x8*s1OP4$oBR>|3<w{0BmeGywnr

literal 0
HcmV?d00001

diff --git a/__pycache__/integer.cpython-38.pyc b/__pycache__/integer.cpython-38.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..91e6300a343d8a92dd621ccef7229f43050bb0d3
GIT binary patch
literal 1896
zcmbtVOK;Oa5Z+xso4!H|lt+I+0|G>aP=!!c0fJjDg^Lwwm1dS=;yCHrDWY;EMEL<d
zpq@B#=|4g~!ih7to|sw3PEt`WU2A4`GVV9uj%TND=I3h+*Uyb-JF7E{{UT>_S?Fw`
zBul7XF<`*Ipd5*Sf!JmZtAoE!ErH$^O7a4gVgUyh2;d;Tu)qQfY_v8w;G%WF10Ssm
zGf+e8!7R+7^<f?s(9Xaj=BVdh7^iAi=?;OHi}pnCIZCpMDrFf@k(#~%JmV`!aD`<|
z3SdOEdB)eyc%xzEwJ-_eByGnXm0L-wb7#LD4OK(rcA}!Uxf8~NVS36m7KEKW>O5(^
zNt8}ny}s6A>xD|XX@Ah#jru$7=$?xAL*0*iDo$G?miGrAb6?6Z4pS*@Vn>Sc8b7F)
zuaw~qr_gB8o=#;>w168t2Yb(olbACc_#=QdO-FBV?H0yEWB3+|J}Pn0YM`a`(MwF}
zrWh2#shScfiD7UHH<TZ+mKi4=hayErnK+_PFPb^Ob1Do2P1H{<O*C?+pT1K%K&n{A
zSbaFp%agJ<jHH~!mq(?k^Ml24X-xDIyw3PtP36;zr06S7R0XrQ0i>kZKeL<YrLy1q
zZ}w!kBjxf%*-i9P*&ke-eOAg;4;6&_Qm#xfSRPludSi+O^-$Fr-|=%(XB-OZi$g0D
znbkG-Zku6;h$Fm*nRUdw;+X4iATrT)^=Gse*-X3_AZ{|SZn8tW@@({+%$kU~l}9lz
zvoo(N`kyi<bGz7q;27K-E#c+{$(h0>Z;V^U3fwYQ;{K>`UBX4?8-Q;XJA>^`VUst;
zE@K6D85?0A^Zw%s-5a5wfHy)vG3eeDI(cLCGFG6Mu`&AB3f<pku??ur)SGF()-<_)
zqp;s}N%d7y^Q5k$dfBkd1<tKV#krFVqA+dv<{s-h#)DZJi4vz|81Dvi=4O|kXg>_Z
z4#|2T+Uw^pnk%K+lkzsAB%7!hck%JL&6h--FN~f#pWI)qeqZ7fd*O<Mg>i=xY_n0L
z0T;J>O3J*3Bc%_+i1u?*?hV^f5z#bc^c<-xr0Cx1Yow_EHT~O|;B7_)%}z7VsNEBq
hBR=<S-$F5ui8XQbnsSb(OZCUO|Fj^pNeF*X*k7wea3=r&

literal 0
HcmV?d00001

diff --git a/__pycache__/logicObjects.cpython-38.pyc b/__pycache__/logicObjects.cpython-38.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..3ee516a383489d10a4e73f31829dad5830946066
GIT binary patch
literal 8096
zcmcIpOOqSb74F*)sYlYt<FWAz;|N2DWx!zP!6SwY4;xGwnb?>jib2Tgwyd#6(%kML
zSf$BkNI|8NACO9=%B+%Eq>8E}KOosA%dC2ttXO8tD&Kc*w^}pf0T)hs>fSl$KF>X`
zd+yQI`T3HC@8RU?_5VC%S^p+7`?)}tP@;dL3ami&ttS85eYIjYZAIAWJ8xUBS%DjP
zA6tR9VK-f1g`fzm2+RZK2XnyYfE9q1f-<l&up+QZFb`}Vm=CNP>;bk1*c`BhU@x$}
zz)HXtgMGmE0V@alg9kpgniaGj2o9q4AX?{v9SRNuI}EG}>`3q+um?kD!)fjTel&Op
z_(Os(1nP=aKlTMqW;N<6De7?4Z+Aj~>STwlv!4xQ2_^a-s?chxz-roo3T#l}1Ww@M
zKR6H+@ZSrHfsg-%U@j=(e=#Uyr%K|!xz>+6Tq*kqv%G>5Q4|w3v0C8j6>C#9HdW$}
z^e|ZK#8KT&+$ikdNc^xLu3YRz@usCY<ICqd&tJP5g*v*nGSs?v?bR^46%R+(y8Yqx
zcK^w6@L^962P@$qzSbXhd!0+ymqRRgYIHmCTdm%p7q?nP?k|L?@jR(KmGyKKy0Xs!
z;Gqb)?*ItYx{9qBL@(PLV8$V9L%nLfcWm9BsMula#6FC+XRLKKQGvt%s|T{a*?IXW
zu*z*D))(A(?9@)y>Tcrc_MjUkPCp!I(waC?tm}^U2^RqO2HiyUgdwIXvj^vcP<5*{
z2P~?fvXrY1s6|y$NAr`KF}n-q5a!`55YDo7%hsYefqlh@$!WZOUKcQ8(>COI!}w;X
zx06z6wZhd_YXJizj<!@qx%Rl6GMjxn2q3$K)u#Z&*gjSpwmxFm24d`kVC|KZ{S(zy
z2B-FDimC1-rC!t<L~(o22{nybxTg;gqVmk}s@Q6+to2*12hf~SSW*l2xRO#RogI>t
zecWQI4I?03Yu$lHxDyw|TFYuf-LmveLKD-b*mltR1#|-BEAX;0aVGXM^}~@_G6I;p
z>Q9_IwwZg_`b;Tn;s&<qfo3^8c-?7eYKg9*s=J!ZHR@4lk4E7jkR#VUBNykxwocse
zqmgb_2I0?InPusHoVJx4nzryDO0<ZIO5@s9bqs2=U@xFfxsrN}M%|~X4caSVtCf_%
zNZ4$jaHZ8+U2FGEkER0Z{j8`_`Uop-G_$#oLERP7sVL$WeC6AI(f9m<w0F?H<>M+#
zDA7?=yL%_FtdKY_4T3Flq)fShs2X`_oX`Z^Z^6x_%Crdw)Yje8QlHs0wx=J#aQ!H&
zZ4BgDPohNBI!hJ6GVGhX6>gY)gr@}5fWTEyIjS_eE5vMIN2v_P=qPx~{0q*~$5GW&
z<8uaUE89qc%=^6+novY{VJRQf_-gEv9(FZ0J$(!v`dh4OtVB{L2<6AhMe{H^>L_wH
zh{n}yxi6vEm-IJ~i5y*jdn=uyJv_koGZKaU<x4u}z6b@~{HSD90TKTj0ARc}J<V`G
zOp_+)+_Kkc(vGyAoH)|zqSc$Y`uxO0v6nrxdytdBMoz{H74%`OniMarjQYJWO1yRy
zK}u8AN!-qG(5V;1O!ap#w(0lG*wa(!Ota9r8Fp@+PXC{ok&K*}(s~ZX2-!XWH@{zv
zi#WB&SW{p#b8=~(L<cYRT$*gTA8G2xxd3^ZeT1hP{uL&spTI!<B&zgs%Nu5BpGx>8
z49pE|A!TqbW^S2%gr_9X3DL^UeU=-R2u#yfvfIpo&2QhDtUia5ZcTTXZT&U8CS#Ve
znPNG@Dzt3*NaqsDJ-M^S@SbBTqmN2IjkWbttV9iRU7*>#!Hr3Qg>zx?du68t2+;op
zSP8t=)N#T!alfSS@-U8vE2*by&O_;A-41%4xHlYZCxk416D4P{Pg1^yy{9qbLN*KR
zbu?RcS7oZf&f9_km_Eaa!UX{Q2=lUi1x2Wuz!@8TA^);tm1xWTwP=?!UFPhRxn;u;
zb0}=N%?I!5eo5MovvquBNCm#-;~q;W_o71fg~2zlRz~EE#S^EiN13_Ok!U*J?E<A{
zF=EcmwR~Zas}?z%eT3;Sgwu=^vS=zm>?AN^?SoLUy4_e~09O0gr=Qk9!Ct_6O2MWw
z4t1M~Q|3*SsT70^69P97D{Yek={7M-zK%fRguaX3t6Yp1ir6z-c2_vMx19>N+v5o*
zEG722)z0j7MVP`B?l6#@jaCp%S}i*_JtuK4zJ4WfE~6@s+8U3bt{$$9plv>;>StN;
z)=2Ep4mZc6zmJke!vzL0<#Vg|FEqSrUYN>jN`n3YiOIPv45qZm&Z)Fy|F3(nEMW$n
zd-`CJ$SDoDkMh-<_A$nKmd-yN_bmIehmGb#09KvTcb8X#1hO|sAL+K#Aw<e3_IOU{
zlvj<zp7bNkcteDD9Dq@61o~=Xe<rcU4D4<=*-OUL&tSA6hSC?I>E{7umdD6fBZskr
zg&aOW$yitdX<6XDS=?RUX?eSc=OpJnu1Y<E=6k;5`$FWF7c*^n`bPRQ5FS{baR_el
zbR%ZtQTHohgd_0Nu?wL%%Xs6g8wNQs(klA>xDdOsFlo8CftS=2^NDTP)6oT4(VO;v
z#poDG8U4BJUW$>D0c^|u6|T7s`Z5vBOBiS5z-uMF)pUsbL?{ukKFQ`sSUt*$ce?~L
z;-V##L2||66KtEBzkrdeC=uU879LnGN=5#TqdqQJRcVgvaLDXO0WYCM-@v;RZVYw1
z-@hLZ<G1y7-UA41#kVAOxVmZlOXA|q86~Q#Uj}{K4^98_3(`%CV2lp`vd7SK4?c!L
zT7cvW?U&a<fNX$ZaybM}ib09c=gM{AHO57={)sQ$T5nJr+fUTKRCRbmxjL4xq<)E&
zkh_~d`XxqW#+1{07oS8|O^X+6e;WYklN?4=rKd5f3^j)JQ`zB-E>iU-P-SJs-krh(
z4}YYR>^nt{0E~w}ApaJVFZ5OB5<Fj@GrIXB>|wG1OMnt@guGD9=LK_JK^Tq*8Jp$_
zvs>UG2Rq0KH2u^u1lwgrXYgy3h{3y2(EU(KDrw0c&rhYcBacHKFk>Y=2mp`=ICCmD
zocZ0@zQa_R%d^Iw>6bLx37pryQ;3V=qn*Q67c&9-%X9FTz>yfS*X`Al6YwK01?Xi)
zRsw_ZxyvS<$;4k&>qWJ}Fs>mpRf~|Os3DQojc?Z4ku>#@POJ@Y)S$^d#H9LmjS9_)
z^>WTn&CpW6!AkUF4<VZs4=IXcvXh*sUq@SJ29=bpvSiZ(r^D4<(=NZk#57m8=vLH%
zdQ7?QxSFy!U8$kZa?jk22qae~mEdEpG2@vlnyvp+&rxQUFAP5d>!SN{A0=5r9LS9A
zQC((ECkLay_yZ3%<1hBlQ1O3r8uPMA&7AdwJ`Wnkl_zS^TIVLzrybYyYiP>6$XkGC
zPO_U9`6Ew4?ZGo^+bJMp<ZO4mJ~&v+=urSLgEYJu9vAbFe4@Z~CrB7&_m-n`iX=YR
zEspsd%VrcUZsqG;&6;9xIOpf6GPC|v+%e2r$Mz@I4J5Mg6M;WbuOd~uq4Wo_bH~LP
zPmH}VW9&!7*o&M`(>4Y!=Dj55?FSC}=6-Aa4h~*f13&fycWUrnV@udUR*^JD<8r4?
ztoIg~g2xir;8x)syyaGB0%hAs>>|eFU1Ohm+Pouj;ZXyVxwGAH!0Y?Pzi?riy^COc
z{ManFQVTtGwm<B&`_YT1rjy1`U7qzxd;qtRot`=yqfCg>#aHoudTq;udvjvOo(6HR
z-Jh;pFBvyRO-LME_`CZu`Ypo@zQ2tP3LC@*$=E-kr1!ugvP^VQjCmLB@xHt8;VV4V
zB`oxNE;i$-9L?4a%9fA9<hSKHo9kE8`2><^x^VqY;`ai0;9h)tiv{r#qQFFBZvcRm
zSh#SItU$;OoB52Ft`oZf)MNuKUFg}mleh5lK^hQgK4kONhO_Q59yO!8m^1OvR+uPU
z)&&Oh<|^8>8;SY|3G#gzRV@SD=!H7*qO}ozE1_qTOC*__UO^_%q}xsw+d**7Tu5)}
zAtuDP>qYZ``yu<w>21}(&4%BIZbpftZ$@%SC0;KW#JBNF+8jJeADKt|B$VG3-1u)O
zQ56+Kuqu8VT7XEAI^3HPJoT%0&l4x}>B^n3kKa#bymkv~YEc^oKYv9L_kxrK@%xf-
zu{Zb-Klz27Ofj&a#2Hf&e}IPAf^aDs5eEW${5&(ka|6E>8R1S_QsKHHTw8?eWuqZn
zI~6XX5eQdQMIPCF`$H7(;$JRA{S%_{UZeOlvkjTNe#!<4O<!Zh7nBJm_|VqEu&vVh
z2intUU`93z>G7wc(QVGp!-1UjWb@y-2u&BPCtlwx_K%;D+i_d8B8()GNs6f|nULmT
zj5Uv%#|g=+huJ4hziLj%7l{NHVz(k#*<yy4>46getodc=MTJ=rGcCTV*uGtTq*|_4
Ss&iGp>Z0uT_o3y;Lg~NYKA|uG

literal 0
HcmV?d00001

diff --git a/__pycache__/proof.cpython-38.pyc b/__pycache__/proof.cpython-38.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..aca1409174df7a03e77fe9d601a16ba89956017c
GIT binary patch
literal 16353
zcmeHOOOPB#TCS?DeoW6p<B@Dhe#qtZOD&IOOZ%`_YkRGyS0InImdvt)?Ae~qno*B>
zx_h!}^r-FGAdq<k5fDBRz~TrgIEe!Xg2NI42RLvbmI#QwRd4{7i#fm<U6$|rvnsp0
zX2uV2#4f~+)LF00tjz!a@_%N%Gd*2*@VAh@v;2=29p}fq82u~Z;&uF@*H9=&xgBTS
zU36WZdmZnxIhL}cpB>AWoi`j+QvUmn@^5>K6;;0EG%6pV52xX#?gbV{TD%<nvoCwp
zb)3*ybd|H{DR<RbbyiBsQ>FLaMRcml?>mdWs;DZCWmQuXI960$P2yNpQ)(K=nwn92
zaGX%H>H!?<YEJFNaZ>G558^nb9#Z>poK^?aK^$k)!|D+n_ozqJV>r&LL+WuHA5ejM
z0>?S^1@$D3d(~6wX&m>dXVkMeKBx|>296J@BkDOE_p5pJJdOv{QS}0j2i1$}7>*CC
z<LZkzKBB&)zKr9e>MQCc93N9JtFPjCNS#n$!|`$Tih32tK)t5Ej^h*Rb#)TQFQ`-M
zG>%Uy7o<FsmM`jFZ)KrX86hCgJ^W7N7ac`0a0kwkGw@KlgAz(_)j?U3(r@#;tXQX_
z9Q5ifXb|3MRMT>&xg2)VdNYbP*ZXn1*G>J^UbB;yqd4qG>CD<@6t`E}ttOvEX({Yp
z2P?vUe6>+Y{V43L=rX#}9FnfGsIizpanI3HINU$pI&tNlDAduF^`6%4D`&#!THNbj
zS?%<eo1N#;V_WyS>tQ#((&t={_HU)NrKNVa9WO1hqi6<&<5ougB{M>nqj|L!$&vr@
z+{aJI^UFAiL4Y+(f6W`X2c6rVJ9d4|(-#J4uto^FFM+a4ASA8<#q1g+z2o0?T&G)$
zf%n_8E<i|sVUt+?*WbIlSo-GKGf8myYC8(>zuSw0_-YtL&Gj&7MsiNNHp*$auiM?Y
zKr4{)YVStF)05~ft#;boaA9*@=x2&)-Y;#0Y7Qq6>FT(1?yUT)d&z_$2cEac+5C^^
z9H3BQ9w(pySF-!--a&#w=rD2(8r|_Y&kQCX{RDsaN<*INS#)yGm0=b~=WljZ?-4wY
z1gkQ%q;3YrM`I%+k62Ac*2M|v>XNQFg8FOjekZ#UYR6s-9<2GdQRj^F?w7XQ*on&n
zTq%D)&+trmi*~A<-Kpev*we;*{sx&_Wg&HvnhY*D5hTI$pYWG>CxZL#M5C(rV6cMu
zw5*%m)i5n}!mdy#Ek&^w=;w@d+XW&C{Q~rmv9RXOxHT~HxSLaoIM{~f0uO;rEcpzZ
z;32MEi`^m*(>;V+@1$MfdLQ1OkI)Zq_H}WPkD<b04swK%4;n@m`r3V@FQdJT?Bhn7
zt;x00E2wK$Scbf`E^m56_cr^D@(2K_#ug`5d4B<mO9+}zrnIX2#ko9=`p<JNluHgl
z=}o!G?8t279b@1eTQ(wJNn%+nV?-Yl7<Wn|3n$rovegQsC{)3a@D1P0Lu4fdn+#q*
z$TO~JQ^-o6ZA$ZD+b`jH#tts~<RLSGVzm~LlK)W#S~>XpxL9?zN|1$a?B4eDGdT0i
z*}#Ql^wzxnc-~#JH7@2glnWVok+rr;gVLSSz`KhT)qOp$DbELaZ9QOLQq#v;cJD&o
zcK1m;m+gi<#86hZspd)x=Zr=wgYQwh8^z6TD@^@2H#>1!>+7D{Y{gMpY4-bJSEUuy
z2z3m4Qd}<9!cIu_am=0_Pu)(Dq&0SS7B#<$HqikTj_bSoumBH0u}n!h<JH}|n=6;R
z!5C4=JVHqX*YDzlB9(#$6XqEN>z2=n#U6<KYdG`e?50fHhnVu$%6Gjjh%CWWc??k%
zXlc~>K7}Ca;aD2D-*-N&WVI?-CRO5W<G14)OfIsamY*5pt62to>p}MSM*Di$4Vr-t
z`#Ow3BvIr+Zw2?(L6D%gycV|Nc~<B&TToV=PLMMoV!d{Z>!8;SgK%S0THDS~^qac5
z9%S0;*ooi*^i~k}f@pIYW<$IghiDu3c4=@tYjC3-UmZ4yU}*5YH-lG$Tl2w<HU_lo
z;BMkM8sFj&^I_Px-GBIPGby!wR`)BW<^2gvO_~PxpFZ8}QgM%rp1t=r<Dl6M&StY;
zXiS)8`~@&S_0Ddj)ogfa>B2WIrKPvOaY>YbS>03@_bNuO*YY8z`Pp$;RM(HOIKDWU
zbwel@!8<)16S_Z-J|jwTr$W5)A1#4r+`0!_V6PDkV=aCT;hzSCZvnzLKMBIO3=nVb
z2w~j-ll2i6&#|BlHwHjW-KMFd^ouNBU@_D!VyqnFy@G-n0Te)c1vNecpwMCrP_+B`
z6PfrQIQdwa*dLVEN|1l0HGiuzC=Yxnmw(TsVJ_#;1EeE-mKa9dZAd`n;mqUNhkhmt
zAwi8S>?T&q{t!}=eM5#y-=$CJTY8kf<t;n(eF)OEw0#uH|FBHyYh-TnUsmX>LsvyX
zAM!Ff5v+>zJ^B1=ryxOK3e1Zmu(H{0(VYrfy>6?sslq5Q&znk7+`?aI2Ho(65lfJ4
z^dz7Jdn@)W1<5PDXTk+imBN}=gp_R?+_)NQNN4s1XAG~WsYwGRAD(UYDcabPB(rbI
zj4z^f7Yd^r-1p{#WO5;d=nOR_d2%pl;?0nu?e%`Ajp;(a$D*>wu$)%Uo9Ag+{L$1W
zfef1IR}2Lz%y4RceVoM?S<pVxUq+F-CsX%S5$<JSOApT@ifyNCq$XX;8YJgaB11>6
zykycyQE4}3<x=@u&*cN?+Ss|1*|7(myDs48#Xc;n@@?+}SHA~asB*`-3-ds^Fbt}3
zjW&<+4#2-T<9y)0TiGh3erZrX=)@B+8UDsxDOh8;Q|BG?bZwGHbAN3Tz|QYasS=Ei
z%Am3~%^I)JA42%V)D=&U?cfzDpI7v(wyLVK<-2(Q#<`7G?ECq)>?(UdNA$`r@0a`8
zc>dR882GdzNwIiFRmJGR;-sezLEsIl*`ha|`5sj>HL|;VAPQ#1{Ptl@P9%R};knZ8
zD&u~yv~?5*{bpM*DGo%C8IH1i+A%!$?sY5;LRG=$h&MG5&BZWQ+x9)a2v0~&S$4qu
za0$U2S`Gu?2w@bgHY^Z6)9ux(ad4F{irOl)eV+S>&W9Mo3m?%*zI^|g^Vz66%^OkB
zYIdKE*&}RWtR?ACUYg9mJ>I9CP1tF#x4W6)ml->a2e`TzX;ER==b15TM2T>T=qFh`
z#o{1~hf$=}j9_Usqf|PX-Jvg*PQf08@gfdYl<vj6y08LoEtwNcUmNe)>Zf}(vyLBN
z=e6)UE4D)YEG`%8nC?k4NBt<DmxT+9laP#9o8l1^m-$RKth1Og?4;jBvxq9wDbK;e
zufyJd$bA_We;q5{$I5>hu6KT3$NgD6PxhIWKi<{PMF0iVHWBo*D*}FCm(<Uy2<U_>
zJ4yikbpX~#0R1{nFYA*iljkms)&GRmtxvHN8f0c&i(R<ey4Gh{?<|XREZ$)84HjZQ
z+U2Ux^IpM{99?rT4F4EaK94n5v@scFw!w@wT#Tz-1U3+wh>?VlV8qcFigKt#x-Y}~
zhW&UKDmYUpxfN*?N;UJd^MG#^3Z-ThO8H;j*ukgn28^8{$U{?ZrKjOJA8yVs&s*cB
zF`wP0I2!RPY2Jz3+Jv`B8>!vx!^gbd)a~YSM;z#u4q+jo9?d}0_t0pv$Sx|N%TO$$
z3%Z-@%f|Miu8~{u)h0Y!WAX834;lzcp|h>`pxFJ0TMCobbO=ofC6~#5=*XUR(fK^Q
z*+%*RvLD^&b!@Nal4mZ9B`RU^(bvQAMI-BvCy$=%Y4O~5Qed<k3m7N7(~6;%L9X~k
z7QXk&Lv6D-H99T*3uvkju_&OsZn`4}{~C`?Dxxw=U4dAU=!-0tIIKA48~s#qs~0fl
zbIJTD!NDLH<H90ih!@HJgsGj?_zbjPoRq#z!<`tQFYZ9$JtK`s=6~3Q%vk`sP<xEl
zG|R1N{#&@PG6H5V*8Wa1!efl>LrF4V&BNP-Us^?c&WBM9S&`kT-Su#P;x>ItW02-?
zJ0m~p%8w`MsqS|&leCVuQzAhmC7S%mE&!3^j4ihNom;^&M1Yup5^RHylt<Z&h`@9+
z@sKT~ZOfCZ8@VF0GHv5A&rjAqmRrFTwIj;p2;Y!(V*;vdAX>_fR>YQVckX`q0^Q8}
zd-I&v$oP{$CdweAOjM-MceBxM1<SXBg?rOGEnySV5Y2O#coEe_yEL6N_NCZ?1-CE{
zvH6^Y7JJeQ5t@VBOiMAXKu}{O#pPY&^f<eJM*q<)3dbyN2@B66D4Yj_^NPCz?gKRb
z9{>(;V~l(RaHTbPH=hi+0ij#|u(T`iD)5D>$qy~NjDKKx`S~JG*!#Jm&bUW*sCEkH
z^d(SPUq+GaGxHe-SmFz^^gFEfEfxiVJ|SJR=l{gh9atW?$sXeY*qUR;KLw06M3`Mh
zUc}jgv9SgLgA5D8{R~tgOF6?p6tX2HW<53zh~V(yn<H$W2?=A2An2c6+wi{fm=#I>
z#7;bm<B!=Ko%S^d^7mj&h)8d85jKPVErhHQYU#$|YN#35ryq+4Bvcmer;ur1Zz6Gt
zG<A=C*cWB8ppVdyHo`zoGueTF3_Ro*ZYP?tL)$KS^0aw|*cY1SFUqQAmkW&=+`OBN
zjv>Y^R;M_ZPm@s$tQfD;YV1Z9I4?_|2$RF$Vym>qcVB>&A+BMO$Mt2HPuDJT96v#A
z!{jo<J3idNDI|T6LCe(ku<GtyUPdPwmtkH?s>cI=_raJ%<mOsQ&&7!7NS1jH+^3qs
z)$KgVgGkI6zsstWT{DDP8Jd~NpILI|d7DwD8JiKxqPq$!G1CY0j3SaJj2wd60Kh2y
z55p{hvTq`=2E!6SK;s}hf`5kbUu@V{W}N364dX}Ojh+#67_#5C5=SLDybuBt&BEA%
zWtg=l2Fkvm2Et@Mhe>uP-&!KW8KP1q5iK;TCZ{K?7L~9>lrR`!@KS`zqR)PH6BSZ7
zH0byh)-H&Fsa9`&8M;eAG7alK;>HRGAgRee6Ab`N=8P;Dtv&`6qSlIo0WKK(hB!b<
zUQ(a{480CO0?S@`2-_WreY1rG!UDnoKstcnor~Q&6+ossDBmd$sv<Iui^!<NxMxKM
zL<9n2$o*vyssTb1BX-8$S<YONXzR+YF+jkA-$|4}0z9`ogc7)oJ4eFzmXGdM{mAmG
zhf$~T-m-n+Zlc4a7&DhgskX$vp(=7gK-Q0h$ZUW2-RHy?PM%!oWs^XJ+%z{$B80#Y
zFNawWCk=D4+0Uw))sojAc^yzyH?rqFunRk#*olFZAZ%A*lm)8<fg-!UgZ2`v61*9(
zQ6m(=HYcwTsGZCP#GP*@2`zG|4yjawbgCg7mC2_A26)?>?hZeVcYk{L4Je-ozd3<l
zIfGwytGr==SGID?7`+t>x}lyj#_b<io_$8p?T(_%P#jf3qc{@TG{V%~Fr-W52O}y;
z!=h+h^khv9d<>ReFc;%kDzqATIS^GFB1*6Dl_H`9Pomd`a_VDHB-mlBQ@2<YMApm@
z3U5Njy|6oiD$s8bU0EP=yxExjO6Sxj?*0%LJ0<Sm_;6DK_kds%17h+18pYU65kwBd
zF0!csnsCj#oohA|xBs*Wyib>8`zMRC^9Zotz%~QKiz5WlubZ@%Y_>C&BcDjJ4Oy-*
zHcpJGP0@x-J~uf)U*%ag+jAzvh(7FRp!a3+24dcdNGZH!r<O>;v1JrOUn&!Rk*0E!
zI|7G;w9S*lXR{3kk&%>z_vB%bD9|s1QTO*>W}wA3fyKumMnUpKpn9_Za5uUDt=SF+
zI#v3YSV$K61)d2|$FpsD+{9+vQm=CizvD%OPRYD3kt=66P7$9o=+bObIN%;)n$61<
z>S)#f!<bAh13w0n;zJi8IfQ`t<(~s4?OW`SM!@`uklfxnd3Gm6+Ij^*>NYr?1UrMz
zHX342z&6C5Kye4`X@+`>IGbdD8O*-93(Ouc>T{&#HoZydcN)Lw-%wb|hdpt~-g5KS
z50Ja%CI#cwm9YtcnOoOnZr^<md0TF_hK!R;Z51s#1MC?#cWmCZguJU~@~+IdZhWxu
zqG^ZhF5A4A_hD+~bq4;b11Wna-`o{X(16^kz`sBsd##S&B*IY$RLeH9JU?pW?v%<s
zjwzUj(_$XNqr6v1{?vlwe3qSqBVp5nCm`)0v4&zVPnYJwC*~{p)Fec)&?UiVeN5PN
zS>(vRW(0#aN+rVd<C3JdwP@}I{W=(w9JH@1=0KAN?W2*&1dSQvBS_j~DB+$$XCpby
zTHe+~ET81lp<uLndo)#P!o|!|>T4{hvKQ;ayyRjDPInQs6Y?J7@jHYpM`5-h(C*t;
znsWoUQeq0S;u#lY))OtB1tV<h|2HruhzaG-3}f8`>9#Xhm^RK_-ABz4z7B<s<*VLc
zm4c~N7ix=${@!O|R=%&83qzWZam&N2O8AM;IfWAj6&N_eLjQ^^WQ372zs|&!v1uf`
z9{mIXxh>gyR6>x*Pwv>&a-JK#5$<H-NQWyOMB-r@iE2R_J~%7^qnoeZ9QynVA$KV^
z^(`8~%nk)nZ#|5!N|b<R5>f=i8=WX*tf?#Jh4}UM)lH_Sbey-Ni)WuDbK3`#JcyUr
zPbKX01w?#=Ny5x=%USrCZS~gQ-hpe#L}LDL=M(=Ua;}bgPGw3AVi+Gbw?A5Oj7Q{;
zRSXi|%lG$EF(AUvPZ45-@mBn6mF&Y2$LvkZIAug|)pE|}60uWvVvKXA-VR%vIs%iB
z2+$!p#|YlSnPIMv(aip4Bn+Y8MaGcZRED(O)9J0YTc$Oso;)^6*k)iJ+ngkQUy?QT
z<6Hf3v2+sKslB(f=BDVhw9u1CIR{eMMA#?|b7w~U6_yNkud>+%j^-XI&*x65j$j+Z
zZJ>Rokw@x{5#C32OL((5u#?I$M2F_X0^m*{#@3*R^F*y#CfGZa5uYiWa<1<XL47G-
z6B2ZQ&S^Cx5cx1Rmq-Tlrfk4d!FpS%PB>f`$$nO36xAdUnBzTs;q03YBJ?JPs&B9m
zgkI;F6)5?xbe|n8mRTM%hi&$<`NrWiNA%|wtR==MAEN)33lok(Dvi-=45%kC1b*Mb
zu+ysSMq5R&>36UfO{fNoCZi9Yk%~3~iCDD=kq_j{CGG&s_dP{D(e#_xX%80*xNK2W
zP)-OAk(b5}<NnyL#BV`7aJ#ngJP;smB0w!tMdv_gd%4X{@(uuZd~7B)EwC4Bm$L2w
zJ>p^*?@P==x6M(3;2BoP!Ahzu*7CO$h5WQIH-F1tkpX0<<CFLxf3}Z$tkyOT@WrR`
ziylIOFCajF{2<2pof)W4>blA1w|kp*w<lJ3KBQnp_tu4;CbMN9STcO8r?1gf1)*2D
z*8sbTg`}Gue6QG!TAN@A#Wu(aw~tHzsBH@}a9Nvg^EkDfE=-T<udygB;#oMXvLJG*
z{4J@%IXeEF{ph4vY0P~agQZ!<ckorjU4iDn<A*+W86!lV!E*OyY`#}af_xoQ!ywDp
z)XNCkQE_D!XQLt(*jZzLYRY{h=)CjYk;Q4mSn9r!`dxlLR3N~Va69Yd?=2(%2U(F>
zFnF|5OQ=H%;g3SV##8<h7d9UVJebWVzy_51LG111MrA4z$rUhPbQy6tSog>;RN)iw
zh~O^j*HAZmf?UILT!oK;P054mZTJ(m20RfwoySvuP*sTC@#)5VM(!GVMiehYW*((6
zWS>y^w(AK<&$>uYlD%p^6J7K#AhM7=qIwXV{60daFJ?x*Wo5CNku2FGyE^2P5%Cd{
zedn@G9C<4W;>Kh#@f(0xL!(?vBy11wy~ScETqi^gEl%Z;4-PH$F^*_)hDbP1Vac13
z(Nf=IbK2*rd)<U;3ml(Ag5+eUBkeFJj_ya~`vJ5upNq{(LVzC%K`eNOC>pZZ?DnQ(
zXdp5y8qVQj;BqM-A1Gg-Vi~}gz}Hx!(N-m6G$y5Y(rRWoELKl<deNp1f%-|rB{S+r
zMg(r*RmDV_`BX}i9I4w(-Q^<kt1Z*xkB6Y2LdXV_oi?6y_Pp^FKhEXaSz1c#OH14!
z-QoGv(h?0u^F%Z7qnT3C6pUu)Ha{!WkF$7!#bFj-Vet}+*H~O&@g|FJvUr=t6&CNZ
zSZ1MEtg^VuVx2{og=P`4h*{iXk+AqKivf#YWpSIuZ?G6bLC&Umk4&Sij3~RXH+-Tt
zQ7hMK_*L<nt?k9X1GPtMhiZFp#or7{-ra+LhwyK@Hi<S9s9&kgN`FXWrJfG8#}}Mo
q@rx+9iB@v7>6930Z^@Tfk<n#43@xp_Vu<}3SY#|)CJp3Y>AwMVZcU~D

literal 0
HcmV?d00001

diff --git a/abelian_proof.py b/abelian_proof.py
index 475f456..341e2bb 100644
--- a/abelian_proof.py
+++ b/abelian_proof.py
@@ -1,6 +1,5 @@
 from proof import *
 from element import *
-from environment import *
 from group import *
 from integer import *
 from logicObjects import *
@@ -9,18 +8,22 @@
 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.introGroup(G)
-G.newElement('a')
-G.newElement('b')
-G.mulElements('a','b')
+#G.newElement('a')
+#G.newElement('b')
+#G.mulElements('a','b')
+p.introElement(G,'a')
+p.introElement(G,'b')
+p.closure(G,'a','b')
 p.accessAssumption()
-p.forallElim(1,['a * b'])
-p.leftMult(G.elements['a'],2)
-p.forallElim(1,['a'])
-p.substituteRHS(3,4)
-p.identleft(5)
-p.identright(6)
-p.rightMult(G.elements['b'],7)
-p.forallElim(1,['b'])
-p.substituteRHS(8,9)
-p.identleft(10)
-p.qed(['b','a'],11)
+p.forallElim(4,['a * b'])
+p.leftMult(G.elements['a'],5)
+p.forallElim(4,['a'])
+p.substituteRHS(6,7)
+p.identleft(8)
+p.identright(9)
+p.rightMult(G.elements['b'],10)
+p.forallElim(4,['b'])
+p.substituteRHS(11,12)
+p.identleft(13)
+p.forAllIntroduction(14,["a","b"],[1,2])
+p.qed(15)
diff --git a/environment.py b/environment.py
deleted file mode 100644
index c8ffba8..0000000
--- a/environment.py
+++ /dev/null
@@ -1,34 +0,0 @@
-import copy
-
-class Environment:
-    env = [{}]
-    assumption = []
-    depth = 0
-    
-    #ELEMENTS
-
-    def getElem(self, elem):
-        return self.env[self.depth]["Elements"][elem]
-
-    def addElemProp(self, elem, type, prop):
-        #type could be in group, or equality, ect
-        self.env[self.depth]["Elements"][elem][type].append(prop)
-
-    #GROUPS
-
-    def getGroup(self, group):
-        return self.env[self.depth]["Groups"][group]
-
-    def addGroupProp(self, group, type, prop):
-        #type could be for all, contains, ect
-        self.env[self.depth]["Groups"][group][type].append(prop)
-    
-    def newSubproof(self, assume):
-        self.env.append(self.env[-1].copy())
-        self.assumption.append(assume)
-        self.depth+=1
-
-    def endSubproof(self):
-        self.env.pop()
-        self.depth -= 1
-        return self.assumption.pop()
\ No newline at end of file
diff --git a/logicObjects.py b/logicObjects.py
index 44d0f49..e90723f 100644
--- a/logicObjects.py
+++ b/logicObjects.py
@@ -82,6 +82,14 @@ class Bottom:
     def elim(self, conclusion):
         return conclusion
 
+class In:
+    def __init__(self, elem, grp):
+        self.elem = elem
+        self.grp = grp
+
+    def __repr__(self):
+        return str(self.elem) + " ∈ " + str(self.grp)
+
 class Eq:
     def __init__(self,LHS,RHS,pg):
         self.LHS = LHS
@@ -131,18 +139,28 @@ def __repr__(self):
         return 'forall(' + str(self.arbelems) + ' in ' + str(self.group) + ', ' + str(self.eq) +')'
 
     def __eq__(self,other):
-        return self.arbelems == other.arbelems and self.group == other.group and self.eq == other.eq
+        if not isinstance(other,forall):
+            return False
+        if len(self.arbelems)==len(other.arbelems):
+            print(self,other)
+            new = copy.deepcopy(self)
+            replaced = new.replace(other.arbelems)
+            return replaced == other.eq
+        else:
+            return False
 
 
     def replace(self, replacements): # replacements = ['x','y'] - strings of the elements
         if len(replacements) == len(self.arbelems):
-            if all(elem in self.group.elements for elem in replacements): # check if replacements are all normal elements of self.group
-                neweq = copy.deepcopy(self.eq)
-                for i in range(len(replacements)):
-                    neweq = neweq.replace(Mult([self.arbelems[i]]),self.group.elements[replacements[i]]) # repeatedly replace
-                return neweq
-            else:
-                print(f"Replacements contains elements that are not in {self.group}")
+            #if all(elem in self.group.elements for elem in replacements): # check if replacements are all normal elements of self.group
+            #The scope of thee elements in a for all should be contained in that for all
+            #Checking if in the group should happen at elimination and introduction
+            neweq = copy.deepcopy(self.eq)
+            for i in range(len(replacements)):
+                 neweq = neweq.replace(Mult([self.arbelems[i]]),self.group.elements[replacements[i]]) # repeatedly replace
+            return neweq
+            #else:
+                #print(f"Replacements contains elements that are not in {self.group}")
         else:
             print("Replacements is not the same length as the list of arbitrary elements")
 
diff --git a/proof.py b/proof.py
index 6508d36..5238355 100644
--- a/proof.py
+++ b/proof.py
@@ -1,5 +1,5 @@
+from re import L
 from element import *
-from environment import *
 from group import *
 from integer import *
 from logicObjects import *
@@ -12,21 +12,17 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []):
         self.goal = goal # this is an implies
         self.steps = []
         self.justifications = []
-        self.environment = {} # add strings names to environment for parsing 
+        self.env = {}
         self.depth = 0
-        # self.currAssumption = [goal.assum] # is this neccessary?
-        self.show() 
     
-    def qed(self, replacements, lineNum):
-        if isinstance(self.goal, forall): # how do I know a line is a replacement of a forall?
-            if self.goal.replace(replacements) == self.steps[lineNum]: # how do I know replacement variables are all arbitrarily introduced?
-                self.steps += [True]
-                self.justifications += [f"Proof is finished by line {lineNum}"]
-                self.show()
-            else:
-                print("Hmm, that line doesn't seem to prove what you think it does. Is there another line you meant? You may have also replaced incorrectly.")
-        else:    
-            return self.goal.conc in self.steps
+    def qed(self, lineNum):
+        print(self.goal, self.steps[lineNum])
+        if self.goal == self.steps[lineNum]:
+            self.steps+=["□"]
+            self.justifications += ["QED"]
+            self.show()
+        else:
+            print("This is not the same as the goal")
 
     def undo(self):
         self.steps = self.steps[:-1]
@@ -50,7 +46,7 @@ def introGroup(self, grp):
         self.steps += [grp]
         self.justifications += ["introGroup"]
         #deal with environments
-        self.environment[grp.groupName] = grp
+        self.env[grp.groupName] = grp
         self.show()
     
     def accessAssumption(self):
@@ -461,3 +457,31 @@ def concludeSubproof(self, lineNum):
         """
         conc = Implies(self.assumption, self.steps[lineNum])
         return conc
+
+    def introElement(self,G, name):
+        self.env[name] = G.newElement(name)
+        self.steps += [In(name, G)]
+        self.justifications += ["Introducing an arbitrary element"]
+        self.show()
+    
+    def forAllIntroduction(self, equationLine, vars, elemIntroLines):
+        evidence = copy.deepcopy(self.steps[equationLine])
+        G = self.steps[elemIntroLines[0]].grp
+        #Checking that the lines introduce the arbitrary variables, and that the variables are all in the same group
+        for i in range(len(vars)):
+            v = vars[i]
+            l = elemIntroLines[i]
+            if self.steps[l].elem!=vars[i]:
+                print("Line", l, "does not introduce variable", v)
+            if self.steps[l].grp!=G:
+                print("Element", v, "is not in group", G)
+        #If you make it here, this is a valid for all intro
+        self.steps+=[forall(vars,G,self.steps[equationLine])]
+        self.justifications+=["For all introduction"]
+        self.show()
+
+    def closure(self,G,a,b):
+        G.mulElements(a,b)
+        self.steps+=[In(G,Mult([a,b]))]
+        self.justifications+=["Closure"]
+        self.show()
diff --git a/proofs/proof1.py b/proofs/proof1.py
deleted file mode 100644
index e69de29..0000000