apply SmallStep.whileDo
case while_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.whileDo B S, s) ⇒ ?while_true.b
no goals