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

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

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