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

State before:
Ss : Stmt × State
t : State
hS : Ss ⟹ t
⊢ RTC SmallStep Ss (Stmt.skip, t)
Tactic:
induction hS with
| skip => exact RTC.refl
| assign =>
  apply RTC.single
  apply SmallStep.assign
| seq S T s t u hS hT ihS ihT =>
  apply RTC.trans
  { exact RTC_SmallStep_seq ihS }
  { apply RTC.head
    apply SmallStep.seq_skip
    assumption }
| if_true B S T s t hB hst ih =>
  apply RTC.head
  { apply SmallStep.if_true
    assumption }
  { assumption }
| if_false B S T s t hB hst ih =>
  apply RTC.head
  { apply SmallStep.if_false
    assumption }
  { assumption }
| while_true B S s t u hB hS hw ihS ihw =>
  apply RTC.head
  { apply SmallStep.whileDo }
  { apply RTC.head
    { apply SmallStep.if_true
      assumption }
    { apply RTC.trans
      { exact RTC_SmallStep_seq ihS }
      { apply RTC.head
        apply SmallStep.seq_skip
        assumption } } }
| while_false B S s hB =>
  apply RTC.tail
  apply RTC.single
  apply SmallStep.whileDo
  apply SmallStep.if_false
  assumption
State after:
no goals

State before:
case skip
Ss : Stmt × State
t s✝ : State
⊢ RTC SmallStep (Stmt.skip, s✝) (Stmt.skip, s✝)
Tactic:
exact RTC.refl
State after:
no goals

State before:
case assign
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : State
⊢ RTC SmallStep (Stmt.assign x✝ a✝, s✝) (Stmt.skip, State.update x✝ (a✝ s✝) s✝)
Tactic:
apply RTC.single
State after:
case assign.hab
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : State
⊢ (Stmt.assign x✝ a✝, s✝) ⇒ (Stmt.skip, State.update x✝ (a✝ s✝) s✝)

State before:
case assign.hab
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : State
⊢ (Stmt.assign x✝ a✝, s✝) ⇒ (Stmt.skip, State.update x✝ (a✝ s✝) s✝)
Tactic:
apply SmallStep.assign
State after:
no goals

State before:
case seq
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) (Stmt.skip, u)
Tactic:
apply RTC.trans
State after:
case seq.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) ?seq.b

case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.b (Stmt.skip, u)

case seq.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State

State before:
case seq.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) ?seq.b

case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.b (Stmt.skip, u)

case seq.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
{ exact RTC_SmallStep_seq ihS }
State after:
case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; T, t) (Stmt.skip, u)

State before:
case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; T, t) (Stmt.skip, u)
Tactic:
{ apply RTC.head
  apply SmallStep.seq_skip
  assumption }
State after:
no goals

State before:
case seq.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) ?seq.b
Tactic:
exact RTC_SmallStep_seq ihS
State after:
no goals

State before:
case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; T, t) (Stmt.skip, u)
Tactic:
apply RTC.head
State after:
case seq.hbc.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ (Stmt.skip; T, t) ⇒ ?seq.hbc.b

case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.hbc.b (Stmt.skip, u)

case seq.hbc.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State

State before:
case seq.hbc.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ (Stmt.skip; T, t) ⇒ ?seq.hbc.b

case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.hbc.b (Stmt.skip, u)

case seq.hbc.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
apply SmallStep.seq_skip
State after:
case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (T, t) (Stmt.skip, u)

State before:
case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (T, t) (Stmt.skip, u)
Tactic:
assumption
State after:
no goals

State before:
case if_true
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (Stmt.ifThenElse B S T, s) (Stmt.skip, t)
Tactic:
apply RTC.head
State after:
case if_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_true.b

case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_true.b (Stmt.skip, t)

case if_true.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ Stmt × State

State before:
case if_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_true.b

case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_true.b (Stmt.skip, t)

case if_true.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ Stmt × State
Tactic:
{ apply SmallStep.if_true
  assumption }
State after:
case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (S, s) (Stmt.skip, t)

State before:
case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (S, s) (Stmt.skip, t)
Tactic:
{ assumption }
State after:
no goals

State before:
case if_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_true.b
Tactic:
apply SmallStep.if_true
State after:
case if_true.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ B s

State before:
case if_true.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ B s
Tactic:
assumption
State after:
no goals

State before:
case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (S, s) (Stmt.skip, t)
Tactic:
assumption
State after:
no goals

State before:
case if_false
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (Stmt.ifThenElse B S T, s) (Stmt.skip, t)
Tactic:
apply RTC.head
State after:
case if_false.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_false.b

case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_false.b (Stmt.skip, t)

case if_false.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ Stmt × State

State before:
case if_false.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_false.b

case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_false.b (Stmt.skip, t)

case if_false.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ Stmt × State
Tactic:
{ apply SmallStep.if_false
  assumption }
State after:
case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (T, s) (Stmt.skip, t)

State before:
case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (T, s) (Stmt.skip, t)
Tactic:
{ assumption }
State after:
no goals

State before:
case if_false.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_false.b
Tactic:
apply SmallStep.if_false
State after:
case if_false.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ ¬B s

State before:
case if_false.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ ¬B s
Tactic:
assumption
State after:
no goals

State before:
case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (T, s) (Stmt.skip, t)
Tactic:
assumption
State after:
no goals

State before:
case while_true
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)
⊢ RTC SmallStep (Stmt.whileDo B S, s) (Stmt.skip, u)
Tactic:
apply RTC.head
State after:
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

case while_true.hbc
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)
⊢ RTC SmallStep ?while_true.b (Stmt.skip, u)

case while_true.b
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 × State

State before:
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

case while_true.hbc
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)
⊢ RTC SmallStep ?while_true.b (Stmt.skip, u)

case while_true.b
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 × State
Tactic:
{ apply SmallStep.whileDo }
State after:
case while_true.hbc
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)
⊢ RTC SmallStep (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) (Stmt.skip, u)

State before:
case while_true.hbc
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)
⊢ RTC SmallStep (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) (Stmt.skip, u)
Tactic:
{ apply RTC.head
  { apply SmallStep.if_true
    assumption }
  { apply RTC.trans
    { exact RTC_SmallStep_seq ihS }
    { apply RTC.head
      apply SmallStep.seq_skip
      assumption } } }
State after:
no goals

State before:
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
Tactic:
apply SmallStep.whileDo
State after:
no goals

State before:
case while_true.hbc
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)
⊢ RTC SmallStep (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) (Stmt.skip, u)
Tactic:
apply RTC.head
State after:
case while_true.hbc.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.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ ?while_true.hbc.b

case while_true.hbc.hbc
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)
⊢ RTC SmallStep ?while_true.hbc.b (Stmt.skip, u)

case while_true.hbc.b
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 × State

State before:
case while_true.hbc.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.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ ?while_true.hbc.b

case while_true.hbc.hbc
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)
⊢ RTC SmallStep ?while_true.hbc.b (Stmt.skip, u)

case while_true.hbc.b
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 × State
Tactic:
{ apply SmallStep.if_true
  assumption }
State after:
case while_true.hbc.hbc
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)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) (Stmt.skip, u)

State before:
case while_true.hbc.hbc
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)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) (Stmt.skip, u)
Tactic:
{ apply RTC.trans
  { exact RTC_SmallStep_seq ihS }
  { apply RTC.head
    apply SmallStep.seq_skip
    assumption } }
State after:
no goals

State before:
case while_true.hbc.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.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ ?while_true.hbc.b
Tactic:
apply SmallStep.if_true
State after:
case while_true.hbc.hab.hcond
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)
⊢ B s

State before:
case while_true.hbc.hab.hcond
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)
⊢ B s
Tactic:
assumption
State after:
no goals

State before:
case while_true.hbc.hbc
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)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) (Stmt.skip, u)
Tactic:
apply RTC.trans
State after:
case while_true.hbc.hbc.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)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) ?while_true.hbc.hbc.b

case while_true.hbc.hbc.hbc
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)
⊢ RTC SmallStep ?while_true.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.b
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 × State

State before:
case while_true.hbc.hbc.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)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) ?while_true.hbc.hbc.b

case while_true.hbc.hbc.hbc
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)
⊢ RTC SmallStep ?while_true.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.b
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 × State
Tactic:
{ exact RTC_SmallStep_seq ihS }
State after:
case while_true.hbc.hbc.hbc
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)
⊢ RTC SmallStep (Stmt.skip; Stmt.whileDo B S, t) (Stmt.skip, u)

State before:
case while_true.hbc.hbc.hbc
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)
⊢ RTC SmallStep (Stmt.skip; Stmt.whileDo B S, t) (Stmt.skip, u)
Tactic:
{ apply RTC.head
  apply SmallStep.seq_skip
  assumption }
State after:
no goals

State before:
case while_true.hbc.hbc.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)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) ?while_true.hbc.hbc.b
Tactic:
exact RTC_SmallStep_seq ihS
State after:
no goals

State before:
case while_true.hbc.hbc.hbc
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)
⊢ RTC SmallStep (Stmt.skip; Stmt.whileDo B S, t) (Stmt.skip, u)
Tactic:
apply RTC.head
State after:
case while_true.hbc.hbc.hbc.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.skip; Stmt.whileDo B S, t) ⇒ ?while_true.hbc.hbc.hbc.b

case while_true.hbc.hbc.hbc.hbc
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)
⊢ RTC SmallStep ?while_true.hbc.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.hbc.b
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 × State

State before:
case while_true.hbc.hbc.hbc.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.skip; Stmt.whileDo B S, t) ⇒ ?while_true.hbc.hbc.hbc.b

case while_true.hbc.hbc.hbc.hbc
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)
⊢ RTC SmallStep ?while_true.hbc.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.hbc.b
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 × State
Tactic:
apply SmallStep.seq_skip
State after:
case while_true.hbc.hbc.hbc.hbc
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)
⊢ RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)

State before:
case while_true.hbc.hbc.hbc.hbc
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)
⊢ RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
Tactic:
assumption
State after:
no goals

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

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

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

State before:
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)
Tactic:
apply SmallStep.if_false
State after:
case while_false.hbc.hcond
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s

State before:
case while_false.hbc.hcond
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s
Tactic:
assumption
State after:
no goals