proposition: Theorem sss_loop_sound x : pre x -> (exists n, C2 (iter f x n)) -> exists n y, P // (i,x) ->> (p,y) /\ spec (iter f x n) y.
proof: Proof. Proof using HP1 HP2 HC. intros H (n & Hn); revert x H Hn. induction n as [ | n IHn ]; intros x Hx Hn. simpl; exists 0; apply HP2; auto. destruct (HC Hx) as [ H | H ]. apply IHn in Hn. destruct Hn as (m & y & H1 & H2). exists (S m), y; split; auto. generalize H1; apply sss_compute_trans. apply HP1; auto. apply HP1; auto. destruct (HP2 Hx) as (y & H1 & H2); auto. exists 0, y; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)