matita/matita/contribs/lambdadelta/basic_1/llt/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/llt/defs.ma".
  18
  19 include "basic_1/leq/fwd.ma".
  20
  21 theorem lweight_repl:
  22  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (eq nat
  23 (lweight a1) (lweight a2)))))
  24 \def
  25  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leq g a1
  26 a2)).(let TMP_3 \def (\lambda (a: A).(\lambda (a0: A).(let TMP_1 \def
  27 (lweight a) in (let TMP_2 \def (lweight a0) in (eq nat TMP_1 TMP_2))))) in
  28 (let TMP_4 \def (\lambda (h1: nat).(\lambda (h2: nat).(\lambda (n1:
  29 nat).(\lambda (n2: nat).(\lambda (k: nat).(\lambda (_: (eq A (aplus g (ASort
  30 h1 n1) k) (aplus g (ASort h2 n2) k))).(refl_equal nat O))))))) in (let TMP_16
  31 \def (\lambda (a0: A).(\lambda (a3: A).(\lambda (_: (leq g a0 a3)).(\lambda
  32 (H1: (eq nat (lweight a0) (lweight a3))).(\lambda (a4: A).(\lambda (a5:
  33 A).(\lambda (_: (leq g a4 a5)).(\lambda (H3: (eq nat (lweight a4) (lweight
  34 a5))).(let TMP_5 \def (lweight a0) in (let TMP_6 \def (lweight a4) in (let
  35 TMP_7 \def (plus TMP_5 TMP_6) in (let TMP_8 \def (lweight a3) in (let TMP_9
  36 \def (lweight a5) in (let TMP_10 \def (plus TMP_8 TMP_9) in (let TMP_11 \def
  37 (lweight a0) in (let TMP_12 \def (lweight a3) in (let TMP_13 \def (lweight
  38 a4) in (let TMP_14 \def (lweight a5) in (let TMP_15 \def (f_equal2 nat nat
  39 nat plus TMP_11 TMP_12 TMP_13 TMP_14 H1 H3) in (f_equal nat nat S TMP_7
  40 TMP_10 TMP_15)))))))))))))))))))) in (leq_ind g TMP_3 TMP_4 TMP_16 a1 a2
  41 H))))))).
  42
  43 theorem llt_repl:
  44  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (\forall
  45 (a3: A).((llt a1 a3) \to (llt a2 a3))))))
  46 \def
  47  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leq g a1
  48 a2)).(\lambda (a3: A).(\lambda (H0: (lt (lweight a1) (lweight a3))).(let
  49 TMP_1 \def (lweight a1) in (let TMP_3 \def (\lambda (n: nat).(let TMP_2 \def
  50 (lweight a3) in (lt n TMP_2))) in (let TMP_4 \def (lweight a2) in (let TMP_5
  51 \def (lweight_repl g a1 a2 H) in (let H1 \def (eq_ind nat TMP_1 TMP_3 H0
  52 TMP_4 TMP_5) in H1)))))))))).
  53
  54 theorem llt_trans:
  55  \forall (a1: A).(\forall (a2: A).(\forall (a3: A).((llt a1 a2) \to ((llt a2
  56 a3) \to (llt a1 a3)))))
  57 \def
  58  \lambda (a1: A).(\lambda (a2: A).(\lambda (a3: A).(\lambda (H: (lt (lweight
  59 a1) (lweight a2))).(\lambda (H0: (lt (lweight a2) (lweight a3))).(let TMP_1
  60 \def (lweight a1) in (let TMP_2 \def (lweight a2) in (let TMP_3 \def (lweight
  61 a3) in (lt_trans TMP_1 TMP_2 TMP_3 H H0)))))))).
  62
  63 theorem llt_head_sx:
  64  \forall (a1: A).(\forall (a2: A).(llt a1 (AHead a1 a2)))
  65 \def
  66  \lambda (a1: A).(\lambda (a2: A).(let TMP_1 \def (lweight a1) in (let TMP_2
  67 \def (lweight a1) in (let TMP_3 \def (lweight a2) in (let TMP_4 \def (plus
  68 TMP_2 TMP_3) in (let TMP_5 \def (lweight a1) in (let TMP_6 \def (lweight a2)
  69 in (let TMP_7 \def (le_plus_l TMP_5 TMP_6) in (le_n_S TMP_1 TMP_4
  70 TMP_7))))))))).
  71
  72 theorem llt_head_dx:
  73  \forall (a1: A).(\forall (a2: A).(llt a2 (AHead a1 a2)))
  74 \def
  75  \lambda (a1: A).(\lambda (a2: A).(let TMP_1 \def (lweight a2) in (let TMP_2
  76 \def (lweight a1) in (let TMP_3 \def (lweight a2) in (let TMP_4 \def (plus
  77 TMP_2 TMP_3) in (let TMP_5 \def (lweight a1) in (let TMP_6 \def (lweight a2)
  78 in (let TMP_7 \def (le_plus_r TMP_5 TMP_6) in (le_n_S TMP_1 TMP_4
  79 TMP_7))))))))).
  80