definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
-definition swap ≝
+definition swap_r ≝
λalpha:FinSet.λfoo:alpha.
mk_TM alpha (swap_states alpha)
(λp.let 〈q,a〉 ≝ p in
t1 = midtape alpha ls b (a::rs) →
t2 = midtape alpha ls a (b::rs).
-lemma sem_swap : ∀alpha,foo.
- swap alpha foo ⊨ Rswap alpha.
+lemma sem_swap_r : ∀alpha,foo.
+ swap_r alpha foo ⊨ Rswap alpha.
#alpha #foo *
[@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
% [% |#a #b #ls #rs #H destruct]
]
qed.
-definition swap_r ≝
+definition swap_l ≝
λalpha:FinSet.λfoo:alpha.
mk_TM alpha (swap_states alpha)
(λp.let 〈q,a〉 ≝ p in
let 〈q',b〉 ≝ q in
- let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *)
+ let q' ≝ pi1 nat (λi.i<4) q' in
match a with
[ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
| Some a' ⇒
〈swap0,foo〉
(λq.\fst q == swap3).
-definition Rswap_r ≝
+definition Rswap_l ≝
λalpha,t1,t2.
∀a,b,ls,rs.
t1 = midtape alpha (a::ls) b rs →
t2 = midtape alpha (b::ls) a rs.
-lemma sem_swap_r : ∀alpha,foo.
- swap_r alpha foo ⊨ Rswap_r alpha.
+lemma sem_swap_l : ∀alpha,foo.
+ swap_l alpha foo ⊨ Rswap_l alpha.
#alpha #foo *
[@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
% [% |#a #b #ls #rs #H destruct]
+++ /dev/null
-include "turing/turing.ma".
-
-(*
-Simboli:
-0 1 *0 *1 # | ,
-
-[lista di simboli] fa match su un simbolo qualunque nella lista
-ad esempio [#|,] fa match con la gratella "#", la barra verticale "|" e la virgola ","
-
-Convenzione variabili:
-- x,y,z,D = bit (non marcati)
-- *x,*y,*z,*D = bit marcati
-- c,d,e = caratteri (bit marcati e non marcati e separatori)
-
-Convenzioni mosse:
-c/D --> Q : leggo c, scrivo c, mi sposto a D e passo allo stato Q
-c/d/D --> Q : leggo c, scrivo d, mi sposto a D e passo allo stato Q
-
-*)
-
-inductive alpha_uni : Type[0] ≝
-| bit : bool → alpha_uni
-| mark : bool → alpha_uni
-| grid : alpha_uni | bar : alpha_uni | comma : alpha_uni.
-
-inductive Qmatch : Type[0] ≝
-| qm0 : Qmatch | qm1 : Qmatch | qm2 : bool → Qmatch | qm3 : bool → Qmatch
-| qm4 : Qmatch | qm5 : Qmatch | qm6 : Qmatch | qm7 : Qmatch
-| qm8 : Qmatch | qm9 : Qmatch
-| qmsuccess : Qmatch | qmfailure : Qmatch | qmsink : Qmatch.
-
-definition bool_eqb ≝ λb1,b2:bool.¬ (xorb b1 b2).
-
-(*
-==================================
-MACCHINE PER SPOSTARE LA "TESTINA"
-================================
-
-Lo spostamento a sx si ottiene mediante
-
-ls x # current y # macchina # rs
-----C--->
-ls x # current # y macchina # rs
-----B--->
-ls x # current # macchina # y rs
-----B--->
-ls # x current # macchina # y rs
-----C--->
-ls # current x # macchina # y rs
-
-
-Lo spostamento a dx si ottiene mediante
-
-ls # current x # macchina # y rs
-----A--->
-ls x # current # macchina # y rs
-----A--->
-ls x # current # macchina y # rs
-----A--->
-ls x # current y # macchina # rs
-
-
-MACCHINA A
-----------
-Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
-
-Input:
-
- ls # cs x rs
- ^
- 0
-
-Output:
- ls x # cs rs
- ^
- 4
-
-STATO 0:
- \forall x.x/L --> 1(x)
-
-STATO 1(x):
- \forall c != #. c/x/R --> 2(c)
- #/x/R --> 3
-
-STATO 2(c):
- \forall d. d/c/L --> 0
-
-STATO 3:
- \forall c. c/#/L --> 4
-
-STATO 4:
- stato finale
-*)
-
-(* struttura generica della semantica *)
-lemma move_char_sem: ∀inc. prec inc → ∃i. ∃outc. loop i step inc = Some outc
-∧ postc outc inc.
-
-lemma sequential : ∀M1,M2.
-
-definition pre c ≝
- let s ≝ state c in
- let tp ≝ tape c in
- let left ≝
-
-definition post c1 c2 ≝
- let s1 ≝ state c1 in
- let tp1 ≝ tape c1 in
- let leftt ≝ left tp1 in
- let rightt ≝ right tp1 in
- c2 = mk_config finals
-
-
-
-match s with
- [ q0 ⇒ match c with
- [ bit x ⇒ 〈q1 x,〈c,L〉〉
- | _ ⇒ 〈qsink,〈c,N〉〉 ]
- | q1 x ⇒ match c with
- [ grid ⇒ 〈q3,〈bit x,R〉〉
- | _ ⇒ 〈q2 c,〈bit x,R〉〉 ]
- | q2 d ⇒ 〈q0,〈d,L〉〉
- | q3 ⇒ 〈q4,〈grid,L〉〉
- | q4 ⇒ (* finale *) ].
-
-(*
-MACCHINA B
-----------
-Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
-
-Input:
-
- ls x cs # rs
- ^
- 0
-
-Output:
- ls cs # x rs
- ^
- 4
-
-STATO 0:
- \forall x.x/R --> 1(x)
-
-STATO 1(x):
- \forall c != #. c/x/L --> 2(c)
- #/x/L --> 3
-
-STATO 2(c):
- \forall d. d/c/R --> 0
-
-STATO 3:
- \forall c. c/#/L --> 4
-
-STATO 4:
- stato finale
-*)
-
-match s with
-[ q0 ⇒ match c with
- [ bit x ⇒ 〈q1 x,〈c,R〉〉
- | _ ⇒ 〈qsink,〈c,N〉〉]
-| q1 x ⇒ match c with
- [ grid ⇒ 〈q3,〈bit x,L〉〉
- | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
-| q2 d ⇒ 〈q0,〈d,R〉〉
-| q3 ⇒ 〈q4,〈grid,L〉〉
-| q4 ⇒ (* finale *) ].
-
-(*
-MACCHINA C
-----------
-Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
-
-Input:
- ls x cs # rs
- ^
- 0
-
-Output:
- ls cs x # rs
- ^
- 3
-
-STATO 0:
- \forall x. x/R --> 1(x)
-
-STATO 1(x):
- \forall c != #. c/x/L --> 2(c)
- #/#/L --> 3
-
-STATO 2(c):
- \forall d. d/c/R --> 0
-
-STATO 3:
- stato finale
-
-*)
-
-match s with
-[ q0 ⇒ match c with
- [ bit x ⇒ 〈q1 x,〈c,R〉〉
- | _ ⇒ 〈qsink,〈c,N〉〉 ]
-| q1 x ⇒ match c with
- [ grid ⇒ 〈q3,〈grid,L〉〉
- | _ ⇒ 〈q2 c,〈bit x,L〉〉
-| q2 d ⇒ 〈q0,〈c,R〉〉
-| q3 ⇒ (* finale *) ].
(λs.match s with
[ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
-notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
+notation "a · b" right associative with precedence 65 for @{ 'middot $a $b}.
interpretation "sequential composition" 'middot a b = (seq ? a b).
definition lift_confL ≝
include "turing/basic_machines.ma".
include "turing/if_machine.ma".
-definition mcc_step ≝ λalpha:FinSet.λsep:alpha.
+definition mcr_step ≝ λalpha:FinSet.λsep:alpha.
ifTM alpha (test_char ? (λc.¬c==sep))
- (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true.
+ (single_finalTM … (swap_l alpha sep · move_r ?)) (nop ?) tc_true.
-definition Rmcc_step_true ≝
+definition Rmcr_step_true ≝
λalpha,sep,t1,t2.
∀a,b,ls,rs.
t1 = midtape alpha (a::ls) b rs →
b ≠ sep ∧
t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
-definition Rmcc_step_false ≝
+definition Rmcr_step_false ≝
λalpha,sep,t1,t2.
left ? t1 ≠ [] → current alpha t1 ≠ None alpha →
current alpha t1 = Some alpha sep ∧ t2 = t1.
-lemma sem_mcc_step :
+lemma sem_mcr_step :
∀alpha,sep.
- mcc_step alpha sep ⊨
- [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep].
+ mcr_step alpha sep ⊨
+ [inr … (inl … (inr … start_nop)): Rmcr_step_true alpha sep, Rmcr_step_false alpha sep].
#alpha #sep
@(acc_sem_if_app …
- (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …))
+ (sem_test_char …) (sem_seq …(sem_swap_l …) (sem_move_r …)) (sem_nop …))
[#intape #outtape #tapea whd in ⊢ (%→%→%);
#Htapea * #tapeb * whd in ⊢ (%→%→?);
#Htapeb #Houttape #a #b #ls #rs #Hintape
(* the move_char (variant c) machine *)
definition move_char_r ≝
- λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))).
+ λalpha,sep.whileTM alpha (mcr_step alpha sep) (inr … (inl … (inr … start_nop))).
definition R_move_char_r ≝
λalpha,sep,t1,t2.
∀alpha,sep.
WRealize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
#alpha #sep #inc #i #outc #Hloop
-lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
+lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%]
-Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
%
∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →
(b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_r alpha sep) t.
#alpha #sep #t #b #a #ls #rs #Ht #Hsep
-@(terminate_while … (sem_mcc_step alpha sep))
+@(terminate_while … (sem_mcr_step alpha sep))
[%
|generalize in match Hsep; -Hsep
generalize in match Ht; -Ht
definition mcl_step ≝ λalpha:FinSet.λsep:alpha.
ifTM alpha (test_char ? (λc.¬c==sep))
- (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true.
+ (single_finalTM … (swap_r alpha sep · move_l ?)) (nop ?) tc_true.
definition Rmcl_step_true ≝
λalpha,sep,t1,t2.
[mcls_acc alpha sep: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
#alpha #sep
@(acc_sem_if_app …
- (sem_test_char …) (sem_seq …(sem_swap …) (sem_move_l …)) (sem_nop …))
+ (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_l …)) (sem_nop …))
[#intape #outtape #tapea whd in ⊢ (%→%→%);
#Htapea * #tapeb * whd in ⊢ (%→%→?);
#Htapeb #Houttape #a #b #ls #rs #Hintape
definition adv_mark_r ≝
λalpha:FinSet.
- seq ? (clear_mark alpha)
- (seq ? (move_r ?) (mark alpha)).
+ clear_mark alpha · move_r ? · mark alpha.
definition R_adv_mark_r ≝ λalpha,t1,t2.
∀ls,c,d,b,rs.
^
*)
-definition adv_both_marks ≝
- λalpha.seq ? (adv_mark_r alpha)
- (seq ? (move_l ?)
- (seq ? (adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha))
- (adv_mark_r alpha))).
+definition adv_both_marks ≝ λalpha.
+ adv_mark_r alpha · move_l ? ·
+ adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) ·
+ adv_mark_r alpha.
definition R_adv_both_marks ≝
λalpha,t1,t2.
else M
*)
-definition comp_step_subcase ≝
- λalpha,c,elseM.ifTM ? (test_char ? (λx.x == c))
- (seq ? (move_r …)
- (seq ? (adv_to_mark_r ? (is_marked alpha))
- (match_and_adv ? (λx.x == c))))
+definition comp_step_subcase ≝ λalpha,c,elseM.
+ ifTM ? (test_char ? (λx.x == c))
+ (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
elseM tc_true.
definition R_comp_step_subcase ≝
*)
definition mark_next_tuple ≝
- seq ? (adv_to_mark_r ? bar_or_grid)
+ adv_to_mark_r ? bar_or_grid ·
(ifTM ? (test_char ? (λc:STape.is_bar (\fst c)))
(move_right_and_mark ?) (nop ?) tc_true).
qed.
definition init_current_on_match ≝
- (seq ? (move_l ?)
- (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_r ?) (mark ?)))).
+ move_l ? · adv_to_mark_l ? (λc:STape.is_grid (\fst c)) · move_r ? · mark ?.
definition R_init_current_on_match ≝ λt1,t2.
∀l1,l2,c,rs. no_grids l1 → is_grid c = false →
*)
definition init_current ≝
- seq ? (adv_to_mark_l ? (is_marked ?))
- (seq ? (clear_mark ?)
- (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_r ?) (mark ?)))).
+ adv_to_mark_l ? (is_marked ?) ·clear_mark ? ·
+ adv_to_mark_l ? (λc:STape.is_grid (\fst c)) · move_r ? · mark ?.
definition R_init_current ≝ λt1,t2.
∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 → is_grid c = false →
definition match_tuple_step ≝
ifTM ? (test_char ? (λc:STape.¬ is_grid (\fst c)))
(single_finalTM ?
- (seq ? compare
+ (compare ·
(ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
(nop ?)
- (seq ? mark_next_tuple
+ (mark_next_tuple ·
(ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
- (mark ?) (seq ? (move_l ?) init_current) tc_true)) tc_true)))
+ (mark ?) (move_l ? · init_current) tc_true)) tc_true)))
(nop ?) tc_true.
definition R_match_tuple_step_true ≝ λt1,t2.
(* l1 # l2 r ---> l1 r # l2
^ ^
*)
-definition mtr_aux ≝
- seq ? (move_l …) (seq ? (move_char_l STape 〈grid,false〉)
- (swap STape 〈grid,false〉)).
-definition R_mtr_aux ≝ λt1,t2.
+definition move_after_left_bar ≝
+ move_l … · move_char_l STape 〈grid,false〉 · swap_r STape 〈grid,false〉.
+
+definition R_move_after_left_bar ≝ λt1,t2.
∀l1,l2,l3,r. t1 = midtape STape (l2@〈grid,false〉::l1) r l3 → no_grids l2 →
t2 = midtape STape l1 r (〈grid,false〉::reverse ? l2@l3).
-lemma sem_mtr_aux : Realize ? mtr_aux R_mtr_aux.
+lemma sem_move_after_left_bar : Realize ? move_after_left_bar R_move_after_left_bar.
#intape
cases (sem_seq … (sem_move_l …) (sem_seq … (ssem_move_char_l STape 〈grid,false〉)
- (sem_swap STape 〈grid,false〉)) intape)
+ (sem_swap_r STape 〈grid,false〉)) intape)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#l1 #l2 #l3 #r #Hintape #Hl2
cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
qed.
definition move_tape_r ≝
- seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
- (seq ? (swap STape 〈grid,false〉)
- (seq ? mtr_aux (seq ? (move_l …) (seq ? mtr_aux (move_r …))))))).
+ move_r … · init_cell · move_l … · swap_r STape 〈grid,false〉 ·
+ move_after_left_bar · move_l … · move_after_left_bar · move_r ….
definition R_move_tape_r ≝ λt1,t2.
∀rs,n,table,c0,bc0,curconfig,ls0.
lemma sem_move_tape_r : Realize ? move_tape_r R_move_tape_r.
#tapein
cases (sem_seq …(sem_move_r …) (sem_seq … sem_init_cell (sem_seq … (sem_move_l …)
- (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … sem_mtr_aux
- (sem_seq … (sem_move_l …) (sem_seq … sem_mtr_aux (sem_move_r …))))))) tapein)
+ (sem_seq … (sem_swap_r STape 〈grid,false〉) (sem_seq … sem_move_after_left_bar
+ (sem_seq … (sem_move_l …) (sem_seq … sem_move_after_left_bar (sem_move_r …))))))) tapein)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Htapein
cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein) -Hta #Hta
^
*)
definition mtl_aux ≝
- seq ? (swap STape 〈grid,false〉)
- (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)))).
+ swap_r STape 〈grid,false〉 · move_r … · move_r … ·
+ move_char_r STape 〈grid,false〉 · move_l ….
definition R_mtl_aux ≝ λt1,t2.
∀l1,l2,l3,r. t1 = midtape STape l1 r (〈grid,false〉::l2@〈grid,false〉::l3) → no_grids l2 →
t2 = midtape STape (reverse ? l2@〈grid,false〉::l1) r (〈grid,false〉::l3).
lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
#intape
-cases (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … (sem_move_r …)
+cases (sem_seq … (sem_swap_r STape 〈grid,false〉) (sem_seq … (sem_move_r …)
(sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉)
(sem_move_l …)))) intape)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
qed.
definition move_tape_l : TM STape ≝
- seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
- (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
- (seq ? (move_l …)
- (seq ? init_cell
- (seq ? mtl_aux
- (seq ? (swap_r STape 〈grid,false〉)
- (seq ? mtl_aux
- (seq ? (swap STape 〈grid,false〉)
- (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
- (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))))))))))).
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+ move_l … · init_cell · mtl_aux · swap_l STape 〈grid,false〉 ·
+ mtl_aux ·swap_r STape 〈grid,false〉 ·
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))).
(* seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
(seq ? (swap STape 〈grid,false〉)
- (seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *)
+ (seq ? move_after_left_bar (seq ? (move_l …) move_after_left_bar))))). *)
definition R_move_tape_l ≝ λt1,t2.
∀rs,n,table,c0,bc0,curconfig,ls0.
(sem_seq … (sem_move_l …)
(sem_seq … sem_init_cell
(sem_seq … sem_mtl_aux
- (sem_seq … (sem_swap_r STape 〈grid,false〉)
+ (sem_seq … (sem_swap_l STape 〈grid,false〉)
(sem_seq … sem_mtl_aux
- (sem_seq … (sem_swap STape 〈grid,false〉)
+ (sem_seq … (sem_swap_r STape 〈grid,false〉)
(sem_seq … sem_ml_atml sem_ml_atml)))))))) tapein)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Hls0 #Htapein
[ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
| _ ⇒ N ].
-definition R_uni_step ≝ λt1,t2.
- ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
- table_TM n table →
- match_in_table n (〈c,false〉::curs) 〈curc,false〉
- (〈c1,false〉::news) 〈newc,false〉 〈mv,false〉 table →
- t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉
- (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) →
- ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs →
- (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉
- (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
- lift_tape ls1 〈newc,false〉 rs1 =
- tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
-
definition no_nulls ≝
λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
ifTM ? (test_char ? (λc:STape.c == 〈bit false,false〉))
(* spostamento a sinistra: verificare se per caso non conviene spostarsi
sulla prima grid invece dell'ultima *)
- (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_l)
+ (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_l)
(ifTM ? (test_char ? (λc:STape.c == 〈bit true,false〉))
- (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_r)
- (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_l …) (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))
+ (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_r)
+ (adv_to_mark_l ? (λc:STape.is_grid (\fst c)) ·
+ move_l … · adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
tc_true) tc_true.
definition R_move_tape ≝ λt1,t2.
*)
definition init_match ≝
- seq ? (mark ?)
- (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_r ?)
- (seq ? (move_r ?)
- (seq ? (mark ?)
- (seq ? (move_l ?)
- (adv_to_mark_l ? (is_marked ?))))))).
+ mark ? · adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_r ? ·
+ move_r ? · mark ? · move_l ? · adv_to_mark_l ? (is_marked ?).
definition R_init_match ≝ λt1,t2.
∀ls,l,rs,c,d. no_grids (〈c,false〉::l) → no_marks l →
>associative_append %
qed.
-
(* init_copy
init_current_on_match; (* no marks in current *)
*)
definition init_copy ≝
- seq ? init_current_on_match
- (seq ? (move_r ?)
- (seq ? (adv_to_mark_r ? (is_marked ?))
- (adv_mark_r ?))).
+ init_current_on_match · move_r ? ·
+ adv_to_mark_r ? (is_marked ?) · adv_mark_r ?.
definition R_init_copy ≝ λt1,t2.
∀l1,l2,c,ls,d,rs.
qed. *)
definition exec_action ≝
- seq ? init_copy
- (seq ? copy
- (seq ? (move_r …) move_tape)).
+ init_copy · copy · move_r … · move_tape.
definition map_move ≝
λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
definition uni_step ≝
ifTM ? (test_char STape (λc.\fst c == bit false))
- (single_finalTM ? (seq ? init_match
- (seq ? match_tuple
+ (single_finalTM ?
+ (init_match · match_tuple ·
(ifTM ? (test_char ? (λc.¬is_marked ? c))
- (seq ? exec_action (move_r …))
- (nop ?) (* sink *)
- tc_true))))
- (nop ?)
- tc_true.
+ (exec_action · move_r …)
+ (nop ?) tc_true)))
+ (nop ?) tc_true.
definition R_uni_step_true ≝ λt1,t2.
∀n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
projects / helm.git / commitdiff