commit by user ricciott

diff --git a/weblib/arithmetics/bigops.ma b/weblib/arithmetics/bigops.ma
index 41c680088eb9987e563a0eac5985c4fb573048e0..7936b5dd038455bea4104679104814fd7ce4d027 100644 (file)
--- a/weblib/arithmetics/bigops.ma
+++ b/weblib/arithmetics/bigops.ma
@@ -42,25 +42,25 @@ qed.
       |false ⇒ bigop k p B nil op f]
    ].
    
-notation "\big  [ op , nil ]_{ ident i < n | p } f"
+notation "ref 'bigop \big  [ op , nil ]_{ ident i < n | p } f"
   with precedence 80
 for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}.
 
-notation "\big [ op , nil ]_{ ident i < n } f"
+notation "ref 'bigop \big [ op , nil ]_{ ident i < n } f"
   with precedence 80
 for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}.
 
 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
 
-notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
+notation "ref 'bigop \big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
   with precedence 80
-for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
+for @{'bigop (minus $b $a) $op $nil (λ${ident j}.((λ${ident j}.$p) (plus ${ident j} $a)))
+  (λ${ident j}.((λ${ident j}.$f)(plus ${ident j} $a)))}.
 
-notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
+notation "ref 'bigop \big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
   with precedence 80
-for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
-  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.  
+for @{'bigop (minus $b $a) $op $nil (λ${ident j}.((λ${ident j}.true) (plus ${ident j} $a)))
+  (λ${ident j}.((λ${ident j}.$f)(plus ${ident j} $a)))}.  
 
 (* notation "\big  [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
   with precedence 80
@@ -70,19 +70,19 @@ for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))
 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
    
 \ 5img class="anchor" src="icons/tick.png" id="bigop_Strue"\ 6lemma bigop_Strue: ∀k,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. p k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
-  \big[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-    op (f k) (\big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)).
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+    op (f k) (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)).
 #k #p #B #nil #op #f #H normalize >H // qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_Sfalse"\ 6lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. p k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 →
-  \big[op,nil]_{ i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-    \big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{ i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+    \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
 #k #p #B #nil #op #f #H normalize >H // qed. 
  
 \ 5img class="anchor" src="icons/tick.png" id="same_bigop"\ 6lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. 
   \ 5a href="cic:/matita/arithmetics/bigops/sameF_upto.def(2)"\ 6sameF_upto\ 5/a\ 6 k \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 p1 p2 → \ 5a href="cic:/matita/arithmetics/bigops/sameF_p.def(2)"\ 6sameF_p\ 5/a\ 6 k p1 B f g →
-  \big[op,nil]_{i < k | p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
-    \big[op,nil]_{i < k | p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i).
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+    \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i).
 #k #p1 #p2 #B #nil #op #f #g (elim k) // 
 #n #Hind #samep #samef normalize >Hind 
   [|@(\ 5a href="cic:/matita/arithmetics/bigops/sameF_p_le.def(5)"\ 6sameF_p_le\ 5/a\ 6 … samef) // |@(\ 5a href="cic:/matita/arithmetics/bigops/sameF_upto_le.def(5)"\ 6sameF_upto_le\ 5/a\ 6 … samep) //]
@@ -91,8 +91,8 @@ normalize // <(samef … (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le
 qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="pad_bigop"\ 6theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k → 
-\big[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
-  \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < k | \ 5font class="Apple-style-span" color="#FF0000"\ 6if\ 5/font\ 6 (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n i) then \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 else p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)
+  \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | \ 5font class="Apple-style-span" color="#FF0000"\ 6if\ 5/font\ 6 (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n i) then \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 else p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
 #k #n #p #B #nil #op #f #lenk (elim lenk) 
   [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti // >(\ 5a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"\ 6not_le_to_leb_false\ 5/a\ 6 …) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
   |#j #leup #Hind >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 … leup) // 
@@ -100,8 +100,8 @@ qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="pad_bigop1"\ 6theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k → 
   (∀i. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) →
-  \big[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) 
-    \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) 
+    \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
 #k #n #p #B #nil #op #f #lenk (elim lenk) 
   [#_ @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti // 
   |#j #leup #Hind #Hfalse >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 
@@ -112,7 +112,7 @@ qed.
 qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_false"\ 6theorem bigop_false: ∀n,B,nil,op.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
-  \big[op,nil]_{i < n | \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil.  
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil.  
 #n #B #nil #op #f elim n // #n1 #Hind 
 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 // 
 qed.
@@ -126,8 +126,8 @@ qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="pad_bigop_nil"\ 6theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 k → 
   (∀i. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 k → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 nil) →
-  \big[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) 
-    \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) 
+    \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < k | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
 #k #n #p #B #nil #op #f #lenk (elim lenk) 
   [#_ @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti // 
   |#j #leup #Hind #Hfalse cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p j)) #Hpj
@@ -143,8 +143,8 @@ qed.
 qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_sum"\ 6theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
-op (\big[op,nil]_{i<k1|p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)) \big[op,nil]_{i<k2|p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-      \big[op,nil]_{i<k1\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6k2|\ 5font class="Apple-style-span" color="#FF0000"\ 6 if \ 5/font\ 6\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 k2 i then p1 (i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6k2) else p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
+op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k1|p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)) \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k2|p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+      \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k1\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6k2|\ 5font class="Apple-style-span" color="#FF0000"\ 6 if \ 5/font\ 6\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 k2 i then p1 (i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6k2) else p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
         (if \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 k2 i then f (i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6k2) else g i).
 #k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
   [normalize >\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 #i #lti 
@@ -161,12 +161,12 @@ qed.
 qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_I"\ 6theorem bigop_I: ∀n,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
-\big[op,nil]_{i∈[\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6,n[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < n|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i). 
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6,n[ |p i\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n|p i}(f i). 
 #n #p #B #nil #op #f <\ 5a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"\ 6minus_n_O\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 //
 qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_I_gen"\ 6theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6b →
-\big[op,nil]_{i∈[a,b[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i < b|\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 a i \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i). 
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[a,b[ |p i}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < b|\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 a i \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p i}(f i). 
 #a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
 cut (∀a,b. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a)) 
   [#a #b cases a // #a1 #lta1 normalize >\ 5a href="cic:/matita/arithmetics/nat/eq_minus_S_pred.def(4)"\ 6eq_minus_S_pred\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/S_pred.def(3)"\ 6S_pred\ 5/a\ 6 
@@ -193,9 +193,9 @@ qed.
           
 \ 5img class="anchor" src="icons/tick.png" id="bigop_sumI"\ 6theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
 a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 c →
-\big[op,nil]_{i∈[a,c[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
-  op (\big[op,nil]_{i ∈ [b,c[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)) 
-      \big[op,nil]_{i ∈ [a,b[ |p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[a,c[ |p i}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+  op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i ∈ [b,c[ |p i}(f i)) 
+      \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i ∈ [a,b[ |p i}(f i).
 #a #b # c #p #B #nil #op #f #leab #lebc 
 >(\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 (c\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a) (b\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6a)) in ⊢ (??%?); /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"\ 6monotonic_le_minus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 >\ 5a href="cic:/matita/arithmetics/nat/minus_plus.def(13)"\ 6minus_plus\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 a) <\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 //
@@ -206,24 +206,24 @@ a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b →
 qed.   
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_a"\ 6theorem bigop_a: ∀a,b,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B. a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b →
-\big[op,nil]_{i∈[a,\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b[ \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
-  op (\big[op,nil]_{i ∈ [a,b[ \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i))) (f a).
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i∈[a,\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b[ }(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+  op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i ∈ [a,b[ }(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i))) (f a).
 #a #b #B #nil #op #f #leab 
 >(\ 5a href="cic:/matita/arithmetics/bigops/bigop_sumI.def(14)"\ 6bigop_sumI\ 5/a\ 6 a (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 a) (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b)) [|@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 //|//] @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 
   [@\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 // |<\ 5a href="cic:/matita/arithmetics/nat/minus_Sn_n.def(4)"\ 6minus_Sn_n\ 5/a\ 6 normalize @\ 5a href="cic:/matita/arithmetics/bigops/nilr.fix(0,2,2)"\ 6nilr\ 5/a\ 6]
 qed.
   
 \ 5img class="anchor" src="icons/tick.png" id="bigop_0"\ 6theorem bigop_0: ∀n,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→B.
-\big[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
-  op (\big[op,nil]_{i < n\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i))) (f \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6).
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+  op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i < n}(f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i))) (f \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6).
 #n #B #nil #op #f 
 <\ 5a href="cic:/matita/arithmetics/bigops/bigop_I.def(7)"\ 6bigop_I\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_a.def(15)"\ 6bigop_a\ 5/a\ 6 [|//] @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 [|//] <\ 5a href="cic:/matita/arithmetics/nat/minus_n_O.def(3)"\ 6minus_n_O\ 5/a\ 6 
 @\ 5a href="cic:/matita/arithmetics/bigops/same_bigop.def(6)"\ 6same_bigop\ 5/a\ 6 //
 qed.    
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_prod"\ 6theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 →\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.
-\big[op,nil]_{x<k1|p1 x\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(\big[op,nil]_{i<k2|p2 x i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f x i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-  \big[op,nil]_{i<k1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6 (p1 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2)) (p2 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 k2))\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{x<k1|p1 x}(\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k2|p2 x i}(f x i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6k2|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6 (p1 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2)) (p2 (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 k2))}
      (f (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 i k2) (i \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 k2)).
 #k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
 #n #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p1 n)) #Hp1
@@ -243,8 +243,8 @@ qed.
   }.
  
 \ 5img class="anchor" src="icons/tick.png" id="bigop_op"\ 6lemma bigop_op: ∀k,p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f,g: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.
-op (\big[op,nil]_{i<k|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i)) (\big[op,nil]_{i<k|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(g i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-  \big[op,nil]_{i<k|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(op (f i) (g i)).
+op (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k|p i}(f i)) (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k|p i}(g i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<k|p i}(op (f i) (g i)).
 #k #p #B #nil #op #f #g (elim k) [normalize @\ 5a href="cic:/matita/arithmetics/bigops/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6]
 -k #k #Hind (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p k))) #H
   [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 //
@@ -256,8 +256,8 @@ qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_diff"\ 6lemma bigop_diff: ∀p,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → B.∀i,n.
   i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → p i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
-  \big[op,nil]_{x<n|p x\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f x)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-    op (f i) (\big[op,nil]_{x<n|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6(\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 i x))(p x)\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f x)).
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{x<n|p x}(f x)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+    op (f i) (\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{x<n|\ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6(\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 i x))(p x)}(f x)).
 #p #B #nil #op #f #i #n (elim n) 
   [#ltO @\ 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/
   |#n #Hind #lein #pi cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …lein)) #Hi
@@ -317,7 +317,7 @@ qed.
 
 \ 5img class="anchor" src="icons/tick.png" id="bigop_iso"\ 6theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f1,f2.
   \ 5a href="cic:/matita/arithmetics/bigops/iso.def(3)"\ 6iso\ 5/a\ 6 B (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 B f1 n1 p1) (\ 5a href="cic:/matita/arithmetics/bigops/range.con(0,1,1)"\ 6mk_range\ 5/a\ 6 B f2 n2 p2) →
-  \big[op,nil]_{i<n1|p1 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f1 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \big[op,nil]_{i<n2|p2 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f2 i).
+  \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n1|p1 i}(f1 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n2|p2 i}(f2 i).
 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
 @(\ 5a href="cic:/matita/arithmetics/nat/le_gen.def(1)"\ 6le_gen\ 5/a\ 6 ? n1) #i generalize in match p2; (elim i) 
   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
@@ -353,8 +353,8 @@ qed.
 \ 5img class="anchor" src="icons/tick.png" id="bigop_commute"\ 6theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:\ 5a href="cic:/matita/arithmetics/bigops/ACop.ind(1,0,2)"\ 6ACop\ 5/a\ 6 B nil.∀f.
 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m →
 (∀i,j. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → j \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → (p11 i \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p12 i j) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (p21 j \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 p22 i j)) →
-\big[op,nil]_{i<n|p11 i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(\big[op,nil]_{j<m|p12 i j\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i j)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
-   \big[op,nil]_{j<m|p21 j\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(\big[op,nil]_{i<n|p22 i j\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i j)).
+\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n|p11 i}(\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{j<m|p12 i j}(f i j)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{j<m|p21 j}(\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[op,nil]_{i<n|p22 i j}(f i j)).
 #n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"\ 6bigop_prod\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/bigops/bigop_prod.def(15)"\ 6bigop_prod\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/bigops/bigop_iso.def(9)"\ 6bigop_iso\ 5/a\ 6 
 %{(λi.(i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m)} %{(λi.(i\ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6n)} % 
@@ -407,8 +407,8 @@ qed.
 \ 5img class="anchor" src="icons/tick.png" id="bigop_distr"\ 6theorem bigop_distr: ∀n,p,B,nil.∀R:\ 5a href="cic:/matita/arithmetics/bigops/Dop.ind(1,0,2)"\ 6Dop\ 5/a\ 6 B nil.\forall f,a.
   let aop \def  \ 5a href="cic:/matita/arithmetics/bigops/sum.fix(0,2,4)"\ 6sum\ 5/a\ 6 B nil R in
   let mop \def \ 5a href="cic:/matita/arithmetics/bigops/prod.fix(0,2,4)"\ 6prod\ 5/a\ 6 B nil R in
-  mop a \big[aop,nil]_{i<n|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
-   \big[aop,nil]_{i<n|p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(mop a (f i)).
+  mop a \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[aop,nil]_{i<n|p i}(f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+   \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6\big\ 5/a\ 6[aop,nil]_{i<n|p i}(mop a (f i)).
 #n #p #B #nil #R #f #a normalize (elim n) [@\ 5a href="cic:/matita/arithmetics/bigops/null.fix(0,2,5)"\ 6null\ 5/a\ 6]
 #n #Hind (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p n))) #H
   [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 // >(\ 5a href="cic:/matita/arithmetics/bigops/distr.fix(0,2,5)"\ 6distr\ 5/a\ 6 B nil R) >Hind //

diff --git a/weblib/arithmetics/min_max.ma b/weblib/arithmetics/min_max.ma
index 3b93593b65701490e0fd34d6ac33f995b9b0d3e4..38f7b4f1a563cc60f49f4ffebeaa0fe51bc25a22 100644 (file)
--- a/weblib/arithmetics/min_max.ma
+++ b/weblib/arithmetics/min_max.ma
@@ -57,4 +57,4 @@ qed.
   ]
 qed.
 
- 
+ 
\ No newline at end of file

diff --git a/weblib/ricciott/cpp2012.ma b/weblib/ricciott/cpp2012.ma
new file mode 100644 (file)
index 0000000..bac60d2
--- /dev/null
+++ b/weblib/ricciott/cpp2012.ma
@@ -0,0 +1,43 @@
+(* new script *)
+
+include "basics/logic.ma".
+include "basics/types.ma".
+include "basics/bool.ma".
+include "arithmetics/nat.ma".
+include "basics/list.ma".
+
+axiom Vector : Type[0] → nat → Type[0].
+axiom tape : Type[0] → Type[0].
+axiom current : ∀T:Type[0]. tape T → option T.
+axiom vec : ∀T:Type[0].∀n:nat.Vector T n → list T.
+coercion vec : ∀T:Type[0].∀n:nat.∀v:Vector T n.list T ≝ vec on _v:Vector ?? to list ?.
+axiom niltape : ∀T.tape T.
+axiom midtape : ∀T.list T → T → list T → tape T.
+axiom change_vec : ∀T,n.Vector T n → T → nat → Vector T n.
+axiom move : Type[0].
+axiom R : move.
+axiom tape_move : ∀T.tape T → option (T × move) → tape T.
+axiom memb: ∀T.T → list T → bool.
+interpretation "boolean membership" 'mem a l = (memb ? a l).
+axiom right : ∀T.tape T → list T.
+
+
+definition R_match_step_true ≝ 
+  λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
+  ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s → 
+  current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
+  (is_startc s = true → 
+   (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
+   (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →  
+    outt = change_vec ?? int 
+          (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧  
+   (∀ls,x,xs,ci,rs,ls0,rs0. 
+     nth src ? int (niltape ?) = midtape ls x (xs@ci::rs) →
+     nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
+     (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → 
+     is_endc ci = false ∧ rs0 ≠ [] ∧
+     ∀cj,rs1.rs0 = cj::rs1 → 
+      ci ≠ cj →
+      (outt = change_vec ?? int 
+          (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))). 
+

diff --git a/weblib/ricciott/test.ma b/weblib/ricciott/test.ma
new file mode 100644 (file)
index 0000000..a2a0c86
--- /dev/null
+++ b/weblib/ricciott/test.ma
@@ -0,0 +1,3 @@
+(* new script *)
+
+include "While/syntax.ma".