From: Wilmer Ricciotti Date: Mon, 4 Feb 2013 16:18:55 +0000 (+0000) Subject: state mte2 renamed to mte_acc X-Git-Tag: make_still_working~1280 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=288c13921e7a8b7df6f66b3f3e67145d13464e67;p=helm.git state mte2 renamed to mte_acc --- diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma index a904414fa..a3af6106c 100644 --- a/matita/matita/lib/turing/multi_universal/moves_2.ma +++ b/matita/matita/lib/turing/multi_universal/moves_2.ma @@ -324,12 +324,12 @@ definition R_mte_step_true ≝ λalpha,D,t1,t2. definition R_mte_step_false ≝ λalpha.λt1,t2:tape alpha. current ? t1 = None ? ∧ t1 = t2. -definition mte2 : ∀alpha,D.states ? (mte_step alpha D) ≝ +definition mte_acc : ∀alpha,D.states ? (mte_step alpha D) ≝ λalpha,D.(inr … (inl … (inr … start_nop))). lemma sem_mte_step : ∀alpha,D.mte_step alpha D ⊨ - [ mte2 … : R_mte_step_true alpha D, R_mte_step_false alpha ] . + [ mte_acc … : R_mte_step_true alpha D, R_mte_step_false alpha ] . #alpha #D #ta @(acc_sem_if_app ??????????? (sem_test_null …) (sem_move_single …) (sem_nop alpha) ??) @@ -342,7 +342,7 @@ lemma sem_mte_step : | #tb #tc #td * #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd % // ] qed. -definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) (mte2 …). +definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) (mte_acc …). definition R_move_to_end_r ≝ λsig,int,outt.