matita/matita/contribs/lambdadelta/basic_1/T/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/T/fwd.ma".
  18
  19 theorem not_abbr_abst:
  20  not (eq B Abbr Abst)
  21 \def
  22  \lambda (H: (eq B Abbr Abst)).(let TMP_1 \def (\lambda (ee: B).(match ee
  23 with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow
  24 False])) in (let H0 \def (eq_ind B Abbr TMP_1 I Abst H) in (False_ind False
  25 H0))).
  26
  27 theorem not_void_abst:
  28  not (eq B Void Abst)
  29 \def
  30  \lambda (H: (eq B Void Abst)).(let TMP_1 \def (\lambda (ee: B).(match ee
  31 with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow
  32 True])) in (let H0 \def (eq_ind B Void TMP_1 I Abst H) in (False_ind False
  33 H0))).
  34
  35 theorem not_abbr_void:
  36  not (eq B Abbr Void)
  37 \def
  38  \lambda (H: (eq B Abbr Void)).(let TMP_1 \def (\lambda (ee: B).(match ee
  39 with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow
  40 False])) in (let H0 \def (eq_ind B Abbr TMP_1 I Void H) in (False_ind False
  41 H0))).
  42
  43 theorem not_abst_void:
  44  not (eq B Abst Void)
  45 \def
  46  \lambda (H: (eq B Abst Void)).(let TMP_1 \def (\lambda (ee: B).(match ee
  47 with [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow
  48 False])) in (let H0 \def (eq_ind B Abst TMP_1 I Void H) in (False_ind False
  49 H0))).
  50
  51 theorem tweight_lt:
  52  \forall (t: T).(lt O (tweight t))
  53 \def
  54  \lambda (t: T).(let TMP_2 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0)
  55 in (lt O TMP_1))) in (let TMP_4 \def (\lambda (_: nat).(let TMP_3 \def (S O)
  56 in (le_n TMP_3))) in (let TMP_6 \def (\lambda (_: nat).(let TMP_5 \def (S O)
  57 in (le_n TMP_5))) in (let TMP_15 \def (\lambda (_: K).(\lambda (t0:
  58 T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O
  59 (tweight t1))).(let TMP_7 \def (S O) in (let TMP_8 \def (tweight t0) in (let
  60 TMP_9 \def (tweight t1) in (let TMP_10 \def (plus TMP_8 TMP_9) in (let TMP_11
  61 \def (S O) in (let TMP_12 \def (tweight t0) in (let TMP_13 \def (tweight t1)
  62 in (let TMP_14 \def (le_plus_trans TMP_11 TMP_12 TMP_13 H) in (le_S TMP_7
  63 TMP_10 TMP_14)))))))))))))) in (T_ind TMP_2 TMP_4 TMP_6 TMP_15 t))))).
  64
  65 theorem tle_r:
  66  \forall (t: T).(tle t t)
  67 \def
  68  \lambda (t: T).(let TMP_3 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0)
  69 in (let TMP_2 \def (tweight t0) in (le TMP_1 TMP_2)))) in (let TMP_5 \def
  70 (\lambda (_: nat).(let TMP_4 \def (S O) in (le_n TMP_4))) in (let TMP_7 \def
  71 (\lambda (_: nat).(let TMP_6 \def (S O) in (le_n TMP_6))) in (let TMP_12 \def
  72 (\lambda (_: K).(\lambda (t0: T).(\lambda (_: (le (tweight t0) (tweight
  73 t0))).(\lambda (t1: T).(\lambda (_: (le (tweight t1) (tweight t1))).(let
  74 TMP_8 \def (tweight t0) in (let TMP_9 \def (tweight t1) in (let TMP_10 \def
  75 (plus TMP_8 TMP_9) in (let TMP_11 \def (S TMP_10) in (le_n TMP_11))))))))))
  76 in (T_ind TMP_3 TMP_5 TMP_7 TMP_12 t))))).
  77