Proof: Assign Constant Example 2

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 = c = 16
16 is constant

then the line at time 1 = 2

Code Editor

LW Python State

Current Line

Current Tab

Time

LW Python Simulator

Line is initially 1. Using Constant Assignment Property 2, we claim that at time 0+1, line is 1+1. After some algebra, we conclude that the line at time 1 = 2.

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 = `c = 16`
4	16 is constant

Proof Table

#	Claim	Reason
1	the line at time (0 + 1) = 1 + 1	if the line at time 0 = 1 and the tab at time 0 = 0 and statement at line 1, tab 0 = `c = 16` and 16 is constant, then the line at time (0 + 1) = 1 + 1 (Constant Assignment Property 2)
2	1 + 1 = 2	1 + 1 = 2 (Fixed Value Statement)
3	the line at time (0 + 1) = 2	if the line at time (0 + 1) = 1 + 1 and 1 + 1 = 2, then the line at time (0 + 1) = 2 (Transitive Property of Equality)
4	0 + 1 = 1	0 + 1 = 1 (Fixed Value Statement)
5	the line at time (0 + 1) = the line at time 1	if 0 + 1 = 1, then the line at time (0 + 1) = the line at time 1 (Substitution)
6	the line at time 1 = 2	if the line at time (0 + 1) = the line at time 1 and the line at time (0 + 1) = 2, then the line at time 1 = 2 (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments