Proof: Write Assign Const Stack At 11

Let's prove the following theorem:

if the following are true:
  • the line at time 11 = 2
  • the tab at time 11 = 1
  • statement at line 2, tab 1 = a = 7
  • 7 is constant
  • stack at time 11 = [ ]

then stack at time 12 = [ ]

Proof:

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

Given
1 the line at time 11 = 2
2 the tab at time 11 = 1
3 statement at line 2, tab 1 = a = 7
4 7 is constant
5 stack at time 11 = [ ]
Proof Table
# Claim Reason
1 stack at time (11 + 1) = stack at time 11 if the line at time 11 = 2 and the tab at time 11 = 1 and statement at line 2, tab 1 = a = 7 and 7 is constant, then stack at time (11 + 1) = stack at time 11
2 stack at time (11 + 1) = [ ] if stack at time (11 + 1) = stack at time 11 and stack at time 11 = [ ], then stack at time (11 + 1) = [ ]
3 11 + 1 = 12 11 + 1 = 12
4 stack at time (11 + 1) = stack at time 12 if 11 + 1 = 12, then stack at time (11 + 1) = stack at time 12
5 stack at time 12 = [ ] if stack at time (11 + 1) = stack at time 12 and stack at time (11 + 1) = [ ], then stack at time 12 = [ ]

Comments

Please log in to add comments