matita/matita/contribs/lambdadelta/basic_1/next_plus/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/next_plus/defs.ma".
  18
  19 theorem next_plus_assoc:
  20  \forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq
  21 nat (next_plus g (next_plus g n h1) h2) (next_plus g n (plus h1 h2))))))
  22 \def
  23  \lambda (g: G).(\lambda (n: nat).(\lambda (h1: nat).(let TMP_5 \def (\lambda
  24 (n0: nat).(\forall (h2: nat).(let TMP_1 \def (next_plus g n n0) in (let TMP_2
  25 \def (next_plus g TMP_1 h2) in (let TMP_3 \def (plus n0 h2) in (let TMP_4
  26 \def (next_plus g n TMP_3) in (eq nat TMP_2 TMP_4))))))) in (let TMP_7 \def
  27 (\lambda (h2: nat).(let TMP_6 \def (next_plus g n h2) in (refl_equal nat
  28 TMP_6))) in (let TMP_47 \def (\lambda (n0: nat).(\lambda (_: ((\forall (h2:
  29 nat).(eq nat (next_plus g (next_plus g n n0) h2) (next_plus g n (plus n0
  30 h2)))))).(\lambda (h2: nat).(let TMP_14 \def (\lambda (n1: nat).(let TMP_8
  31 \def (next_plus g n n0) in (let TMP_9 \def (next g TMP_8) in (let TMP_10 \def
  32 (next_plus g TMP_9 n1) in (let TMP_11 \def (plus n0 n1) in (let TMP_12 \def
  33 (next_plus g n TMP_11) in (let TMP_13 \def (next g TMP_12) in (eq nat TMP_10
  34 TMP_13)))))))) in (let TMP_19 \def (\lambda (n1: nat).(let TMP_15 \def
  35 (next_plus g n n0) in (let TMP_16 \def (next g TMP_15) in (let TMP_17 \def
  36 (next_plus g n n1) in (let TMP_18 \def (next g TMP_17) in (eq nat TMP_16
  37 TMP_18)))))) in (let TMP_20 \def (next_plus g n n0) in (let TMP_21 \def (next
  38 g TMP_20) in (let TMP_22 \def (refl_equal nat TMP_21) in (let TMP_23 \def
  39 (plus n0 O) in (let TMP_24 \def (plus_n_O n0) in (let TMP_25 \def (eq_ind nat
  40 n0 TMP_19 TMP_22 TMP_23 TMP_24) in (let TMP_46 \def (\lambda (n1:
  41 nat).(\lambda (H0: (eq nat (next_plus g (next g (next_plus g n n0)) n1) (next
  42 g (next_plus g n (plus n0 n1))))).(let TMP_26 \def (plus n0 n1) in (let
  43 TMP_27 \def (S TMP_26) in (let TMP_34 \def (\lambda (n2: nat).(let TMP_28
  44 \def (next_plus g n n0) in (let TMP_29 \def (next g TMP_28) in (let TMP_30
  45 \def (next_plus g TMP_29 n1) in (let TMP_31 \def (next g TMP_30) in (let
  46 TMP_32 \def (next_plus g n n2) in (let TMP_33 \def (next g TMP_32) in (eq nat
  47 TMP_31 TMP_33)))))))) in (let TMP_35 \def (next g) in (let TMP_36 \def
  48 (next_plus g n n0) in (let TMP_37 \def (next g TMP_36) in (let TMP_38 \def
  49 (next_plus g TMP_37 n1) in (let TMP_39 \def (plus n0 n1) in (let TMP_40 \def
  50 (next_plus g n TMP_39) in (let TMP_41 \def (next g TMP_40) in (let TMP_42
  51 \def (f_equal nat nat TMP_35 TMP_38 TMP_41 H0) in (let TMP_43 \def (S n1) in
  52 (let TMP_44 \def (plus n0 TMP_43) in (let TMP_45 \def (plus_n_Sm n0 n1) in
  53 (eq_ind nat TMP_27 TMP_34 TMP_42 TMP_44 TMP_45))))))))))))))))) in (nat_ind
  54 TMP_14 TMP_25 TMP_46 h2))))))))))))) in (nat_ind TMP_5 TMP_7 TMP_47 h1)))))).
  55
  56 theorem next_plus_next:
  57  \forall (g: G).(\forall (n: nat).(\forall (h: nat).(eq nat (next_plus g
  58 (next g n) h) (next g (next_plus g n h)))))
  59 \def
  60  \lambda (g: G).(\lambda (n: nat).(\lambda (h: nat).(let TMP_1 \def (S O) in
  61 (let TMP_2 \def (plus TMP_1 h) in (let TMP_3 \def (next_plus g n TMP_2) in
  62 (let TMP_6 \def (\lambda (n0: nat).(let TMP_4 \def (next_plus g n h) in (let
  63 TMP_5 \def (next g TMP_4) in (eq nat n0 TMP_5)))) in (let TMP_7 \def
  64 (next_plus g n h) in (let TMP_8 \def (next g TMP_7) in (let TMP_9 \def
  65 (refl_equal nat TMP_8) in (let TMP_10 \def (S O) in (let TMP_11 \def
  66 (next_plus g n TMP_10) in (let TMP_12 \def (next_plus g TMP_11 h) in (let
  67 TMP_13 \def (S O) in (let TMP_14 \def (next_plus_assoc g n TMP_13 h) in
  68 (eq_ind_r nat TMP_3 TMP_6 TMP_9 TMP_12 TMP_14))))))))))))))).
  69
  70 theorem next_plus_lt:
  71  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(lt n (next_plus g (next
  72 g n) h))))
  73 \def
  74  \lambda (g: G).(\lambda (h: nat).(let TMP_3 \def (\lambda (n: nat).(\forall
  75 (n0: nat).(let TMP_1 \def (next g n0) in (let TMP_2 \def (next_plus g TMP_1
  76 n) in (lt n0 TMP_2))))) in (let TMP_4 \def (\lambda (n: nat).(next_lt g n))
  77 in (let TMP_22 \def (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0
  78 (next_plus g (next g n0) n))))).(\lambda (n0: nat).(let TMP_5 \def (next g
  79 n0) in (let TMP_6 \def (next g TMP_5) in (let TMP_7 \def (next_plus g TMP_6
  80 n) in (let TMP_8 \def (\lambda (n1: nat).(lt n0 n1)) in (let TMP_9 \def (next
  81 g n0) in (let TMP_10 \def (next g n0) in (let TMP_11 \def (next g TMP_10) in
  82 (let TMP_12 \def (next_plus g TMP_11 n) in (let TMP_13 \def (next_lt g n0) in
  83 (let TMP_14 \def (next g n0) in (let TMP_15 \def (H TMP_14) in (let TMP_16
  84 \def (lt_trans n0 TMP_9 TMP_12 TMP_13 TMP_15) in (let TMP_17 \def (next g n0)
  85 in (let TMP_18 \def (next_plus g TMP_17 n) in (let TMP_19 \def (next g
  86 TMP_18) in (let TMP_20 \def (next g n0) in (let TMP_21 \def (next_plus_next g
  87 TMP_20 n) in (eq_ind nat TMP_7 TMP_8 TMP_16 TMP_19
  88 TMP_21))))))))))))))))))))) in (nat_ind TMP_3 TMP_4 TMP_22 h))))).
  89