apply RTC.head
case hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep
    (Stmt.ifThenElse (fun s => s "x" > s "y")
        ((Stmt.skip; Stmt.assign "x" fun s => s "x" - 1);
          Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1))
        Stmt.skip,
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
case hbc.hbc.hbc.hbc.hbc.hbc.hab

⊢ (Stmt.ifThenElse (fun s => s "x" > s "y")
        ((Stmt.skip; Stmt.assign "x" fun s => s "x" - 1);
          Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1))
        Stmt.skip,
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⇒
    ?hbc.hbc.hbc.hbc.hbc.hbc.b

case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep ?hbc.hbc.hbc.hbc.hbc.hbc.b (Stmt.skip, fun x => 0)

case hbc.hbc.hbc.hbc.hbc.hbc.b

⊢ Stmt × State