apply SmallStep.whileDo
case while_false.hab.hab
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⇒ ?while_false.b

case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ?while_false.b ⇒ (Stmt.skip, s)

case while_false.b
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ Stmt × State
case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ (Stmt.skip, s)