proposition: Theorem decode_string_lt : forall len (lt_len : lt 0 len) (b3 : B) (cd0 : CacheDecode) (a : string) (b' : B) (cd' : CacheDecode), decode_string len b3 cd0 = Some (a, b', cd') -> lt_B b' b3.
proof: Proof. induction len; simpl; intros; try omega. destruct (decode_ascii b3 cd0) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate. eapply ascii_decode_lt in Heqo. destruct (decode_string len b c) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate. injections. inversion lt_len; subst; simpl in *. - injections; eauto. - eapply IHlen in Heqo0; eauto; unfold lt_B in *; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.AsciiOpt Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String