Proof: Write Assign Const Line 25

Let's prove the following theorem:

if the following are true:
  • the line at time 25 = 6
  • the tab at time 25 = 1
  • statement at line 6, tab 1 = a = 9
  • 9 is constant

then the line at time 26 = 7

Proof:

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

Given
1 the line at time 25 = 6
2 the tab at time 25 = 1
3 statement at line 6, tab 1 = a = 9
4 9 is constant
Proof Table
# Claim Reason
1 the line at time (25 + 1) = 6 + 1 if the line at time 25 = 6 and the tab at time 25 = 1 and statement at line 6, tab 1 = a = 9 and 9 is constant, then the line at time (25 + 1) = 6 + 1
2 6 + 1 = 7 6 + 1 = 7
3 the line at time (25 + 1) = 7 if the line at time (25 + 1) = 6 + 1 and 6 + 1 = 7, then the line at time (25 + 1) = 7
4 25 + 1 = 26 25 + 1 = 26
5 the line at time (25 + 1) = the line at time 26 if 25 + 1 = 26, then the line at time (25 + 1) = the line at time 26
6 the line at time 26 = 7 if the line at time (25 + 1) = the line at time 26 and the line at time (25 + 1) = 7, then the line at time 26 = 7

Comments

Please log in to add comments