From 388c27d3b8aab39c4c0d23b118b47f75144293d6 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 29 Jan 2013 10:46:18 +0000 Subject: [PATCH] Proved old axiom. --- matita/matita/lib/turing/inject.ma | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma index 0e9ffe090..ecb854b4a 100644 --- a/matita/matita/lib/turing/inject.ma +++ b/matita/matita/lib/turing/inject.ma @@ -30,9 +30,16 @@ lapply (trans sig M) #trans #x lapply (trans x) * * #s #a #m % [ @s | % [ @a | @m ] ] qed. -axiom current_chars_change_vec: ∀sig,n,v,a,i. i < S n → +lemma current_chars_change_vec: ∀sig,n,v,a,i. i < S n → current_chars sig ? (change_vec ? (S n) v a i) = change_vec ? (S n)(current_chars ?? v) (current ? a) i. +#sig #n #v #a #i #Hi @(eq_vec … (None ?)) #i0 #Hi0 +change with (vec_map ?????) in match (current_chars ???); +<(nth_vec_map … (niltape ?)) +cases (decidable_eq_nat i i0) #Hii0 +[ >Hii0 >nth_change_vec // >nth_change_vec // +| >nth_change_vec_neq // >nth_change_vec_neq // @nth_vec_map ] +qed. lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n → ∀M,v,s,a,sn,an,mn. -- 2.39.2