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).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
  23 (eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0
  24 \def (match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S y)
  25 O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in nat with [O
  26 \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq bool
  27 (blt y O) true) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m)
  28 O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat with [O
  29 \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S
  30 y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal nat O)))))
  31 (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq bool (blt
  32 y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n))
  33 \to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S n))).(refl_equal
  34 bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool
  35 (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)])
  36 true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1)))))
  37 y)))) x).
  38
  39 theorem le_bge:
  40  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false)))
  41 \def
  42  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to
  43 (eq bool (blt y n) false)))) (\lambda (y: nat).(\lambda (_: (le O
  44 y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y:
  45 nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind
  46 (\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false)))
  47 (\lambda (H0: (le (S n) O)).(let H1 \def (match H0 in le with [le_n
  48 \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n)
  49 (\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
  50 \Rightarrow True])) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2)))
  51 | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def
  52 (eq_ind nat (S m) (\lambda (e: nat).(match e in nat with [O \Rightarrow False
  53 | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to (eq bool
  54 (blt O (S n)) false)) H3)) H1))]) in (H1 (refl_equal nat O)))) (\lambda (n0:
  55 nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n))
  56 false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 (le_S_n n n0 H1))))) y))))
  57 x).
  58
  59 theorem blt_lt:
  60  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x)))
  61 \def
  62  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt
  63 y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O)
  64 true)).(let H0 \def (match H in eq with [refl_equal \Rightarrow (\lambda (H0:
  65 (eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) (\lambda (e:
  66 bool).(match e in bool with [true \Rightarrow False | false \Rightarrow
  67 True])) I true H0) in (False_ind (lt y O) H1)))]) in (H0 (refl_equal bool
  68 true))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y
  69 n) true) \to (lt y n))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq
  70 bool (blt n0 (S n)) true) \to (lt n0 (S n)))) (\lambda (_: (eq bool true
  71 true)).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n)))))
  72 (\lambda (n0: nat).(\lambda (_: (((eq bool (match n0 with [O \Rightarrow true
  73 | (S m) \Rightarrow (blt m n)]) true) \to (lt n0 (S n))))).(\lambda (H1: (eq
  74 bool (blt n0 n) true)).(lt_n_S n0 n (H n0 H1))))) y)))) x).
  75
  76 theorem bge_le:
  77  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
  78 \def
  79  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt
  80 y n) false) \to (le n y)))) (\lambda (y: nat).(\lambda (_: (eq bool (blt y O)
  81 false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq
  82 bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda
  83 (n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0:
  84 (eq bool (blt O (S n)) false)).(let H1 \def (match H0 in eq with [refl_equal
  85 \Rightarrow (\lambda (H1: (eq bool (blt O (S n)) false)).(let H2 \def (eq_ind
  86 bool (blt O (S n)) (\lambda (e: bool).(match e in bool with [true \Rightarrow
  87 True | false \Rightarrow False])) I false H1) in (False_ind (le (S n) O)
  88 H2)))]) in (H1 (refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_:
  89 (((eq bool (blt n0 (S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool
  90 (blt (S n0) (S n)) false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S
  91 n n0 (H n0 H1))))))) y)))) x).
  92