proposition: Fact pctm_sss_total ρ s : { s' | ρ // s -1> s' }.
proof: Proof. destruct s as (i,t). destruct ρ as [ d | b | j p ]. + exists (1+i,mv d t); constructor. + destruct t as ((l,x),r). exists (1+i,(l,b,r)); constructor. + destruct t as ((l,b),r). exists (if b then j else p,(l,b,r)); constructor. Qed.
imports: List Bool Arith Lia Undecidability.Shared.Libs.DLW(subcode sss) Undecidability.TM(SBTM)