1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc".
19 include "leq/defs.ma".
21 include "aplus/props.ma".
24 \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (leq g
25 (asucc g a1) (asucc g a2)))))
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)))).
85 \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (asucc g a1) (asucc
86 g a2)) \to (leq g a1 a2))))