From c449d8972928eb8e6fcce842aeb388118c0c314e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 21 Nov 2012 09:05:44 +0000 Subject: [PATCH] match --- .../lib/turing/multi_universal/match.ma | 24 +++++++++++-------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index 5e1b501ed..d054a9c83 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -394,13 +394,20 @@ lemma sem_match_step : | >nth_change_vec_neq [|@sym_not_eq //] nth_change_vec_neq [|@sym_not_eq //] - STOP. - - >nth_change_vec in Htbdst; // #Htbdst >(Htbdst - … Htadst_mid) >Hta_mid cases rs // - | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Htbelse @sym_not_eq // ] - | >Hcurtc in Hcurta_src; #H destruct (H) cases (is_endc s) in Hcend; + (* STOP. *) + cases (decidable_eq_nat i src) #Hisrc + [ >Hisrc >nth_change_vec // >Htasrc_mid // + | >nth_change_vec_neq [|@sym_not_eq //] + <(Htbelse i) [|@sym_not_eq // ] + >Hcomp2 >nth_change_vec_neq [|@sym_not_eq // ] + >nth_change_vec_neq [|@sym_not_eq // ] // + ] + ] + | >Hcomp2 in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //] + >nth_change_vec // whd in ⊢ (??%?→?); + #H destruct (H) cases (is_endc c) in Hcend; normalize #H destruct (H) // ] + ] |#intape #outtape #ta * #Hcomp1 #Hcomp2 * #tb * * #Hc #Htb whd in ⊢ (%→?); #Hout >Hout >Htb whd lapply (current_to_midtape sig (nth src ? intape (niltape ?))) @@ -436,11 +443,8 @@ lemma sem_match_step : ] ] ] +qed. -2:#t1 #t2 #t3 whd in ⊢ (%→?); * #Hc #H #H1 whd #ls #c #rs #Ht1 % - [lapply(Hc c ?) [>Ht1 %] #Hgrid @injective_notb @Hgrid |>H1 @H] - - -- 2.39.2