matita/matita/contribs/lambdadelta/basic_1/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 include "basic_1/aprem/fwd.ma".
  18
  19 include "basic_1/leq/fwd.ma".
  20
  21 lemma aprem_repl:
  22  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (\forall
  23 (i: nat).(\forall (b2: A).((aprem i a2 b2) \to (ex2 A (\lambda (b1: A).(leq g
  24 b1 b2)) (\lambda (b1: A).(aprem i a1 b1)))))))))
  25 \def
  26  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leq g a1
  27 a2)).(leq_ind g (\lambda (a: A).(\lambda (a0: A).(\forall (i: nat).(\forall
  28 (b2: A).((aprem i a0 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda
  29 (b1: A).(aprem i a b1)))))))) (\lambda (h1: nat).(\lambda (h2: nat).(\lambda
  30 (n1: nat).(\lambda (n2: nat).(\lambda (k: nat).(\lambda (_: (eq A (aplus g
  31 (ASort h1 n1) k) (aplus g (ASort h2 n2) k))).(\lambda (i: nat).(\lambda (b2:
  32 A).(\lambda (H1: (aprem i (ASort h2 n2) b2)).(let H_x \def (aprem_gen_sort b2
  33 i h2 n2 H1) in (let H2 \def H_x in (False_ind (ex2 A (\lambda (b1: A).(leq g
  34 b1 b2)) (\lambda (b1: A).(aprem i (ASort h1 n1) b1))) H2)))))))))))) (\lambda
  35 (a0: A).(\lambda (a3: A).(\lambda (H0: (leq g a0 a3)).(\lambda (_: ((\forall
  36 (i: nat).(\forall (b2: A).((aprem i a3 b2) \to (ex2 A (\lambda (b1: A).(leq g
  37 b1 b2)) (\lambda (b1: A).(aprem i a0 b1)))))))).(\lambda (a4: A).(\lambda
  38 (a5: A).(\lambda (_: (leq g a4 a5)).(\lambda (H3: ((\forall (i: nat).(\forall
  39 (b2: A).((aprem i a5 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda
  40 (b1: A).(aprem i a4 b1)))))))).(\lambda (i: nat).(\lambda (b2: A).(\lambda
  41 (H4: (aprem i (AHead a3 a5) b2)).(nat_ind (\lambda (n: nat).((aprem n (AHead
  42 a3 a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem
  43 n (AHead a0 a4) b1))))) (\lambda (H5: (aprem O (AHead a3 a5) b2)).(let H_y
  44 \def (aprem_gen_head_O a3 a5 b2 H5) in (eq_ind_r A a3 (\lambda (a: A).(ex2 A
  45 (\lambda (b1: A).(leq g b1 a)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1))))
  46 (ex_intro2 A (\lambda (b1: A).(leq g b1 a3)) (\lambda (b1: A).(aprem O (AHead
  47 a0 a4) b1)) a0 H0 (aprem_zero a0 a4)) b2 H_y))) (\lambda (i0: nat).(\lambda
  48 (_: (((aprem i0 (AHead a3 a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2))
  49 (\lambda (b1: A).(aprem i0 (AHead a0 a4) b1)))))).(\lambda (H5: (aprem (S i0)
  50 (AHead a3 a5) b2)).(let H_y \def (aprem_gen_head_S a3 a5 b2 i0 H5) in (let
  51 H_x \def (H3 i0 b2 H_y) in (let H6 \def H_x in (ex2_ind A (\lambda (b1:
  52 A).(leq g b1 b2)) (\lambda (b1: A).(aprem i0 a4 b1)) (ex2 A (\lambda (b1:
  53 A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 a4) b1))) (\lambda
  54 (x: A).(\lambda (H7: (leq g x b2)).(\lambda (H8: (aprem i0 a4 x)).(ex_intro2
  55 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0
  56 a4) b1)) x H7 (aprem_succ a4 x i0 H8 a0))))) H6))))))) i H4)))))))))))) a1 a2
  57 H)))).
  58
  59 lemma aprem_asucc:
  60  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (i: nat).((aprem i
  61 a1 a2) \to (aprem i (asucc g a1) a2)))))
  62 \def
  63  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (i: nat).(\lambda
  64 (H: (aprem i a1 a2)).(aprem_ind (\lambda (n: nat).(\lambda (a: A).(\lambda
  65 (a0: A).(aprem n (asucc g a) a0)))) (\lambda (a0: A).(\lambda (a3:
  66 A).(aprem_zero a0 (asucc g a3)))) (\lambda (a0: A).(\lambda (a: A).(\lambda
  67 (i0: nat).(\lambda (_: (aprem i0 a0 a)).(\lambda (H1: (aprem i0 (asucc g a0)
  68 a)).(\lambda (a3: A).(aprem_succ (asucc g a0) a i0 H1 a3))))))) i a1 a2
  69 H))))).
  70