λ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.
| whd in ⊢ (??%%→?); #H destruct (H)]
| #_ % //]
]
-qed.
-
\ No newline at end of file
+qed.
\ No newline at end of file