Proof: Get Begin Expr Params Unchanged3

Let's prove the following theorem:

if the following are true:
  • the expression at time 3 = 1
  • expression state at time 3 = "begin_expr"
  • 1 is constant
  • arguments stack at time 3 = [ [ 3, [ ] ], [ ] ]

then arguments stack at time 4 = [ [ 3, [ ] ], [ ] ]

Proof:

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

Given
1 the expression at time 3 = 1
2 expression state at time 3 = "begin_expr"
3 1 is constant
4 arguments stack at time 3 = [ [ 3, [ ] ], [ ] ]
Proof Table
# Claim Reason
1 arguments stack at time (3 + 1) = arguments stack at time 3 if expression state at time 3 = "begin_expr" and the expression at time 3 = 1 and 1 is constant, then arguments stack at time (3 + 1) = arguments stack at time 3
2 arguments stack at time (3 + 1) = [ [ 3, [ ] ], [ ] ] if arguments stack at time (3 + 1) = arguments stack at time 3 and arguments stack at time 3 = [ [ 3, [ ] ], [ ] ], then arguments stack at time (3 + 1) = [ [ 3, [ ] ], [ ] ]
3 3 + 1 = 4 3 + 1 = 4
4 arguments stack at time (3 + 1) = arguments stack at time 4 if 3 + 1 = 4, then arguments stack at time (3 + 1) = arguments stack at time 4
5 arguments stack at time 4 = [ [ 3, [ ] ], [ ] ] if arguments stack at time (3 + 1) = arguments stack at time 4 and arguments stack at time (3 + 1) = [ [ 3, [ ] ], [ ] ], then arguments stack at time 4 = [ [ 3, [ ] ], [ ] ]

Comments

Please log in to add comments