Proof: Write Else Tab24

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 tab at time 25 = 1

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 tab at time (24 + 1) = 0 + 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 tab at time (24 + 1) = 0 + 1 (Else Statement Tab Property)
3	0 + 1 = 1	0 + 1 = 1 (Fixed Value Statement)
4	the tab at time (24 + 1) = 1	if the tab at time (24 + 1) = 0 + 1 and 0 + 1 = 1, then the tab at time (24 + 1) = 1 (Transitive Property of Equality)
5	24 + 1 = 25	24 + 1 = 25 (Fixed Value Statement)
6	the tab at time (24 + 1) = the tab at time 25	if 24 + 1 = 25, then the tab at time (24 + 1) = the tab at time 25 (Substitution)
7	the tab at time 25 = 1	if the tab at time (24 + 1) = the tab at time 25 and the tab at time (24 + 1) = 1, then the tab at time 25 = 1 (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments