From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 10 Feb 2011 11:55:27 +0000 (+0000)
Subject: Added lambda
X-Git-Tag: make_still_working~2580
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6bbf27282bad84e066bb952e41dbc8f72b31de6c;p=helm.git

Added lambda
---

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index 4d99c59c8..798f57629 100644
--- a/matita/matita/lib/basics/list.ma
+++ b/matita/matita/lib/basics/list.ma
@@ -10,7 +10,7 @@
       V_______________________________________________________________ *)
 
 include "basics/types.ma".
-include "basics/bool.ma".
+include "arithmetics/nat.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -114,6 +114,21 @@ match l1 with
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
   ].
 
+(**************************** length ******************************)
+
+let rec length (A:Type[0]) (l:list A) on l ≝ 
+  match l with 
+    [ nil ⇒ 0
+    | cons a tl ⇒ S (length A tl)].
+
+notation "|M|" non associative with precedence 60 for @{'norm $M}.
+interpretation "norm" 'norm l = (length ? l).
+
+let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
+  match n with
+    [O ⇒ hd A l d
+    |S m ⇒ nth m A (tail A l) d].
+
 (**************************** fold *******************************)
 
 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 0754d7afc..1b801a14b 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -141,7 +141,7 @@ definition R0 ≝ λT:Type[0].λt:T.t.
   
 definition R1 ≝ eq_rect_Type0.
 
-
+(* useless stuff
 definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
@@ -216,7 +216,7 @@ definition R4 :
 @(eq_rect_Type0 ????? e3) 
 @(R3 ????????? e0 ? e1 ? e2) 
 @a4 
-qed.
+qed. *)
 
 (* TODO concrete definition by means of proof irrelevance *)
 axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma
new file mode 100644
index 000000000..85bef55e1
--- /dev/null
+++ b/matita/matita/lib/lambda/subst.ma
@@ -0,0 +1,234 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/nat.ma".
+
+inductive T : Type[0] ≝
+  | Sort: nat → T
+  | Rel: nat → T 
+  | App: T → T → T 
+  | Lambda: T → T → T (* type, body *)
+  | Prod: T → T → T (* type, body *)
+  | D: T →T
+.
+
+let rec lift t k p ≝
+  match t with 
+    [ Sort n ⇒ Sort n
+    | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
+    | App m n ⇒ App (lift m k p) (lift n k p)
+    | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p)
+    | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p)
+    | D n ⇒ D (lift n k p)
+    ].
+
+(* 
+ndefinition lift ≝ λt.λp.lift_aux t 0 p.
+
+notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift O $M}.
+notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
+*)
+(* interpretation "Lift" 'Lift n M = (lift M n). *)
+interpretation "Lift" 'Lift n k M = (lift M k n).
+
+let rec subst t k a ≝ 
+  match t with 
+    [ Sort n ⇒ Sort n
+    | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
+        (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1)))
+    | App m n ⇒ App (subst m k a) (subst n k a)
+    | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
+    | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)
+    | D n ⇒ D (subst n k a)
+    ].
+
+(* meglio non definire 
+ndefinition subst ≝ λa.λt.subst_aux t 0 a.
+notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
+*)
+
+notation "M [ k := N ]" non associative with precedence 90 for @{'Subst $M $k $N}.
+
+(* interpretation "Subst" 'Subst N M = (subst N M). *)
+interpretation "Subst" 'Subst M k N = (subst M k N).
+
+(*** properties of lift and subst ***)
+
+lemma lift_0: ∀t:T.∀k. lift t k 0 = t.
+#t (elim t) normalize // #n #k cases (leb (S n) k) normalize // 
+qed.
+
+(* nlemma lift_0: ∀t:T. lift t 0 = t.
+#t; nelim t; nnormalize; //; nqed. *)
+
+lemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i.
+// qed.
+
+lemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n).
+// qed.
+
+lemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i).
+#i (change with (lift (Rel i) 0 1 = Rel (1 + i))) //
+qed.
+
+lemma lift_lift: ∀t.∀i,j.j ≤ i  → ∀h,k. 
+  lift (lift t k i) (j+k) h = lift t k (i+h).
+#t #i #j #h (elim t) normalize // #n #h #k
+@(leb_elim (S n) k) #Hnk normalize
+  [>(le_to_leb_true (S n) (j+k) ?) normalize /2/
+  |>(lt_to_leb_false (S n+i) (j+k) ?)
+     normalize // @le_S_S >(commutative_plus j k)
+     @le_plus // @not_lt_to_le /2/
+  ]
+qed.
+
+lemma lift_lift1: ∀t.∀i,j,k. 
+  lift(lift t k j) k i = lift t k (j+i).
+/2/ qed.
+
+lemma lift_lift2: ∀t.∀i,j,k. 
+  lift (lift t k j) (j+k) i = lift t k (j+i).
+/2/ qed.
+
+(*
+nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
+nnormalize; //; nqed. *)
+
+lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
+#A #B (elim B) normalize /2/ #n #k
+@(leb_elim (S n) k) normalize #Hnk
+  [>(le_to_leb_true ?? Hnk) normalize //
+  |>(lt_to_leb_false (S (n + 1)) k ?) normalize
+    [>(not_eq_to_eqb_false (n+1) k ?) normalize /2/
+    |@le_S (applyS (not_le_to_lt (S n) k Hnk))
+    ]
+  ]
+qed.
+
+(*
+nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
+nnormalize; //; nqed. *)
+
+lemma subst_sort: ∀A.∀n,k.(Sort n) [k ≝ A] = Sort n.
+// qed.
+
+lemma subst_rel: ∀A.(Rel 0) [0 ≝ A] = A.
+normalize // qed.
+
+lemma subst_rel1: ∀A.∀k,i. i < k → 
+  (Rel i) [k ≝ A] = Rel i.
+#A #k #i normalize #ltik >(le_to_leb_true (S i) k) //
+qed.
+
+lemma subst_rel2: ∀A.∀k. 
+  (Rel k) [k ≝ A] = lift A 0 k.
+#A #k normalize >(lt_to_leb_false (S k) k) // >(eq_to_eqb_true … (refl …)) //
+qed.
+
+lemma subst_rel3: ∀A.∀k,i. k < i → 
+  (Rel i) [k ≝ A] = Rel (i-1).
+#A #k #i normalize #ltik >(lt_to_leb_false (S i) k) /2/ 
+>(not_eq_to_eqb_false i k) // @sym_not_eq @lt_to_not_eq //
+qed.
+
+lemma lift_subst_ijk: ∀A,B.∀i,j,k.
+  lift (B [j+k := A]) k i = (lift B k i) [j+k+i ≝ A].
+#A #B #i #j (elim B) normalize /2/ #n #k
+@(leb_elim (S n) (j + k)) normalize #Hnjk
+  [(elim (leb (S n) k))
+    [>(subst_rel1 A (j+k+i) n) /2/
+    |>(subst_rel1 A (j+k+i) (n+i)) /2/
+    ]
+  |@(eqb_elim n (j+k)) normalize #Heqnjk 
+    [>(lt_to_leb_false (S n) k);
+      [(cut (j+k+i = n+i)) [//] #Heq
+       >Heq >(subst_rel2 A ?) normalize (applyS lift_lift) //
+      |/2/
+      ]
+    |(cut (j + k < n))
+      [@not_eq_to_le_to_lt;
+        [/2/ |@le_S_S_to_le @not_le_to_lt /2/ ]
+      |#ltjkn
+       (cut (O < n)) [/2/] #posn (cut (k ≤ n)) [/2/] #lekn
+       >(lt_to_leb_false (S (n-1)) k) normalize
+        [>(lt_to_leb_false … (le_S_S … lekn))
+         >(subst_rel3 A (j+k+i) (n+i)); [/3/ |/2/]
+        |@le_S_S; (* /3/; 65 *) (applyS monotonic_pred) @le_plus_b //
+        ]
+     ]
+  ]
+qed. 
+
+theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → 
+  (lift B i (S k)) [j ≝ A] = lift B i k.
+#A #B (elim B) normalize /2/
+  [2,3,4: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
+   @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
+  |5:#T #Hind #i #j #k #leij #lejk @eq_f @Hind //
+  |#n #i #j #k #leij #ltjk @(leb_elim (S n) i) normalize #len
+    [>(le_to_leb_true (S n) j) /2/
+    |>(lt_to_leb_false (S (n+S k)) j);
+      [normalize >(not_eq_to_eqb_false (n+S k) j)normalize 
+       /2/ @(not_to_not …len) #H @(le_plus_to_le_r k) normalize //
+      |@le_S_S @(transitive_le … ltjk) @le_plus // @not_lt_to_le /2/
+      ]
+    ]
+  ]
+qed.
+     
+(********************* substitution lemma ***********************)    
+
+lemma subst_lemma: ∀A,B,C.∀k,i. 
+  (A [i ≝ B]) [k+i ≝ C] = 
+    (A [S (k+i) := C]) [i ≝ B [k ≝ C]].
+#A #B #C #k (elim A) normalize // (* WOW *)
+#n #i @(leb_elim (S n) i) #Hle
+  [(cut (n < k+i)) [/2/] #ltn (* lento *) (cut (n ≤ k+i)) [/2/] #len
+   >(subst_rel1 C (k+i) n ltn) >(le_to_leb_true n (k+i) len) >(subst_rel1 … Hle) // 
+  |@(eqb_elim n i) #eqni
+    [>eqni >(le_to_leb_true i (k+i)) // >(subst_rel2 …); 
+     normalize @sym_eq (applyS (lift_subst_ijk C B i k O))
+    |@(leb_elim (S (n-1)) (k+i)) #nk
+      [>(subst_rel1 C (k+i) (n-1) nk) >(le_to_leb_true n (k+i));
+        [>(subst_rel3 ? i n) // @not_eq_to_le_to_lt;
+          [/2/ |@not_lt_to_le /2/]
+        |@(transitive_le … nk) //
+        ]
+      |(cut (i < n)) [@not_eq_to_le_to_lt; [/2/] @(not_lt_to_le … Hle)]
+       #ltin (cut (O < n)) [/2/] #posn
+       @(eqb_elim (n-1) (k+i)) #H
+        [>H >(subst_rel2 C (k+i)) >(lt_to_leb_false n (k+i));
+          [>(eq_to_eqb_true n (S(k+i))); 
+            [normalize |<H (applyS plus_minus_m_m) // ]
+           (generalize in match ltin)
+           <H @(lt_O_n_elim … posn) #m #leim >delift normalize /2/
+          |<H @(lt_O_n_elim … posn) #m normalize //
+          ]
+        |(cut (k+i < n-1))
+          [@not_eq_to_le_to_lt; [@sym_not_eq @H |@(not_lt_to_le … nk)]]
+         #Hlt >(lt_to_leb_false n (k+i));
+          [>(not_eq_to_eqb_false n (S(k+i)));
+            [>(subst_rel3 C (k+i) (n-1) Hlt);
+             >(subst_rel3 ? i (n-1)) // @(le_to_lt_to_lt … Hlt) //
+            |@(not_to_not … H) #Hn >Hn normalize //
+            ]
+          |@(transitive_lt … Hlt) @(lt_O_n_elim … posn) normalize // 
+          ]
+        ]
+      ]
+    ]
+  ] 
+qed.
+
+  
+
+
+
diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
new file mode 100644
index 000000000..09ecd4e05
--- /dev/null
+++ b/matita/matita/lib/lambda/types.ma
@@ -0,0 +1,219 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "lambda/subst.ma".
+include "basics/list.ma".
+
+
+(*************************** substl *****************************)
+
+let rec substl (G:list T) (N:T) : list T ≝  
+  match G with
+    [ nil ⇒ nil T
+    | cons A D ⇒ ((subst A (length T D) N)::(substl D N))
+    ].
+
+(*
+nlemma substl_cons: ∀A,N.∀G.
+substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
+//; nqed.
+*)
+
+(*
+nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
+/2/; nqed.*)
+
+(****************************************************************)
+
+axiom A: nat → nat → Prop.
+axiom R: nat → nat → nat → Prop.
+axiom conv: T → T → Prop.
+
+inductive TJ: list T → T → T → Prop ≝
+  | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
+  | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
+  | weak: ∀G.∀A,B,C.∀i.
+     TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
+  | prod: ∀G.∀A,B.∀i,j,k. R i j k →
+     TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
+  | app: ∀G.∀F,A,B,a. 
+     TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a)
+  | abs: ∀G.∀A,B,b.∀i. 
+     TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
+  | conv: ∀G.∀A,B,C.∀i. conv B C →
+     TJ G A B → TJ G B (Sort i) → TJ G A C.
+     
+notation "hvbox(G break  ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
+interpretation "type judgement" 'TJ G A B = (TJ G A B).
+
+(* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
+
+(**** definitions ****)
+
+inductive Glegal (G: list T) : Prop ≝
+glegalk : ∀A,B. G ⊢ A : B → Glegal G.
+
+inductive Gterm (G: list T) (A:T) : Prop ≝
+  | is_term: ∀B.G ⊢ A:B → Gterm G A
+  | is_type: ∀B.G ⊢ B:A → Gterm G A.
+
+inductive Gtype (G: list T) (A:T) : Prop ≝ 
+gtypek: ∀i.G ⊢ A : Sort i → Gtype G A.
+
+inductive Gelement (G:list T) (A:T) : Prop ≝
+gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
+
+inductive Tlegal (A:T) : Prop ≝ 
+tlegalk: ∀G. Gterm G A → Tlegal A.
+
+(*
+ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
+
+ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
+
+ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
+
+ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
+
+ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
+*)
+
+(*
+ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
+subst C A 
+#G; #i; #j; #axij; #Gleg; ncases Gleg; 
+#A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
+*)
+
+theorem start_lemma1: ∀G.∀i,j. 
+A i j → Glegal G → G ⊢ Sort i: Sort j.
+#G #i #j #axij #Gleg (cases Gleg) 
+#A #B #tjAB (elim tjAB) /2/
+(* bello *) qed.
+
+theorem start_rel: ∀G.∀A.∀C.∀n,i,q.
+G ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i).
+#G #A #C #n #i #p #tjC #tjn
+ (applyS (weak G (Rel n))) //. (* bello *)
+ (*
+ nrewrite > (plus_n_O i); 
+ nrewrite > (plus_n_Sm i O); 
+ nrewrite < (lift_lift A 1 i);
+ nrewrite > (plus_n_O n);  nrewrite > (plus_n_Sm n O); 
+ applyS (weak G (Rel n) (lift A i) C p tjn tjC). *)
+qed.
+  
+theorem start_lemma2: ∀G.
+Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
+#G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/
+  [#i #j #axij #p normalize #abs @False_ind @(absurd … abs) // 
+  |#G #A #i #tjA #Hind #m (cases m) /2/
+   #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle
+  |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
+     /2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle
+  ]
+qed.
+
+(*
+nlet rec TJm G D on D : Prop ≝
+  match D with
+    [ nil ⇒ True
+    | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
+    ].
+    
+nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
+#G; #D; #A; *; //; nqed.
+
+ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B → 
+  ∀G. Glegal G → TJm G D → TJ G A B.
+#D; #A; #B; #tjAB; nelim tjAB;
+  ##[/2/;
+  ##|/2/;
+  ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
+     #tjGcons; 
+     napply weak;
+*)
+(*
+ntheorem substitution_tj: 
+∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
+  TJ G (subst N M) (subst N B).
+#G;#A;#B;#N;#M;#tjM; 
+  napply (TJ_inv2 (A::G) M B); 
+  ##[nnormalize; /3/;
+  ##|#G; #A; #N; #tjA; #Hind; #Heq;
+     ndestruct;//; 
+  ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
+     ndestruct;//;
+  ##|nnormalize; #E; #A; #B; #i; #j; #k;
+     #Ax; #tjA; #tjB; #Hind1; #_;
+     #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
+      ##[/2/;
+      ##|nnormalize; napplyS weak;
+
+*)
+
+
+axiom conv_subst: ∀P,Q,N,i.conv P Q → conv P[i := N] Q[i := N].
+
+theorem substitution_tj: 
+∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A → 
+  ((substl D N)@G) ⊢ M[|D| := N]: B[|D| := N].
+#E #A #B #M #tjMB (elim tjMB)
+  [normalize #i #j #k #G #D #N (cases D) 
+    [normalize #isnil destruct
+    |#P #L normalize #isnil destruct
+    ]
+  |#G #A1 #i #tjA #Hind #G1 #D (cases D) 
+    [#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) //
+     (normalize in Heq) destruct /2/
+    |#H #L #N1 #Heq (normalize in Heq)
+     #tjN1 normalize destruct; (applyS start) /2/
+    ]
+  |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N
+   (cases D) normalize
+    [#Heq destruct #tjN //
+    |#H #L #Heq #tjN1 destruct;
+       (* napplyS weak non va *)
+     (cut (S (length T L) = (length T L)+0+1)) [//] 
+     #Hee (applyS weak) /2/
+    ]
+  |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2
+   #G1 #D #N #Heq #tjN normalize @(prod … Ax);
+    [/2/
+    |(cut (S (length T D) = (length T D)+1)) [//] 
+     #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
+    ]
+  |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
+   #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
+   >(plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?))
+   >(subst_lemma R S N ? 0) (applyS app) /2/
+  |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
+   #G1 #D #N #Heq #tjN normalize
+   (applyS abs) 
+    [normalize in Hind2 /2/
+    |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
+     generalize in match (Hind1 G1 (P::D) N ? tjN);
+      [#H (normalize in H) (applyS H) | normalize // ]
+    ]
+  |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
+   #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
+   @(conv …(conv_subst … convQR) ? (Hind2 …)) //
+   @Hind1 //
+  ]
+qed.
+ 
+  
+ 
+
+
+
+
+