more porting to machines that can move without writing

[helm.git] / matita / matita / lib / turing / multi_universal / par_test.ma

diff --git a/matita/matita/lib/turing/multi_universal/par_test.ma b/matita/matita/lib/turing/multi_universal/par_test.ma
index 615efdc2e9dd2de576922a0233fc776dd8331a43..1ab0e34a4572e4eb9980db3dfec342cecc52386a 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/par_test.ma
+++ b/matita/matita/lib/turing/multi_universal/par_test.ma
@@ -39,31 +39,29 @@ definition R_partest_false ≝
   λsig,n,test.λint,outt: Vector (tape sig) (S n).
   test (current_chars ?? int) = false ∧ outt = int.
 
-axiom partest_q0_q1:
+lemma partest_q0_q1:
   ∀sig,n,test,v.
   test (current_chars ?? v) = true → 
   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
     = mk_mconfig ??? partest1 v.
-(*#sig #n #test #v #Htest
+#sig #n #test #v #Htest
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 @eq_f2
 [ whd in ⊢ (??(???%)?); >Htest %
-| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
-qed.*)
+| whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
+qed.
 
-axiom partest_q0_q2:
+lemma partest_q0_q2:
   ∀sig,n,test,v.
   test (current_chars ?? v) = false → 
   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
     = mk_mconfig ??? partest2 v.
-(*
 #sig #n #test #v #Htest
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 @eq_f2
 [ whd in ⊢ (??(???%)?); >Htest %
-| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
 qed.
-*)
 
 lemma sem_partest:
   ∀sig,n,test.
@@ -80,5 +78,4 @@ cases (true_or_false (test (current_chars ?? int))) #Htest
       | whd in ⊢ (??%%→?); #H destruct (H)]
   | #_ % //]
 ]
-qed.
-     
\ No newline at end of file
+qed.
\ No newline at end of file