matita/matita/contribs/lambdadelta/legacy_1/coq/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 "Legacy-1/coq/defs.ma".
  18
  19 theorem f_equal:
  20  \forall (A: Set).(\forall (B: Set).(\forall (f: ((A \to B))).(\forall (x:
  21 A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
  22 \def
  23  \lambda (A: Set).(\lambda (B: Set).(\lambda (f: ((A \to B))).(\lambda (x:
  24 A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x (\lambda (a: A).(eq B
  25 (f x) (f a))) (refl_equal B (f x)) y H)))))).
  26 (* COMMENTS
  27 Initial nodes: 51
  28 END *)
  29
  30 theorem f_equal2:
  31  \forall (A1: Set).(\forall (A2: Set).(\forall (B: Set).(\forall (f: ((A1 \to
  32 (A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2: A2).(\forall
  33 (y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2) (f y1
  34 y2)))))))))))
  35 \def
  36  \lambda (A1: Set).(\lambda (A2: Set).(\lambda (B: Set).(\lambda (f: ((A1 \to
  37 (A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda
  38 (y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2
  39 x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 y2)).(eq_ind
  40 A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B (f x1 x2)) y2
  41 H0)) y1 H))))))))).
  42 (* COMMENTS
  43 Initial nodes: 109
  44 END *)
  45
  46 theorem f_equal3:
  47  \forall (A1: Set).(\forall (A2: Set).(\forall (A3: Set).(\forall (B:
  48 Set).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1: A1).(\forall
  49 (y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3: A3).(\forall (y3:
  50 A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2
  51 x3) (f y1 y2 y3)))))))))))))))
  52 \def
  53  \lambda (A1: Set).(\lambda (A2: Set).(\lambda (A3: Set).(\lambda (B:
  54 Set).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1: A1).(\lambda
  55 (y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3: A3).(\lambda (y3:
  56 A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2 x2 y2)
  57 \to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3))))) (\lambda (H0: (eq
  58 A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3) \to (eq B (f x1 x2
  59 x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 x3 (\lambda (a:
  60 A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 x3)) y3 H1)) y2
  61 H0)) y1 H)))))))))))).
  62 (* COMMENTS
  63 Initial nodes: 183
  64 END *)
  65
  66 theorem sym_eq:
  67  \forall (A: Set).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y
  68 x))))
  69 \def
  70  \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
  71 y)).(eq_ind A x (\lambda (a: A).(eq A a x)) (refl_equal A x) y H)))).
  72 (* COMMENTS
  73 Initial nodes: 39
  74 END *)
  75
  76 theorem eq_ind_r:
  77  \forall (A: Set).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
  78 (\forall (y: A).((eq A y x) \to (P y))))))
  79 \def
  80  \lambda (A: Set).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda (H:
  81 (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) in
  82 eq return (\lambda (a: A).(\lambda (_: (eq ? ? a)).(P a))) with [refl_equal
  83 \Rightarrow H])))))).
  84 (* COMMENTS
  85 Initial nodes: 38
  86 END *)
  87
  88 theorem trans_eq:
  89  \forall (A: Set).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A x y)
  90 \to ((eq A y z) \to (eq A x z))))))
  91 \def
  92  \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (z: A).(\lambda
  93 (H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda (a: A).(eq A x
  94 a)) H z H0)))))).
  95 (* COMMENTS
  96 Initial nodes: 45
  97 END *)
  98
  99 theorem sym_not_eq:
 100  \forall (A: Set).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to (not
 101 (eq A y x)))))
 102 \def
 103  \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq A x
 104 y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a y))
 105 (refl_equal A y) x h2)))))).
 106 (* COMMENTS
 107 Initial nodes: 51
 108 END *)
 109
 110 theorem nat_double_ind:
 111  \forall (R: ((nat \to (nat \to Prop)))).(((\forall (n: nat).(R O n))) \to
 112 (((\forall (n: nat).(R (S n) O))) \to (((\forall (n: nat).(\forall (m:
 113 nat).((R n m) \to (R (S n) (S m)))))) \to (\forall (n: nat).(\forall (m:
 114 nat).(R n m))))))
 115 \def
 116  \lambda (R: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (n: nat).(R O
 117 n)))).(\lambda (H0: ((\forall (n: nat).(R (S n) O)))).(\lambda (H1: ((\forall
 118 (n: nat).(\forall (m: nat).((R n m) \to (R (S n) (S m))))))).(\lambda (n:
 119 nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(R n0 m))) H (\lambda (n0:
 120 nat).(\lambda (H2: ((\forall (m: nat).(R n0 m)))).(\lambda (m: nat).(nat_ind
 121 (\lambda (n1: nat).(R (S n0) n1)) (H0 n0) (\lambda (n1: nat).(\lambda (_: (R
 122 (S n0) n1)).(H1 n0 n1 (H2 n1)))) m)))) n))))).
 123 (* COMMENTS
 124 Initial nodes: 111
 125 END *)
 126
 127 theorem eq_add_S:
 128  \forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
 129 \def
 130  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S
 131 m))).(f_equal nat nat pred (S n) (S m) H))).
 132 (* COMMENTS
 133 Initial nodes: 33
 134 END *)
 135
 136 theorem O_S:
 137  \forall (n: nat).(not (eq nat O (S n)))
 138 \def
 139  \lambda (n: nat).(\lambda (H: (eq nat O (S n))).(eq_ind nat (S n) (\lambda
 140 (n0: nat).(IsSucc n0)) I O (sym_eq nat O (S n) H))).
 141 (* COMMENTS
 142 Initial nodes: 41
 143 END *)
 144
 145 theorem not_eq_S:
 146  \forall (n: nat).(\forall (m: nat).((not (eq nat n m)) \to (not (eq nat (S
 147 n) (S m)))))
 148 \def
 149  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda
 150 (H0: (eq nat (S n) (S m))).(H (eq_add_S n m H0))))).
 151 (* COMMENTS
 152 Initial nodes: 35
 153 END *)
 154
 155 theorem pred_Sn:
 156  \forall (m: nat).(eq nat m (pred (S m)))
 157 \def
 158  \lambda (m: nat).(refl_equal nat (pred (S m))).
 159 (* COMMENTS
 160 Initial nodes: 11
 161 END *)
 162
 163 theorem S_pred:
 164  \forall (n: nat).(\forall (m: nat).((lt m n) \to (eq nat n (S (pred n)))))
 165 \def
 166  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt m n)).(le_ind (S m)
 167 (\lambda (n0: nat).(eq nat n0 (S (pred n0)))) (refl_equal nat (S (pred (S
 168 m)))) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (_: (eq nat m0
 169 (S (pred m0)))).(refl_equal nat (S (pred (S m0))))))) n H))).
 170 (* COMMENTS
 171 Initial nodes: 79
 172 END *)
 173
 174 theorem le_trans:
 175  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((le m p)
 176 \to (le n p)))))
 177 \def
 178  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 179 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(le n n0)) H
 180 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (le n m0)).(le_S n
 181 m0 IHle)))) p H0))))).
 182 (* COMMENTS
 183 Initial nodes: 57
 184 END *)
 185
 186 theorem le_trans_S:
 187  \forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
 188 \def
 189  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(le_trans n (S
 190 n) m (le_S n n (le_n n)) H))).
 191 (* COMMENTS
 192 Initial nodes: 33
 193 END *)
 194
 195 theorem le_n_S:
 196  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
 197 \def
 198  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
 199 (n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
 200 n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
 201 (* COMMENTS
 202 Initial nodes: 65
 203 END *)
 204
 205 theorem le_O_n:
 206  \forall (n: nat).(le O n)
 207 \def
 208  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le O n0)) (le_n O) (\lambda
 209 (n0: nat).(\lambda (IHn: (le O n0)).(le_S O n0 IHn))) n).
 210 (* COMMENTS
 211 Initial nodes: 33
 212 END *)
 213
 214 theorem le_S_n:
 215  \forall (n: nat).(\forall (m: nat).((le (S n) (S m)) \to (le n m)))
 216 \def
 217  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) (S m))).(le_ind (S
 218 n) (\lambda (n0: nat).(le (pred (S n)) (pred n0))) (le_n n) (\lambda (m0:
 219 nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S
 220 n m0 H0)))) (S m) H))).
 221 (* COMMENTS
 222 Initial nodes: 69
 223 END *)
 224
 225 theorem le_Sn_O:
 226  \forall (n: nat).(not (le (S n) O))
 227 \def
 228  \lambda (n: nat).(\lambda (H: (le (S n) O)).(le_ind (S n) (\lambda (n0:
 229 nat).(IsSucc n0)) I (\lambda (m: nat).(\lambda (_: (le (S n) m)).(\lambda (_:
 230 (IsSucc m)).I))) O H)).
 231 (* COMMENTS
 232 Initial nodes: 43
 233 END *)
 234
 235 theorem le_Sn_n:
 236  \forall (n: nat).(not (le (S n) n))
 237 \def
 238  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(not (le (S n0) n0))) (le_Sn_O
 239 O) (\lambda (n0: nat).(\lambda (IHn: (not (le (S n0) n0))).(\lambda (H: (le
 240 (S (S n0)) (S n0))).(IHn (le_S_n (S n0) n0 H))))) n).
 241 (* COMMENTS
 242 Initial nodes: 57
 243 END *)
 244
 245 theorem le_antisym:
 246  \forall (n: nat).(\forall (m: nat).((le n m) \to ((le m n) \to (eq nat n
 247 m))))
 248 \def
 249  \lambda (n: nat).(\lambda (m: nat).(\lambda (h: (le n m)).(le_ind n (\lambda
 250 (n0: nat).((le n0 n) \to (eq nat n n0))) (\lambda (_: (le n n)).(refl_equal
 251 nat n)) (\lambda (m0: nat).(\lambda (H: (le n m0)).(\lambda (_: (((le m0 n)
 252 \to (eq nat n m0)))).(\lambda (H1: (le (S m0) n)).(False_ind (eq nat n (S
 253 m0)) (let H2 \def (le_trans (S m0) n m0 H1 H) in ((let H3 \def (le_Sn_n m0)
 254 in (\lambda (H4: (le (S m0) m0)).(H3 H4))) H2))))))) m h))).
 255 (* COMMENTS
 256 Initial nodes: 119
 257 END *)
 258
 259 theorem le_n_O_eq:
 260  \forall (n: nat).((le n O) \to (eq nat O n))
 261 \def
 262  \lambda (n: nat).(\lambda (H: (le n O)).(le_antisym O n (le_O_n n) H)).
 263 (* COMMENTS
 264 Initial nodes: 19
 265 END *)
 266
 267 theorem le_elim_rel:
 268  \forall (P: ((nat \to (nat \to Prop)))).(((\forall (p: nat).(P O p))) \to
 269 (((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p q) \to (P (S p) (S
 270 q))))))) \to (\forall (n: nat).(\forall (m: nat).((le n m) \to (P n m))))))
 271 \def
 272  \lambda (P: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (p: nat).(P O
 273 p)))).(\lambda (H0: ((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p
 274 q) \to (P (S p) (S q)))))))).(\lambda (n: nat).(nat_ind (\lambda (n0:
 275 nat).(\forall (m: nat).((le n0 m) \to (P n0 m)))) (\lambda (m: nat).(\lambda
 276 (_: (le O m)).(H m))) (\lambda (n0: nat).(\lambda (IHn: ((\forall (m:
 277 nat).((le n0 m) \to (P n0 m))))).(\lambda (m: nat).(\lambda (Le: (le (S n0)
 278 m)).(le_ind (S n0) (\lambda (n1: nat).(P (S n0) n1)) (H0 n0 n0 (le_n n0) (IHn
 279 n0 (le_n n0))) (\lambda (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_:
 280 (P (S n0) m0)).(H0 n0 m0 (le_trans_S n0 m0 H1) (IHn m0 (le_trans_S n0 m0
 281 H1)))))) m Le))))) n)))).
 282 (* COMMENTS
 283 Initial nodes: 181
 284 END *)
 285
 286 theorem lt_n_n:
 287  \forall (n: nat).(not (lt n n))
 288 \def
 289  le_Sn_n.
 290 (* COMMENTS
 291 Initial nodes: 1
 292 END *)
 293
 294 theorem lt_n_S:
 295  \forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
 296 \def
 297  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_n_S (S n) m
 298 H))).
 299 (* COMMENTS
 300 Initial nodes: 19
 301 END *)
 302
 303 theorem lt_n_Sn:
 304  \forall (n: nat).(lt n (S n))
 305 \def
 306  \lambda (n: nat).(le_n (S n)).
 307 (* COMMENTS
 308 Initial nodes: 7
 309 END *)
 310
 311 theorem lt_S_n:
 312  \forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
 313 \def
 314  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(le_S_n (S
 315 n) m H))).
 316 (* COMMENTS
 317 Initial nodes: 23
 318 END *)
 319
 320 theorem lt_n_O:
 321  \forall (n: nat).(not (lt n O))
 322 \def
 323  le_Sn_O.
 324 (* COMMENTS
 325 Initial nodes: 1
 326 END *)
 327
 328 theorem lt_trans:
 329  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((lt m p)
 330 \to (lt n p)))))
 331 \def
 332  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 333 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) (le_S
 334 (S n) m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt
 335 n m0)).(le_S (S n) m0 IHle)))) p H0))))).
 336 (* COMMENTS
 337 Initial nodes: 71
 338 END *)
 339
 340 theorem lt_O_Sn:
 341  \forall (n: nat).(lt O (S n))
 342 \def
 343  \lambda (n: nat).(le_n_S O n (le_O_n n)).
 344 (* COMMENTS
 345 Initial nodes: 11
 346 END *)
 347
 348 theorem lt_le_S:
 349  \forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
 350 \def
 351  \lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
 352 (* COMMENTS
 353 Initial nodes: 11
 354 END *)
 355
 356 theorem le_not_lt:
 357  \forall (n: nat).(\forall (m: nat).((le n m) \to (not (lt m n))))
 358 \def
 359  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
 360 (n0: nat).(not (lt n0 n))) (lt_n_n n) (\lambda (m0: nat).(\lambda (_: (le n
 361 m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(IHle
 362 (le_trans_S (S m0) n H1)))))) m H))).
 363 (* COMMENTS
 364 Initial nodes: 67
 365 END *)
 366
 367 theorem le_lt_n_Sm:
 368  \forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
 369 \def
 370  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
 371 (* COMMENTS
 372 Initial nodes: 17
 373 END *)
 374
 375 theorem le_lt_trans:
 376  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((lt m p)
 377 \to (lt n p)))))
 378 \def
 379  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 380 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0))
 381 (le_n_S n m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle:
 382 (lt n m0)).(le_S (S n) m0 IHle)))) p H0))))).
 383 (* COMMENTS
 384 Initial nodes: 69
 385 END *)
 386
 387 theorem lt_le_trans:
 388  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((le m p)
 389 \to (lt n p)))))
 390 \def
 391  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 392 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(lt n n0)) H
 393 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (lt n m0)).(le_S
 394 (S n) m0 IHle)))) p H0))))).
 395 (* COMMENTS
 396 Initial nodes: 59
 397 END *)
 398
 399 theorem lt_le_weak:
 400  \forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
 401 \def
 402  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m
 403 H))).
 404 (* COMMENTS
 405 Initial nodes: 17
 406 END *)
 407
 408 theorem lt_n_Sm_le:
 409  \forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
 410 \def
 411  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m
 412 H))).
 413 (* COMMENTS
 414 Initial nodes: 19
 415 END *)
 416
 417 theorem le_lt_or_eq:
 418  \forall (n: nat).(\forall (m: nat).((le n m) \to (or (lt n m) (eq nat n m))))
 419 \def
 420  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
 421 (n0: nat).(or (lt n n0) (eq nat n n0))) (or_intror (lt n n) (eq nat n n)
 422 (refl_equal nat n)) (\lambda (m0: nat).(\lambda (H0: (le n m0)).(\lambda (_:
 423 (or (lt n m0) (eq nat n m0))).(or_introl (lt n (S m0)) (eq nat n (S m0))
 424 (le_n_S n m0 H0))))) m H))).
 425 (* COMMENTS
 426 Initial nodes: 109
 427 END *)
 428
 429 theorem le_or_lt:
 430  \forall (n: nat).(\forall (m: nat).(or (le n m) (lt m n)))
 431 \def
 432  \lambda (n: nat).(\lambda (m: nat).(nat_double_ind (\lambda (n0:
 433 nat).(\lambda (n1: nat).(or (le n0 n1) (lt n1 n0)))) (\lambda (n0:
 434 nat).(or_introl (le O n0) (lt n0 O) (le_O_n n0))) (\lambda (n0:
 435 nat).(or_intror (le (S n0) O) (lt O (S n0)) (lt_le_S O (S n0) (lt_O_Sn n0))))
 436 (\lambda (n0: nat).(\lambda (m0: nat).(\lambda (H: (or (le n0 m0) (lt m0
 437 n0))).(or_ind (le n0 m0) (lt m0 n0) (or (le (S n0) (S m0)) (lt (S m0) (S
 438 n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S
 439 n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S
 440 m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
 441 (* COMMENTS
 442 Initial nodes: 209
 443 END *)
 444
 445 theorem plus_n_O:
 446  \forall (n: nat).(eq nat n (plus n O))
 447 \def
 448  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (plus n0 O)))
 449 (refl_equal nat O) (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0
 450 O))).(f_equal nat nat S n0 (plus n0 O) H))) n).
 451 (* COMMENTS
 452 Initial nodes: 57
 453 END *)
 454
 455 theorem plus_n_Sm:
 456  \forall (n: nat).(\forall (m: nat).(eq nat (S (plus n m)) (plus n (S m))))
 457 \def
 458  \lambda (m: nat).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (S
 459 (plus n0 n)) (plus n0 (S n)))) (refl_equal nat (S n)) (\lambda (n0:
 460 nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S n)))).(f_equal nat nat
 461 S (S (plus n0 n)) (plus n0 (S n)) H))) m)).
 462 (* COMMENTS
 463 Initial nodes: 85
 464 END *)
 465
 466 theorem plus_sym:
 467  \forall (n: nat).(\forall (m: nat).(eq nat (plus n m) (plus m n)))
 468 \def
 469  \lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(eq nat (plus
 470 n0 m) (plus m n0))) (plus_n_O m) (\lambda (y: nat).(\lambda (H: (eq nat (plus
 471 y m) (plus m y))).(eq_ind nat (S (plus m y)) (\lambda (n0: nat).(eq nat (S
 472 (plus y m)) n0)) (f_equal nat nat S (plus y m) (plus m y) H) (plus m (S y))
 473 (plus_n_Sm m y)))) n)).
 474 (* COMMENTS
 475 Initial nodes: 111
 476 END *)
 477
 478 theorem plus_Snm_nSm:
 479  \forall (n: nat).(\forall (m: nat).(eq nat (plus (S n) m) (plus n (S m))))
 480 \def
 481  \lambda (n: nat).(\lambda (m: nat).(eq_ind_r nat (plus m n) (\lambda (n0:
 482 nat).(eq nat (S n0) (plus n (S m)))) (eq_ind_r nat (plus (S m) n) (\lambda
 483 (n0: nat).(eq nat (S (plus m n)) n0)) (refl_equal nat (plus (S m) n)) (plus n
 484 (S m)) (plus_sym n (S m))) (plus n m) (plus_sym n m))).
 485 (* COMMENTS
 486 Initial nodes: 99
 487 END *)
 488
 489 theorem plus_assoc_l:
 490  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus n (plus m
 491 p)) (plus (plus n m) p))))
 492 \def
 493  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 494 nat).(eq nat (plus n0 (plus m p)) (plus (plus n0 m) p))) (refl_equal nat
 495 (plus m p)) (\lambda (n0: nat).(\lambda (H: (eq nat (plus n0 (plus m p))
 496 (plus (plus n0 m) p))).(f_equal nat nat S (plus n0 (plus m p)) (plus (plus n0
 497 m) p) H))) n))).
 498 (* COMMENTS
 499 Initial nodes: 101
 500 END *)
 501
 502 theorem plus_assoc_r:
 503  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus (plus n
 504 m) p) (plus n (plus m p)))))
 505 \def
 506  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(sym_eq nat (plus n
 507 (plus m p)) (plus (plus n m) p) (plus_assoc_l n m p)))).
 508 (* COMMENTS
 509 Initial nodes: 37
 510 END *)
 511
 512 theorem simpl_plus_l:
 513  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus n m)
 514 (plus n p)) \to (eq nat m p))))
 515 \def
 516  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(\forall (p:
 517 nat).((eq nat (plus n0 m) (plus n0 p)) \to (eq nat m p))))) (\lambda (m:
 518 nat).(\lambda (p: nat).(\lambda (H: (eq nat m p)).H))) (\lambda (n0:
 519 nat).(\lambda (IHn: ((\forall (m: nat).(\forall (p: nat).((eq nat (plus n0 m)
 520 (plus n0 p)) \to (eq nat m p)))))).(\lambda (m: nat).(\lambda (p:
 521 nat).(\lambda (H: (eq nat (S (plus n0 m)) (S (plus n0 p)))).(IHn m p (IHn
 522 (plus n0 m) (plus n0 p) (f_equal nat nat (plus n0) (plus n0 m) (plus n0 p)
 523 (eq_add_S (plus n0 m) (plus n0 p) H))))))))) n).
 524 (* COMMENTS
 525 Initial nodes: 161
 526 END *)
 527
 528 theorem minus_n_O:
 529  \forall (n: nat).(eq nat n (minus n O))
 530 \def
 531  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (minus n0 O)))
 532 (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0
 533 O))).(refl_equal nat (S n0)))) n).
 534 (* COMMENTS
 535 Initial nodes: 47
 536 END *)
 537
 538 theorem minus_n_n:
 539  \forall (n: nat).(eq nat O (minus n n))
 540 \def
 541  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat O (minus n0 n0)))
 542 (refl_equal nat O) (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0
 543 n0))).IHn)) n).
 544 (* COMMENTS
 545 Initial nodes: 41
 546 END *)
 547
 548 theorem minus_Sn_m:
 549  \forall (n: nat).(\forall (m: nat).((le m n) \to (eq nat (S (minus n m))
 550 (minus (S n) m))))
 551 \def
 552  \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le m n)).(le_elim_rel
 553 (\lambda (n0: nat).(\lambda (n1: nat).(eq nat (S (minus n1 n0)) (minus (S n1)
 554 n0)))) (\lambda (p: nat).(f_equal nat nat S (minus p O) p (sym_eq nat p
 555 (minus p O) (minus_n_O p)))) (\lambda (p: nat).(\lambda (q: nat).(\lambda (_:
 556 (le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match p with [O \Rightarrow
 557 (S q) | (S l) \Rightarrow (minus q l)]))).H0)))) m n Le))).
 558 (* COMMENTS
 559 Initial nodes: 111
 560 END *)
 561
 562 theorem plus_minus:
 563  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat n (plus m p))
 564 \to (eq nat p (minus n m)))))
 565 \def
 566  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_double_ind
 567 (\lambda (n0: nat).(\lambda (n1: nat).((eq nat n1 (plus n0 p)) \to (eq nat p
 568 (minus n1 n0))))) (\lambda (n0: nat).(\lambda (H: (eq nat n0 p)).(eq_ind nat
 569 n0 (\lambda (n1: nat).(eq nat p n1)) (sym_eq nat n0 p H) (minus n0 O)
 570 (minus_n_O n0)))) (\lambda (n0: nat).(\lambda (H: (eq nat O (S (plus n0
 571 p)))).(False_ind (eq nat p O) (let H0 \def H in ((let H1 \def (O_S (plus n0
 572 p)) in (\lambda (H2: (eq nat O (S (plus n0 p)))).(H1 H2))) H0))))) (\lambda
 573 (n0: nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq
 574 nat p (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(H
 575 (eq_add_S m0 (plus n0 p) H0)))))) m n))).
 576 (* COMMENTS
 577 Initial nodes: 199
 578 END *)
 579
 580 theorem minus_plus:
 581  \forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
 582 \def
 583  \lambda (n: nat).(\lambda (m: nat).(sym_eq nat m (minus (plus n m) n)
 584 (plus_minus (plus n m) n m (refl_equal nat (plus n m))))).
 585 (* COMMENTS
 586 Initial nodes: 41
 587 END *)
 588
 589 theorem le_pred_n:
 590  \forall (n: nat).(le (pred n) n)
 591 \def
 592  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le (pred n0) n0)) (le_n O)
 593 (\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(le_S (pred (S n0)) n0
 594 (le_n n0)))) n).
 595 (* COMMENTS
 596 Initial nodes: 43
 597 END *)
 598
 599 theorem le_plus_l:
 600  \forall (n: nat).(\forall (m: nat).(le n (plus n m)))
 601 \def
 602  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(le n0 (plus
 603 n0 m)))) (\lambda (m: nat).(le_O_n m)) (\lambda (n0: nat).(\lambda (IHn:
 604 ((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(le_n_S n0 (plus
 605 n0 m) (IHn m))))) n).
 606 (* COMMENTS
 607 Initial nodes: 55
 608 END *)
 609
 610 theorem le_plus_r:
 611  \forall (n: nat).(\forall (m: nat).(le m (plus n m)))
 612 \def
 613  \lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(le m (plus
 614 n0 m))) (le_n m) (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(le_S m
 615 (plus n0 m) H))) n)).
 616 (* COMMENTS
 617 Initial nodes: 47
 618 END *)
 619
 620 theorem simpl_le_plus_l:
 621  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((le (plus p n) (plus p
 622 m)) \to (le n m))))
 623 \def
 624  \lambda (p: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (m:
 625 nat).((le (plus n n0) (plus n m)) \to (le n0 m))))) (\lambda (n:
 626 nat).(\lambda (m: nat).(\lambda (H: (le n m)).H))) (\lambda (p0:
 627 nat).(\lambda (IHp: ((\forall (n: nat).(\forall (m: nat).((le (plus p0 n)
 628 (plus p0 m)) \to (le n m)))))).(\lambda (n: nat).(\lambda (m: nat).(\lambda
 629 (H: (le (S (plus p0 n)) (S (plus p0 m)))).(IHp n m (le_S_n (plus p0 n) (plus
 630 p0 m) H))))))) p).
 631 (* COMMENTS
 632 Initial nodes: 113
 633 END *)
 634
 635 theorem le_plus_trans:
 636  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le n
 637 (plus m p)))))
 638 \def
 639  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 640 m)).(le_trans n m (plus m p) H (le_plus_l m p))))).
 641 (* COMMENTS
 642 Initial nodes: 31
 643 END *)
 644
 645 theorem le_reg_l:
 646  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le (plus
 647 p n) (plus p m)))))
 648 \def
 649  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 650 nat).((le n m) \to (le (plus n0 n) (plus n0 m)))) (\lambda (H: (le n m)).H)
 651 (\lambda (p0: nat).(\lambda (IHp: (((le n m) \to (le (plus p0 n) (plus p0
 652 m))))).(\lambda (H: (le n m)).(le_n_S (plus p0 n) (plus p0 m) (IHp H)))))
 653 p))).
 654 (* COMMENTS
 655 Initial nodes: 85
 656 END *)
 657
 658 theorem le_plus_plus:
 659  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
 660 n m) \to ((le p q) \to (le (plus n p) (plus m q)))))))
 661 \def
 662  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 663 nat).(\lambda (H: (le n m)).(\lambda (H0: (le p q)).(le_ind n (\lambda (n0:
 664 nat).(le (plus n p) (plus n0 q))) (le_reg_l p q n H0) (\lambda (m0:
 665 nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus m0 q))).(le_S
 666 (plus n p) (plus m0 q) H2)))) m H)))))).
 667 (* COMMENTS
 668 Initial nodes: 91
 669 END *)
 670
 671 theorem le_plus_minus:
 672  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus n (minus m
 673 n)))))
 674 \def
 675  \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le n m)).(le_elim_rel
 676 (\lambda (n0: nat).(\lambda (n1: nat).(eq nat n1 (plus n0 (minus n1 n0)))))
 677 (\lambda (p: nat).(minus_n_O p)) (\lambda (p: nat).(\lambda (q: nat).(\lambda
 678 (_: (le p q)).(\lambda (H0: (eq nat q (plus p (minus q p)))).(f_equal nat nat
 679 S q (plus p (minus q p)) H0))))) n m Le))).
 680 (* COMMENTS
 681 Initial nodes: 91
 682 END *)
 683
 684 theorem le_plus_minus_r:
 685  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat (plus n (minus m
 686 n)) m)))
 687 \def
 688  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(sym_eq nat m
 689 (plus n (minus m n)) (le_plus_minus n m H)))).
 690 (* COMMENTS
 691 Initial nodes: 33
 692 END *)
 693
 694 theorem simpl_lt_plus_l:
 695  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt (plus p n) (plus p
 696 m)) \to (lt n m))))
 697 \def
 698  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 699 nat).((lt (plus n0 n) (plus n0 m)) \to (lt n m))) (\lambda (H: (lt n m)).H)
 700 (\lambda (p0: nat).(\lambda (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n
 701 m)))).(\lambda (H: (lt (S (plus p0 n)) (S (plus p0 m)))).(IHp (le_S_n (S
 702 (plus p0 n)) (plus p0 m) H))))) p))).
 703 (* COMMENTS
 704 Initial nodes: 99
 705 END *)
 706
 707 theorem lt_reg_l:
 708  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
 709 p n) (plus p m)))))
 710 \def
 711  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 712 nat).((lt n m) \to (lt (plus n0 n) (plus n0 m)))) (\lambda (H: (lt n m)).H)
 713 (\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to (lt (plus p0 n) (plus p0
 714 m))))).(\lambda (H: (lt n m)).(lt_n_S (plus p0 n) (plus p0 m) (IHp H)))))
 715 p))).
 716 (* COMMENTS
 717 Initial nodes: 85
 718 END *)
 719
 720 theorem lt_reg_r:
 721  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
 722 n p) (plus m p)))))
 723 \def
 724  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 725 m)).(eq_ind_r nat (plus p n) (\lambda (n0: nat).(lt n0 (plus m p))) (eq_ind_r
 726 nat (plus p m) (\lambda (n0: nat).(lt (plus p n) n0)) (nat_ind (\lambda (n0:
 727 nat).(lt (plus n0 n) (plus n0 m))) H (\lambda (n0: nat).(\lambda (_: (lt
 728 (plus n0 n) (plus n0 m))).(lt_reg_l n m (S n0) H))) p) (plus m p) (plus_sym m
 729 p)) (plus n p) (plus_sym n p))))).
 730 (* COMMENTS
 731 Initial nodes: 129
 732 END *)
 733
 734 theorem le_lt_plus_plus:
 735  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
 736 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
 737 \def
 738  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 739 nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(eq_ind_r nat (plus n
 740 (S p)) (\lambda (n0: nat).(le n0 (plus m q))) (le_plus_plus n m (S p) q H H0)
 741 (plus (S n) p) (plus_Snm_nSm n p))))))).
 742 (* COMMENTS
 743 Initial nodes: 75
 744 END *)
 745
 746 theorem lt_le_plus_plus:
 747  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
 748 n m) \to ((le p q) \to (lt (plus n p) (plus m q)))))))
 749 \def
 750  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 751 nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(le_plus_plus (S n) m
 752 p q H H0)))))).
 753 (* COMMENTS
 754 Initial nodes: 37
 755 END *)
 756
 757 theorem lt_plus_plus:
 758  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
 759 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
 760 \def
 761  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 762 nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(lt_le_plus_plus n m p q
 763 H (lt_le_weak p q H0))))))).
 764 (* COMMENTS
 765 Initial nodes: 39
 766 END *)
 767
 768 theorem well_founded_ltof:
 769  \forall (A: Set).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
 770 \def
 771  \lambda (A: Set).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n:
 772 nat).(nat_ind (\lambda (n0: nat).(\forall (a: A).((lt (f a) n0) \to (Acc A
 773 (ltof A f) a)))) (\lambda (a: A).(\lambda (H: (lt (f a) O)).(False_ind (Acc A
 774 (ltof A f) a) (let H0 \def H in ((let H1 \def (lt_n_O (f a)) in (\lambda (H2:
 775 (lt (f a) O)).(H1 H2))) H0))))) (\lambda (n0: nat).(\lambda (IHn: ((\forall
 776 (a: A).((lt (f a) n0) \to (Acc A (ltof A f) a))))).(\lambda (a: A).(\lambda
 777 (ltSma: (lt (f a) (S n0))).(Acc_intro A (ltof A f) a (\lambda (b: A).(\lambda
 778 (ltfafb: (lt (f b) (f a))).(IHn b (lt_le_trans (f b) (f a) n0 ltfafb
 779 (lt_n_Sm_le (f a) n0 ltSma)))))))))) n)) in (\lambda (a: A).(H (S (f a)) a
 780 (le_n (S (f a))))))).
 781 (* COMMENTS
 782 Initial nodes: 189
 783 END *)
 784
 785 theorem lt_wf:
 786  well_founded nat lt
 787 \def
 788  well_founded_ltof nat (\lambda (m: nat).m).
 789 (* COMMENTS
 790 Initial nodes: 7
 791 END *)
 792
 793 theorem lt_wf_ind:
 794  \forall (p: nat).(\forall (P: ((nat \to Prop))).(((\forall (n:
 795 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n)))) \to (P p)))
 796 \def
 797  \lambda (p: nat).(\lambda (P: ((nat \to Prop))).(\lambda (H: ((\forall (n:
 798 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n))))).(Acc_ind nat lt
 799 (\lambda (n: nat).(P n)) (\lambda (x: nat).(\lambda (_: ((\forall (y:
 800 nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall (y: nat).((lt y
 801 x) \to (P y))))).(H x H1)))) p (lt_wf p)))).
 802 (* COMMENTS
 803 Initial nodes: 77
 804 END *)
 805