proposition: Fact sss_step_dec P st1 st2 : { P // st1 :1> st2 } + { ~ P // st1 :1> st2 }.
proof: Proof. Proof using sss_fun sss_dec. destruct st1 as (j,d). destruct P as (k,ll). destruct (le_lt_dec k j) as [ H1 | H1 ]. + destruct (le_lt_dec (S j) (k+length ll)) as [ H2 | H2 ]. * destruct (@list_pick _ ll (j-k)) as (i & l & r & ? & ?). - lia. - assert (j = k+length l) by lia; subst. destruct (sss_dec i (k+length l,d) st2) as [ | C ]. ++ left; apply in_sss_step; auto. ++ right; contradict C. destruct C as (k1 & l1 & i1 & r1 & d1 & H3 & H4 & H5). inversion H3; subst. inversion H4; subst. apply list_app_inj in H7 as (-> & H7); try lia. inversion H7; subst; auto. * right; intros (k1 & l1 & i1 & r1 & d1 & H3 & H4 & H5). inversion H3; subst. inversion H4; subst. rewrite app_length in H2; simpl in H2; lia. + right; intros (k1 & l1 & i1 & r1 & d1 & H3 & H4 & H5). inversion H3; subst. inversion H4; subst. lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)