Proof: Do Expr At Unchanged 45

Let's prove the following theorem:

if the following are true:

expression state at time 45 = "begin_expr"
the expression at time 45 = __add__(self.x, 5)

then the expression at time 46 = __add__(self.x, 5)

Proof:

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

Given

1	expression state at time 45 = "begin_expr"
2	the expression at time 45 = `__add__(self.x, 5)`

Proof Table

#	Claim	Reason
1	the expression at time (45 + 1) = the expression at time 45	if expression state at time 45 = "begin_expr", then the expression at time (45 + 1) = the expression at time 45 (Insn Count Begin Expression (1))
2	the expression at time (45 + 1) = `__add__(self.x, 5)`	if the expression at time (45 + 1) = the expression at time 45 and the expression at time 45 = `__add__(self.x, 5)`, then the expression at time (45 + 1) = `__add__(self.x, 5)` (Transitive Property of Equality)
3	45 + 1 = 46	45 + 1 = 46 (Fixed Value Statement)
4	the expression at time (45 + 1) = the expression at time 46	if 45 + 1 = 46, then the expression at time (45 + 1) = the expression at time 46 (Substitution)
5	the expression at time 46 = `__add__(self.x, 5)`	if the expression at time (45 + 1) = the expression at time 46 and the expression at time (45 + 1) = `__add__(self.x, 5)`, then the expression at time 46 = `__add__(self.x, 5)` (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments