X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fpar_test.ma;h=1ab0e34a4572e4eb9980db3dfec342cecc52386a;hb=a1dd5e64f21738a3f9ee1f635affeb9033e90954;hp=615efdc2e9dd2de576922a0233fc776dd8331a43;hpb=3f37ee83ce3c43f34d38729d192e72510f998a53;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/par_test.ma b/matita/matita/lib/turing/multi_universal/par_test.ma
index 615efdc2e..1ab0e34a4 100644
--- 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