Proof: Get Begin Expr Params Unchanged6

Let's prove the following theorem:

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

then arguments stack at time 7 = [ [ ], [ ] ]

Proof:

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

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

Comments

Please log in to add comments