proposition: Fact MOVE_R_spec t : (i,MOVE_R) // (i, enc_tape t) ->> (END, enc_tape (mv Rmove t)).
proof: Proof. unfold MOVE_R. destruct t as [[ls c] rs]; destruct rs as [ | r rs], c as [ [] | ]. - bsm sss POP one with CURR (8 + i) (5 + i) []. bsm sss POP empty with RIGHT (14 + i) (12 + i). bsm sss PUSH with LEFT true. bsm sss POP empty with ZERO END END. bsm sss stop. - bsm sss POP zero with CURR (8 + i) (5 + i) []. bsm sss POP empty with RIGHT (21 + i) (19 + i). bsm sss PUSH with LEFT false. bsm sss POP empty with ZERO END END. bsm sss stop. - bsm sss POP empty with CURR (8 + i) (5 + i). bsm sss POP empty with RIGHT (17 + i) END. bsm sss stop. - bsm sss POP one with CURR (8 + i) (5 + i) []. destruct r. + bsm sss POP one with RIGHT (14 + i) (12 + i) rs. bsm sss PUSH with CURR true. bsm sss PUSH with LEFT true. bsm sss POP empty with ZERO END END. bsm sss stop. + bsm sss POP zero with RIGHT (14 + i) (12 + i) rs. bsm sss PUSH with CURR false. bsm sss PUSH with LEFT true. bsm sss POP empty with ZERO END END. bsm sss stop. - bsm sss POP zero with CURR (8 + i) (5 + i) []. destruct r. + bsm sss POP one with RIGHT (21 + i) (19 + i) rs. bsm sss PUSH with CURR true. bsm sss PUSH with LEFT false. bsm sss POP empty with ZERO END END. bsm sss stop. + bsm sss POP zero with RIGHT (21 + i) (19 + i) rs. bsm sss PUSH with CURR false. bsm sss PUSH with LEFT false. bsm sss stop. - bsm sss POP empty with CURR (8 + i) (5 + i). destruct r. + bsm sss POP one with RIGHT (17 + i) END rs. bsm sss PUSH with CURR true. bsm sss POP empty with ZERO END END. bsm sss stop. + bsm sss POP zero with RIGHT (17 + i) END rs. bsm sss PUSH with CURR false. bsm sss POP empty with ZERO END END. bsm sss stop. Qed.
imports: Undecidability.TM.KOSBTM.KOSBTM Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(bsm_defs)