commit by user ricciott

diff --git a/weblib/cr/lambda.ma b/weblib/cr/lambda.ma
index 493f63304d1727a5d42a849009ce7a4f73f7aa7d..f368613c72ff4ef57bba5c9451c14e4353b5363e 100644 (file)
--- a/weblib/cr/lambda.ma
+++ b/weblib/cr/lambda.ma
@@ -661,6 +661,30 @@ definition body ≝ λx,M.match M with
  [ Abs M0 ⇒ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
  | _  ⇒ M ].
 
+inductive dupfree (A:Type[0]) : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+| df_nil  : dupfree A \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
+| df_cons : ∀x,xl.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → dupfree A xl → dupfree A (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:xl).
+
+record df_list (A:Type[0]) : Type[0] ≝ {
+  list_of_dfl :> \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A;
+  dfl_dupfree : \ 5a href="cic:/matita/cr/lambda/dupfree.ind(1,0,1)"\ 6dupfree\ 5/a\ 6 A list_of_dfl
+}.
+
+(* ciascuno dei pre_tm utilizzati nella costruzione deve essere un ext_tm 0 *)
+inductive tm : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
+| tm_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
+| tm_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
+| tm_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.∀M:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:xl) M) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/Lam.def(5)"\ 6Lam\ 5/a\ 6 x M)).
+
+
+inductive tm2 : pre_tm → Prop ≝
+| tm2_Par : ∀xl:df_list X.∀x.x ∈ xl → tm2 (Judg xl (Par x))
+| tm2_App : ∀xl:df_list X.∀M1,M2.tm2 (Judg xl M1) → tm2 (Judg xl M2) → tm2 (Judg xl (App M1 M2))
+| tm2_Lam : ∀xl:df_list X.∀M,C.(∀x.x ∉ xl@C → tm2 (Judg (x::xl) (body x M))) → tm2 (Judg xl (Abs M)).
+
+
+
+
 inductive L (F:X → S_exp → Y) : S_exp → Prop \def
 | LPar : ∀x:X.L F (Par x)
 | LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N)