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

State before:
⊢ RTC SmallStep (sillyLoop, State.update "x" 1 fun x => 0) (Stmt.skip, fun x => 0)
Tactic:
rw [sillyLoop]
State after:
⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)

State before:
⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
State after:
case hab

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

case hbc

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

case b

⊢ Stmt × State

State before:
case hab

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

case hbc

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

case b

⊢ Stmt × State
Tactic:
{ apply SmallStep.whileDo }
State after:
case 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" 1 fun x => 0)
    (Stmt.skip, fun x => 0)

State before:
case 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" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.if_true
    simp }
  { apply RTC.head
    { apply SmallStep.seq_step
      apply SmallStep.seq_skip }
    { apply RTC.head
      { apply SmallStep.seq_step
        apply SmallStep.assign }
      { apply RTC.head
        { apply SmallStep.seq_skip }
        { apply RTC.head
          { apply SmallStep.whileDo }
          { apply RTC.head
            { apply SmallStep.if_false
              simp }
            { simp
              apply RTC.refl } } } } } } }
State after:
no goals

State before:
case hab

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0) ⇒
    ?b
Tactic:
apply SmallStep.whileDo
State after:
no goals

State before:
case 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" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
State after:
case 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" 1 fun x => 0) ⇒
    ?hbc.b

case hbc.hbc

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

case hbc.b

⊢ Stmt × State

State before:
case 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" 1 fun x => 0) ⇒
    ?hbc.b

case hbc.hbc

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

case hbc.b

⊢ Stmt × State
Tactic:
{ apply SmallStep.if_true
  simp }
State after:
case hbc.hbc

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)

State before:
case hbc.hbc

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.seq_step
    apply SmallStep.seq_skip }
  { apply RTC.head
    { apply SmallStep.seq_step
      apply SmallStep.assign }
    { apply RTC.head
      { apply SmallStep.seq_skip }
      { apply RTC.head
        { apply SmallStep.whileDo }
        { apply RTC.head
          { apply SmallStep.if_false
            simp }
          { simp
            apply RTC.refl } } } } } }
State after:
no goals

State before:
case 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" 1 fun x => 0) ⇒
    ?hbc.b
Tactic:
apply SmallStep.if_true
State after:
case hbc.hab.hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"

State before:
case hbc.hab.hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"
Tactic:
simp
State after:
no goals

State before:
case hbc.hbc

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
State after:
case hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.b

case hbc.hbc.hbc

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

case hbc.hbc.b

⊢ Stmt × State

State before:
case hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.b

case hbc.hbc.hbc

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

case hbc.hbc.b

⊢ Stmt × State
Tactic:
{ apply SmallStep.seq_step
  apply SmallStep.seq_skip }
State after:
case hbc.hbc.hbc

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)

State before:
case hbc.hbc.hbc

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.seq_step
    apply SmallStep.assign }
  { apply RTC.head
    { apply SmallStep.seq_skip }
    { apply RTC.head
      { apply SmallStep.whileDo }
      { apply RTC.head
        { apply SmallStep.if_false
          simp }
        { simp
          apply RTC.refl } } } } }
State after:
no goals

State before:
case hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.b
Tactic:
apply SmallStep.seq_step
State after:
case hbc.hbc.hab.hS

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hab.S', ?hbc.hbc.hab.s')

case hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hab.s'

⊢ State

State before:
case hbc.hbc.hab.hS

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hab.S', ?hbc.hbc.hab.s')

case hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hab.s'

⊢ State
Tactic:
apply SmallStep.seq_skip
State after:
no goals

State before:
case hbc.hbc.hbc

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
State after:
case hbc.hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.hbc.b

case hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.b

⊢ Stmt × State

State before:
case hbc.hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.hbc.b

case hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.b

⊢ Stmt × State
Tactic:
{ apply SmallStep.seq_step
  apply SmallStep.assign }
State after:
case hbc.hbc.hbc.hbc

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

State before:
case hbc.hbc.hbc.hbc

⊢ RTC SmallStep
    (Stmt.skip; Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.seq_skip }
  { apply RTC.head
    { apply SmallStep.whileDo }
    { apply RTC.head
      { apply SmallStep.if_false
        simp }
      { simp
        apply RTC.refl } } } }
State after:
no goals

State before:
case hbc.hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.hbc.b
Tactic:
apply SmallStep.seq_step
State after:
case hbc.hbc.hbc.hab.hS

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hbc.hab.S', ?hbc.hbc.hbc.hab.s')

case hbc.hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hbc.hab.s'

⊢ State

State before:
case hbc.hbc.hbc.hab.hS

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hbc.hab.S', ?hbc.hbc.hbc.hab.s')

case hbc.hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hbc.hab.s'

⊢ State
Tactic:
apply SmallStep.assign
State after:
no goals

State before:
case hbc.hbc.hbc.hbc

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

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

case hbc.hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.hbc.b

⊢ Stmt × State

State before:
case hbc.hbc.hbc.hbc.hab

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

case hbc.hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.hbc.b

⊢ Stmt × State
Tactic:
{ apply SmallStep.seq_skip }
State after:
case hbc.hbc.hbc.hbc.hbc

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

State before:
case hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.whileDo }
  { apply RTC.head
    { apply SmallStep.if_false
      simp }
    { simp
      apply RTC.refl } } }
State after:
no goals

State before:
case hbc.hbc.hbc.hbc.hab

⊢ (Stmt.skip; Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⇒
    ?hbc.hbc.hbc.hbc.b
Tactic:
apply SmallStep.seq_skip
State after:
no goals

State before:
case hbc.hbc.hbc.hbc.hbc

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

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

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

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

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

⊢ Stmt × State

State before:
case hbc.hbc.hbc.hbc.hbc.hab

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

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

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

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

⊢ Stmt × State
Tactic:
{ apply SmallStep.whileDo }
State after:
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)

State before:
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)
Tactic:
{ apply RTC.head
  { apply SmallStep.if_false
    simp }
  { simp
    apply RTC.refl } }
State after:
no goals

State before:
case hbc.hbc.hbc.hbc.hbc.hab

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⇒
    ?hbc.hbc.hbc.hbc.hbc.b
Tactic:
apply SmallStep.whileDo
State after:
no goals

State before:
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)
Tactic:
apply RTC.head
State after:
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

State before:
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
Tactic:
{ apply SmallStep.if_false
  simp }
State after:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (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)

State before:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (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)
Tactic:
{ simp
  apply RTC.refl }
State after:
no goals

State before:
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
Tactic:
apply SmallStep.if_false
State after:
case hbc.hbc.hbc.hbc.hbc.hbc.hab.hcond

⊢ ¬State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "x" >
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "y"

State before:
case hbc.hbc.hbc.hbc.hbc.hbc.hab.hcond

⊢ ¬State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "x" >
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "y"
Tactic:
simp
State after:
no goals

State before:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (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)
Tactic:
simp
State after:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

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

State before:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (Stmt.skip, fun x => 0) (Stmt.skip, fun x => 0)
Tactic:
apply RTC.refl
State after:
no goals