apply RTC.tail
case while_false
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ RTC SmallStep (Stmt.whileDo B S, s) (Stmt.skip, s)
case while_false.hab
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ RTC SmallStep (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