From a69c0f03bc2a70cf1ee4a87e4016dfc83a13c60a Mon Sep 17 00:00:00 2001 From: Cristian Armentano Date: Mon, 17 Sep 2007 14:40:36 +0000 Subject: [PATCH] simplified version of a theorem. --- matita/library/Z/sigma_p.ma | 2 +- matita/library/nat/iteration2.ma | 34 +++++++++++++++++++++++++++++++- 2 files changed, 34 insertions(+), 2 deletions(-) diff --git a/matita/library/Z/sigma_p.ma b/matita/library/Z/sigma_p.ma index 92b215396..b246b8444 100644 --- a/matita/library/Z/sigma_p.ma +++ b/matita/library/Z/sigma_p.ma @@ -168,7 +168,7 @@ theorem eq_sigma_p_gh: (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to -sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g. +sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g. intros. unfold sigma_p. apply (eq_iter_p_gen_gh Z OZ Zplus ? ? ? g h h1 n n1 p1 p2) diff --git a/matita/library/nat/iteration2.ma b/matita/library/nat/iteration2.ma index 3a6bab396..e00bb4420 100644 --- a/matita/library/nat/iteration2.ma +++ b/matita/library/nat/iteration2.ma @@ -173,7 +173,7 @@ theorem eq_sigma_p_gh: (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to -sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g. +sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g. intros. unfold sigma_p. apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2) @@ -580,3 +580,35 @@ rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?) | apply lt_O_times_S_S ] qed. + +theorem sigma_p_knm: +\forall g: nat \to nat. +\forall h2:nat \to nat \to nat. +\forall h11,h12:nat \to nat. +\forall k,n,m. +\forall p1,p21:nat \to bool. +\forall p22:nat \to nat \to bool. +(\forall x. x < k \to p1 x = true \to +p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true +\land h2 (h11 x) (h12 x) = x +\land (h11 x) < n \land (h12 x) < m) \to +(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to +p1 (h2 i j) = true \land +h11 (h2 i j) = i \land h12 (h2 i j) = j +\land h2 i j < k) \to +sigma_p k p1 g= +sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))). +intros. +unfold sigma_p. +unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)). +apply iter_p_gen_knm + [apply symmetricIntPlus + |apply associative_plus + |intro.rewrite < plus_n_O.reflexivity + |exact h11 + |exact h12 + |assumption + |assumption + ] +qed. + \ No newline at end of file -- 2.39.2