From 05b38c588708726f48288227221a8b706544b0a7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Nov 2008 09:36:23 +0000 Subject: [PATCH] fixed scripts --- helm/software/matita/contribs/didactic/shannon.ma | 9 ++++----- helm/software/matita/library/demo/power_derivative.ma | 4 ++-- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma index 5e1db41e8..233c323a2 100644 --- a/helm/software/matita/contribs/didactic/shannon.ma +++ b/helm/software/matita/contribs/didactic/shannon.ma @@ -557,10 +557,9 @@ DOCEND*) = ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v). = ([[ (FNot f)[ FBot/x ] ]]_v). = ([[ FNot (f[ FBot/x ]) ]]_v). - (* FIXME, ASSERT IN PARAMOD = (1 - [[ f[ FBot/x ] ]]_v). = [[ FNot f ]]_v). *) - change with (1 - [[ f[ FBot/x ] ]]_v = [[ FNot f ]]_v). + = (1 - [[ f[ FBot/x ] ]]_v). = (1 - [[ f ]]_v) by H5. - change with ([[ FNot f ]]_v = [[ FNot f ]]_v). + = ([[ FNot f ]]_v). done. case Right. by H1, H we proved @@ -572,9 +571,9 @@ DOCEND*) = ([[ if false then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v). = ([[ (FNot f)[ FTop/x ] ]]_v). = ([[ FNot (f[ FTop/x ]) ]]_v). - change with (1 - [[ f[ FTop/x ] ]]_v = [[ FNot f ]]_v) . + = (1 - [[ f[ FTop/x ] ]]_v). = (1 - [[ f ]]_v) by H5. - change with ([[ FNot f ]]_v = [[ FNot f ]]_v). + = ([[ FNot f ]]_v). done. qed. diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index 8ab638da8..adf852499 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -264,10 +264,10 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n). case left. suppose (0 < m) (m_pos). using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1). - done. + by H1 done. case right. suppose (0=m) (m_zero). - done. + by m_zero, Fmult_zero_f done. conclude (D[x \sup (1+m)]) = (D[x · x \sup m]). -- 2.39.2