Proof: Write Else Line 24

Let's prove the following theorem:

if the following are true:

the line at time 24 = 5
the tab at time 24 = 0
statement at line 5, tab 0 = else:
Control Map at time 24 = [ entry 0: (pair ("if", False)), [ ] ]

then the line at time 25 = 6

Proof:

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

Given

1	the line at time 24 = 5
2	the tab at time 24 = 0
3	statement at line 5, tab 0 = `else:`
4	Control Map at time 24 = [ entry 0: (pair ("if", False)), [ ] ]

Proof Table

#	Claim	Reason
1	value at 0 in map (Control Map at time 24) = pair ("if", False)	if Control Map at time 24 = [ entry 0: (pair ("if", False)), [ ] ], then value at 0 in map (Control Map at time 24) = pair ("if", False) (Get Key Value Control Map At 24)
2	the line at time (24 + 1) = 5 + 1	if the line at time 24 = 5 and the tab at time 24 = 0 and statement at line 5, tab 0 = `else:` and value at 0 in map (Control Map at time 24) = pair ("if", False), then the line at time (24 + 1) = 5 + 1 (Else Statement Line Property)
3	5 + 1 = 6	5 + 1 = 6 (Fixed Value Statement)
4	the line at time (24 + 1) = 6	if the line at time (24 + 1) = 5 + 1 and 5 + 1 = 6, then the line at time (24 + 1) = 6 (Transitive Property of Equality)
5	24 + 1 = 25	24 + 1 = 25 (Fixed Value Statement)
6	the line at time (24 + 1) = the line at time 25	if 24 + 1 = 25, then the line at time (24 + 1) = the line at time 25 (Substitution)
7	the line at time 25 = 6	if the line at time (24 + 1) = the line at time 25 and the line at time (24 + 1) = 6, then the line at time 25 = 6 (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments