Proof: Write Class Def 7

Let's prove the following theorem:

if the following are true:

the line at time 7 = 7
the tab at time 7 = 0
statement at line 7, tab 0 = class Dog(Animal):
Class Map at time 7 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

then Class Map at time 8 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]

Proof:

View as a tree | View dependent proofs | Try proving it

Given

1	the line at time 7 = 7
2	the tab at time 7 = 0
3	statement at line 7, tab 0 = `class Dog(Animal):`
4	Class Map at time 7 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

Proof Table

#	Claim	Reason
1	Class Map at time (7 + 1) = result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7)	if the line at time 7 = 7 and the tab at time 7 = 0 and statement at line 7, tab 0 = `class Dog(Animal):`, then Class Map at time (7 + 1) = result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) (Class Statement Property)
2	result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) = result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]	if Class Map at time 7 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ], then result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) = result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] (Substitution)
3	result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]	result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] (do_set_key_value_7_0)
4	result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]	if result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) = result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] and result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] (Transitive Property of Equality)
5	Class Map at time (7 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]	if Class Map at time (7 + 1) = result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) and result of storing [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ] at key: "Dog" in map: (Class Map at time 7) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then Class Map at time (7 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] (Transitive Property of Equality)
6	7 + 1 = 8	7 + 1 = 8 (Fixed Value Statement)
7	Class Map at time (7 + 1) = Class Map at time 8	if 7 + 1 = 8, then Class Map at time (7 + 1) = Class Map at time 8 (Substitution)
8	Class Map at time 8 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]	if Class Map at time (7 + 1) = Class Map at time 8 and Class Map at time (7 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then Class Map at time 8 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments