proposition: Lemma CorrectEncoder_Fix' (encode_body : EncodeM S T -> EncodeM S T) (format_body : FormatM S T -> FormatM S T) (format_body_OK : Frame.monotonic_function (format_body : funType [S; CacheFormat] (T * CacheFormat) -> funType [S; CacheFormat] (T * CacheFormat))) (measure : S -> nat) (encode_body_correct : forall n encode, (CorrectEncoder (Restrict_Format (fun s => measure s < n) (Fix_Format format_body)) encode) -> CorrectEncoder (Restrict_Format (fun s => measure s < Datatypes.S n) (format_body (Fix_Format format_body))) (encode_body encode)) : forall n, CorrectEncoder (Restrict_Format (fun s => measure s < n) (Fix_Format format_body)) (FueledFix' encode_body n).
proof: Proof. induction n; simpl; intros. - split; unfold Restrict_Format, Compose_Format; intros. + discriminate. + intro H'; rewrite @unfold_computes in H'; destruct_ex; omega. - split; unfold Restrict_Format, Compose_Format in *; intros. + apply unfold_computes; intuition eauto. eapply encode_body_correct in H; eauto. rewrite @unfold_computes in H; destruct_ex; split_and. apply_in_hyp (unroll_LeastFixedPoint' format_body_OK); eauto. + intro H'; rewrite unfold_computes in H'. eapply encode_body_correct in H; eauto; eapply H. destruct_ex; split_and. apply unfold_computes. eexists; subst; intuition eauto. eapply (unroll_LeastFixedPoint format_body_OK); eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.Base.FMapFormat Fiat.Computation.FixComp