Proof: Get Begin Expr Params Unchanged15

Let's prove the following theorem:

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

then arguments stack at time 16 = [ [ 9, [ ] ], [ ] ]

Proof:

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

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

Comments

Please log in to add comments