proposition: Fact sbtm_op_spec t t' : let o := if rd t then o1 else o0 in let d := if rd t then d1 else d0 in let b := if rd t then b1 else b0 in let j := if rd t then j1 else j0 in t' = mv d (wr t b) -> (i,sbtm_op) // (i,t) -+> if o then (j,t') else (k,t).
proof: Proof. intros o d b j ->. unfold sbtm_op. destruct t as ((l,[]),r); simpl in * |-; unfold d, b, j, o in *; clear d b j o. + pctm sss BR with (1+i) (5+i); simpl rd. pctm sss JMP with (if o1 then 2+i else k). destruct o1; cbv match. * pctm sss WR with b1. pctm sss MV with d1. pctm sss JMP with j1. pctm sss stop. * pctm sss stop. + pctm sss BR with (1+i) (5+i); simpl rd. pctm sss JMP with (if o0 then 6+i else k). destruct o0; cbv match. * pctm sss WR with b0. pctm sss MV with d0. pctm sss JMP with j0. pctm sss stop. * pctm sss stop. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)