-definition copy ≝ λsrc,dst,sig,n.
- whileTM … (copy_step src dst sig n) copy1.
-
-definition R_copy ≝
- λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
- ((current ? (nth src ? int (niltape ?)) = None ? ∨
- current ? (nth dst ? int (niltape ?)) = None ?) → outt = int) ∧
- (∀ls,x,x0,rs,ls0,rs0.
- nth src ? int (niltape ?) = midtape sig ls x rs →
- nth dst ? int (niltape ?) = midtape sig ls0 x0 rs0 →
- (∃rs01,rs02.rs0 = rs01@rs02 ∧ |rs01| = |rs| ∧
- outt = change_vec ??
- (change_vec ?? int
- (mk_tape sig (reverse sig rs@x::ls) (None sig) []) src)
- (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs02)
- (tail sig rs02)) dst) ∨
- (∃rs1,rs2.rs = rs1@rs2 ∧ |rs1| = |rs0| ∧
- outt = change_vec ??
- (change_vec ?? int
- (mk_tape sig (reverse sig rs1@x::ls) (option_hd sig rs2)
- (tail sig rs2)) src)
- (mk_tape sig (reverse sig rs1@x::ls0) (None sig) []) dst)).
+definition FSUnialpha ≝
+ mk_FinSet DeqUnialpha [bit true;bit false;bar]
+ unialpha_unique unialpha_complete.
+
+(*************************** testing characters *******************************)
+definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
+definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
+
+definition obj ≝ 0.
+definition cfg ≝ 1.
+definition prg ≝ 2.
+
+definition obj_to_cfg ≝
+ mmove cfg FSUnialpha 2 L ·
+ mmove cfg FSUnialpha 2 L ·
+ (ifTM ?? (inject_TM ? (test_null ?) 2 obj)
+ (inject_TM ? (write FSUnialpha (bit false)) 2 cfg ·
+ inject_TM ? (move_r FSUnialpha) 2 cfg ·
+ inject_TM ? (write FSUnialpha (bit false)) 2 cfg)
+ (inject_TM ? (write FSUnialpha (bit true)) 2 cfg ·
+ inject_TM ? (move_r FSUnialpha) 2 cfg ·
+ copy_step obj cfg FSUnialpha 2) tc_true ·
+ inject_TM ? (move_l FSUnialpha) 2 cfg) ·
+ inject_TM ? (move_to_end FSUnialpha L) 2 cfg ·
+ inject_TM ? (move_r FSUnialpha) 2 cfg.
+
+definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3.
+ ∀c,opt,ls.
+ nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::opt::ls) (None ?) [ ] →
+ (∀lso,x,rso.nth obj ? t1 (niltape ?) = midtape FSUnialpha lso x rso →
+ t2 = change_vec ?? t1
+ (mk_tape ? [ ] (option_hd ? (reverse ? (c::opt::ls))) (tail ? (reverse ? (c::opt::ls)))) cfg) ∧
+ (current ? (nth obj ? t1 (niltape ?)) = None ? →
+ t2 = change_vec ?? t1
+ (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (bit false::bit false::ls)))
+ (tail ? (reverse ? (bit false :: bit false::ls)))) cfg).
+
+axiom sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig.
+
+lemma sem_obj_to_cfg : obj_to_cfg ⊨ R_obj_to_cfg.
+@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
+ (sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?)
+ (sem_seq_app ???????
+ (sem_seq_app ???????
+ (sem_if ? 2 ????????
+ (sem_test_null_multi ?? obj ?)
+ (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))
+ (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
+ (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?) ?)
+ ?)
+ ??) ??) ?) ?)
+[|||||||||||||||| @
+
+ ??) ??) ??) ?) ?)
+ ?) ?) ?) ?)
+
+
+@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?) ??)
+[||
+@(sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?) ??)
+[|| @sem_seq_app
+[|| @sem_seq_app
+[|| @(sem_if ? 2 ???????? (sem_test_null_multi ?? obj ?))
+[|||@(sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?)
+[||@(sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
+ (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?)
+[||
+
+@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
+ (sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?)
+ (sem_seq_app ???????
+ (sem_if ? 2 ????????
+ (sem_test_null_multi ?? obj ?)
+ (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))
+ (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
+ (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?) ?)
+ ?)
+ (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
+ (sem_inject ???? cfg ? (sem_move_r ?)) ?) ?) ?) ?)
+