Parameter aexp : Set.
Parameter bexp : Set.

Inductive state :=
  | Nil : state
  | Cons : nat → state → state
.

Notation "[]" := Nil.
Notation "x :: y" := (Cons x y).

Parameter evalA : aexp → state → nat.
Parameter evalB : bexp → state → bool.

Inductive winstr :=
| Skip : winstr
| Assign : nat → aexp → winstr
| Seq : winstr → winstr → winstr
| If : bexp → winstr → winstr → winstr
| While : bexp → winstr → winstr
.

Fixpoint update (i:nat) (v:nat) (s:state) : state :=
  match i, s with
  | 0, _ :: s' ⇒ v :: s'
  | 0, [] ⇒ v :: []
  | S i', v' :: s' ⇒ v' :: update i' v s'
  | S i', [] ⇒ 0 :: update i' v []
  end.

Fail Fixpoint evalW (i : winstr) (s : state) {struct i} : state :=
  match i with
  | Skip ⇒ s
  | Assign x e ⇒ update x (evalA e s) s
  | Seq i1 i2 ⇒ let s1 := evalW i1 s in evalW i2 s1
               
  | If e i1 i2 ⇒ match evalB e s with
                  | true ⇒ evalW i1 s
                  | false ⇒ evalW i2 s
                  end
  | (While e i1) as i ⇒ match evalB e s with
                  | true ⇒
                    let s1 := evalW i1 s in evalW (While e i1) s1
               
                  | false ⇒ s
                  end
  end.

Inductive SN: winstr → state → state → Prop :=
| SN_Skip : ∀ s,
                   SN Skip s s
| SN_Assign : ∀ x e s,
                   SN (Assign x e) s (update x (evalA e s) s)
| SN_Seq : ∀ i1 i2 s s1 s2,
                   SN i1 s s1 → SN i2 s1 s2 → SN (Seq i1 i2) s s2
| SN_If_true : ∀ e i1 i2 s s1,
                   (evalB e s = true) → SN i1 s s1 → SN (If e i1 i2) s s1
| SN_If_false : ∀ e i1 i2 s s2,
                   (evalB e s = false) → SN i2 s s2 → SN (If e i1 i2) s s2
| SN_While_false : ∀ e i s,
                   (evalB e s = false) → SN (While e i) s s
| SN_While_true : ∀ e i s s1 s2,
                   (evalB e s = true) → SN i s s1 → SN (While e i) s1 s2
               → SN (While e i) s s2
.