matita/matita/contribs/lambdadelta/basic_1/getl/getl.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/getl/drop.ma".
  18
  19 include "basic_1/getl/clear.ma".
  20
  21 theorem getl_conf_le:
  22  \forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
  23 (e: C).(\forall (h: nat).((getl h c e) \to ((le h i) \to (getl (minus i h) e
  24 a))))))))
  25 \def
  26  \lambda (i: nat).(\lambda (a: C).(\lambda (c: C).(\lambda (H: (getl i c
  27 a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (H0: (getl h c e)).(\lambda
  28 (H1: (le h i)).(let H2 \def (getl_gen_all c e h H0) in (let TMP_1 \def
  29 (\lambda (e0: C).(drop h O c e0)) in (let TMP_2 \def (\lambda (e0: C).(clear
  30 e0 e)) in (let TMP_3 \def (minus i h) in (let TMP_4 \def (getl TMP_3 e a) in
  31 (let TMP_7 \def (\lambda (x: C).(\lambda (H3: (drop h O c x)).(\lambda (H4:
  32 (clear x e)).(let TMP_5 \def (minus i h) in (let TMP_6 \def
  33 (getl_drop_conf_ge i a c H x h O H3 H1) in (getl_clear_conf TMP_5 x a TMP_6 e
  34 H4)))))) in (ex2_ind C TMP_1 TMP_2 TMP_4 TMP_7 H2)))))))))))))).
  35
  36 theorem getl_trans:
  37  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl
  38 h c1 c2) \to (\forall (e2: C).((getl i c2 e2) \to (getl (plus i h) c1
  39 e2)))))))
  40 \def
  41  \lambda (i: nat).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h:
  42 nat).(\lambda (H: (getl h c1 c2)).(\lambda (e2: C).(\lambda (H0: (getl i c2
  43 e2)).(let H1 \def (getl_gen_all c2 e2 i H0) in (let TMP_1 \def (\lambda (e:
  44 C).(drop i O c2 e)) in (let TMP_2 \def (\lambda (e: C).(clear e e2)) in (let
  45 TMP_3 \def (plus i h) in (let TMP_4 \def (getl TMP_3 c1 e2) in (let TMP_14
  46 \def (\lambda (x: C).(\lambda (H2: (drop i O c2 x)).(\lambda (H3: (clear x
  47 e2)).(let TMP_6 \def (\lambda (n: nat).((drop n O c2 x) \to (let TMP_5 \def
  48 (plus n h) in (getl TMP_5 c1 e2)))) in (let TMP_10 \def (\lambda (H4: (drop O
  49 O c2 x)).(let TMP_7 \def (\lambda (c: C).(clear c e2)) in (let TMP_8 \def
  50 (drop_gen_refl c2 x H4) in (let H5 \def (eq_ind_r C x TMP_7 H3 c2 TMP_8) in
  51 (let TMP_9 \def (plus O h) in (getl_clear_trans TMP_9 c1 c2 H e2 H5)))))) in
  52 (let TMP_13 \def (\lambda (i0: nat).(\lambda (_: (((drop i0 O c2 x) \to (getl
  53 (plus i0 h) c1 e2)))).(\lambda (H4: (drop (S i0) O c2 x)).(let H_y \def
  54 (getl_drop_trans c1 c2 h H x i0 H4) in (let TMP_11 \def (S i0) in (let TMP_12
  55 \def (plus TMP_11 h) in (getl_intro TMP_12 c1 e2 x H_y H3))))))) in (nat_ind
  56 TMP_6 TMP_10 TMP_13 i H2))))))) in (ex2_ind C TMP_1 TMP_2 TMP_4 TMP_14
  57 H1))))))))))))).
  58