Section Format.



 Parameter Induct : Set.

 Inductive l_ch : Set :=
   | nil : l_ch
   | consbl : bool → l_ch → l_ch
   | consltr : Induct → l_ch → l_ch.

 Definition l_ch_it (C : Set) (x : C) (f1 : bool → C → C)
   (f2 : Induct → C → C) : l_ch → C :=
   fix F (l : l_ch) : C :=
     match l with
     | nil ⇒ x
     | consbl b l0 ⇒ f1 b (F l0)
     | consltr i l0 ⇒ f2 i (F l0)
     end.

 Definition nat_it (C : Set) (x : C) (f : C → C) :
   nat → C :=
   fix F (n : nat) : C := match n with
                          | O ⇒ x
                          | S m ⇒ f (F m)
                          end.

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


Section Casebl_section.

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

End Casebl_section.


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


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

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

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


 Parameter max : nat.


Inductive word : l_ch → Prop :=
  | wordnil : word nil
  | wordltr : ∀ (j : Induct) (l : l_ch), word l → word (consltr j l).


Inductive space : l_ch → Prop :=
  | space_bl : ∀ b : bool, space (consbl b nil)
  | space_co_bl : ∀ (b : bool) (l : l_ch), space l → space (consbl b l).


 Parameter inf sup : nat → Prop.
 Axiom ax1 : ∀ n : nat, {inf n} + {sup n}.

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

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

 Let plus_l_ch (m : l_ch) (n : nat) : nat := nat_it nat n S (lgth m).


Inductive valide : l_ch → Set :=
  | vword : ∀ m : l_ch, word m → inflg m → valide m
  | vapp :
      ∀ m1 m2 p : l_ch,
      word m1 →
      inflg m1 → space m2 → valide p → valide (app m1 (app m2 p)).


 Hypothesis infmax : inf 0.


Inductive NV : l_ch → Prop :=
  | NVword : ∀ l : l_ch, word l → suplg l → NV l
  | NVapp1 : ∀ l m : l_ch, NV l → NV (app l m)
  | NVapp2 : ∀ l m : l_ch, NV l → NV (app m l).


Inductive val_or_no (l : l_ch) : Set :=
  | inval : valide l → val_or_no l
  | inNV : NV l → val_or_no l.


Remark valbl : ∀ (b : bool) (l : l_ch), valide l → valide (consbl b l).
intros; apply (vapp nil (consbl b nil) l); auto with v62.
apply wordnil.
apply space_bl.
Qed.


Remark valltr :
 ∀ (i : Induct) (l : l_ch), valide l → val_or_no (consltr i l).
intros; elim H; intros.
elim (ax1 (S (lgth m))); intros.
apply (inval (consltr i m)).
apply vword; auto with v62.
apply wordltr; auto with v62.
apply (inNV (consltr i m)).
apply NVword; auto with v62.
apply wordltr; auto with v62.
elim (ax1 (S (lgth m1))); intros.
apply (inval (consltr i (app m1 (app m2 p)))).
apply (vapp (consltr i m1) m2 p); auto with v62.
apply wordltr; auto with v62.
apply (inNV (consltr i (app m1 (app m2 p)))).
apply (NVapp1 (consltr i m1) (app m2 p)).
apply NVword; auto with v62.
apply wordltr; auto with v62.
Qed.


Lemma preproc : ∀ l : l_ch, val_or_no l.
intro; elim l; intros.
apply (inval nil).
apply vword; auto with v62.
apply wordnil.
elim H; intros.
apply (inval (consbl b l0)).
apply valbl; auto with v62.
apply (inNV (consbl b l0)).
apply (NVapp2 l0 (consbl b nil)); auto with v62.
elim H; intros.
apply valltr; auto with v62.
apply (inNV (consltr i l0)).
apply (NVapp2 l0 (consltr i nil)); auto with v62.
Qed.


Section Equivalence.

Inductive Eq : l_ch → l_ch → Prop :=
  | Eq_nil : Eq nil nil
  | Eq_bl_nil : ∀ (b : bool) (l : l_ch), Eq l nil → Eq (consbl b l) nil
  | Eq_co_bl :
      ∀ (b c : bool) (l m : l_ch),
      Eq l m → Eq (consbl b l) (consbl c m)
  | Eq_co_ltr :
      ∀ (i : Induct) (l m : l_ch),
      Eq l m → Eq (consltr i l) (consltr i m)
  | Eq_bl_bl :
      ∀ (b c : bool) (l m : l_ch),
      Eq l (consbl b m) → Eq (consbl c l) (consbl b m)
  | Eq_tran : ∀ l m n : l_ch, Eq l m → Eq m n → Eq l n.



 Theorem Eq_re : ∀ l : l_ch, Equivalence.Eq l l.
 intro; elim l; intros.
 apply Eq_nil.
 apply Eq_co_bl; auto with v62.
 apply Eq_co_ltr; auto with v62.
 Qed.


 Theorem Eq_app :
  ∀ l m n : l_ch,
  Equivalence.Eq m n → Equivalence.Eq (app l m) (app l n).
 intros; elim l; intros; auto with v62.
 apply (Eq_co_bl b b (app l0 m) (app l0 n)); auto with v62.
 apply (Eq_co_ltr i (app l0 m) (app l0 n)); auto with v62.
 Qed.


 Theorem Eq_app_nil :
  ∀ l m : l_ch, Equivalence.Eq m nil → Equivalence.Eq (app l m) l.
 intros; elim l; intros; auto with v62.
 apply (Eq_co_bl b b (app l0 m) l0); auto with v62.
 apply (Eq_co_ltr i (app l0 m) l0); auto with v62.
 Qed.

 Theorem Eq_space_bl :
  ∀ (b : bool) (l m n : l_ch),
  space l →
  Equivalence.Eq m (consbl b n) → Equivalence.Eq (app l m) (consbl b n).
 intros.
 elim H; intros.
 apply (Eq_bl_bl b b0 m n); auto with v62.
 apply (Eq_bl_bl b b0 (app l0 m) n); auto with v62.
 Qed.

 Theorem Eq_space_nil :
  ∀ m : l_ch, space m → Equivalence.Eq (app m nil) nil.
 intros; elim H; intros.
 apply (Eq_bl_nil b nil Eq_nil); auto with v62.
 apply (Eq_bl_nil b (app l nil) H1); auto with v62.
 Qed.

 Theorem Eq_space :
  ∀ l m n : l_ch,
  space l → Equivalence.Eq m n → Equivalence.Eq (app l m) (conssp n).
 intros; elim H; intros.
 apply (Eq_co_bl b true m n); auto with v62.
 apply (Eq_bl_bl true b (app l0 m) n); auto with v62.
 Qed.

End Equivalence.


Inductive formn : nat → l_ch → Prop :=
  | fword : ∀ m : l_ch, word m → inflg m → formn (lgth m) m
  | fwordinf :
      ∀ (p : nat) (m1 : l_ch) (b : bool) (m2 : l_ch),
      inf (plus_l_ch m1 p) →
      word m1 →
      formn p (consbl b m2) → formn (plus_l_ch m1 p) (appsp m1 m2)
  | fwordsup :
      ∀ (p : nat) (m1 : l_ch) (b : bool) (m2 : l_ch),
      sup (plus_l_ch m1 p) →
      word m1 →
      inflg m1 → formn p (consbl b m2) → formn (lgth m1) (applf m1 m2)
  | fsp :
      ∀ (p : nat) (i : Induct) (m : l_ch),
      formn p (consltr i m) → formn (S p) (conssp (consltr i m)).


 Inductive SigFormat (l : l_ch) : Set :=
     ExFormat :
       ∀ (n : nat) (m : l_ch), formn n m → Format.Eq l m → SigFormat l.


Lemma Lem1 :
 ∀ (b : bool) (p m1 m2 : l_ch) (n : nat) (h1 : word m1)
   (h2 : inflg m1) (t1 : formn n (consbl b m2))
   (t2 : Format.Eq p (consbl b m2)), SigFormat (app m1 p).
intros.
elim (ax1 (plus_l_ch m1 n)); intros.
apply (ExFormat (app m1 p) (plus_l_ch m1 n) (appsp m1 m2)).
apply (fwordinf n m1 b m2); auto with v62.
apply (Eq_app m1 p (conssp m2)); auto with v62.
apply (Eq_tran p (consbl b m2) (conssp m2)); auto with v62.
apply (Eq_co_bl b true m2 m2); auto with v62.
apply Eq_re.
apply (ExFormat (app m1 p) (lgth m1) (applf m1 m2)).
apply (fwordsup n m1 b m2); auto with v62.
apply (Eq_app m1 p (conslf m2)); auto with v62.
apply (Eq_tran p (consbl b m2) (conslf m2)); auto with v62.
apply (Eq_co_bl b false m2 m2); auto with v62.
apply Eq_re.
Qed.

Let prop2 (m1 m2 p : l_ch) (n : nat) (u : l_ch) :=
  formn n u → Format.Eq p u → SigFormat (app m1 (app m2 p)).

Lemma Lem2 :
 ∀ (m1 m2 p : l_ch) (h1 : word m1) (h2 : inflg m1)
   (h3 : space m2) (n : nat) (p0 : l_ch), prop2 m1 m2 p n p0.
intros.
elim p0; intros.
red in |- *; intros.
apply (ExFormat (app m1 (app m2 p)) (lgth m1) m1).
apply (fword m1); auto with v62.
apply (Eq_app_nil m1 (app m2 p)); auto with v62.
apply (Eq_tran (app m2 p) (app m2 nil) nil); auto with v62.
apply (Eq_app m2 p nil); auto with v62.
apply (Eq_space_nil m2); auto with v62.
red in |- *; intros.
apply (Lem1 b (app m2 p) m1 l n); auto with v62.
apply (Eq_space_bl b m2 p l); auto with v62.
red in |- *; intros.
apply (Lem1 true (app m2 p) m1 (consltr i l) (S n)); auto with v62.
apply (fsp n i l); auto with v62.
apply (Eq_space m2 p (consltr i l)); auto with v62.
Qed.


 Theorem format : ∀ l : l_ch, valide l → SigFormat l.
 intros.
 elim H; intros.
 apply (ExFormat m (lgth m) m).
 apply (fword m); auto with v62.
 apply Eq_re.
 elim H0; intros.
 apply (Lem2 m1 m2 p w i s n m); auto with v62.
 Qed.


 Theorem format_all : ∀ l : l_ch, SigFormat l + {NV l}.
 intro; elim (preproc l); intros.
 left; apply format; auto with v62.
 right; auto with v62.
 Qed.

End Format.