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=e461bb10382fe2ea65bd37dd56be46c6aec67db7;hp=04c4fe79dc23d194a9bd462440e8257a043ba8a5;hpb=4854493daa451ed14c980665f9901cd8a9dc5fbe;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 04c4fe79d..1ab0e34a4 100644
--- a/matita/matita/lib/turing/multi_universal/par_test.ma
+++ b/matita/matita/lib/turing/multi_universal/par_test.ma
@@ -48,7 +48,7 @@ lemma partest_q0_q1:
 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 partest_q0_q2:
@@ -60,7 +60,7 @@ lemma partest_q0_q2:
 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:
@@ -78,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