Theorem: LoVe.BigStep_while_true_Iff (LoVe/Lectures/LoVe09_OperationalSemantics_Demo.lean)

State before:
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (Stmt.whileDo B S, s) ⟹ u ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
rw [BigStep_while_Iff]
State after:
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u

State before:
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
simp [hcond]
State after:
no goals