Proof: Prove Find Method Params 39

Let's prove the following theorem:

if Class Map at time 39 = [ 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 "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then method parameters where the Class Map is (Class Map at time 39), class name is "Dog", and method name is "move" = [ self, [ ] ]

Proof:

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

Given
1 Class Map at time 39 = [ 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 "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]
Proof Table
# Claim Reason
1 definition of method "move" of class "Dog" in (Class Map at time 39) = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ] if Class Map at time 39 = [ 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 "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then definition of method "move" of class "Dog" in (Class Map at time 39) = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ]
2 value at "params" in map [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ] = [ self, [ ] ] value at "params" in map [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ] = [ self, [ ] ]
3 method parameters where the Class Map is (Class Map at time 39), class name is "Dog", and method name is "move" = [ self, [ ] ] if definition of method "move" of class "Dog" in (Class Map at time 39) = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ] and value at "params" in map [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ] = [ self, [ ] ], then method parameters where the Class Map is (Class Map at time 39), class name is "Dog", and method name is "move" = [ self, [ ] ]

Comments

Please log in to add comments