X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fiteration2.ma;h=0230362e72aaa9610ffb25034c21f0028d4e8b69;hb=59cce4c27057cff97d9b4311a379c3107c5ee9a3;hp=e00bb442089752014f6ed9c630bf7ad445b867d9;hpb=b58315ef220a130a44acbf528cd6885ddadad642;p=helm.git

diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index e00bb4420..0230362e7 100644
--- a/helm/software/matita/library/nat/iteration2.ma
+++ b/helm/software/matita/library/nat/iteration2.ma
@@ -611,4 +611,36 @@ apply iter_p_gen_knm
   |assumption
   ]
 qed.
-  
\ No newline at end of file
+  
+  
+theorem sigma_p2_eq: 
+\forall g: nat \to nat \to nat.
+\forall h11,h12,h21,h22: nat \to nat \to nat. 
+\forall n1,m1,n2,m2.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n1 \land h12 i j < m1) \to
+(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n2 \land (h22 i j) < m2) \to
+sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
+sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
+intros.
+unfold sigma_p.
+unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
+unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
+
+apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
+[ apply symmetricIntPlus
+| apply associative_plus
+| intro.
+  rewrite < (plus_n_O).
+  reflexivity
+| assumption
+| assumption
+]
+qed.
\ No newline at end of file