Proof: Get Begin Expr Params 1

Let's prove the following theorem:

if the following are true:
  • expression state at time 1 = "begin_expr"
  • the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}
  • arguments stack at time 1 = [ ]

then arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]

Proof:

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

Given
1 expression state at time 1 = "begin_expr"
2 the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}
3 arguments stack at time 1 = [ ]
Proof Table
# Claim Reason
1 arguments stack at time (1 + 1) = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], arguments stack at time 1 ] if expression state at time 1 = "begin_expr" and the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}, then arguments stack at time (1 + 1) = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], arguments stack at time 1 ]
2 [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], arguments stack at time 1 ] = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ] if arguments stack at time 1 = [ ], then [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], arguments stack at time 1 ] = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]
3 arguments stack at time (1 + 1) = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ] if arguments stack at time (1 + 1) = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], arguments stack at time 1 ] and [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], arguments stack at time 1 ] = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ], then arguments stack at time (1 + 1) = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]
4 1 + 1 = 2 1 + 1 = 2
5 arguments stack at time (1 + 1) = arguments stack at time 2 if 1 + 1 = 2, then arguments stack at time (1 + 1) = arguments stack at time 2
6 arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ] if arguments stack at time (1 + 1) = arguments stack at time 2 and arguments stack at time (1 + 1) = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ], then arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]

Comments

Please log in to add comments