Proof: Write Class Def 0

Let's prove the following theorem:

if the following are true:
  • the line at time 0 = 1
  • the tab at time 0 = 0
  • statement at line 1, tab 0 = class Animal:
  • Class Map at time 0 = [ ]

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

Proof:

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

Given
1 the line at time 0 = 1
2 the tab at time 0 = 0
3 statement at line 1, tab 0 = class Animal:
4 Class Map at time 0 = [ ]
Proof Table
# Claim Reason
1 Class Map at time (0 + 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) if the line at time 0 = 1 and the tab at time 0 = 0 and statement at line 1, tab 0 = class Animal:, then Class Map at time (0 + 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0)
2 result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) = result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ ] if Class Map at time 0 = [ ], then result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) = result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ ]
3 result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ]
4 result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] if result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) = result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ ] and result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: [ ] = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ], then result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ]
5 Class Map at time (0 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] if Class Map at time (0 + 1) = result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) and result of storing [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ] at key: "Animal" in map: (Class Map at time 0) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ], then Class Map at time (0 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ]
6 0 + 1 = 1 0 + 1 = 1
7 Class Map at time (0 + 1) = Class Map at time 1 if 0 + 1 = 1, then Class Map at time (0 + 1) = Class Map at time 1
8 Class Map at time 1 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ] if Class Map at time (0 + 1) = Class Map at time 1 and Class Map at time (0 + 1) = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ], then Class Map at time 1 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ ], [ entry "line": 1, [ ] ] ] ], [ ] ]

Comments

Please log in to add comments