]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1A/s/props.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_1A / s / props.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "basic_1A/s/defs.ma".
18
19 lemma s_S:
20  \forall (k: K).(\forall (i: nat).(eq nat (s k (S i)) (S (s k i))))
21 \def
22  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(eq nat (s k0 (S 
23 i)) (S (s k0 i))))) (\lambda (b: B).(\lambda (i: nat).(refl_equal nat (S (s 
24 (Bind b) i))))) (\lambda (f: F).(\lambda (i: nat).(refl_equal nat (S (s (Flat 
25 f) i))))) k).
26
27 lemma s_plus:
28  \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (s k (plus i j)) 
29 (plus (s k i) j))))
30 \def
31  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
32 nat).(eq nat (s k0 (plus i j)) (plus (s k0 i) j))))) (\lambda (b: B).(\lambda 
33 (i: nat).(\lambda (j: nat).(refl_equal nat (plus (s (Bind b) i) j))))) 
34 (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus (s 
35 (Flat f) i) j))))) k).
36
37 lemma s_plus_sym:
38  \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (s k (plus i j)) 
39 (plus i (s k j)))))
40 \def
41  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
42 nat).(eq nat (s k0 (plus i j)) (plus i (s k0 j)))))) (\lambda (_: B).(\lambda 
43 (i: nat).(\lambda (j: nat).(eq_ind_r nat (plus i (S j)) (\lambda (n: nat).(eq 
44 nat n (plus i (S j)))) (refl_equal nat (plus i (S j))) (S (plus i j)) 
45 (plus_n_Sm i j))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: 
46 nat).(refl_equal nat (plus i (s (Flat f) j)))))) k).
47
48 lemma s_minus:
49  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((le j i) \to (eq nat (s 
50 k (minus i j)) (minus (s k i) j)))))
51 \def
52  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
53 nat).((le j i) \to (eq nat (s k0 (minus i j)) (minus (s k0 i) j)))))) 
54 (\lambda (_: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (le j 
55 i)).(eq_ind_r nat (minus (S i) j) (\lambda (n: nat).(eq nat n (minus (S i) 
56 j))) (refl_equal nat (minus (S i) j)) (S (minus i j)) (minus_Sn_m i j H)))))) 
57 (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (_: (le j 
58 i)).(refl_equal nat (minus (s (Flat f) i) j)))))) k).
59
60 lemma minus_s_s:
61  \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (minus (s k i) (s 
62 k j)) (minus i j))))
63 \def
64  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
65 nat).(eq nat (minus (s k0 i) (s k0 j)) (minus i j))))) (\lambda (_: 
66 B).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (minus i j))))) 
67 (\lambda (_: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (minus i 
68 j))))) k).
69
70 lemma s_le:
71  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((le i j) \to (le (s k i) 
72 (s k j)))))
73 \def
74  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
75 nat).((le i j) \to (le (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i: 
76 nat).(\lambda (j: nat).(\lambda (H: (le i j)).(le_n_S i j H))))) (\lambda (_: 
77 F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (le i j)).H)))) k).
78
79 lemma s_lt:
80  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((lt i j) \to (lt (s k i) 
81 (s k j)))))
82 \def
83  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
84 nat).((lt i j) \to (lt (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i: 
85 nat).(\lambda (j: nat).(\lambda (H: (lt i j)).(lt_n_S i j H))))) (\lambda (_: 
86 F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt i j)).H)))) k).
87
88 lemma s_inc:
89  \forall (k: K).(\forall (i: nat).(le i (s k i)))
90 \def
91  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(le i (s k0 i)))) 
92 (\lambda (b: B).(\lambda (i: nat).(le_S_n i (s (Bind b) i) (le_S_n (S i) (S 
93 (s (Bind b) i)) (le_S_n (S (S i)) (S (S (s (Bind b) i))) (le_S (S (S (S i))) 
94 (S (S (s (Bind b) i))) (le_n (S (S (s (Bind b) i)))))))))) (\lambda (f: 
95 F).(\lambda (i: nat).(le_n (s (Flat f) i)))) k).
96
97 lemma s_arith0:
98  \forall (k: K).(\forall (i: nat).(eq nat (minus (s k i) (s k O)) i))
99 \def
100  \lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (minus i O) (\lambda (n: 
101 nat).(eq nat n i)) (eq_ind nat i (\lambda (n: nat).(eq nat n i)) (refl_equal 
102 nat i) (minus i O) (minus_n_O i)) (minus (s k i) (s k O)) (minus_s_s k i O))).
103
104 lemma s_arith1:
105  \forall (b: B).(\forall (i: nat).(eq nat (minus (s (Bind b) i) (S O)) i))
106 \def
107  \lambda (_: B).(\lambda (i: nat).(eq_ind nat i (\lambda (n: nat).(eq nat n 
108 i)) (refl_equal nat i) (minus i O) (minus_n_O i))).
109