diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000..c8693d7 Binary files /dev/null and b/.DS_Store differ diff --git a/__pycache__/element.cpython-39.pyc b/__pycache__/element.cpython-39.pyc index 9dd0787..b886ac3 100644 Binary files a/__pycache__/element.cpython-39.pyc and b/__pycache__/element.cpython-39.pyc differ diff --git a/__pycache__/group.cpython-39.pyc b/__pycache__/group.cpython-39.pyc index e2a172c..bb40103 100644 Binary files a/__pycache__/group.cpython-39.pyc and b/__pycache__/group.cpython-39.pyc differ diff --git a/__pycache__/integer.cpython-39.pyc b/__pycache__/integer.cpython-39.pyc index 2546654..504441c 100644 Binary files a/__pycache__/integer.cpython-39.pyc and b/__pycache__/integer.cpython-39.pyc differ diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc index 74f4fb5..a913b8e 100644 Binary files a/__pycache__/logicObjects.cpython-39.pyc and b/__pycache__/logicObjects.cpython-39.pyc differ diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index 9a283a2..e9a55eb 100644 Binary files a/__pycache__/proof.cpython-39.pyc and b/__pycache__/proof.cpython-39.pyc differ 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)) +