commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 27246556114db8b79129f2aa31a180ee0e948e35..76065b6dbac07ba30ade03af9332d108d71cb997 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -178,16 +178,26 @@ lemma if_epsilon_true : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def
 #S * #pi #b * [normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] cases b normalize // @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
 qed.
 
-definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
+definition lor ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="por" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 b〉.
 
 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
-interpretation "oplus" 'oplus a b = (lo ? a b).
+interpretation "oplus" 'oplus a b = (lor ? a b).
 
-ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
-   match a with [ mk_pair e1 b1 ⇒
-   match b1 with 
-   [ false ⇒ 〈e1 · \fst b, \snd b〉 
-   | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
+definition item_concat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
+ λS,i,e.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i \ 5a title="pcat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e〉.
+
+definition lcat: ∀S:Alpha.∀bcast:(∀S:Alpha.pre S →pre S).pre S → pre S → pre S
+ ≝ λS:Alpha.λbcast:∀S:Alpha.pre S → pre S.λe1,e2:pre S.
+  match e1 with [ mk_pair i1 b1 ⇒ e2]. 
+
+  match e1 with [ _ => e1].
+
+ match b1 with 
+   [ false ⇒ e2 | _ => e1 ]].
+
+ | true ⇒ item_concat S i1 (bcast S e2)
+   ]
+].
    
 notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
 interpretation "lc" 'lc op a b = (lc ? op a b).