LDWS := $(shell find -name "*.ldw.xml")
TBLS := $(shell find -name "*.tbl")
-all:
- ../../matitac.opt
-
# MAS ########################################################################
define MAS_TEMPLATE
$(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG))))
+all:
+ @echo " MATITAC $(PACKAGES)"
+ $(H)../../matitac.opt $(MAS)
+
# XMAS #######################################################################
define XMAS_TEMPLATE
(* *)
(**************************************************************************)
-include "Ground-1/theory.ma".
+include "ground_1/theory.ma".
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
-definition blt:
- nat \to (nat \to bool)
-\def
- let rec blt (m: nat) (n: nat) on n: bool \def (match n with [O \Rightarrow
+let rec blt (m: nat) (n: nat) on n: bool \def match n with [O \Rightarrow
false | (S n0) \Rightarrow (match m with [O \Rightarrow true | (S m0)
-\Rightarrow (blt m0 n0)])]) in blt.
+\Rightarrow (blt m0 n0)])].
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/blt/defs.ma".
+include "ground_1/blt/defs.ma".
theorem lt_blt:
\forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true)))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
(eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0
-\def (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat
-n O) \to (eq bool (blt y O) true)))) with [le_n \Rightarrow (\lambda (H0: (eq
-nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in
-nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true) H1))) |
-(le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind
-nat (S m) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop)
-with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind
-((le (S y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal
-nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to
-(eq bool (blt y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0:
-nat).((lt n0 (S n)) \to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S
-n))).(refl_equal bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n))
-\to (eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m
-n)]) true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1)))))
+\def (match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S y)
+O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in nat with [O
+\Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq bool
+(blt y O) true) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m)
+O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat with [O
+\Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S
+y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal nat O)))))
+(\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq bool (blt
+y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n))
+\to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S n))).(refl_equal
+bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool
+(match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)])
+true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1)))))
y)))) x).
-(* COMMENTS
-Initial nodes: 291
-END *)
theorem le_bge:
\forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false)))
y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y:
nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind
(\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false)))
-(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 in le return (\lambda (n0:
-nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to (eq bool (blt O (S n))
-false)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
-(eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_:
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in
-(False_ind (eq bool (blt O (S n)) false) H2))) | (le_S m H1) \Rightarrow
-(\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e:
-nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False
+(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 in le with [le_n
+\Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n)
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
+\Rightarrow True])) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2)))
+| (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def
+(eq_ind nat (S m) (\lambda (e: nat).(match e in nat with [O \Rightarrow False
| (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to (eq bool
(blt O (S n)) false)) H3)) H1))]) in (H1 (refl_equal nat O)))) (\lambda (n0:
nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n))
false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 (le_S_n n n0 H1))))) y))))
x).
-(* COMMENTS
-Initial nodes: 293
-END *)
theorem blt_lt:
\forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x)))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt
y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O)
-true)).(let H0 \def (match H in eq return (\lambda (b: bool).(\lambda (_: (eq
-? ? b)).((eq bool b true) \to (lt y O)))) with [refl_equal \Rightarrow
-(\lambda (H0: (eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O)
-(\lambda (e: bool).(match e in bool return (\lambda (_: bool).Prop) with
-[true \Rightarrow False | false \Rightarrow True])) I true H0) in (False_ind
-(lt y O) H1)))]) in (H0 (refl_equal bool true))))) (\lambda (n: nat).(\lambda
-(H: ((\forall (y: nat).((eq bool (blt y n) true) \to (lt y n))))).(\lambda
-(y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) true) \to (lt
-n0 (S n)))) (\lambda (_: (eq bool true true)).(le_S_n (S O) (S n) (le_n_S (S
-O) (S n) (le_n_S O n (le_O_n n))))) (\lambda (n0: nat).(\lambda (_: (((eq
-bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)
-\to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_n_S n0 n (H
-n0 H1))))) y)))) x).
-(* COMMENTS
-Initial nodes: 252
-END *)
+true)).(let H0 \def (match H in eq with [refl_equal \Rightarrow (\lambda (H0:
+(eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) (\lambda (e:
+bool).(match e in bool with [true \Rightarrow False | false \Rightarrow
+True])) I true H0) in (False_ind (lt y O) H1)))]) in (H0 (refl_equal bool
+true))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y
+n) true) \to (lt y n))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq
+bool (blt n0 (S n)) true) \to (lt n0 (S n)))) (\lambda (_: (eq bool true
+true)).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n)))))
+(\lambda (n0: nat).(\lambda (_: (((eq bool (match n0 with [O \Rightarrow true
+| (S m) \Rightarrow (blt m n)]) true) \to (lt n0 (S n))))).(\lambda (H1: (eq
+bool (blt n0 n) true)).(lt_n_S n0 n (H n0 H1))))) y)))) x).
theorem bge_le:
\forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq
bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda
(n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0:
-(eq bool (blt O (S n)) false)).(let H1 \def (match H0 in eq return (\lambda
-(b: bool).(\lambda (_: (eq ? ? b)).((eq bool b false) \to (le (S n) O))))
-with [refl_equal \Rightarrow (\lambda (H1: (eq bool (blt O (S n))
-false)).(let H2 \def (eq_ind bool (blt O (S n)) (\lambda (e: bool).(match e
-in bool return (\lambda (_: bool).Prop) with [true \Rightarrow True | false
-\Rightarrow False])) I false H1) in (False_ind (le (S n) O) H2)))]) in (H1
-(refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: (((eq bool (blt n0
-(S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) (S n))
-false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0
-H1))))))) y)))) x).
-(* COMMENTS
-Initial nodes: 262
-END *)
+(eq bool (blt O (S n)) false)).(let H1 \def (match H0 in eq with [refl_equal
+\Rightarrow (\lambda (H1: (eq bool (blt O (S n)) false)).(let H2 \def (eq_ind
+bool (blt O (S n)) (\lambda (e: bool).(match e in bool with [true \Rightarrow
+True | false \Rightarrow False])) I false H1) in (False_ind (le (S n) O)
+H2)))]) in (H1 (refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_:
+(((eq bool (blt n0 (S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool
+(blt (S n0) (S n)) false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S
+n n0 (H n0 H1))))))) y)))) x).
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/types/defs.ma".
+include "ground_1/types/defs.ma".
-include "Ground-1/blt/defs.ma".
+include "ground_1/blt/defs.ma".
-include "Ground-1/plist/defs.ma".
+include "ground_1/plist/defs.ma".
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
theorem nat_dec:
\forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to
((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq
nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S
n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match
-ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _)
-\Rightarrow False])) I (S n) H0) in (False_ind P H1))))))) n2)) (\lambda (n:
-nat).(\lambda (H: ((\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to
-(\forall (P: Prop).P)))))).(\lambda (n2: nat).(nat_ind (\lambda (n0: nat).(or
-(eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) (or_intror
-(eq nat (S n) O) ((eq nat (S n) O) \to (\forall (P: Prop).P)) (\lambda (H0:
-(eq nat (S n) O)).(\lambda (P: Prop).(let H1 \def (eq_ind nat (S n) (\lambda
-(ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
-False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) (\lambda
-(n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall
-(P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P:
-Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P:
-Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0
-(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P:
-Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S
-n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat
-(S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat
-(S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P:
-Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
-(\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P:
-Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return
-(\lambda (_: nat).nat) with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n)
-(S n0) H2) in (let H4 \def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3)
-\to (\forall (P0: Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0
-(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0:
-Prop).P0)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2))))
-n1).
-(* COMMENTS
-Initial nodes: 676
-END *)
+ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I (S n) H0)
+in (False_ind P H1))))))) n2)) (\lambda (n: nat).(\lambda (H: ((\forall (n2:
+nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda
+(n2: nat).(nat_ind (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n)
+n0) \to (\forall (P: Prop).P)))) (or_intror (eq nat (S n) O) ((eq nat (S n)
+O) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat (S n) O)).(\lambda (P:
+Prop).(let H1 \def (eq_ind nat (S n) (\lambda (ee: nat).(match ee in nat with
+[O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind P
+H1))))) (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n)
+n0) \to (\forall (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to
+(\forall (P: Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
+(\forall (P: Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r
+nat n0 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to
+(\forall (P: Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq
+nat (S n) (S n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P))))
+(or_introl (eq nat (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P:
+Prop).P)) (refl_equal nat (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to
+(\forall (P: Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S
+n0)) \to (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda
+(P: Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat
+with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n) (S n0) H2) in (let H4
+\def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) \to (\forall (P0:
+Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 (\lambda (n3: nat).(or
+(eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: Prop).P0)))) H0 n H3)
+in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).
theorem simpl_plus_r:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n)
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat
(plus m n) (plus p n))).(simpl_plus_l n m p (eq_ind_r nat (plus m n) (\lambda
(n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0:
-nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_sym n
-p)) (plus m n) H) (plus n m) (plus_sym n m)))))).
-(* COMMENTS
-Initial nodes: 119
-END *)
+nat).(eq nat n0 (plus n p))) (plus_sym p n) (plus m n) H) (plus n m)
+(plus_sym n m)))))).
theorem minus_Sx_Sy:
\forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
\def
\lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
-(* COMMENTS
-Initial nodes: 13
-END *)
theorem minus_plus_r:
\forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
\def
\lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0:
nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
-(* COMMENTS
-Initial nodes: 45
-END *)
theorem plus_permute_2_in_3:
\forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x
nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y)))
(refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z
y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
-(* COMMENTS
-Initial nodes: 163
-END *)
theorem plus_permute_2_in_3_assoc:
\forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n
nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0))
(refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k
h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
-(* COMMENTS
-Initial nodes: 119
-END *)
theorem plus_O:
\forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat
(H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O)
H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O)
\to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq
-nat (plus (S n) y) O)).(let H1 \def (match H0 in eq return (\lambda (n0:
-nat).(\lambda (_: (eq ? ? n0)).((eq nat n0 O) \to (land (eq nat (S n) O) (eq
-nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n)
-y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e in
-nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y
-O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
-(* COMMENTS
-Initial nodes: 233
-END *)
+nat (plus (S n) y) O)).(let H1 \def (match H0 in eq with [refl_equal
+\Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat
+(plus (S n) y) (\lambda (e: nat).(match e in nat with [O \Rightarrow False |
+(S _) \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq
+nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
theorem minus_Sx_SO:
\forall (x: nat).(eq nat (minus (S x) (S O)) x)
\def
\lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal
nat x) (minus x O) (minus_n_O x)).
-(* COMMENTS
-Initial nodes: 33
-END *)
-theorem eq_nat_dec:
+theorem nat_dec_neg:
\forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
\def
\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq
n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not
(eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H
n0)))) j)))) i).
-(* COMMENTS
-Initial nodes: 401
-END *)
theorem neq_eq_e:
\forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j))
\def
\lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not
(eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def
-(eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
-(* COMMENTS
-Initial nodes: 61
-END *)
+(nat_dec_neg i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
theorem le_false:
\forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S
\lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P:
Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P:
Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match
-H0 in le return (\lambda (n0: nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to
-P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
-(eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_:
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in
-(False_ind P H2))) | (le_S m0 H1) \Rightarrow (\lambda (H2: (eq nat (S m0)
-O)).((let H3 \def (eq_ind nat (S m0) (\lambda (e: nat).(match e in nat return
-(\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True]))
-I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1 (refl_equal
-nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P:
-Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind
-(\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n))
-\to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S
-O) (S n))).(let H2 \def (match H0 in le return (\lambda (n1: nat).(\lambda
-(_: (le ? n1)).((eq nat n1 O) \to P))) with [le_n \Rightarrow (\lambda (H2:
-(eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e
-in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
+H0 in le with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
+(eq_ind nat (S n) (\lambda (e: nat).(match e in nat with [O \Rightarrow False
+| (S _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m0 H1)
+\Rightarrow (\lambda (H2: (eq nat (S m0) O)).((let H3 \def (eq_ind nat (S m0)
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
+\Rightarrow True])) I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))])
+in (H1 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0:
+nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda
+(n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to
+((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n)
+O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 in le with [le_n
+\Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n)
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
\Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow
(\lambda (H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda
-(e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
-False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m0) \to P)
-H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_:
-((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda
-(P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S
+(e: nat).(match e in nat with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H3) in (False_ind ((le (S n) m0) \to P) H4)) H2))]) in (H2
+(refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P:
+Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P:
+Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S
n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
-(* COMMENTS
-Initial nodes: 409
-END *)
theorem le_Sx_x:
\forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
\def
\lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def
le_Sn_n in (False_ind P (H0 x H))))).
-(* COMMENTS
-Initial nodes: 23
-END *)
theorem le_n_pred:
\forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
(n0: nat).(le (pred n) (pred n0))) (le_n (pred n)) (\lambda (m0:
nat).(\lambda (_: (le n m0)).(\lambda (H1: (le (pred n) (pred m0))).(le_trans
(pred n) (pred m0) m0 H1 (le_pred_n m0))))) m H))).
-(* COMMENTS
-Initial nodes: 71
-END *)
theorem minus_le:
\forall (x: nat).(\forall (y: nat).(le (minus x y) x))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n
-y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall
-(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda (n0:
-nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: nat).(\lambda
-(_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)])
-(S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
-(* COMMENTS
-Initial nodes: 101
-END *)
+y) n))) (\lambda (_: nat).(le_O_n O)) (\lambda (n: nat).(\lambda (H:
+((\forall (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda
+(n0: nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0:
+nat).(\lambda (_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow
+(minus n l)]) (S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
theorem le_plus_minus_sym:
\forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n)
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat
(plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H)
(plus (minus m n) n) (plus_sym (minus m n) n)))).
-(* COMMENTS
-Initial nodes: 61
-END *)
theorem le_minus_minus:
\forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z)
(eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat
z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z
(le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
-(* COMMENTS
-Initial nodes: 117
-END *)
theorem le_minus_plus:
\forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat
\def
\lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to
(\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y))))))
-(\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le return
-(\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) \to (\forall (y:
-nat).(eq nat (minus (plus x y) O) (plus (minus x O) y)))))) with [le_n
-\Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n:
+(\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le with
+[le_n \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n:
nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))
(\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O)
(minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq
(minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S
z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n
(S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def
-(match H0 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
-\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))))) with
-[le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat
-(S z0) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with
-[O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq
-nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1)
+(match H0 in le with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let
+H2 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e in nat with [O
+\Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat
+(minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1)
\Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m)
-(\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
-\Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S
-z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3))
-H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S
-z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n
-(S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n
-(le_S_n z0 n H1) y))))) x)))) z).
-(* COMMENTS
-Initial nodes: 603
-END *)
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
+\Rightarrow True])) I O H2) in (False_ind ((le (S z0) m) \to (eq nat (minus
+(plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal
+nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S z0) n) \to (\forall (y:
+nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0))
+y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n (le_S_n z0 n
+H1) y))))) x)))) z).
theorem le_minus:
\forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to
x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z
y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x
y))))).
-(* COMMENTS
-Initial nodes: 69
-END *)
theorem le_trans_plus_r:
\forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus
x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
-(* COMMENTS
-Initial nodes: 35
-END *)
theorem lt_x_O:
\forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
\def
\lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let H_y \def
(le_n_O_eq (S x) H) in (let H0 \def (eq_ind nat O (\lambda (ee: nat).(match
-ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _)
-\Rightarrow False])) I (S x) H_y) in (False_ind P H0))))).
-(* COMMENTS
-Initial nodes: 48
-END *)
+ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x) H_y)
+in (False_ind P H0))))).
theorem le_gen_S:
\forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n:
nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
\def
\lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def
-(match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x)
-\to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m
-n0)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat
-(S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0)))
+(match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind
+nat (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0)))
(\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S
m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x
H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat
m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n:
nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2))))
x H1 H0))]) in (H0 (refl_equal nat x))))).
-(* COMMENTS
-Initial nodes: 261
-END *)
theorem lt_x_plus_x_Sy:
\forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
\lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n:
nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x))
(le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
-(* COMMENTS
-Initial nodes: 83
-END *)
theorem simpl_lt_plus_r:
\forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m
(\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_sym n p)) in (let
H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0
(plus p m) (plus_sym m p)) in H1)))))).
-(* COMMENTS
-Initial nodes: 101
-END *)
theorem minus_x_Sy:
\forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
(eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H:
-(lt y O)).(let H0 \def (match H in le return (\lambda (n: nat).(\lambda (_:
-(le ? n)).((eq nat n O) \to (eq nat (minus O y) (S (minus O (S y))))))) with
-[le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S
-y) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
-\Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat
-(minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda
-(H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e:
-nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False
-| (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat
-(minus O y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O)))))
-(\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat
-(minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0:
-nat).((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))
-(\lambda (_: (lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S
-n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0:
+(lt y O)).(let H0 \def (match H in le with [le_n \Rightarrow (\lambda (H0:
+(eq nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e
+in nat with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in
+(False_ind (eq nat (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0)
+\Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m)
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
+\Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat (minus O
+y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda
+(n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S
+(minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0
+(S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda (_:
+(lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S n0)))
+(refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0:
nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S
n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0)
n H1) in (H n0 H2))))) y)))) x).
-(* COMMENTS
-Initial nodes: 383
-END *)
theorem lt_plus_minus:
\forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S
x) y H))).
-(* COMMENTS
-Initial nodes: 19
-END *)
theorem lt_plus_minus_r:
\forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat
(plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x
y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
-(* COMMENTS
-Initial nodes: 69
-END *)
theorem minus_x_SO:
\forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
\lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n:
nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal
nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
-(* COMMENTS
-Initial nodes: 77
-END *)
theorem le_x_pred_y:
\forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
\def
\lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to
(le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def
-(match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
-\to (le x O)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let
-H1 \def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat return (\lambda
-(_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0)
-in (False_ind (le x O) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat
-(S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat
-return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
-True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0
-(refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt
-x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S
-n))).(le_S_n x n H0))))) y).
-(* COMMENTS
-Initial nodes: 189
-END *)
+(match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let H1
+\def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat with [O \Rightarrow
+False | (S _) \Rightarrow True])) I O H0) in (False_ind (le x O) H1))) |
+(le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind
+nat (S m) (\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
+\Rightarrow True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2))
+H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall
+(x: nat).((lt x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0:
+(lt x (S n))).(le_S_n x n H0))))) y).
theorem lt_le_minus:
\forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S
O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O))
(plus_sym x (S O)))))).
-(* COMMENTS
-Initial nodes: 57
-END *)
theorem lt_le_e:
\forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P))
\lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n
d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in
(or_ind (le d n) (lt n d) P H0 H H1)))))).
-(* COMMENTS
-Initial nodes: 49
-END *)
theorem lt_eq_e:
\forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
\lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x
y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x
y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
-(* COMMENTS
-Initial nodes: 59
-END *)
theorem lt_eq_gt_e:
\forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x)
\to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda
(H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
-(* COMMENTS
-Initial nodes: 79
-END *)
theorem lt_gen_xS:
\forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2
(\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0)))
(ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt
m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
-(* COMMENTS
-Initial nodes: 243
-END *)
theorem le_lt_false:
\forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P:
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt
y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
-(* COMMENTS
-Initial nodes: 31
-END *)
theorem lt_neq:
\forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq
nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in
(lt_n_n y H1))))).
-(* COMMENTS
-Initial nodes: 43
-END *)
theorem arith0:
\forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n)
(le_plus_plus (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_sym h2
d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1)
(minus_plus h2 (plus d2 h1))))))).
-(* COMMENTS
-Initial nodes: 235
-END *)
theorem O_minus:
\forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
O)).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le x0
n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H1: (eq nat O (S
x1))).(\lambda (_: (le x0 x1)).(let H3 \def (eq_ind nat O (\lambda (ee:
-nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
-| (S _) \Rightarrow False])) I (S x1) H1) in (False_ind (eq nat (S x0) O)
-H3))))) (le_gen_S x0 O H0))) (\lambda (n: nat).(\lambda (_: (((le (S x0) n)
-\to (eq nat (match n with [O \Rightarrow (S x0) | (S l) \Rightarrow (minus x0
-l)]) O)))).(\lambda (H1: (le (S x0) (S n))).(H n (le_S_n x0 n H1))))) y))))
-x).
-(* COMMENTS
-Initial nodes: 252
-END *)
+nat).(match ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I
+(S x1) H1) in (False_ind (eq nat (S x0) O) H3))))) (le_gen_S x0 O H0)))
+(\lambda (n: nat).(\lambda (_: (((le (S x0) n) \to (eq nat (match n with [O
+\Rightarrow (S x0) | (S l) \Rightarrow (minus x0 l)]) O)))).(\lambda (H1: (le
+(S x0) (S n))).(H n (le_S_n x0 n H1))))) y)))) x).
theorem minus_minus:
\forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y)
z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le
z0 n)) (eq nat O y) (\lambda (x0: nat).(\lambda (H2: (eq nat O (S
x0))).(\lambda (_: (le z0 x0)).(let H4 \def (eq_ind nat O (\lambda (ee:
-nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
-| (S _) \Rightarrow False])) I (S x0) H2) in (False_ind (eq nat O y) H4)))))
-(le_gen_S z0 O H)))))) (\lambda (x0: nat).(\lambda (_: ((\forall (y:
-nat).((le (S z0) x0) \to ((le (S z0) y) \to ((eq nat (minus x0 (S z0)) (minus
-y (S z0))) \to (eq nat x0 y))))))).(\lambda (y: nat).(nat_ind (\lambda (n:
-nat).((le (S z0) (S x0)) \to ((le (S z0) n) \to ((eq nat (minus (S x0) (S
-z0)) (minus n (S z0))) \to (eq nat (S x0) n))))) (\lambda (H: (le (S z0) (S
-x0))).(\lambda (H0: (le (S z0) O)).(\lambda (_: (eq nat (minus (S x0) (S z0))
-(minus O (S z0)))).(let H_y \def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda
-(n: nat).(eq nat O (S n))) (\lambda (n: nat).(le z0 n)) (eq nat (S x0) O)
-(\lambda (x1: nat).(\lambda (H2: (eq nat O (S x1))).(\lambda (_: (le z0
-x1)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat return
-(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
-I (S x1) H2) in (False_ind (eq nat (S x0) O) H4))))) (le_gen_S z0 O H0))))))
-(\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to
-((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0)
-y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S
-y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S
+nat).(match ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I
+(S x0) H2) in (False_ind (eq nat O y) H4))))) (le_gen_S z0 O H)))))) (\lambda
+(x0: nat).(\lambda (_: ((\forall (y: nat).((le (S z0) x0) \to ((le (S z0) y)
+\to ((eq nat (minus x0 (S z0)) (minus y (S z0))) \to (eq nat x0
+y))))))).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((le (S z0) (S x0)) \to
+((le (S z0) n) \to ((eq nat (minus (S x0) (S z0)) (minus n (S z0))) \to (eq
+nat (S x0) n))))) (\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0)
+O)).(\lambda (_: (eq nat (minus (S x0) (S z0)) (minus O (S z0)))).(let H_y
+\def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda (n: nat).(eq nat O (S n)))
+(\lambda (n: nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda
+(H2: (eq nat O (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O
+(\lambda (ee: nat).(match ee in nat with [O \Rightarrow True | (S _)
+\Rightarrow False])) I (S x1) H2) in (False_ind (eq nat (S x0) O) H4)))))
+(le_gen_S z0 O H0)))))) (\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0))
+\to ((le (S z0) y0) \to ((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to
+(eq nat (S x0) y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S
+z0) (S y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S
z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0)
H1))))))) y)))) x)))) z).
-(* COMMENTS
-Initial nodes: 751
-END *)
theorem plus_plus:
\forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1:
x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4
y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3))))
x1)))) z).
-(* COMMENTS
-Initial nodes: 1495
-END *)
theorem le_S_minus:
\forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to
\def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus n h) h)
(le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S
d (minus n h) (le_minus d n h H))))))).
-(* COMMENTS
-Initial nodes: 107
-END *)
theorem lt_x_pred_y:
\forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
\lambda (x: nat).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((lt x (pred
n)) \to (lt (S x) n))) (\lambda (H: (lt x O)).(lt_x_O x H (lt (S x) O)))
(\lambda (n: nat).(\lambda (_: (((lt x (pred n)) \to (lt (S x) n)))).(\lambda
-(H0: (lt x n)).(le_S_n (S (S x)) (S n) (le_n_S (S (S x)) (S n) (le_n_S (S x)
-n H0)))))) y)).
-(* COMMENTS
-Initial nodes: 103
-END *)
+(H0: (lt x n)).(lt_n_S x n H0)))) y)).
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
theorem insert_eq:
- \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G:
-((S \to Prop))).(((\forall (y: S).((P y) \to ((eq S y x) \to (G y))))) \to
-((P x) \to (G x))))))
+ \forall (S: Type[0]).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall
+(G: ((S \to Prop))).(((\forall (y: S).((P y) \to ((eq S y x) \to (G y)))))
+\to ((P x) \to (G x))))))
\def
- \lambda (S: Set).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda (G:
-((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to (G
-y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).
-(* COMMENTS
-Initial nodes: 45
-END *)
+ \lambda (S: Type[0]).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda
+(G: ((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to
+(G y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).
theorem unintro:
- \forall (A: Set).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall (x:
-A).(P x))) \to (P a))))
+ \forall (A: Type[0]).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall
+(x: A).(P x))) \to (P a))))
\def
- \lambda (A: Set).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda (H:
-((\forall (x: A).(P x)))).(H a)))).
-(* COMMENTS
-Initial nodes: 17
-END *)
+ \lambda (A: Type[0]).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda
+(H: ((\forall (x: A).(P x)))).(H a)))).
theorem xinduction:
- \forall (A: Set).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall (x:
-A).((eq A t x) \to (P x)))) \to (P t))))
+ \forall (A: Type[0]).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall
+(x: A).((eq A t x) \to (P x)))) \to (P t))))
\def
- \lambda (A: Set).(\lambda (t: A).(\lambda (P: ((A \to Prop))).(\lambda (H:
-((\forall (x: A).((eq A t x) \to (P x))))).(H t (refl_equal A t))))).
-(* COMMENTS
-Initial nodes: 31
-END *)
+ \lambda (A: Type[0]).(\lambda (t: A).(\lambda (P: ((A \to Prop))).(\lambda
+(H: ((\forall (x: A).((eq A t x) \to (P x))))).(H t (refl_equal A t))))).
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
-inductive PList: Set \def
+inductive PList: Type[0] \def
| PNil: PList
| PCons: nat \to (nat \to (PList \to PList)).
-definition PConsTail:
- PList \to (nat \to (nat \to PList))
-\def
- let rec PConsTail (hds: PList) on hds: (nat \to (nat \to PList)) \def
-(\lambda (h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow
-(PCons h0 d0 PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0
-h0 d0))]))) in PConsTail.
+let rec PConsTail (hds: PList) on hds: nat \to (nat \to PList) \def \lambda
+(h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow (PCons h0 d0
+PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 h0 d0))])).
-definition Ss:
- PList \to PList
-\def
- let rec Ss (hds: PList) on hds: PList \def (match hds with [PNil \Rightarrow
-PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))]) in Ss.
+let rec Ss (hds: PList) on hds: PList \def match hds with [PNil \Rightarrow
+PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))].
-definition papp:
- PList \to (PList \to PList)
-\def
- let rec papp (a: PList) on a: (PList \to PList) \def (\lambda (b:
-PList).(match a with [PNil \Rightarrow b | (PCons h d a0) \Rightarrow (PCons
-h d (papp a0 b))])) in papp.
+let rec papp (a: PList) on a: PList \to PList \def \lambda (b: PList).(match
+a with [PNil \Rightarrow b | (PCons h d a0) \Rightarrow (PCons h d (papp a0
+b))]).
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/plist/defs.ma".
+include "ground_1/plist/defs.ma".
theorem papp_ss:
\forall (is1: PList).(\forall (is2: PList).(eq PList (papp (Ss is1) (Ss
(Ss (papp p is2)) (\lambda (p0: PList).(eq PList (PCons n (S n0) p0) (PCons n
(S n0) (Ss (papp p is2))))) (refl_equal PList (PCons n (S n0) (Ss (papp p
is2)))) (papp (Ss p) (Ss is2)) (H is2))))))) is1).
-(* COMMENTS
-Initial nodes: 151
-END *)
(* *)
(**************************************************************************)
-include "Legacy-1/theory.ma".
+include "legacy_1/theory.ma".
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/theory.ma".
+include "ground_1/theory.ma".
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/ext/tactics.ma".
+include "ground_1/ext/tactics.ma".
-include "Ground-1/ext/arith.ma".
+include "ground_1/types/props.ma".
-include "Ground-1/types/props.ma".
+include "ground_1/ext/arith.ma".
-include "Ground-1/blt/props.ma".
+include "ground_1/blt/props.ma".
-include "Ground-1/plist/props.ma".
+include "ground_1/plist/props.ma".
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
| and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
| or5_intro3: P3 \to (or5 P0 P1 P2 P3 P4)
| or5_intro4: P4 \to (or5 P0 P1 P2 P3 P4).
-inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
+inductive ex3 (A0: Type[0]) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
Prop): Prop \def
| ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0
P0 P1 P2)))).
-inductive ex4 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to Prop)
-(P3: A0 \to Prop): Prop \def
+inductive ex4 (A0: Type[0]) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
+Prop) (P3: A0 \to Prop): Prop \def
| ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0)
\to (ex4 A0 P0 P1 P2 P3))))).
-inductive ex_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)): Prop \def
+inductive ex_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)): Prop
+\def
| ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1
P0))).
-inductive ex2_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
-(A1 \to Prop)): Prop \def
+inductive ex2_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1:
+A0 \to (A1 \to Prop)): Prop \def
| ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
\to (ex2_2 A0 A1 P0 P1)))).
-inductive ex3_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
-(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
+inductive ex3_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1:
+A0 \to (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
| ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
\to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
-inductive ex4_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
-(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)): Prop
-\def
+inductive ex4_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1:
+A0 \to (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)):
+Prop \def
| ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
\to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
-inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
-Prop))): Prop \def
+inductive ex_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
+(A2 \to Prop))): Prop \def
| ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1
x2) \to (ex_3 A0 A1 A2 P0)))).
-inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
+inductive ex2_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
| ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
-inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to
-Prop))): Prop \def
+inductive ex3_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2
+\to Prop))): Prop \def
| ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1
P2)))))).
-inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to
-Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
+inductive ex4_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2
+\to Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
| ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0
A1 A2 P0 P1 P2 P3))))))).
-inductive ex5_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to
-Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to
+inductive ex5_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2
+\to Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to
Prop))): Prop \def
| ex5_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to ((P4 x0
x1 x2) \to (ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)))))))).
-inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to
-(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0
-\to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
+inductive ex3_4 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (P0:
+A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
+Prop)))) (P2: A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
| ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
(ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
-inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to
-(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0
-\to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2 \to (A3 \to
-Prop)))): Prop \def
+inductive ex4_4 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (P0:
+A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
+Prop)))) (P2: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2
+\to (A3 \to Prop)))): Prop \def
| ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
-inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to
-(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
-(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:
-A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
+inductive ex4_5 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
+Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to
+(A4 \to Prop))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop
+\def
| ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1
P2 P3))))))))).
-inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to
-(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
-(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:
-A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4: A0 \to (A1 \to (A2 \to
-(A3 \to (A4 \to Prop))))): Prop \def
+inductive ex5_5 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
+Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to
+(A4 \to Prop))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4:
+A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
| ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to
(ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
-inductive ex6_6 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set)
-(P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1: A0 \to
-(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2: A0 \to (A1 \to (A2
-\to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to
-(A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
-\to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
-Prop)))))): Prop \def
+inductive ex6_6 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
+Type[0]) (A5: Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
+Prop)))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop))))))
+(P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to
+(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2
+\to (A3 \to (A4 \to (A5 \to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to
+(A4 \to (A5 \to Prop)))))): Prop \def
| ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1
x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5)
\to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2
A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
-inductive ex6_7 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set)
-(A6: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+inductive ex6_7 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
+Type[0]) (A5: Type[0]) (A6: Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4
+\to (A5 \to (A6 \to Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
+(A5 \to (A6 \to Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
+\to (A6 \to Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
+(A6 \to Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6
+\to Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
Prop))))))): Prop \def
| ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2
(* This file was automatically generated: do not edit *********************)
-include "Ground-1/types/defs.ma".
+include "ground_1/types/defs.ma".
theorem ex2_sym:
- \forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to
+ \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to
Prop))).((ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x))) \to (ex2 A
(\lambda (x: A).(Q x)) (\lambda (x: A).(P x))))))
\def
- \lambda (A: Set).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to
+ \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to
Prop))).(\lambda (H: (ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q
x)))).(ex2_ind A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x)) (ex2 A
(\lambda (x: A).(Q x)) (\lambda (x: A).(P x))) (\lambda (x: A).(\lambda (H0:
(P x)).(\lambda (H1: (Q x)).(ex_intro2 A (\lambda (x0: A).(Q x0)) (\lambda
(x0: A).(P x0)) x H1 H0)))) H)))).
-(* COMMENTS
-Initial nodes: 91
-END *)
(* This file was automatically generated: do not edit *********************)
-include "Legacy-1/preamble.ma".
+include "legacy_1/preamble.ma".
-inductive eq (A: Set) (x: A): A \to Prop \def
+inductive eq (A: Type[0]) (x: A): A \to Prop \def
| refl_equal: eq A x x.
inductive True: Prop \def
| or_introl: A \to (or A B)
| or_intror: B \to (or A B).
-inductive ex (A: Set) (P: A \to Prop): Prop \def
+inductive ex (A: Type[0]) (P: A \to Prop): Prop \def
| ex_intro: \forall (x: A).((P x) \to (ex A P)).
-inductive ex2 (A: Set) (P: A \to Prop) (Q: A \to Prop): Prop \def
+inductive ex2 (A: Type[0]) (P: A \to Prop) (Q: A \to Prop): Prop \def
| ex_intro2: \forall (x: A).((P x) \to ((Q x) \to (ex2 A P Q))).
definition not:
\def
\lambda (A: Prop).(A \to False).
-inductive bool: Set \def
+inductive bool: Type[0] \def
| true: bool
| false: bool.
-inductive nat: Set \def
+inductive nat: Type[0] \def
| O: nat
| S: nat \to nat.
\def
\lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
-definition plus:
- nat \to (nat \to nat)
-\def
- let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n
-with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus.
+let rec plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
+[O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
-definition minus:
- nat \to (nat \to nat)
-\def
- let rec minus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n
-with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k)
-| (S l) \Rightarrow (minus k l)])])) in minus.
+let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
+[O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S
+l) \Rightarrow (minus k l)])]).
-inductive Acc (A: Set) (R: A \to (A \to Prop)): A \to Prop \def
+inductive Acc (A: Type[0]) (R: A \to (A \to Prop)): A \to Prop \def
| Acc_intro: \forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to
(Acc A R x)).
definition well_founded:
- \forall (A: Set).(((A \to (A \to Prop))) \to Prop)
+ \forall (A: Type[0]).(((A \to (A \to Prop))) \to Prop)
\def
- \lambda (A: Set).(\lambda (R: ((A \to (A \to Prop)))).(\forall (a: A).(Acc A
-R a))).
+ \lambda (A: Type[0]).(\lambda (R: ((A \to (A \to Prop)))).(\forall (a:
+A).(Acc A R a))).
definition ltof:
- \forall (A: Set).(((A \to nat)) \to (A \to (A \to Prop)))
+ \forall (A: Type[0]).(((A \to nat)) \to (A \to (A \to Prop)))
\def
- \lambda (A: Set).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda (b:
-A).(lt (f a) (f b))))).
+ \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda
+(b: A).(lt (f a) (f b))))).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "legacy_1/coq/defs.ma".
+
+theorem False_rect:
+ \forall (P: Type[0]).(False \to P)
+\def
+ \lambda (P: Type[0]).(\lambda (f: False).(match f in False with [])).
+
+theorem False_ind:
+ \forall (P: Prop).(False \to P)
+\def
+ \lambda (P: Prop).(False_rect P).
+
+theorem land_rect:
+ \forall (A: Prop).(\forall (B: Prop).(\forall (P: Type[0]).(((A \to (B \to
+P))) \to ((land A B) \to P))))
+\def
+ \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Type[0]).(\lambda (f: ((A
+\to (B \to P)))).(\lambda (a: (land A B)).(match a in land with [(conj x x0)
+\Rightarrow (f x x0)]))))).
+
+theorem land_ind:
+ \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to (B \to P)))
+\to ((land A B) \to P))))
+\def
+ \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Prop).(land_rect A B P))).
+
+theorem or_ind:
+ \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to P)) \to
+(((B \to P)) \to ((or A B) \to P)))))
+\def
+ \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Prop).(\lambda (f: ((A \to
+P))).(\lambda (f0: ((B \to P))).(\lambda (o: (or A B)).(match o in or with
+[(or_introl x) \Rightarrow (f x) | (or_intror x) \Rightarrow (f0 x)])))))).
+
+theorem ex_ind:
+ \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (P0:
+Prop).(((\forall (x: A).((P x) \to P0))) \to ((ex A P) \to P0))))
+\def
+ \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (P0:
+Prop).(\lambda (f: ((\forall (x: A).((P x) \to P0)))).(\lambda (e: (ex A
+P)).(match e in ex with [(ex_intro x x0) \Rightarrow (f x x0)]))))).
+
+theorem ex2_ind:
+ \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to
+Prop))).(\forall (P0: Prop).(((\forall (x: A).((P x) \to ((Q x) \to P0))))
+\to ((ex2 A P Q) \to P0)))))
+\def
+ \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to
+Prop))).(\lambda (P0: Prop).(\lambda (f: ((\forall (x: A).((P x) \to ((Q x)
+\to P0))))).(\lambda (e: (ex2 A P Q)).(match e in ex2 with [(ex_intro2 x x0
+x1) \Rightarrow (f x x0 x1)])))))).
+
+theorem eq_rect:
+ \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Type[0]))).((P x)
+\to (\forall (y: A).((eq A x y) \to (P y))))))
+\def
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to
+Type[0]))).(\lambda (f: (P x)).(\lambda (y: A).(\lambda (e: (eq A x
+y)).(match e in eq with [refl_equal \Rightarrow f])))))).
+
+theorem eq_ind:
+ \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
+(\forall (y: A).((eq A x y) \to (P y))))))
+\def
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(eq_rect A
+x P))).
+
+let rec le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall (m:
+nat).((le n m) \to ((P m) \to (P (S m)))))) (n0: nat) (l: le n n0) on l: P n0
+\def match l in le with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (f0 m
+l0 ((le_ind n P f f0) m l0))].
+
+let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to Prop)) (f:
+(\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall
+(y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a
+\def match a0 in Acc with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y:
+A).(\lambda (r: (R y x)).((Acc_ind A R P f) y (a1 y r)))))].
+
(* This file was automatically generated: do not edit *********************)
-include "Legacy-1/coq/defs.ma".
+include "legacy_1/coq/elim.ma".
theorem f_equal:
- \forall (A: Set).(\forall (B: Set).(\forall (f: ((A \to B))).(\forall (x:
-A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
+ \forall (A: Type[0]).(\forall (B: Type[0]).(\forall (f: ((A \to
+B))).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
\def
- \lambda (A: Set).(\lambda (B: Set).(\lambda (f: ((A \to B))).(\lambda (x:
-A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x (\lambda (a: A).(eq B
-(f x) (f a))) (refl_equal B (f x)) y H)))))).
-(* COMMENTS
-Initial nodes: 51
-END *)
+ \lambda (A: Type[0]).(\lambda (B: Type[0]).(\lambda (f: ((A \to
+B))).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x
+(\lambda (a: A).(eq B (f x) (f a))) (refl_equal B (f x)) y H)))))).
theorem f_equal2:
- \forall (A1: Set).(\forall (A2: Set).(\forall (B: Set).(\forall (f: ((A1 \to
-(A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2: A2).(\forall
-(y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2) (f y1
-y2)))))))))))
-\def
- \lambda (A1: Set).(\lambda (A2: Set).(\lambda (B: Set).(\lambda (f: ((A1 \to
-(A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda
-(y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2
-x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 y2)).(eq_ind
-A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B (f x1 x2)) y2
-H0)) y1 H))))))))).
-(* COMMENTS
-Initial nodes: 109
-END *)
+ \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (B: Type[0]).(\forall
+(f: ((A1 \to (A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2:
+A2).(\forall (y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2)
+(f y1 y2)))))))))))
+\def
+ \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (B: Type[0]).(\lambda
+(f: ((A1 \to (A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2:
+A2).(\lambda (y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a:
+A1).((eq A2 x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2
+y2)).(eq_ind A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B
+(f x1 x2)) y2 H0)) y1 H))))))))).
theorem f_equal3:
- \forall (A1: Set).(\forall (A2: Set).(\forall (A3: Set).(\forall (B:
-Set).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1: A1).(\forall
-(y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3: A3).(\forall (y3:
-A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2
-x3) (f y1 y2 y3)))))))))))))))
-\def
- \lambda (A1: Set).(\lambda (A2: Set).(\lambda (A3: Set).(\lambda (B:
-Set).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1: A1).(\lambda
-(y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3: A3).(\lambda (y3:
-A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2 x2 y2)
-\to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3))))) (\lambda (H0: (eq
-A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3) \to (eq B (f x1 x2
-x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 x3 (\lambda (a:
-A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 x3)) y3 H1)) y2
-H0)) y1 H)))))))))))).
-(* COMMENTS
-Initial nodes: 183
-END *)
+ \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (A3: Type[0]).(\forall
+(B: Type[0]).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1:
+A1).(\forall (y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3:
+A3).(\forall (y3: A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3)
+\to (eq B (f x1 x2 x3) (f y1 y2 y3)))))))))))))))
+\def
+ \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (A3: Type[0]).(\lambda
+(B: Type[0]).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1:
+A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3:
+A3).(\lambda (y3: A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a:
+A1).((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3)))))
+(\lambda (H0: (eq A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3)
+\to (eq B (f x1 x2 x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3
+x3 (\lambda (a: A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2
+x3)) y3 H1)) y2 H0)) y1 H)))))))))))).
theorem sym_eq:
- \forall (A: Set).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y
+ \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y
x))))
\def
- \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
y)).(eq_ind A x (\lambda (a: A).(eq A a x)) (refl_equal A x) y H)))).
-(* COMMENTS
-Initial nodes: 39
-END *)
theorem eq_ind_r:
- \forall (A: Set).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
+ \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
(\forall (y: A).((eq A y x) \to (P y))))))
\def
- \lambda (A: Set).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda (H:
-(P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) in
-eq return (\lambda (a: A).(\lambda (_: (eq ? ? a)).(P a))) with [refl_equal
-\Rightarrow H])))))).
-(* COMMENTS
-Initial nodes: 38
-END *)
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda
+(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0)
+in eq with [refl_equal \Rightarrow H])))))).
theorem trans_eq:
- \forall (A: Set).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A x y)
-\to ((eq A y z) \to (eq A x z))))))
+ \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A
+x y) \to ((eq A y z) \to (eq A x z))))))
\def
- \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (z: A).(\lambda
-(H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda (a: A).(eq A x
-a)) H z H0)))))).
-(* COMMENTS
-Initial nodes: 45
-END *)
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (z:
+A).(\lambda (H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda
+(a: A).(eq A x a)) H z H0)))))).
theorem sym_not_eq:
- \forall (A: Set).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to (not
-(eq A y x)))))
+ \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to
+(not (eq A y x)))))
\def
- \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq A x
-y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a y))
-(refl_equal A y) x h2)))))).
-(* COMMENTS
-Initial nodes: 51
-END *)
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq
+A x y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a
+y)) (refl_equal A y) x h2)))))).
theorem nat_double_ind:
\forall (R: ((nat \to (nat \to Prop)))).(((\forall (n: nat).(R O n))) \to
nat).(\lambda (H2: ((\forall (m: nat).(R n0 m)))).(\lambda (m: nat).(nat_ind
(\lambda (n1: nat).(R (S n0) n1)) (H0 n0) (\lambda (n1: nat).(\lambda (_: (R
(S n0) n1)).(H1 n0 n1 (H2 n1)))) m)))) n))))).
-(* COMMENTS
-Initial nodes: 111
-END *)
theorem eq_add_S:
\forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S
m))).(f_equal nat nat pred (S n) (S m) H))).
-(* COMMENTS
-Initial nodes: 33
-END *)
theorem O_S:
\forall (n: nat).(not (eq nat O (S n)))
\def
\lambda (n: nat).(\lambda (H: (eq nat O (S n))).(eq_ind nat (S n) (\lambda
(n0: nat).(IsSucc n0)) I O (sym_eq nat O (S n) H))).
-(* COMMENTS
-Initial nodes: 41
-END *)
theorem not_eq_S:
\forall (n: nat).(\forall (m: nat).((not (eq nat n m)) \to (not (eq nat (S
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda
(H0: (eq nat (S n) (S m))).(H (eq_add_S n m H0))))).
-(* COMMENTS
-Initial nodes: 35
-END *)
theorem pred_Sn:
\forall (m: nat).(eq nat m (pred (S m)))
\def
\lambda (m: nat).(refl_equal nat (pred (S m))).
-(* COMMENTS
-Initial nodes: 11
-END *)
theorem S_pred:
\forall (n: nat).(\forall (m: nat).((lt m n) \to (eq nat n (S (pred n)))))
(\lambda (n0: nat).(eq nat n0 (S (pred n0)))) (refl_equal nat (S (pred (S
m)))) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (_: (eq nat m0
(S (pred m0)))).(refl_equal nat (S (pred (S m0))))))) n H))).
-(* COMMENTS
-Initial nodes: 79
-END *)
theorem le_trans:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((le m p)
m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(le n n0)) H
(\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (le n m0)).(le_S n
m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 57
-END *)
theorem le_trans_S:
\forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(le_trans n (S
n) m (le_S n n (le_n n)) H))).
-(* COMMENTS
-Initial nodes: 33
-END *)
theorem le_n_S:
\forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
(n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
-(* COMMENTS
-Initial nodes: 65
-END *)
theorem le_O_n:
\forall (n: nat).(le O n)
\def
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(le O n0)) (le_n O) (\lambda
(n0: nat).(\lambda (IHn: (le O n0)).(le_S O n0 IHn))) n).
-(* COMMENTS
-Initial nodes: 33
-END *)
theorem le_S_n:
\forall (n: nat).(\forall (m: nat).((le (S n) (S m)) \to (le n m)))
n) (\lambda (n0: nat).(le (pred (S n)) (pred n0))) (le_n n) (\lambda (m0:
nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S
n m0 H0)))) (S m) H))).
-(* COMMENTS
-Initial nodes: 69
-END *)
theorem le_Sn_O:
\forall (n: nat).(not (le (S n) O))
\lambda (n: nat).(\lambda (H: (le (S n) O)).(le_ind (S n) (\lambda (n0:
nat).(IsSucc n0)) I (\lambda (m: nat).(\lambda (_: (le (S n) m)).(\lambda (_:
(IsSucc m)).I))) O H)).
-(* COMMENTS
-Initial nodes: 43
-END *)
theorem le_Sn_n:
\forall (n: nat).(not (le (S n) n))
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(not (le (S n0) n0))) (le_Sn_O
O) (\lambda (n0: nat).(\lambda (IHn: (not (le (S n0) n0))).(\lambda (H: (le
(S (S n0)) (S n0))).(IHn (le_S_n (S n0) n0 H))))) n).
-(* COMMENTS
-Initial nodes: 57
-END *)
theorem le_antisym:
\forall (n: nat).(\forall (m: nat).((le n m) \to ((le m n) \to (eq nat n
\to (eq nat n m0)))).(\lambda (H1: (le (S m0) n)).(False_ind (eq nat n (S
m0)) (let H2 \def (le_trans (S m0) n m0 H1 H) in ((let H3 \def (le_Sn_n m0)
in (\lambda (H4: (le (S m0) m0)).(H3 H4))) H2))))))) m h))).
-(* COMMENTS
-Initial nodes: 119
-END *)
theorem le_n_O_eq:
\forall (n: nat).((le n O) \to (eq nat O n))
\def
\lambda (n: nat).(\lambda (H: (le n O)).(le_antisym O n (le_O_n n) H)).
-(* COMMENTS
-Initial nodes: 19
-END *)
theorem le_elim_rel:
\forall (P: ((nat \to (nat \to Prop)))).(((\forall (p: nat).(P O p))) \to
n0 (le_n n0))) (\lambda (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_:
(P (S n0) m0)).(H0 n0 m0 (le_trans_S n0 m0 H1) (IHn m0 (le_trans_S n0 m0
H1)))))) m Le))))) n)))).
-(* COMMENTS
-Initial nodes: 181
-END *)
theorem lt_n_n:
\forall (n: nat).(not (lt n n))
\def
le_Sn_n.
-(* COMMENTS
-Initial nodes: 1
-END *)
theorem lt_n_S:
\forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_n_S (S n) m
H))).
-(* COMMENTS
-Initial nodes: 19
-END *)
theorem lt_n_Sn:
\forall (n: nat).(lt n (S n))
\def
\lambda (n: nat).(le_n (S n)).
-(* COMMENTS
-Initial nodes: 7
-END *)
theorem lt_S_n:
\forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(le_S_n (S
n) m H))).
-(* COMMENTS
-Initial nodes: 23
-END *)
theorem lt_n_O:
\forall (n: nat).(not (lt n O))
\def
le_Sn_O.
-(* COMMENTS
-Initial nodes: 1
-END *)
theorem lt_trans:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((lt m p)
m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) (le_S
(S n) m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt
n m0)).(le_S (S n) m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 71
-END *)
theorem lt_O_Sn:
\forall (n: nat).(lt O (S n))
\def
\lambda (n: nat).(le_n_S O n (le_O_n n)).
-(* COMMENTS
-Initial nodes: 11
-END *)
theorem lt_le_S:
\forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
\def
\lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
-(* COMMENTS
-Initial nodes: 11
-END *)
theorem le_not_lt:
\forall (n: nat).(\forall (m: nat).((le n m) \to (not (lt m n))))
(n0: nat).(not (lt n0 n))) (lt_n_n n) (\lambda (m0: nat).(\lambda (_: (le n
m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(IHle
(le_trans_S (S m0) n H1)))))) m H))).
-(* COMMENTS
-Initial nodes: 67
-END *)
theorem le_lt_n_Sm:
\forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
-(* COMMENTS
-Initial nodes: 17
-END *)
theorem le_lt_trans:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((lt m p)
m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0))
(le_n_S n m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle:
(lt n m0)).(le_S (S n) m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 69
-END *)
theorem lt_le_trans:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((le m p)
m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(lt n n0)) H
(\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (lt n m0)).(le_S
(S n) m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 59
-END *)
theorem lt_le_weak:
\forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m
H))).
-(* COMMENTS
-Initial nodes: 17
-END *)
theorem lt_n_Sm_le:
\forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m
H))).
-(* COMMENTS
-Initial nodes: 19
-END *)
theorem le_lt_or_eq:
\forall (n: nat).(\forall (m: nat).((le n m) \to (or (lt n m) (eq nat n m))))
(refl_equal nat n)) (\lambda (m0: nat).(\lambda (H0: (le n m0)).(\lambda (_:
(or (lt n m0) (eq nat n m0))).(or_introl (lt n (S m0)) (eq nat n (S m0))
(le_n_S n m0 H0))))) m H))).
-(* COMMENTS
-Initial nodes: 109
-END *)
theorem le_or_lt:
\forall (n: nat).(\forall (m: nat).(or (le n m) (lt m n)))
n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S
n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S
m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
-(* COMMENTS
-Initial nodes: 209
-END *)
theorem plus_n_O:
\forall (n: nat).(eq nat n (plus n O))
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (plus n0 O)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0
O))).(f_equal nat nat S n0 (plus n0 O) H))) n).
-(* COMMENTS
-Initial nodes: 57
-END *)
theorem plus_n_Sm:
\forall (n: nat).(\forall (m: nat).(eq nat (S (plus n m)) (plus n (S m))))
(plus n0 n)) (plus n0 (S n)))) (refl_equal nat (S n)) (\lambda (n0:
nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S n)))).(f_equal nat nat
S (S (plus n0 n)) (plus n0 (S n)) H))) m)).
-(* COMMENTS
-Initial nodes: 85
-END *)
theorem plus_sym:
\forall (n: nat).(\forall (m: nat).(eq nat (plus n m) (plus m n)))
y m) (plus m y))).(eq_ind nat (S (plus m y)) (\lambda (n0: nat).(eq nat (S
(plus y m)) n0)) (f_equal nat nat S (plus y m) (plus m y) H) (plus m (S y))
(plus_n_Sm m y)))) n)).
-(* COMMENTS
-Initial nodes: 111
-END *)
theorem plus_Snm_nSm:
\forall (n: nat).(\forall (m: nat).(eq nat (plus (S n) m) (plus n (S m))))
nat).(eq nat (S n0) (plus n (S m)))) (eq_ind_r nat (plus (S m) n) (\lambda
(n0: nat).(eq nat (S (plus m n)) n0)) (refl_equal nat (plus (S m) n)) (plus n
(S m)) (plus_sym n (S m))) (plus n m) (plus_sym n m))).
-(* COMMENTS
-Initial nodes: 99
-END *)
theorem plus_assoc_l:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus n (plus m
(plus m p)) (\lambda (n0: nat).(\lambda (H: (eq nat (plus n0 (plus m p))
(plus (plus n0 m) p))).(f_equal nat nat S (plus n0 (plus m p)) (plus (plus n0
m) p) H))) n))).
-(* COMMENTS
-Initial nodes: 101
-END *)
theorem plus_assoc_r:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus (plus n
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(sym_eq nat (plus n
(plus m p)) (plus (plus n m) p) (plus_assoc_l n m p)))).
-(* COMMENTS
-Initial nodes: 37
-END *)
theorem simpl_plus_l:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus n m)
nat).(\lambda (H: (eq nat (S (plus n0 m)) (S (plus n0 p)))).(IHn m p (IHn
(plus n0 m) (plus n0 p) (f_equal nat nat (plus n0) (plus n0 m) (plus n0 p)
(eq_add_S (plus n0 m) (plus n0 p) H))))))))) n).
-(* COMMENTS
-Initial nodes: 161
-END *)
theorem minus_n_O:
\forall (n: nat).(eq nat n (minus n O))
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (minus n0 O)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0
O))).(refl_equal nat (S n0)))) n).
-(* COMMENTS
-Initial nodes: 47
-END *)
theorem minus_n_n:
\forall (n: nat).(eq nat O (minus n n))
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat O (minus n0 n0)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0
n0))).IHn)) n).
-(* COMMENTS
-Initial nodes: 41
-END *)
theorem minus_Sn_m:
\forall (n: nat).(\forall (m: nat).((le m n) \to (eq nat (S (minus n m))
(minus p O) (minus_n_O p)))) (\lambda (p: nat).(\lambda (q: nat).(\lambda (_:
(le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match p with [O \Rightarrow
(S q) | (S l) \Rightarrow (minus q l)]))).H0)))) m n Le))).
-(* COMMENTS
-Initial nodes: 111
-END *)
theorem plus_minus:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat n (plus m p))
(n0: nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq
nat p (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(H
(eq_add_S m0 (plus n0 p) H0)))))) m n))).
-(* COMMENTS
-Initial nodes: 199
-END *)
theorem minus_plus:
\forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
\def
\lambda (n: nat).(\lambda (m: nat).(sym_eq nat m (minus (plus n m) n)
(plus_minus (plus n m) n m (refl_equal nat (plus n m))))).
-(* COMMENTS
-Initial nodes: 41
-END *)
theorem le_pred_n:
\forall (n: nat).(le (pred n) n)
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(le (pred n0) n0)) (le_n O)
(\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(le_S (pred (S n0)) n0
(le_n n0)))) n).
-(* COMMENTS
-Initial nodes: 43
-END *)
theorem le_plus_l:
\forall (n: nat).(\forall (m: nat).(le n (plus n m)))
n0 m)))) (\lambda (m: nat).(le_O_n m)) (\lambda (n0: nat).(\lambda (IHn:
((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(le_n_S n0 (plus
n0 m) (IHn m))))) n).
-(* COMMENTS
-Initial nodes: 55
-END *)
theorem le_plus_r:
\forall (n: nat).(\forall (m: nat).(le m (plus n m)))
\lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(le m (plus
n0 m))) (le_n m) (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(le_S m
(plus n0 m) H))) n)).
-(* COMMENTS
-Initial nodes: 47
-END *)
theorem simpl_le_plus_l:
\forall (p: nat).(\forall (n: nat).(\forall (m: nat).((le (plus p n) (plus p
(plus p0 m)) \to (le n m)))))).(\lambda (n: nat).(\lambda (m: nat).(\lambda
(H: (le (S (plus p0 n)) (S (plus p0 m)))).(IHp n m (le_S_n (plus p0 n) (plus
p0 m) H))))))) p).
-(* COMMENTS
-Initial nodes: 113
-END *)
theorem le_plus_trans:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le n
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
m)).(le_trans n m (plus m p) H (le_plus_l m p))))).
-(* COMMENTS
-Initial nodes: 31
-END *)
theorem le_reg_l:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le (plus
(\lambda (p0: nat).(\lambda (IHp: (((le n m) \to (le (plus p0 n) (plus p0
m))))).(\lambda (H: (le n m)).(le_n_S (plus p0 n) (plus p0 m) (IHp H)))))
p))).
-(* COMMENTS
-Initial nodes: 85
-END *)
theorem le_plus_plus:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
nat).(le (plus n p) (plus n0 q))) (le_reg_l p q n H0) (\lambda (m0:
nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus m0 q))).(le_S
(plus n p) (plus m0 q) H2)))) m H)))))).
-(* COMMENTS
-Initial nodes: 91
-END *)
theorem le_plus_minus:
\forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus n (minus m
(\lambda (p: nat).(minus_n_O p)) (\lambda (p: nat).(\lambda (q: nat).(\lambda
(_: (le p q)).(\lambda (H0: (eq nat q (plus p (minus q p)))).(f_equal nat nat
S q (plus p (minus q p)) H0))))) n m Le))).
-(* COMMENTS
-Initial nodes: 91
-END *)
theorem le_plus_minus_r:
\forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat (plus n (minus m
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(sym_eq nat m
(plus n (minus m n)) (le_plus_minus n m H)))).
-(* COMMENTS
-Initial nodes: 33
-END *)
theorem simpl_lt_plus_l:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt (plus p n) (plus p
(\lambda (p0: nat).(\lambda (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n
m)))).(\lambda (H: (lt (S (plus p0 n)) (S (plus p0 m)))).(IHp (le_S_n (S
(plus p0 n)) (plus p0 m) H))))) p))).
-(* COMMENTS
-Initial nodes: 99
-END *)
theorem lt_reg_l:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
(\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to (lt (plus p0 n) (plus p0
m))))).(\lambda (H: (lt n m)).(lt_n_S (plus p0 n) (plus p0 m) (IHp H)))))
p))).
-(* COMMENTS
-Initial nodes: 85
-END *)
theorem lt_reg_r:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
nat).(lt (plus n0 n) (plus n0 m))) H (\lambda (n0: nat).(\lambda (_: (lt
(plus n0 n) (plus n0 m))).(lt_reg_l n m (S n0) H))) p) (plus m p) (plus_sym m
p)) (plus n p) (plus_sym n p))))).
-(* COMMENTS
-Initial nodes: 129
-END *)
theorem le_lt_plus_plus:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(eq_ind_r nat (plus n
(S p)) (\lambda (n0: nat).(le n0 (plus m q))) (le_plus_plus n m (S p) q H H0)
(plus (S n) p) (plus_Snm_nSm n p))))))).
-(* COMMENTS
-Initial nodes: 75
-END *)
theorem lt_le_plus_plus:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(le_plus_plus (S n) m
p q H H0)))))).
-(* COMMENTS
-Initial nodes: 37
-END *)
theorem lt_plus_plus:
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(lt_le_plus_plus n m p q
H (lt_le_weak p q H0))))))).
-(* COMMENTS
-Initial nodes: 39
-END *)
theorem well_founded_ltof:
- \forall (A: Set).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
+ \forall (A: Type[0]).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
\def
- \lambda (A: Set).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n:
+ \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n:
nat).(nat_ind (\lambda (n0: nat).(\forall (a: A).((lt (f a) n0) \to (Acc A
(ltof A f) a)))) (\lambda (a: A).(\lambda (H: (lt (f a) O)).(False_ind (Acc A
(ltof A f) a) (let H0 \def H in ((let H1 \def (lt_n_O (f a)) in (\lambda (H2:
(ltfafb: (lt (f b) (f a))).(IHn b (lt_le_trans (f b) (f a) n0 ltfafb
(lt_n_Sm_le (f a) n0 ltSma)))))))))) n)) in (\lambda (a: A).(H (S (f a)) a
(le_n (S (f a))))))).
-(* COMMENTS
-Initial nodes: 189
-END *)
theorem lt_wf:
well_founded nat lt
\def
well_founded_ltof nat (\lambda (m: nat).m).
-(* COMMENTS
-Initial nodes: 7
-END *)
theorem lt_wf_ind:
\forall (p: nat).(\forall (P: ((nat \to Prop))).(((\forall (n:
(\lambda (n: nat).(P n)) (\lambda (x: nat).(\lambda (_: ((\forall (y:
nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall (y: nat).((lt y
x) \to (P y))))).(H x H1)))) p (lt_wf p)))).
-(* COMMENTS
-Initial nodes: 77
-END *)
(* This file was automatically generated: do not edit *********************)
-include "Legacy-1/coq/defs.ma".
+include "legacy_1/coq/defs.ma".
(* *)
(**************************************************************************)
+include "basics/pts.ma".
+
inductive False: Prop \def .
(* This file was automatically generated: do not edit *********************)
-include "Legacy-1/theory.ma".
+include "legacy_1/theory.ma".
(* This file was automatically generated: do not edit *********************)
-include "Legacy-1/coq/props.ma".
+include "legacy_1/coq/props.ma".
projects / helm.git / commitdiff