matita/contribs/LAMBDA-TYPES/Base-1/spare.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/spare".
  18
  19 include "theory.ma".
  20 (*
  21 inductive pr: Set \def
  22 | pr_zero: pr
  23 | pr_succ: pr
  24 | pr_proj: nat \to pr
  25 | pr_comp: ((nat \to pr)) \to (pr \to pr)
  26 | pr_prec: pr \to (pr \to pr).
  27
  28 definition pr_type:
  29  Set
  30 \def
  31  ((nat \to nat)) \to nat.
  32
  33 definition prec_appl:
  34  pr_type \to (pr_type \to (nat \to pr_type))
  35 \def
  36  let rec prec_appl (f: pr_type) (g: pr_type) (n: nat) on n: pr_type \def
  37 (match n with [O \Rightarrow f | (S m) \Rightarrow (\lambda (ns: ((nat \to
  38 nat))).(g (\lambda (i: nat).(match i with [O \Rightarrow (prec_appl f g m ns)
  39 | (S n0) \Rightarrow (match n0 with [O \Rightarrow m | (S j) \Rightarrow (ns
  40 j)])]))))]) in prec_appl.
  41
  42 definition pr_appl:
  43  pr \to pr_type
  44 \def
  45  let rec pr_appl (h: pr) on h: pr_type \def (match h with [pr_zero
  46 \Rightarrow (\lambda (_: ((nat \to nat))).O) | pr_succ \Rightarrow (\lambda
  47 (ns: ((nat \to nat))).(S (ns O))) | (pr_proj i) \Rightarrow (\lambda (ns:
  48 ((nat \to nat))).(ns i)) | (pr_comp fs g) \Rightarrow (\lambda (ns: ((nat \to
  49 nat))).(pr_appl g (\lambda (i: nat).(pr_appl (fs i) ns)))) | (pr_prec f g)
  50 \Rightarrow (\lambda (ns: ((nat \to nat))).(prec_appl (pr_appl f) (pr_appl g)
  51 (ns O) (\lambda (i: nat).(ns (S i)))))]) in pr_appl.
  52
  53 inductive pr_arity: pr \to (nat \to Prop) \def
  54 | pr_arity_zero: \forall (n: nat).(pr_arity pr_zero n)
  55 | pr_arity_succ: \forall (n: nat).((lt O n) \to (pr_arity pr_succ n))
  56 | pr_arity_proj: \forall (n: nat).(\forall (i: nat).((lt i n) \to (pr_arity
  57 (pr_proj i) n)))
  58 | pr_arity_comp: \forall (n: nat).(\forall (m: nat).(\forall (fs: ((nat \to
  59 pr))).(\forall (g: pr).((pr_arity g m) \to (((\forall (i: nat).((lt i m) \to
  60 (pr_arity (fs i) n)))) \to (pr_arity (pr_comp fs g) n))))))
  61 | pr_arity_prec: \forall (n: nat).(\forall (f: pr).(\forall (g: pr).((lt O n)
  62 \to ((pr_arity f (pred n)) \to ((pr_arity g (S n)) \to (pr_arity (pr_prec f
  63 g) n)))))).
  64
  65 theorem pr_arity_le:
  66  \forall (h: pr).(\forall (m: nat).((pr_arity h m) \to (\forall (n: nat).((le
  67 m n) \to (pr_arity h n)))))
  68 \def
  69  \lambda (h: pr).(\lambda (m: nat).(\lambda (H: (pr_arity h m)).(pr_arity_ind
  70 (\lambda (p: pr).(\lambda (n: nat).(\forall (n0: nat).((le n n0) \to
  71 (pr_arity p n0))))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (_: (le n
  72 n0)).(pr_arity_zero n0)))) (\lambda (n: nat).(\lambda (H0: (lt O n)).(\lambda
  73 (n0: nat).(\lambda (H1: (le n n0)).(pr_arity_succ n0 (lt_le_trans O n n0 H0
  74 H1)))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (H0: (lt i n)).(\lambda
  75 (n0: nat).(\lambda (H1: (le n n0)).(pr_arity_proj n0 i (lt_le_trans i n n0 H0
  76 H1))))))) (\lambda (n: nat).(\lambda (m0: nat).(\lambda (fs: ((nat \to
  77 pr))).(\lambda (g: pr).(\lambda (H0: (pr_arity g m0)).(\lambda (_: ((\forall
  78 (n0: nat).((le m0 n0) \to (pr_arity g n0))))).(\lambda (_: ((\forall (i:
  79 nat).((lt i m0) \to (pr_arity (fs i) n))))).(\lambda (H3: ((\forall (i:
  80 nat).((lt i m0) \to (\forall (n0: nat).((le n n0) \to (pr_arity (fs i)
  81 n0))))))).(\lambda (n0: nat).(\lambda (H4: (le n n0)).(pr_arity_comp n0 m0 fs
  82 g H0 (\lambda (i: nat).(\lambda (H5: (lt i m0)).(H3 i H5 n0 H4))))))))))))))
  83 (\lambda (n: nat).(\lambda (f: pr).(\lambda (g: pr).(\lambda (H0: (lt O
  84 n)).(\lambda (_: (pr_arity f (pred n))).(\lambda (H2: ((\forall (n0:
  85 nat).((le (pred n) n0) \to (pr_arity f n0))))).(\lambda (_: (pr_arity g (S
  86 n))).(\lambda (H4: ((\forall (n0: nat).((le (S n) n0) \to (pr_arity g
  87 n0))))).(\lambda (n0: nat).(\lambda (H5: (le n n0)).(pr_arity_prec n0 f g
  88 (lt_le_trans O n n0 H0 H5) (H2 (pred n0) (le_n_pred n n0 H5)) (H4 (S n0)
  89 (le_n_S n n0 H5))))))))))))) h m H))).
  90
  91 theorem pr_arity_appl:
  92  \forall (h: pr).(\forall (n: nat).((pr_arity h n) \to (\forall (ns: ((nat
  93 \to nat))).(\forall (ms: ((nat \to nat))).(((\forall (i: nat).((lt i n) \to
  94 (eq nat (ns i) (ms i))))) \to (eq nat (pr_appl h ns) (pr_appl h ms)))))))
  95 \def
  96  \lambda (h: pr).(\lambda (n: nat).(\lambda (H: (pr_arity h n)).(pr_arity_ind
  97 (\lambda (p: pr).(\lambda (n0: nat).(\forall (ns: ((nat \to nat))).(\forall
  98 (ms: ((nat \to nat))).(((\forall (i: nat).((lt i n0) \to (eq nat (ns i) (ms
  99 i))))) \to (eq nat (pr_appl p ns) (pr_appl p ms))))))) (\lambda (n0:
 100 nat).(\lambda (ns: ((nat \to nat))).(\lambda (ms: ((nat \to nat))).(\lambda
 101 (_: ((\forall (i: nat).((lt i n0) \to (eq nat (ns i) (ms i)))))).(refl_equal
 102 nat O))))) (\lambda (n0: nat).(\lambda (H0: (lt O n0)).(\lambda (ns: ((nat
 103 \to nat))).(\lambda (ms: ((nat \to nat))).(\lambda (H1: ((\forall (i:
 104 nat).((lt i n0) \to (eq nat (ns i) (ms i)))))).(f_equal nat nat S (ns O) (ms
 105 O) (H1 O H0))))))) (\lambda (n0: nat).(\lambda (i: nat).(\lambda (H0: (lt i
 106 n0)).(\lambda (ns: ((nat \to nat))).(\lambda (ms: ((nat \to nat))).(\lambda
 107 (H1: ((\forall (i0: nat).((lt i0 n0) \to (eq nat (ns i0) (ms i0)))))).(H1 i
 108 H0))))))) (\lambda (n0: nat).(\lambda (m: nat).(\lambda (fs: ((nat \to
 109 pr))).(\lambda (g: pr).(\lambda (_: (pr_arity g m)).(\lambda (H1: ((\forall
 110 (ns: ((nat \to nat))).(\forall (ms: ((nat \to nat))).(((\forall (i: nat).((lt
 111 i m) \to (eq nat (ns i) (ms i))))) \to (eq nat (pr_appl g ns) (pr_appl g
 112 ms))))))).(\lambda (_: ((\forall (i: nat).((lt i m) \to (pr_arity (fs i)
 113 n0))))).(\lambda (H3: ((\forall (i: nat).((lt i m) \to (\forall (ns: ((nat
 114 \to nat))).(\forall (ms: ((nat \to nat))).(((\forall (i0: nat).((lt i0 n0)
 115 \to (eq nat (ns i0) (ms i0))))) \to (eq nat (pr_appl (fs i) ns) (pr_appl (fs
 116 i) ms))))))))).(\lambda (ns: ((nat \to nat))).(\lambda (ms: ((nat \to
 117 nat))).(\lambda (H4: ((\forall (i: nat).((lt i n0) \to (eq nat (ns i) (ms
 118 i)))))).(H1 (\lambda (i: nat).(pr_appl (fs i) ns)) (\lambda (i: nat).(pr_appl
 119 (fs i) ms)) (\lambda (i: nat).(\lambda (H5: (lt i m)).(H3 i H5 ns ms
 120 H4))))))))))))))) (\lambda (n0: nat).(\lambda (f: pr).(\lambda (g:
 121 pr).(\lambda (H0: (lt O n0)).(\lambda (_: (pr_arity f (pred n0))).(\lambda
 122 (H2: ((\forall (ns: ((nat \to nat))).(\forall (ms: ((nat \to
 123 nat))).(((\forall (i: nat).((lt i (pred n0)) \to (eq nat (ns i) (ms i)))))
 124 \to (eq nat (pr_appl f ns) (pr_appl f ms))))))).(\lambda (_: (pr_arity g (S
 125 n0))).(\lambda (H4: ((\forall (ns: ((nat \to nat))).(\forall (ms: ((nat \to
 126 nat))).(((\forall (i: nat).((lt i (S n0)) \to (eq nat (ns i) (ms i))))) \to
 127 (eq nat (pr_appl g ns) (pr_appl g ms))))))).(\lambda (ns: ((nat \to
 128 nat))).(\lambda (ms: ((nat \to nat))).(\lambda (H5: ((\forall (i: nat).((lt i
 129 n0) \to (eq nat (ns i) (ms i)))))).(eq_ind nat (ns O) (\lambda (n1: nat).(eq
 130 nat (prec_appl (pr_appl f) (pr_appl g) (ns O) (\lambda (i: nat).(ns (S i))))
 131 (prec_appl (pr_appl f) (pr_appl g) n1 (\lambda (i: nat).(ms (S i)))))) (let
 132 n1 \def (ns O) in (nat_ind (\lambda (n2: nat).(eq nat (prec_appl (pr_appl f)
 133 (pr_appl g) n2 (\lambda (i: nat).(ns (S i)))) (prec_appl (pr_appl f) (pr_appl
 134 g) n2 (\lambda (i: nat).(ms (S i)))))) (H2 (\lambda (i: nat).(ns (S i)))
 135 (\lambda (i: nat).(ms (S i))) (\lambda (i: nat).(\lambda (H6: (lt i (pred
 136 n0))).(H5 (S i) (lt_x_pred_y i n0 H6))))) (\lambda (n2: nat).(\lambda (IHn0:
 137 (eq nat (prec_appl (pr_appl f) (pr_appl g) n2 (\lambda (i: nat).(ns (S i))))
 138 (prec_appl (pr_appl f) (pr_appl g) n2 (\lambda (i: nat).(ms (S i)))))).(H4
 139 (\lambda (i: nat).(match i with [O \Rightarrow (prec_appl (pr_appl f)
 140 (pr_appl g) n2 (\lambda (i0: nat).(ns (S i0)))) | (S n3) \Rightarrow (match
 141 n3 with [O \Rightarrow n2 | (S j) \Rightarrow (ns (S j))])])) (\lambda (i:
 142 nat).(match i with [O \Rightarrow (prec_appl (pr_appl f) (pr_appl g) n2
 143 (\lambda (i0: nat).(ms (S i0)))) | (S n3) \Rightarrow (match n3 with [O
 144 \Rightarrow n2 | (S j) \Rightarrow (ms (S j))])])) (\lambda (i: nat).(\lambda
 145 (H6: (lt i (S n0))).(nat_ind (\lambda (n3: nat).((lt n3 (S n0)) \to (eq nat
 146 (match n3 with [O \Rightarrow (prec_appl (pr_appl f) (pr_appl g) n2 (\lambda
 147 (i0: nat).(ns (S i0)))) | (S n4) \Rightarrow (match n4 with [O \Rightarrow n2
 148 | (S j) \Rightarrow (ns (S j))])]) (match n3 with [O \Rightarrow (prec_appl
 149 (pr_appl f) (pr_appl g) n2 (\lambda (i0: nat).(ms (S i0)))) | (S n4)
 150 \Rightarrow (match n4 with [O \Rightarrow n2 | (S j) \Rightarrow (ms (S
 151 j))])])))) (\lambda (_: (lt O (S n0))).IHn0) (\lambda (i0: nat).(\lambda (_:
 152 (((lt i0 (S n0)) \to (eq nat (match i0 with [O \Rightarrow (prec_appl
 153 (pr_appl f) (pr_appl g) n2 (\lambda (i1: nat).(ns (S i1)))) | (S n3)
 154 \Rightarrow (match n3 with [O \Rightarrow n2 | (S j) \Rightarrow (ns (S
 155 j))])]) (match i0 with [O \Rightarrow (prec_appl (pr_appl f) (pr_appl g) n2
 156 (\lambda (i1: nat).(ms (S i1)))) | (S n3) \Rightarrow (match n3 with [O
 157 \Rightarrow n2 | (S j) \Rightarrow (ms (S j))])]))))).(\lambda (H7: (lt (S
 158 i0) (S n0))).(let H_y \def (H5 i0 (lt_S_n i0 n0 H7)) in (nat_ind (\lambda
 159 (n3: nat).((eq nat (ns n3) (ms n3)) \to (eq nat (match n3 with [O \Rightarrow
 160 n2 | (S j) \Rightarrow (ns (S j))]) (match n3 with [O \Rightarrow n2 | (S j)
 161 \Rightarrow (ms (S j))])))) (\lambda (_: (eq nat (ns O) (ms O))).(refl_equal
 162 nat n2)) (\lambda (i1: nat).(\lambda (_: (((eq nat (ns i1) (ms i1)) \to (eq
 163 nat (match i1 with [O \Rightarrow n2 | (S j) \Rightarrow (ns (S j))]) (match
 164 i1 with [O \Rightarrow n2 | (S j) \Rightarrow (ms (S j))]))))).(\lambda (H8:
 165 (eq nat (ns (S i1)) (ms (S i1)))).H8))) i0 H_y))))) i H6)))))) n1)) (ms O)
 166 (H5 O H0))))))))))))) h n H))).
 167
 168 theorem pr_arity_comp_proj_zero:
 169  \forall (n: nat).(pr_arity (pr_comp pr_proj pr_zero) n)
 170 \def
 171  \lambda (n: nat).(pr_arity_comp n n pr_proj pr_zero (pr_arity_zero n)
 172 (\lambda (i: nat).(\lambda (H: (lt i n)).(pr_arity_proj n i H)))).
 173
 174 *)