-
-
- cut ((mk_tape FSUnialpha []
- (option_hd FSUnialpha
- (reverse FSUnialpha (m0::[]@reverse FSUnialpha (sn@[cn])@[fn; bar])))
- (tail FSUnialpha
- (reverse FSUnialpha (m0::[]@reverse FSUnialpha (sn@[cn])@[fn; bar])))) =
- midtape ? [ ] bar (fn::sn@[cn;m0]))
- [cut (reverse FSUnialpha (m0::[]@reverse FSUnialpha (sn@[cn])@[fn; bar]) =
- bar::fn::sn@[cn;m0])
- [>reverse_cons whd in ⊢ (??(??(??%)?)?); >reverse_append >reverse_reverse
- >append_cons in ⊢ (???%); % ] #Hrev >Hrev % ] #Hmk_tape >Hmk_tape -Hmk_tape
- >change_vec_commute
-
- >reverse_append >reverse_append
- check reverse_cons
- <reverse_cons >reverse_cons
- -Htg #Htg
-
->(change_vec_commute ????? cfg prg) [2:@eqb_false_to_not_eq %]
->nth_change_vec_neq [2:@eqb_false_to_not_eq %]
->nth_change_vec_neq [2:@eqb_false_to_not_eq %]
-lapply (append_l1_injective ?????? Hrs1rs2)
-[ >Hsnlen >Hrs1len >length_append >length_append >length_append >length_append
- normalize >Hsolen >Hsnlen % ]
-#Hrs1 <Hrs1 >reverse_append #Htg cases (Htg ?? (refl ??)) -Htg
-cases m0
- [#mv #_ #Htg #_
-
-
-
-
-
-[ *
-
- match_m cfg prg FSUnialpha 2 ·
- restart_tape cfg · copy prg cfg FSUnialpha 2 ·
- cfg_to_obj · tape_move_obj · restart_tape prg · obj_to_cfg.
-