Proof: Write Method Def 1

Let's prove the following theorem:

if the following are true:

the line at time 1 = 2
the tab at time 1 = 1
statement at line 2, tab 1 = def __init__(self):
value at "Animal" in map (Class Map at time 1) = [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]
value at "methods" in map [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ ]
Class Map at time 1 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ]

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

Proof:

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

Given

1	the line at time 1 = 2
2	the tab at time 1 = 1
3	statement at line 2, tab 1 = `def __init__(self):`
4	value at "Animal" in map (Class Map at time 1) = [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]
5	value at "methods" in map [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ ]
6	Class Map at time 1 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ]

Proof Table

#	Claim	Reason
1	Class Map at time (1 + 1) = result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1)	if the line at time 1 = 2 and the tab at time 1 = 1 and statement at line 2, tab 1 = `def __init__(self):` and value at "Animal" in map (Class Map at time 1) = [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] and value at "methods" in map [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ ], then Class Map at time (1 + 1) = result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) (Method Definition Property)
2	result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ] = [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ]	result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ] = [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ] (do_set_key_value_1_0)
3	result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = result of storing [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ] at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]	if result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ] = [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], then result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = result of storing [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ] at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] (Substitution)
4	result of storing [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ] at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ]	result of storing [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ] at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] (do_set_key_value_1_1)
5	result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ]	if result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = result of storing [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ] at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] and result of storing [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ] at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], then result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] (Transitive Property of Equality)
6	result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1)	if result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], then result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) (Substitution)
7	result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ]	if Class Map at time 1 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ], then result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] (Substitution)
8	result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]	result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] (do_set_key_value_1_2)
9	result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]	if result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] and result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ], then result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] (Transitive Property of Equality)
10	result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]	if result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) and result of storing [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ], then result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] (Transitive Property of Equality)
11	Class Map at time (1 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]	if Class Map at time (1 + 1) = result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) and result of storing (result of storing (result of storing [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ] at key: "__init__" in map: [ ]) at key: "methods" in map: [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ]) at key: "Animal" in map: (Class Map at time 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ], then Class Map at time (1 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] (Transitive Property of Equality)
12	1 + 1 = 2	1 + 1 = 2 (Fixed Value Statement)
13	Class Map at time (1 + 1) = Class Map at time 2	if 1 + 1 = 2, then Class Map at time (1 + 1) = Class Map at time 2 (Substitution)
14	Class Map at time 2 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]	if Class Map at time (1 + 1) = Class Map at time 2 and Class Map at time (1 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ], then Class Map at time 2 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments