matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aprem/props.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/Level-1/LambdaDelta/aprem/props".
  18
  19 include "aprem/defs.ma".
  20
  21 include "leq/defs.ma".
  22
  23 theorem aprem_repl:
  24  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (\forall
  25 (i: nat).(\forall (b2: A).((aprem i a2 b2) \to (ex2 A (\lambda (b1: A).(leq g
  26 b1 b2)) (\lambda (b1: A).(aprem i a1 b1)))))))))
  27 \def
  28  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leq g a1
  29 a2)).(leq_ind g (\lambda (a: A).(\lambda (a0: A).(\forall (i: nat).(\forall
  30 (b2: A).((aprem i a0 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda
  31 (b1: A).(aprem i a b1)))))))) (\lambda (h1: nat).(\lambda (h2: nat).(\lambda
  32 (n1: nat).(\lambda (n2: nat).(\lambda (k: nat).(\lambda (_: (eq A (aplus g
  33 (ASort h1 n1) k) (aplus g (ASort h2 n2) k))).(\lambda (i: nat).(\lambda (b2:
  34 A).(\lambda (H1: (aprem i (ASort h2 n2) b2)).(let H2 \def (match H1 in aprem
  35 return (\lambda (n: nat).(\lambda (a: A).(\lambda (a0: A).(\lambda (_: (aprem
  36 n a a0)).((eq nat n i) \to ((eq A a (ASort h2 n2)) \to ((eq A a0 b2) \to (ex2
  37 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem i (ASort h1 n1)
  38 b1)))))))))) with [(aprem_zero a0 a3) \Rightarrow (\lambda (H2: (eq nat O
  39 i)).(\lambda (H3: (eq A (AHead a0 a3) (ASort h2 n2))).(\lambda (H4: (eq A a0
  40 b2)).(eq_ind nat O (\lambda (n: nat).((eq A (AHead a0 a3) (ASort h2 n2)) \to
  41 ((eq A a0 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
  42 A).(aprem n (ASort h1 n1) b1)))))) (\lambda (H5: (eq A (AHead a0 a3) (ASort
  43 h2 n2))).(let H6 \def (eq_ind A (AHead a0 a3) (\lambda (e: A).(match e in A
  44 return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
  45 _) \Rightarrow True])) I (ASort h2 n2) H5) in (False_ind ((eq A a0 b2) \to
  46 (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem O (ASort h1
  47 n1) b1)))) H6))) i H2 H3 H4)))) | (aprem_succ a0 a i0 H2 a3) \Rightarrow
  48 (\lambda (H3: (eq nat (S i0) i)).(\lambda (H4: (eq A (AHead a3 a0) (ASort h2
  49 n2))).(\lambda (H5: (eq A a b2)).(eq_ind nat (S i0) (\lambda (n: nat).((eq A
  50 (AHead a3 a0) (ASort h2 n2)) \to ((eq A a b2) \to ((aprem i0 a0 a) \to (ex2 A
  51 (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem n (ASort h1 n1)
  52 b1))))))) (\lambda (H6: (eq A (AHead a3 a0) (ASort h2 n2))).(let H7 \def
  53 (eq_ind A (AHead a3 a0) (\lambda (e: A).(match e in A return (\lambda (_:
  54 A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
  55 True])) I (ASort h2 n2) H6) in (False_ind ((eq A a b2) \to ((aprem i0 a0 a)
  56 \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0)
  57 (ASort h1 n1) b1))))) H7))) i H3 H4 H5 H2))))]) in (H2 (refl_equal nat i)
  58 (refl_equal A (ASort h2 n2)) (refl_equal A b2)))))))))))) (\lambda (a0:
  59 A).(\lambda (a3: A).(\lambda (H0: (leq g a0 a3)).(\lambda (_: ((\forall (i:
  60 nat).(\forall (b2: A).((aprem i a3 b2) \to (ex2 A (\lambda (b1: A).(leq g b1
  61 b2)) (\lambda (b1: A).(aprem i a0 b1)))))))).(\lambda (a4: A).(\lambda (a5:
  62 A).(\lambda (_: (leq g a4 a5)).(\lambda (H3: ((\forall (i: nat).(\forall (b2:
  63 A).((aprem i a5 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
  64 A).(aprem i a4 b1)))))))).(\lambda (i: nat).(\lambda (b2: A).(\lambda (H4:
  65 (aprem i (AHead a3 a5) b2)).((match i in nat return (\lambda (n: nat).((aprem
  66 n (AHead a3 a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
  67 A).(aprem n (AHead a0 a4) b1))))) with [O \Rightarrow (\lambda (H5: (aprem O
  68 (AHead a3 a5) b2)).(let H6 \def (match H5 in aprem return (\lambda (n:
  69 nat).(\lambda (a: A).(\lambda (a6: A).(\lambda (_: (aprem n a a6)).((eq nat n
  70 O) \to ((eq A a (AHead a3 a5)) \to ((eq A a6 b2) \to (ex2 A (\lambda (b1:
  71 A).(leq g b1 b2)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1)))))))))) with
  72 [(aprem_zero a6 a7) \Rightarrow (\lambda (_: (eq nat O O)).(\lambda (H7: (eq
  73 A (AHead a6 a7) (AHead a3 a5))).(\lambda (H8: (eq A a6 b2)).((let H9 \def
  74 (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with
  75 [(ASort _ _) \Rightarrow a7 | (AHead _ a) \Rightarrow a])) (AHead a6 a7)
  76 (AHead a3 a5) H7) in ((let H10 \def (f_equal A A (\lambda (e: A).(match e in
  77 A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a6 | (AHead a _)
  78 \Rightarrow a])) (AHead a6 a7) (AHead a3 a5) H7) in (eq_ind A a3 (\lambda (a:
  79 A).((eq A a7 a5) \to ((eq A a b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2))
  80 (\lambda (b1: A).(aprem O (AHead a0 a4) b1)))))) (\lambda (H11: (eq A a7
  81 a5)).(eq_ind A a5 (\lambda (_: A).((eq A a3 b2) \to (ex2 A (\lambda (b1:
  82 A).(leq g b1 b2)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1))))) (\lambda
  83 (H12: (eq A a3 b2)).(eq_ind A b2 (\lambda (_: A).(ex2 A (\lambda (b1: A).(leq
  84 g b1 b2)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1)))) (eq_ind A a3
  85 (\lambda (a: A).(ex2 A (\lambda (b1: A).(leq g b1 a)) (\lambda (b1: A).(aprem
  86 O (AHead a0 a4) b1)))) (ex_intro2 A (\lambda (b1: A).(leq g b1 a3)) (\lambda
  87 (b1: A).(aprem O (AHead a0 a4) b1)) a0 H0 (aprem_zero a0 a4)) b2 H12) a3
  88 (sym_eq A a3 b2 H12))) a7 (sym_eq A a7 a5 H11))) a6 (sym_eq A a6 a3 H10)))
  89 H9)) H8)))) | (aprem_succ a6 a i0 H6 a7) \Rightarrow (\lambda (H7: (eq nat (S
  90 i0) O)).(\lambda (H8: (eq A (AHead a7 a6) (AHead a3 a5))).(\lambda (H9: (eq A
  91 a b2)).((let H10 \def (eq_ind nat (S i0) (\lambda (e: nat).(match e in nat
  92 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
  93 True])) I O H7) in (False_ind ((eq A (AHead a7 a6) (AHead a3 a5)) \to ((eq A
  94 a b2) \to ((aprem i0 a6 a) \to (ex2 A (\lambda (b1: A).(leq g b1 b2))
  95 (\lambda (b1: A).(aprem O (AHead a0 a4) b1)))))) H10)) H8 H9 H6))))]) in (H6
  96 (refl_equal nat O) (refl_equal A (AHead a3 a5)) (refl_equal A b2)))) | (S n)
  97 \Rightarrow (\lambda (H5: (aprem (S n) (AHead a3 a5) b2)).(let H6 \def (match
  98 H5 in aprem return (\lambda (n0: nat).(\lambda (a: A).(\lambda (a6:
  99 A).(\lambda (_: (aprem n0 a a6)).((eq nat n0 (S n)) \to ((eq A a (AHead a3
 100 a5)) \to ((eq A a6 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda
 101 (b1: A).(aprem (S n) (AHead a0 a4) b1)))))))))) with [(aprem_zero a6 a7)
 102 \Rightarrow (\lambda (H6: (eq nat O (S n))).(\lambda (H7: (eq A (AHead a6 a7)
 103 (AHead a3 a5))).(\lambda (H8: (eq A a6 b2)).((let H9 \def (eq_ind nat O
 104 (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
 105 \Rightarrow True | (S _) \Rightarrow False])) I (S n) H6) in (False_ind ((eq
 106 A (AHead a6 a7) (AHead a3 a5)) \to ((eq A a6 b2) \to (ex2 A (\lambda (b1:
 107 A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S n) (AHead a0 a4) b1))))) H9)) H7
 108 H8)))) | (aprem_succ a6 a i0 H6 a7) \Rightarrow (\lambda (H7: (eq nat (S i0)
 109 (S n))).(\lambda (H8: (eq A (AHead a7 a6) (AHead a3 a5))).(\lambda (H9: (eq A
 110 a b2)).((let H10 \def (f_equal nat nat (\lambda (e: nat).(match e in nat
 111 return (\lambda (_: nat).nat) with [O \Rightarrow i0 | (S n0) \Rightarrow
 112 n0])) (S i0) (S n) H7) in (eq_ind nat n (\lambda (n0: nat).((eq A (AHead a7
 113 a6) (AHead a3 a5)) \to ((eq A a b2) \to ((aprem n0 a6 a) \to (ex2 A (\lambda
 114 (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S n) (AHead a0 a4) b1)))))))
 115 (\lambda (H11: (eq A (AHead a7 a6) (AHead a3 a5))).(let H12 \def (f_equal A A
 116 (\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _)
 117 \Rightarrow a6 | (AHead _ a8) \Rightarrow a8])) (AHead a7 a6) (AHead a3 a5)
 118 H11) in ((let H13 \def (f_equal A A (\lambda (e: A).(match e in A return
 119 (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a7 | (AHead a8 _)
 120 \Rightarrow a8])) (AHead a7 a6) (AHead a3 a5) H11) in (eq_ind A a3 (\lambda
 121 (_: A).((eq A a6 a5) \to ((eq A a b2) \to ((aprem n a6 a) \to (ex2 A (\lambda
 122 (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S n) (AHead a0 a4) b1)))))))
 123 (\lambda (H14: (eq A a6 a5)).(eq_ind A a5 (\lambda (a8: A).((eq A a b2) \to
 124 ((aprem n a8 a) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
 125 A).(aprem (S n) (AHead a0 a4) b1)))))) (\lambda (H15: (eq A a b2)).(eq_ind A
 126 b2 (\lambda (a8: A).((aprem n a5 a8) \to (ex2 A (\lambda (b1: A).(leq g b1
 127 b2)) (\lambda (b1: A).(aprem (S n) (AHead a0 a4) b1))))) (\lambda (H16:
 128 (aprem n a5 b2)).(let H_x \def (H3 n b2 H16) in (let H17 \def H_x in (ex2_ind
 129 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem n a4 b1)) (ex2 A
 130 (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S n) (AHead a0 a4)
 131 b1))) (\lambda (x: A).(\lambda (H18: (leq g x b2)).(\lambda (H19: (aprem n a4
 132 x)).(ex_intro2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S
 133 n) (AHead a0 a4) b1)) x H18 (aprem_succ a4 x n H19 a0))))) H17)))) a (sym_eq
 134 A a b2 H15))) a6 (sym_eq A a6 a5 H14))) a7 (sym_eq A a7 a3 H13))) H12))) i0
 135 (sym_eq nat i0 n H10))) H8 H9 H6))))]) in (H6 (refl_equal nat (S n))
 136 (refl_equal A (AHead a3 a5)) (refl_equal A b2))))]) H4)))))))))))) a1 a2
 137 H)))).
 138
 139 theorem aprem_asucc:
 140  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (i: nat).((aprem i
 141 a1 a2) \to (aprem i (asucc g a1) a2)))))
 142 \def
 143  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (i: nat).(\lambda
 144 (H: (aprem i a1 a2)).(aprem_ind (\lambda (n: nat).(\lambda (a: A).(\lambda
 145 (a0: A).(aprem n (asucc g a) a0)))) (\lambda (a0: A).(\lambda (a3:
 146 A).(aprem_zero a0 (asucc g a3)))) (\lambda (a0: A).(\lambda (a: A).(\lambda
 147 (i0: nat).(\lambda (_: (aprem i0 a0 a)).(\lambda (H1: (aprem i0 (asucc g a0)
 148 a)).(\lambda (a3: A).(aprem_succ (asucc g a0) a i0 H1 a3))))))) i a1 a2
 149 H))))).
 150