matita/matita/contribs/lambdadelta/basic_1/flt/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/flt/defs.ma".
  18
  19 include "basic_1/C/props.ma".
  20
  21 theorem flt_thead_sx:
  22  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c u c
  23 (THead k u t)))))
  24 \def
  25  \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
  26 \def (tweight u) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
  27 t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (S TMP_4) in (let
  28 TMP_6 \def (cweight c) in (let TMP_7 \def (tweight u) in (let TMP_8 \def
  29 (tweight u) in (let TMP_9 \def (tweight t) in (let TMP_10 \def (plus TMP_8
  30 TMP_9) in (let TMP_11 \def (tweight u) in (let TMP_12 \def (tweight t) in
  31 (let TMP_13 \def (le_plus_l TMP_11 TMP_12) in (let TMP_14 \def (le_n_S TMP_7
  32 TMP_10 TMP_13) in (lt_reg_l TMP_1 TMP_5 TMP_6 TMP_14)))))))))))))))))).
  33
  34 theorem flt_thead_dx:
  35  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c t c
  36 (THead k u t)))))
  37 \def
  38  \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
  39 \def (tweight t) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
  40 t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (S TMP_4) in (let
  41 TMP_6 \def (cweight c) in (let TMP_7 \def (tweight t) in (let TMP_8 \def
  42 (tweight u) in (let TMP_9 \def (tweight t) in (let TMP_10 \def (plus TMP_8
  43 TMP_9) in (let TMP_11 \def (tweight u) in (let TMP_12 \def (tweight t) in
  44 (let TMP_13 \def (le_plus_r TMP_11 TMP_12) in (let TMP_14 \def (le_n_S TMP_7
  45 TMP_10 TMP_13) in (lt_reg_l TMP_1 TMP_5 TMP_6 TMP_14)))))))))))))))))).
  46
  47 theorem flt_shift:
  48  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt (CHead c
  49 k u) t c (THead k u t)))))
  50 \def
  51  \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
  52 \def (cweight c) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
  53 t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (plus TMP_1
  54 TMP_4) in (let TMP_6 \def (S TMP_5) in (let TMP_12 \def (\lambda (n:
  55 nat).(let TMP_7 \def (cweight c) in (let TMP_8 \def (tweight u) in (let TMP_9
  56 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (tweight t) in (let TMP_11 \def
  57 (plus TMP_9 TMP_10) in (lt TMP_11 n))))))) in (let TMP_13 \def (cweight c) in
  58 (let TMP_14 \def (tweight u) in (let TMP_15 \def (plus TMP_13 TMP_14) in (let
  59 TMP_16 \def (tweight t) in (let TMP_17 \def (plus TMP_15 TMP_16) in (let
  60 TMP_24 \def (\lambda (n: nat).(let TMP_18 \def (cweight c) in (let TMP_19
  61 \def (tweight u) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def
  62 (tweight t) in (let TMP_22 \def (plus TMP_20 TMP_21) in (let TMP_23 \def (S
  63 n) in (lt TMP_22 TMP_23)))))))) in (let TMP_25 \def (cweight c) in (let
  64 TMP_26 \def (tweight u) in (let TMP_27 \def (plus TMP_25 TMP_26) in (let
  65 TMP_28 \def (tweight t) in (let TMP_29 \def (plus TMP_27 TMP_28) in (let
  66 TMP_30 \def (S TMP_29) in (let TMP_31 \def (le_n TMP_30) in (let TMP_32 \def
  67 (cweight c) in (let TMP_33 \def (tweight u) in (let TMP_34 \def (tweight t)
  68 in (let TMP_35 \def (plus TMP_33 TMP_34) in (let TMP_36 \def (plus TMP_32
  69 TMP_35) in (let TMP_37 \def (cweight c) in (let TMP_38 \def (tweight u) in
  70 (let TMP_39 \def (tweight t) in (let TMP_40 \def (plus_assoc_l TMP_37 TMP_38
  71 TMP_39) in (let TMP_41 \def (eq_ind_r nat TMP_17 TMP_24 TMP_31 TMP_36 TMP_40)
  72 in (let TMP_42 \def (cweight c) in (let TMP_43 \def (tweight u) in (let
  73 TMP_44 \def (tweight t) in (let TMP_45 \def (plus TMP_43 TMP_44) in (let
  74 TMP_46 \def (S TMP_45) in (let TMP_47 \def (plus TMP_42 TMP_46) in (let
  75 TMP_48 \def (cweight c) in (let TMP_49 \def (tweight u) in (let TMP_50 \def
  76 (tweight t) in (let TMP_51 \def (plus TMP_49 TMP_50) in (let TMP_52 \def
  77 (plus_n_Sm TMP_48 TMP_51) in (eq_ind nat TMP_6 TMP_12 TMP_41 TMP_47
  78 TMP_52))))))))))))))))))))))))))))))))))))))))))))).
  79
  80 theorem flt_arith0:
  81  \forall (k: K).(\forall (c: C).(\forall (t: T).(\forall (i: nat).(flt c t
  82 (CHead c k t) (TLRef i)))))
  83 \def
  84  \lambda (_: K).(\lambda (c: C).(\lambda (t: T).(\lambda (_: nat).(let TMP_1
  85 \def (cweight c) in (let TMP_2 \def (tweight t) in (let TMP_3 \def (plus
  86 TMP_1 TMP_2) in (lt_x_plus_x_Sy TMP_3 O))))))).
  87
  88 theorem flt_arith1:
  89  \forall (k1: K).(\forall (c1: C).(\forall (c2: C).(\forall (t1: T).((cle
  90 (CHead c1 k1 t1) c2) \to (\forall (k2: K).(\forall (t2: T).(\forall (i:
  91 nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef i)))))))))
  92 \def
  93  \lambda (_: K).(\lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda
  94 (H: (le (plus (cweight c1) (tweight t1)) (cweight c2))).(\lambda (_:
  95 K).(\lambda (t2: T).(\lambda (_: nat).(let TMP_1 \def (cweight c1) in (let
  96 TMP_2 \def (tweight t1) in (let TMP_3 \def (plus TMP_1 TMP_2) in (let TMP_4
  97 \def (cweight c2) in (let TMP_5 \def (cweight c2) in (let TMP_6 \def (tweight
  98 t2) in (let TMP_7 \def (plus TMP_5 TMP_6) in (let TMP_8 \def (S O) in (let
  99 TMP_9 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (S O) in (let TMP_11 \def
 100 (cweight c2) in (let TMP_12 \def (tweight t2) in (let TMP_13 \def (plus
 101 TMP_11 TMP_12) in (let TMP_14 \def (plus TMP_10 TMP_13) in (let TMP_16 \def
 102 (\lambda (n: nat).(let TMP_15 \def (cweight c2) in (lt TMP_15 n))) in (let
 103 TMP_17 \def (cweight c2) in (let TMP_18 \def (cweight c2) in (let TMP_19 \def
 104 (tweight t2) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def
 105 (cweight c2) in (let TMP_22 \def (tweight t2) in (let TMP_23 \def (le_plus_l
 106 TMP_21 TMP_22) in (let TMP_24 \def (le_lt_n_Sm TMP_17 TMP_20 TMP_23) in (let
 107 TMP_25 \def (cweight c2) in (let TMP_26 \def (tweight t2) in (let TMP_27 \def
 108 (plus TMP_25 TMP_26) in (let TMP_28 \def (S O) in (let TMP_29 \def (plus
 109 TMP_27 TMP_28) in (let TMP_30 \def (cweight c2) in (let TMP_31 \def (tweight
 110 t2) in (let TMP_32 \def (plus TMP_30 TMP_31) in (let TMP_33 \def (S O) in
 111 (let TMP_34 \def (plus_sym TMP_32 TMP_33) in (let TMP_35 \def (eq_ind_r nat
 112 TMP_14 TMP_16 TMP_24 TMP_29 TMP_34) in (le_lt_trans TMP_3 TMP_4 TMP_9 H
 113 TMP_35)))))))))))))))))))))))))))))))))))))))))).
 114
 115 theorem flt_arith2:
 116  \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (i: nat).((flt c1
 117 t1 c2 (TLRef i)) \to (\forall (k2: K).(\forall (t2: T).(\forall (j: nat).(flt
 118 c1 t1 (CHead c2 k2 t2) (TLRef j)))))))))
 119 \def
 120  \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (_: nat).(\lambda
 121 (H: (lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O)))).(\lambda
 122 (_: K).(\lambda (t2: T).(\lambda (_: nat).(let TMP_1 \def (cweight c1) in
 123 (let TMP_2 \def (tweight t1) in (let TMP_3 \def (plus TMP_1 TMP_2) in (let
 124 TMP_4 \def (cweight c2) in (let TMP_5 \def (S O) in (let TMP_6 \def (plus
 125 TMP_4 TMP_5) in (let TMP_7 \def (cweight c2) in (let TMP_8 \def (tweight t2)
 126 in (let TMP_9 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (S O) in (let
 127 TMP_11 \def (plus TMP_9 TMP_10) in (let TMP_12 \def (cweight c2) in (let
 128 TMP_13 \def (cweight c2) in (let TMP_14 \def (tweight t2) in (let TMP_15 \def
 129 (plus TMP_13 TMP_14) in (let TMP_16 \def (S O) in (let TMP_17 \def (S O) in
 130 (let TMP_18 \def (cweight c2) in (let TMP_19 \def (tweight t2) in (let TMP_20
 131 \def (le_plus_l TMP_18 TMP_19) in (let TMP_21 \def (S O) in (let TMP_22 \def
 132 (le_n TMP_21) in (let TMP_23 \def (le_plus_plus TMP_12 TMP_15 TMP_16 TMP_17
 133 TMP_20 TMP_22) in (lt_le_trans TMP_3 TMP_6 TMP_11 H
 134 TMP_23))))))))))))))))))))))))))))))).
 135
 136 theorem cle_flt_trans:
 137  \forall (c1: C).(\forall (c2: C).((cle c1 c2) \to (\forall (c3: C).(\forall
 138 (u2: T).(\forall (u3: T).((flt c2 u2 c3 u3) \to (flt c1 u2 c3 u3)))))))
 139 \def
 140  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (le (cweight c1) (cweight
 141 c2))).(\lambda (c3: C).(\lambda (u2: T).(\lambda (u3: T).(\lambda (H0: (lt
 142 (plus (cweight c2) (tweight u2)) (plus (cweight c3) (tweight u3)))).(let
 143 TMP_1 \def (cweight c1) in (let TMP_2 \def (tweight u2) in (let TMP_3 \def
 144 (plus TMP_1 TMP_2) in (let TMP_4 \def (cweight c2) in (let TMP_5 \def
 145 (tweight u2) in (let TMP_6 \def (plus TMP_4 TMP_5) in (let TMP_7 \def
 146 (cweight c3) in (let TMP_8 \def (tweight u3) in (let TMP_9 \def (plus TMP_7
 147 TMP_8) in (let TMP_10 \def (cweight c1) in (let TMP_11 \def (cweight c2) in
 148 (let TMP_12 \def (tweight u2) in (let TMP_13 \def (tweight u2) in (let TMP_14
 149 \def (tweight u2) in (let TMP_15 \def (le_n TMP_14) in (let TMP_16 \def
 150 (le_plus_plus TMP_10 TMP_11 TMP_12 TMP_13 H TMP_15) in (le_lt_trans TMP_3
 151 TMP_6 TMP_9 TMP_16 H0))))))))))))))))))))))).
 152
 153 theorem flt_trans:
 154  \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (t2: T).((flt c1
 155 t1 c2 t2) \to (\forall (c3: C).(\forall (t3: T).((flt c2 t2 c3 t3) \to (flt
 156 c1 t1 c3 t3))))))))
 157 \def
 158  \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
 159 (H: (lt (fweight c1 t1) (fweight c2 t2))).(\lambda (c3: C).(\lambda (t3:
 160 T).(\lambda (H0: (lt (fweight c2 t2) (fweight c3 t3))).(let TMP_1 \def
 161 (fweight c1 t1) in (let TMP_2 \def (fweight c2 t2) in (let TMP_3 \def
 162 (fweight c3 t3) in (lt_trans TMP_1 TMP_2 TMP_3 H H0))))))))))).
 163