Proof: Get Begin Expr Params Unchanged70

Let's prove the following theorem:

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

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

Proof:

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

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

Comments

Please log in to add comments