helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc.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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc".
  18
  19 include "leq/defs.ma".
  20
  21 include "aplus/props.ma".
  22
  23 theorem asucc_repl:
  24  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (leq g
  25 (asucc g a1) (asucc g a2)))))
  26 \def
  27  \lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leq g a1
  28 a2)).(leq_ind g (\lambda (a: A).(\lambda (a0: A).(leq g (asucc g a) (asucc g
  29 a0)))) (\lambda (h1: nat).(\lambda (h2: nat).(\lambda (n1: nat).(\lambda (n2:
  30 nat).(\lambda (k: nat).(\lambda (H0: (eq A (aplus g (ASort h1 n1) k) (aplus g
  31 (ASort h2 n2) k))).((match h1 in nat return (\lambda (n: nat).((eq A (aplus g
  32 (ASort n n1) k) (aplus g (ASort h2 n2) k)) \to (leq g (match n with [O
  33 \Rightarrow (ASort O (next g n1)) | (S h) \Rightarrow (ASort h n1)]) (match
  34 h2 with [O \Rightarrow (ASort O (next g n2)) | (S h) \Rightarrow (ASort h
  35 n2)])))) with [O \Rightarrow (\lambda (H1: (eq A (aplus g (ASort O n1) k)
  36 (aplus g (ASort h2 n2) k))).((match h2 in nat return (\lambda (n: nat).((eq A
  37 (aplus g (ASort O n1) k) (aplus g (ASort n n2) k)) \to (leq g (ASort O (next
  38 g n1)) (match n with [O \Rightarrow (ASort O (next g n2)) | (S h) \Rightarrow
  39 (ASort h n2)])))) with [O \Rightarrow (\lambda (H2: (eq A (aplus g (ASort O
  40 n1) k) (aplus g (ASort O n2) k))).(leq_sort g O O (next g n1) (next g n2) k
  41 (eq_ind A (aplus g (ASort O n1) (S k)) (\lambda (a: A).(eq A a (aplus g
  42 (ASort O (next g n2)) k))) (eq_ind A (aplus g (ASort O n2) (S k)) (\lambda
  43 (a: A).(eq A (aplus g (ASort O n1) (S k)) a)) (eq_ind_r A (aplus g (ASort O
  44 n2) k) (\lambda (a: A).(eq A (asucc g a) (asucc g (aplus g (ASort O n2) k))))
  45 (refl_equal A (asucc g (aplus g (ASort O n2) k))) (aplus g (ASort O n1) k)
  46 H2) (aplus g (ASort O (next g n2)) k) (aplus_sort_O_S_simpl g n2 k)) (aplus g
  47 (ASort O (next g n1)) k) (aplus_sort_O_S_simpl g n1 k)))) | (S n) \Rightarrow
  48 (\lambda (H2: (eq A (aplus g (ASort O n1) k) (aplus g (ASort (S n) n2)
  49 k))).(leq_sort g O n (next g n1) n2 k (eq_ind A (aplus g (ASort O n1) (S k))
  50 (\lambda (a: A).(eq A a (aplus g (ASort n n2) k))) (eq_ind A (aplus g (ASort
  51 (S n) n2) (S k)) (\lambda (a: A).(eq A (aplus g (ASort O n1) (S k)) a))
  52 (eq_ind_r A (aplus g (ASort (S n) n2) k) (\lambda (a: A).(eq A (asucc g a)
  53 (asucc g (aplus g (ASort (S n) n2) k)))) (refl_equal A (asucc g (aplus g
  54 (ASort (S n) n2) k))) (aplus g (ASort O n1) k) H2) (aplus g (ASort n n2) k)
  55 (aplus_sort_S_S_simpl g n2 n k)) (aplus g (ASort O (next g n1)) k)
  56 (aplus_sort_O_S_simpl g n1 k))))]) H1)) | (S n) \Rightarrow (\lambda (H1: (eq
  57 A (aplus g (ASort (S n) n1) k) (aplus g (ASort h2 n2) k))).((match h2 in nat
  58 return (\lambda (n0: nat).((eq A (aplus g (ASort (S n) n1) k) (aplus g (ASort
  59 n0 n2) k)) \to (leq g (ASort n n1) (match n0 with [O \Rightarrow (ASort O
  60 (next g n2)) | (S h) \Rightarrow (ASort h n2)])))) with [O \Rightarrow
  61 (\lambda (H2: (eq A (aplus g (ASort (S n) n1) k) (aplus g (ASort O n2)
  62 k))).(leq_sort g n O n1 (next g n2) k (eq_ind A (aplus g (ASort O n2) (S k))
  63 (\lambda (a: A).(eq A (aplus g (ASort n n1) k) a)) (eq_ind A (aplus g (ASort
  64 (S n) n1) (S k)) (\lambda (a: A).(eq A a (aplus g (ASort O n2) (S k))))
  65 (eq_ind_r A (aplus g (ASort O n2) k) (\lambda (a: A).(eq A (asucc g a) (asucc
  66 g (aplus g (ASort O n2) k)))) (refl_equal A (asucc g (aplus g (ASort O n2)
  67 k))) (aplus g (ASort (S n) n1) k) H2) (aplus g (ASort n n1) k)
  68 (aplus_sort_S_S_simpl g n1 n k)) (aplus g (ASort O (next g n2)) k)
  69 (aplus_sort_O_S_simpl g n2 k)))) | (S n0) \Rightarrow (\lambda (H2: (eq A
  70 (aplus g (ASort (S n) n1) k) (aplus g (ASort (S n0) n2) k))).(leq_sort g n n0
  71 n1 n2 k (eq_ind A (aplus g (ASort (S n) n1) (S k)) (\lambda (a: A).(eq A a
  72 (aplus g (ASort n0 n2) k))) (eq_ind A (aplus g (ASort (S n0) n2) (S k))
  73 (\lambda (a: A).(eq A (aplus g (ASort (S n) n1) (S k)) a)) (eq_ind_r A (aplus
  74 g (ASort (S n0) n2) k) (\lambda (a: A).(eq A (asucc g a) (asucc g (aplus g
  75 (ASort (S n0) n2) k)))) (refl_equal A (asucc g (aplus g (ASort (S n0) n2)
  76 k))) (aplus g (ASort (S n) n1) k) H2) (aplus g (ASort n0 n2) k)
  77 (aplus_sort_S_S_simpl g n2 n0 k)) (aplus g (ASort n n1) k)
  78 (aplus_sort_S_S_simpl g n1 n k))))]) H1))]) H0))))))) (\lambda (a3:
  79 A).(\lambda (a4: A).(\lambda (H0: (leq g a3 a4)).(\lambda (_: (leq g (asucc g
  80 a3) (asucc g a4))).(\lambda (a5: A).(\lambda (a6: A).(\lambda (_: (leq g a5
  81 a6)).(\lambda (H3: (leq g (asucc g a5) (asucc g a6))).(leq_head g a3 a4 H0
  82 (asucc g a5) (asucc g a6) H3))))))))) a1 a2 H)))).
  83
  84 axiom asucc_inj:
  85  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (asucc g a1) (asucc
  86 g a2)) \to (leq g a1 a2))))
  87 .
  88