Proof: If Test True Store Example

Let's prove the following theorem:

if the following are true:

the line at time 10 = 1
the tab at time 10 = 0
statement at line 1, tab 0 = if __eq__(3, 3):
expression state at time 10 = "end_expr"
Return Value at time 10 = True
Control Map at time 10 = [ ]

then Control Map at time 11 = [ entry 0: (pair ("if", True)), [ ] ]

Code Editor

LW Python State

Current Line

Current Tab

Time

LW Python Simulator

The proof uses the If Test True Store Property to show that pair "if":True is set to the "Control" map at time 10 + 1, then some algebra to simplify the time to 11.

Proof:

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

Given

1	the line at time 10 = 1
2	the tab at time 10 = 0
3	statement at line 1, tab 0 = `if __eq__(3, 3):`
4	expression state at time 10 = "end_expr"
5	Return Value at time 10 = True
6	Control Map at time 10 = [ ]

Proof Table

#	Claim	Reason
1	Control Map at time (10 + 1) = result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10)	if the line at time 10 = 1 and the tab at time 10 = 0 and statement at line 1, tab 0 = `if __eq__(3, 3):` and expression state at time 10 = "end_expr" and Return Value at time 10 = True, then Control Map at time (10 + 1) = result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) (If Test True Store Property)
2	result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) = result of storing (pair ("if", True)) at key: 0 in map: [ ]	if Control Map at time 10 = [ ], then result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) = result of storing (pair ("if", True)) at key: 0 in map: [ ] (Substitution)
3	result of storing (pair ("if", True)) at key: 0 in map: [ ] = [ entry 0: (pair ("if", True)), [ ] ]	result of storing (pair ("if", True)) at key: 0 in map: [ ] = [ entry 0: (pair ("if", True)), [ ] ] (do_set_key_value_10_0)
4	result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) = [ entry 0: (pair ("if", True)), [ ] ]	if result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) = result of storing (pair ("if", True)) at key: 0 in map: [ ] and result of storing (pair ("if", True)) at key: 0 in map: [ ] = [ entry 0: (pair ("if", True)), [ ] ], then result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) = [ entry 0: (pair ("if", True)), [ ] ] (Transitive Property of Equality)
5	Control Map at time (10 + 1) = [ entry 0: (pair ("if", True)), [ ] ]	if Control Map at time (10 + 1) = result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) and result of storing (pair ("if", True)) at key: 0 in map: (Control Map at time 10) = [ entry 0: (pair ("if", True)), [ ] ], then Control Map at time (10 + 1) = [ entry 0: (pair ("if", True)), [ ] ] (Transitive Property of Equality)
6	10 + 1 = 11	10 + 1 = 11 (Fixed Value Statement)
7	Control Map at time (10 + 1) = Control Map at time 11	if 10 + 1 = 11, then Control Map at time (10 + 1) = Control Map at time 11 (Substitution)
8	Control Map at time 11 = [ entry 0: (pair ("if", True)), [ ] ]	if Control Map at time (10 + 1) = Control Map at time 11 and Control Map at time (10 + 1) = [ entry 0: (pair ("if", True)), [ ] ], then Control Map at time 11 = [ entry 0: (pair ("if", True)), [ ] ] (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments