From d97f69b313893900ca2d57544fcd200eb06ee286 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Jun 2008 20:48:25 +0000 Subject: [PATCH] few more steps --- .../matita/contribs/dama/dama/models/q_function.ma | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma index 624755ed7..bb3ba55fc 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -51,11 +51,11 @@ whd in ⊢ (% → ?); simplify in H3; cut (\fst w2 = O); [2: clear H10; symmetry; apply le_n_O_to_eq; rewrite > (sum_bases_O l1 (\fst w2)); [apply le_n] apply (q_le_trans ??? H9); rewrite < H4; rewrite > q_d_x_x; - left; reflexivity;] + apply q_eq_to_le; reflexivity;] rewrite > Hcut; clear Hcut H10 H9; simplify in H5 H6; cut (ⅆ[input,init] = Qpos w) as E; [2: rewrite > H2; rewrite < H4; rewrite > q_d_sym; - rewrite > q_d_noabs; [reflexivity] right; assumption;] + rewrite > q_d_noabs; [reflexivity] apply q_lt_to_le; assumption;] cases (\fst w1) in H5 H6; intros; [1: cases (?:False); clear H5; simplify in H6; apply (q_lt_corefl ⅆ[input,init]); @@ -69,10 +69,13 @@ whd in ⊢ (% → ?); simplify in H3; apply q_le_minus_r; rewrite < q_minus_r; rewrite < E in ⊢ (??%); assumption;] |2: intros; rewrite > H8; rewrite > H7; clear H8 H7; - simplify in H5 H6 ⊢ %; - simplify in H5:(? ? (? ? %)); + simplify in H5 H6 ⊢ %; + cases (\fst w1) in H5 H6; [intros; reflexivity] + cases (bars l1); + [1: intros; simplify; elim n [reflexivity] simplify; assumption; + |2: simplify; intros; cases (?:False); - +STOP alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". -- 2.39.2