Require Export IncrDecr.
Require Export Memo.

Parameter a_size d_size : nat.
Parameter di_init cx_init al_init : BV.
Parameter mem_init : Memo.

Axiom di_initsize : lengthbv di_init = a_size.
Axiom cx_initsize : lengthbv cx_init = a_size.
Axiom al_initsize : lengthbv al_init = d_size.
Axiom mem_initsize : MemoSize mem_init = a_size.

Fixpoint IsNull (v : BV) : bool :=
  match v return bool with
  | nil ⇒ true
  | b :: w ⇒
      match b return bool with
      | true ⇒ false
      | false ⇒ IsNull w
      end
  end.

Lemma IsNull_nil : IsNull nilbv = true.
auto with v62.
Qed.

Lemma IsNull_false :
 ∀ (a : bool) (v : BV), IsNull (consbv a v) = true → a = false.
simple induction a. simpl in |- ×. auto with v62. trivial with v62.
Qed.

Lemma IsNull_cons :
 ∀ (a : bool) (v : BV), IsNull (consbv a v) = true → IsNull v = true.
simple induction a. simpl in |- ×. intros. absurd (false = true).
auto with v62. exact H. intros v. auto with v62.
Qed.

Lemma IsNull_null : ∀ n : nat, IsNull (BV_null n) = true.
simple induction n. simpl in |- ×. trivial with v62.
intros. simpl in |- ×. exact H.
Qed.

Lemma IsNull_BV_null :
 ∀ v : BV, IsNull v = true → v = BV_null (lengthbv v).
simple induction v. simpl in |- ×. unfold BV_null in |- ×. auto with v62.
intros a l H. intro.
change (a :: l = false :: BV_null (lengthbv l)) in |- ×.
rewrite <- H. generalize H0. replace a with false. trivial with v62.
symmetry in |- ×. apply IsNull_false with (v := l). exact H0.
apply IsNull_cons with (a := a). exact H0.
Qed.