proposition: Lemma sss_terminates_mma_f_ind {T : Type} {n : nat} (f : T -> (mm_state n)) (P : nat * list (mm_instr (pos n))) (R : T -> Prop) : (forall t, out_code (fst (f t)) P -> R t) -> (forall t1, (forall t2, sss_progress (mma_sss (n:=n)) P (f t1) (f t2) -> R t2) -> R t1) -> forall t, sss_terminates (mma_sss (n:=n)) P (f t) -> R t.
proof: Proof. move=> H1 H2 t. move Et: (f t) => st Hst. pose R' := fun st' => forall t', f t' = st' -> R t'. suff: R' st by apply. move: Hst. apply: sss_terminates_ind. - by apply: mma_defs.mma_sss_fun. - move=> st' Hst' t' Ht'. apply: H1. by rewrite Ht'. - move=> st1' Hst1' t1' Ht1'. apply: H2. move=> t2'. rewrite Ht1' => /Hst1'. by apply; [apply: subcode_refl|]. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun