matita/matita/contribs/lambdadelta/ground_1/blt/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 "ground_1/blt/defs.ma".
  18
  19 theorem lt_blt:
  20  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true)))
  21 \def
  22  \lambda (x: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (y: nat).((lt y
  23 n) \to (let TMP_1 \def (blt y n) in (eq bool TMP_1 true))))) in (let TMP_13
  24 \def (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 \def (match H with
  25 [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let TMP_8 \def (S y) in
  26 (let TMP_9 \def (\lambda (e: nat).(match e with [O \Rightarrow False | (S _)
  27 \Rightarrow True])) in (let H1 \def (eq_ind nat TMP_8 TMP_9 I O H0) in (let
  28 TMP_10 \def (blt y O) in (let TMP_11 \def (eq bool TMP_10 true) in (False_ind
  29 TMP_11 H1))))))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m)
  30 O)).(let TMP_3 \def (S m) in (let TMP_4 \def (\lambda (e: nat).(match e with
  31 [O \Rightarrow False | (S _) \Rightarrow True])) in (let H2 \def (eq_ind nat
  32 TMP_3 TMP_4 I O H1) in (let TMP_6 \def ((le (S y) m) \to (let TMP_5 \def (blt
  33 y O) in (eq bool TMP_5 true))) in (let TMP_7 \def (False_ind TMP_6 H2) in
  34 (TMP_7 H0)))))))]) in (let TMP_12 \def (refl_equal nat O) in (H0 TMP_12)))))
  35 in (let TMP_21 \def (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y
  36 n) \to (eq bool (blt y n) true))))).(\lambda (y: nat).(let TMP_16 \def
  37 (\lambda (n0: nat).((lt n0 (S n)) \to (let TMP_14 \def (S n) in (let TMP_15
  38 \def (blt n0 TMP_14) in (eq bool TMP_15 true))))) in (let TMP_17 \def
  39 (\lambda (_: (lt O (S n))).(refl_equal bool true)) in (let TMP_20 \def
  40 (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool (match n0 with
  41 [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)))).(\lambda (H1:
  42 (lt (S n0) (S n))).(let TMP_18 \def (S n0) in (let TMP_19 \def (le_S_n TMP_18
  43 n H1) in (H n0 TMP_19)))))) in (nat_ind TMP_16 TMP_17 TMP_20 y))))))) in
  44 (nat_ind TMP_2 TMP_13 TMP_21 x)))).
  45
  46 theorem le_bge:
  47  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false)))
  48 \def
  49  \lambda (x: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (y: nat).((le n
  50 y) \to (let TMP_1 \def (blt y n) in (eq bool TMP_1 false))))) in (let TMP_3
  51 \def (\lambda (y: nat).(\lambda (_: (le O y)).(refl_equal bool false))) in
  52 (let TMP_22 \def (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((le n y)
  53 \to (eq bool (blt y n) false))))).(\lambda (y: nat).(let TMP_6 \def (\lambda
  54 (n0: nat).((le (S n) n0) \to (let TMP_4 \def (S n) in (let TMP_5 \def (blt n0
  55 TMP_4) in (eq bool TMP_5 false))))) in (let TMP_19 \def (\lambda (H0: (le (S
  56 n) O)).(let H1 \def (match H0 with [le_n \Rightarrow (\lambda (H1: (eq nat (S
  57 n) O)).(let TMP_13 \def (S n) in (let TMP_14 \def (\lambda (e: nat).(match e
  58 with [O \Rightarrow False | (S _) \Rightarrow True])) in (let H2 \def (eq_ind
  59 nat TMP_13 TMP_14 I O H1) in (let TMP_15 \def (S n) in (let TMP_16 \def (blt
  60 O TMP_15) in (let TMP_17 \def (eq bool TMP_16 false) in (False_ind TMP_17
  61 H2)))))))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).(let
  62 TMP_7 \def (S m) in (let TMP_8 \def (\lambda (e: nat).(match e with [O
  63 \Rightarrow False | (S _) \Rightarrow True])) in (let H3 \def (eq_ind nat
  64 TMP_7 TMP_8 I O H2) in (let TMP_11 \def ((le (S n) m) \to (let TMP_9 \def (S
  65 n) in (let TMP_10 \def (blt O TMP_9) in (eq bool TMP_10 false)))) in (let
  66 TMP_12 \def (False_ind TMP_11 H3) in (TMP_12 H1)))))))]) in (let TMP_18 \def
  67 (refl_equal nat O) in (H1 TMP_18)))) in (let TMP_21 \def (\lambda (n0:
  68 nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n))
  69 false)))).(\lambda (H1: (le (S n) (S n0))).(let TMP_20 \def (le_S_n n n0 H1)
  70 in (H n0 TMP_20))))) in (nat_ind TMP_6 TMP_19 TMP_21 y))))))) in (nat_ind
  71 TMP_2 TMP_3 TMP_22 x)))).
  72
  73 theorem blt_lt:
  74  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x)))
  75 \def
  76  \lambda (x: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (y: nat).((eq
  77 bool (blt y n) true) \to (lt y n)))) in (let TMP_6 \def (\lambda (y:
  78 nat).(\lambda (H: (eq bool (blt y O) true)).(let H0 \def (match H with
  79 [refl_equal \Rightarrow (\lambda (H0: (eq bool (blt y O) true)).(let TMP_2
  80 \def (blt y O) in (let TMP_3 \def (\lambda (e: bool).(match e with [true
  81 \Rightarrow False | false \Rightarrow True])) in (let H1 \def (eq_ind bool
  82 TMP_2 TMP_3 I true H0) in (let TMP_4 \def (lt y O) in (False_ind TMP_4
  83 H1))))))]) in (let TMP_5 \def (refl_equal bool true) in (H0 TMP_5))))) in
  84 (let TMP_19 \def (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool
  85 (blt y n) true) \to (lt y n))))).(\lambda (y: nat).(let TMP_8 \def (\lambda
  86 (n0: nat).((eq bool (blt n0 (S n)) true) \to (let TMP_7 \def (S n) in (lt n0
  87 TMP_7)))) in (let TMP_16 \def (\lambda (_: (eq bool true true)).(let TMP_9
  88 \def (S O) in (let TMP_10 \def (S n) in (let TMP_11 \def (S O) in (let TMP_12
  89 \def (S n) in (let TMP_13 \def (le_O_n n) in (let TMP_14 \def (le_n_S O n
  90 TMP_13) in (let TMP_15 \def (le_n_S TMP_11 TMP_12 TMP_14) in (le_S_n TMP_9
  91 TMP_10 TMP_15))))))))) in (let TMP_18 \def (\lambda (n0: nat).(\lambda (_:
  92 (((eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)])
  93 true) \to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(let
  94 TMP_17 \def (H n0 H1) in (lt_n_S n0 n TMP_17))))) in (nat_ind TMP_8 TMP_16
  95 TMP_18 y))))))) in (nat_ind TMP_1 TMP_6 TMP_19 x)))).
  96
  97 theorem bge_le:
  98  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
  99 \def
 100  \lambda (x: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (y: nat).((eq
 101 bool (blt y n) false) \to (le n y)))) in (let TMP_2 \def (\lambda (y:
 102 nat).(\lambda (_: (eq bool (blt y O) false)).(le_O_n y))) in (let TMP_20 \def
 103 (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y n) false)
 104 \to (le n y))))).(\lambda (y: nat).(let TMP_4 \def (\lambda (n0: nat).((eq
 105 bool (blt n0 (S n)) false) \to (let TMP_3 \def (S n) in (le TMP_3 n0)))) in
 106 (let TMP_11 \def (\lambda (H0: (eq bool (blt O (S n)) false)).(let H1 \def
 107 (match H0 with [refl_equal \Rightarrow (\lambda (H1: (eq bool (blt O (S n))
 108 false)).(let TMP_5 \def (S n) in (let TMP_6 \def (blt O TMP_5) in (let TMP_7
 109 \def (\lambda (e: bool).(match e with [true \Rightarrow True | false
 110 \Rightarrow False])) in (let H2 \def (eq_ind bool TMP_6 TMP_7 I false H1) in
 111 (let TMP_8 \def (S n) in (let TMP_9 \def (le TMP_8 O) in (False_ind TMP_9
 112 H2))))))))]) in (let TMP_10 \def (refl_equal bool false) in (H1 TMP_10)))) in
 113 (let TMP_19 \def (\lambda (n0: nat).(\lambda (_: (((eq bool (blt n0 (S n))
 114 false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) (S n))
 115 false)).(let TMP_12 \def (S n) in (let TMP_13 \def (S n0) in (let TMP_14 \def
 116 (S n) in (let TMP_15 \def (S n0) in (let TMP_16 \def (H n0 H1) in (let TMP_17
 117 \def (le_n_S n n0 TMP_16) in (let TMP_18 \def (le_n_S TMP_14 TMP_15 TMP_17)
 118 in (le_S_n TMP_12 TMP_13 TMP_18))))))))))) in (nat_ind TMP_4 TMP_11 TMP_19
 119 y))))))) in (nat_ind TMP_1 TMP_2 TMP_20 x)))).
 120