proposition: Theorem sss_loop_complete x y q : pre x -> out_code q P -> P // (i,x) ->> (q,y) -> p = q /\ exists n, C2 (iter f x n) /\ spec (iter f x n) y.
proof: Proof. Proof using sss_fun HP1 HP2 HC Hp Hf. intros Hx Hq (k & Hk); revert x Hx y q Hq Hk. induction k as [ k IHk ] using (well_founded_induction lt_wf); intros x Hx y q Hq Hk. destruct (HC Hx) as [ H | H ]. * apply HP1 in H; auto; destruct H as [ H1 H2 ]. destruct (@sss_compute_step_out_inv P k (i,x) (i,f x) (q,y)) as (k' & H3 & H4); auto. { inversion 1 as [ H3 ]; revert H3; apply Hf. } destruct IHk with (2 := H2) (4 := H4) as (E & n & Hn); auto. split; auto; exists (S n); auto. * destruct HP2 with (2 := H) as (z & Hz & Hy); auto. apply ex_intro with (x := k) in Hk. generalize (@sss_compute_fun _ _ (p,z) (q,y) Hp Hq Hz Hk). inversion 1; subst; auto. split; auto. exists 0; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)