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 04c4fe79dc23d194a9bd462440e8257a043ba8a5..1ab0e34a4572e4eb9980db3dfec342cecc52386a 100644 (file)
--- 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