Require Import Base.



 Variable Ind : Spec.
 Definition l_ch :=
   ∀ A : Spec, A → (bool → A → A) → (Ind → A → A) → A.

 Definition nil : l_ch :=
   fun (A : Spec) (x0 : A) (x1 : bool → A → A) (x2 : Ind → A → A) ⇒ x0.
 Definition consbl (b : bool) (l : l_ch) : l_ch :=
   fun (A : Spec) (x0 : A) (x1 : bool → A → A) (x2 : Ind → A → A) ⇒
   x1 b (l A x0 x1 x2).
 Definition consltr (i : Ind) (l : l_ch) : l_ch :=
   fun (A : Spec) (x0 : A) (x1 : bool → A → A) (x2 : Ind → A → A) ⇒
   x2 i (l A x0 x1 x2).

 Definition conssp := consbl true.
 Definition conslf := consbl false.


 Hypothesis
   LCH_Ind :
     ∀ (x : l_ch) (P : l_ch → Prop),
     P nil →
     (∀ (b : bool) (l : l_ch), P l → P (consbl b l)) →
     (∀ (i : Ind) (l : l_ch), P l → P (consltr i l)) → P x.

 Hypothesis
   LCH_rec :
     ∀ (x : l_ch) (P : l_ch → Spec),
     P nil →
     (∀ (b : bool) (l : l_ch), P l → P (consbl b l)) →
     (∀ (i : Ind) (l : l_ch), P l → P (consltr i l)) → P x.


Section Casebl.

 Variable A : Spec.
 Definition Casebl (c : l_ch) (xnil : A) (xbl xltr : A → A) : A :=
   c A xnil (fun b : bool ⇒ xbl) (fun i : Ind ⇒ xltr).

End Casebl.


 Definition lgth (l : l_ch) : nat := Casebl nat l O S S.


 Definition app (l m : l_ch) : l_ch := l l_ch m consbl consltr.

 Definition appsp (l m : l_ch) := app l (conssp m).

 Definition applf (l m : l_ch) := app l (conslf m).


 Variable max : nat.


 Definition word (l : l_ch) : Prop :=
   ∀ P : l_ch → Prop,
   P nil → (∀ (i : Ind) (m : l_ch), P m → P (consltr i m)) → P l.

 Definition wordnil : word nil :=
   fun (P : l_ch → Prop) (h1 : P nil)
     (h2 : ∀ (i : Ind) (m : l_ch), P m → P (consltr i m)) ⇒ h1.

 Definition wordltr (j : Ind) (l : l_ch) (h : word l) :
   word (consltr j l) :=
   fun (P : l_ch → Prop) (h1 : P nil)
     (h2 : ∀ (i : Ind) (m : l_ch), P m → P (consltr i m)) ⇒
   h2 j l (h P h1 h2).

 Definition space (l : l_ch) : Prop :=
   ∀ P : l_ch → Prop,
   (∀ b : bool, P (consbl b nil)) →
   (∀ (b : bool) (m : l_ch), P m → P (consbl b m)) → P l.

 Definition space_bl : ∀ b : bool, space (consbl b nil) :=
   fun (c : bool) (P : l_ch → Prop) (h1 : ∀ b : bool, P (consbl b nil))
     (h2 : ∀ (b : bool) (m : l_ch), P m → P (consbl b m)) ⇒
   h1 c.

 Definition space_co_bl :
   ∀ (b : bool) (l : l_ch), space l → space (consbl b l) :=
   fun (c : bool) (l : l_ch) (h : space l) (P : l_ch → Prop)
     (h1 : ∀ b : bool, P (consbl b nil))
     (h2 : ∀ (b : bool) (m : l_ch), P m → P (consbl b m)) ⇒
   h2 c l (h P h1 h2).



 Variable inf sup : nat → Prop.
 Hypothesis ax1 : ∀ n : nat, {inf n} + {sup n}.

 Definition inflg (m : l_ch) := inf (lgth m).

 Definition suplg (m : l_ch) := sup (lgth m).

 Definition plus (m : l_ch) (n : nat) : nat := lgth m nat S n.


 Definition valide (l : l_ch) :=
   ∀ P : l_ch → Spec,
   (∀ m : l_ch, word m → inflg m → P m) →
   (∀ m1 m2 p : l_ch,
    word m1 → inflg m1 → space m2 → P p → P (app m1 (app m2 p))) →
   P l.


 Definition vword : ∀ m : l_ch, word m → inflg m → valide m :=
   fun (x : l_ch) (h1 : word x) (h2 : inflg x) (P : l_ch → Spec)
     (t1 : ∀ m : l_ch, word m → inflg m → P m)
     (t2 : ∀ m1 m2 p : l_ch,
           word m1 → inflg m1 → space m2 → P p → P (app m1 (app m2 p))) ⇒
   t1 x h1 h2.

 Definition vapp :
   ∀ m1 m2 p : l_ch,
   word m1 → inflg m1 → space m2 → valide p → valide (app m1 (app m2 p)) :=
   fun (x1 x2 m : l_ch) (h1 : word x1) (h2 : inflg x1)
     (h3 : space x2) (h : valide m) (P : l_ch → Spec)
     (t1 : ∀ l : l_ch, word l → inflg l → P l)
     (t2 : ∀ m1 m2 p : l_ch,
           word m1 → inflg m1 → space m2 → P p → P (app m1 (app m2 p))) ⇒
   t2 x1 x2 m h1 h2 h3 (h P t1 t2).



 Hypothesis infmax : inf O.


 Definition NV (x : l_ch) :=
   ∀ P : l_ch → Prop,
   (∀ l : l_ch, word l → suplg l → P l) →
   (∀ l m : l_ch, P l → P (app l m)) →
   (∀ l m : l_ch, P l → P (app m l)) → P x.


 Definition NVword : ∀ l : l_ch, word l → suplg l → NV l :=
   fun (x : l_ch) (h1 : word x) (h2 : suplg x) (P : l_ch → Prop)
     (t1 : ∀ l : l_ch, word l → suplg l → P l)
     (t2 : ∀ l m : l_ch, P l → P (app l m))
     (t3 : ∀ l m : l_ch, P l → P (app m l)) ⇒
   t1 x h1 h2.

 Definition NVapp1 : ∀ l m : l_ch, NV l → NV (app l m) :=
   fun (x y : l_ch) (h : NV x) (P : l_ch → Prop)
     (t1 : ∀ l : l_ch, word l → suplg l → P l)
     (t2 : ∀ l m : l_ch, P l → P (app l m))
     (t3 : ∀ l m : l_ch, P l → P (app m l)) ⇒
   t2 x y (h P t1 t2 t3).

 Definition NVapp2 : ∀ l m : l_ch, NV l → NV (app m l) :=
   fun (x y : l_ch) (h : NV x) (P : l_ch → Prop)
     (t1 : ∀ l : l_ch, word l → suplg l → P l)
     (t2 : ∀ l m : l_ch, P l → P (app l m))
     (t3 : ∀ l m : l_ch, P l → P (app m l)) ⇒
   t3 x y (h P t1 t2 t3).


 Definition val_or_no (l : l_ch) := valide l + {NV l}.
 Definition inval (l : l_ch) := inleft (valide l) (NV l).
 Definition inNV (l : l_ch) := inright (valide l) (NV l).


 Definition valbl (b : bool) (l : l_ch) (h : valide l) : valide (consbl b l) :=
   vapp nil (consbl b nil) l wordnil infmax (space_bl b) h.


Section Valltr.

Variable i : Ind.
Variable l : l_ch.

 Definition Valltr := valide l & val_or_no (consltr i l).
 Definition Vfst := fst (valide l) (val_or_no (consltr i l)).
 Definition Vsnd := snd (valide l) (val_or_no (consltr i l)).
 Definition Vand := pair (valide l) (val_or_no (consltr i l)).

End Valltr.

 Lemma valltr :
  ∀ (i : Ind) (l : l_ch), valide l → val_or_no (consltr i l).
 Proof
   fun (i : Ind) (l : l_ch) (h : valide l) ⇒
   Vsnd i l
     (h (Valltr i)
        (fun (m : l_ch) (t1 : word m) (t2 : inflg m) ⇒
         Vand i m (vword m t1 t2)
           (ax1 (S (lgth m)) (val_or_no (consltr i m))
              (fun h1 : inflg (consltr i m) ⇒
               inval (consltr i m) (vword (consltr i m) (wordltr i m t1) h1))
              (fun h2 : suplg (consltr i m) ⇒
               inNV (consltr i m) (NVword (consltr i m) (wordltr i m t1) h2))))
        (fun (m1 m2 p : l_ch) (t1 : word m1) (t2 : inflg m1)
           (t3 : space m2) (f : Valltr i p) ⇒
         Vand i (app m1 (app m2 p)) (vapp m1 m2 p t1 t2 t3 (Vfst i p f))
           (ax1 (S (lgth m1)) (val_or_no (consltr i (app m1 (app m2 p))))
              (fun h11 : inflg (consltr i m1) ⇒
               inval (consltr i (app m1 (app m2 p)))
                 (vapp (consltr i m1) m2 p (wordltr i m1 t1) h11 t3
                    (Vfst i p f)))
              (fun h12 : suplg (consltr i m1) ⇒
               inNV (consltr i (app m1 (app m2 p)))
                 (NVapp1 (consltr i m1) (app m2 p)
                    (NVword (consltr i m1) (wordltr i m1 t1) h12)))))).


 Definition preproc (l : l_ch) : valide l + {NV l} :=
   LCH_rec l val_or_no (inval nil (vword nil wordnil infmax))
     (fun (b : bool) (m : l_ch) (h : val_or_no m) ⇒
      h (val_or_no (consbl b m))
        (fun h1 : valide m ⇒ inval (consbl b m) (valbl b m h1))
        (fun h2 : NV m ⇒ inNV (consbl b m) (NVapp2 m (consbl b nil) h2)))
     (fun (i : Ind) (m : l_ch) (h : val_or_no m) ⇒
      h (val_or_no (consltr i m)) (valltr i m)
        (fun t : NV m ⇒ inNV (consltr i m) (NVapp2 m (consltr i nil) t))).



 Definition Eq (x y : l_ch) :=
   ∀ R : l_ch → l_ch → Prop,
   R nil nil →
   (∀ (b : bool) (l : l_ch), R l nil → R (consbl b l) nil) →
   (∀ (b c : bool) (l m : l_ch), R l m → R (consbl b l) (consbl c m)) →
   (∀ (i : Ind) (l m : l_ch), R l m → R (consltr i l) (consltr i m)) →
   (∀ (b c : bool) (l m : l_ch),
    R l (consbl b m) → R (consbl c l) (consbl b m)) →
   (∀ l m n : l_ch, R l m → R m n → R l n) → R x y.

 Definition Eq_nil : Eq nil nil :=
   fun (R : l_ch → l_ch → Prop) (h0 : R nil nil)
     (h1 : ∀ (b : bool) (l : l_ch), R l nil → R (consbl b l) nil)
     (h2 : ∀ (b c : bool) (l m : l_ch),
           R l m → R (consbl b l) (consbl c m))
     (h3 : ∀ (i : Ind) (l m : l_ch),
           R l m → R (consltr i l) (consltr i m))
     (h4 : ∀ (b c : bool) (l m : l_ch),
           R l (consbl b m) → R (consbl c l) (consbl b m))
     (h5 : ∀ l m n : l_ch, R l m → R m n → R l n) ⇒ h0.

 Definition Eq_bl_nil :
   ∀ (b : bool) (l : l_ch),
   Eq l nil → Eq (consbl b l) nil :=
   fun (d : bool) (x : l_ch) (h : Eq x nil)
     (R : l_ch → l_ch → Prop) (h0 : R nil nil)
     (h1 : ∀ (b : bool) (l : l_ch), R l nil → R (consbl b l) nil)
     (h2 : ∀ (b c : bool) (l m : l_ch),
           R l m → R (consbl b l) (consbl c m))
     (h3 : ∀ (i : Ind) (l m : l_ch),
           R l m → R (consltr i l) (consltr i m))
     (h4 : ∀ (b c : bool) (l m : l_ch),
           R l (consbl b m) → R (consbl c l) (consbl b m))
     (h5 : ∀ l m n : l_ch, R l m → R m n → R l n) ⇒
   h1 d x (h R h0 h1 h2 h3 h4 h5).

 Definition Eq_co_bl :
   ∀ (b c : bool) (l m : l_ch),
   Eq l m → Eq (consbl b l) (consbl c m) :=
   fun (d e : bool) (x y : l_ch) (h : Eq x y)
     (R : l_ch → l_ch → Prop) (h0 : R nil nil)
     (h1 : ∀ (b : bool) (l : l_ch), R l nil → R (consbl b l) nil)
     (h2 : ∀ (b c : bool) (l m : l_ch),
           R l m → R (consbl b l) (consbl c m))
     (h3 : ∀ (i : Ind) (l m : l_ch),
           R l m → R (consltr i l) (consltr i m))
     (h4 : ∀ (b c : bool) (l m : l_ch),
           R l (consbl b m) → R (consbl c l) (consbl b m))
     (h5 : ∀ l m n : l_ch, R l m → R m n → R l n) ⇒
   h2 d e x y (h R h0 h1 h2 h3 h4 h5).

 Definition Eq_co_ltr :
   ∀ (i : Ind) (l m : l_ch),
   Eq l m → Eq (consltr i l) (consltr i m) :=
   fun (j : Ind) (x y : l_ch) (h : Eq x y) (R : l_ch → l_ch → Prop)
     (h0 : R nil nil)
     (h1 : ∀ (b : bool) (l : l_ch), R l nil → R (consbl b l) nil)
     (h2 : ∀ (b c : bool) (l m : l_ch),
           R l m → R (consbl b l) (consbl c m))
     (h3 : ∀ (i : Ind) (l m : l_ch),
           R l m → R (consltr i l) (consltr i m))
     (h4 : ∀ (b c : bool) (l m : l_ch),
           R l (consbl b m) → R (consbl c l) (consbl b m))
     (h5 : ∀ l m n : l_ch, R l m → R m n → R l n) ⇒
   h3 j x y (h R h0 h1 h2 h3 h4 h5).

 Definition Eq_bl_bl :
   ∀ (b c : bool) (l m : l_ch),
   Eq l (consbl b m) → Eq (consbl c l) (consbl b m) :=
   fun (d e : bool) (x y : l_ch) (h : Eq x (consbl d y))
     (R : l_ch → l_ch → Prop) (h0 : R nil nil)
     (h1 : ∀ (b : bool) (l : l_ch), R l nil → R (consbl b l) nil)
     (h2 : ∀ (b c : bool) (l m : l_ch),
           R l m → R (consbl b l) (consbl c m))
     (h3 : ∀ (i : Ind) (l m : l_ch),
           R l m → R (consltr i l) (consltr i m))
     (h4 : ∀ (b c : bool) (l m : l_ch),
           R l (consbl b m) → R (consbl c l) (consbl b m))
     (h5 : ∀ l m n : l_ch, R l m → R m n → R l n) ⇒
   h4 d e x y (h R h0 h1 h2 h3 h4 h5).

 Definition Eq_tran :
   ∀ l m n : l_ch, Eq l m → Eq m n → Eq l n :=
   fun (x y z : l_ch) (t1 : Eq x y) (t2 : Eq y z)
     (R : l_ch → l_ch → Prop) (h0 : R nil nil)
     (h1 : ∀ (b : bool) (l : l_ch), R l nil → R (consbl b l) nil)
     (h2 : ∀ (b c : bool) (l m : l_ch),
           R l m → R (consbl b l) (consbl c m))
     (h3 : ∀ (i : Ind) (l m : l_ch),
           R l m → R (consltr i l) (consltr i m))
     (h4 : ∀ (b c : bool) (l m : l_ch),
           R l (consbl b m) → R (consbl c l) (consbl b m))
     (h5 : ∀ l m n : l_ch, R l m → R m n → R l n) ⇒
   h5 x y z (t1 R h0 h1 h2 h3 h4 h5) (t2 R h0 h1 h2 h3 h4 h5).



 Definition Eq_re (l : l_ch) : Eq l l :=
   LCH_Ind l (fun u : l_ch ⇒ Eq u u) Eq_nil
     (fun (b : bool) (m : l_ch) ⇒ Eq_co_bl b b m m)
     (fun (i : Ind) (m : l_ch) ⇒ Eq_co_ltr i m m).