Require Import List.
Import ListNotations.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import ZArith.

Require Import QuickChick.Show.

(* Proof that Show for string round-trips. *)

Lemma not_digit_when (c : ascii) (x : nat) :
  (nat_of_ascii c < 48) \/ (57 < nat_of_ascii c) ->
  unit_digit x <> c.
Proof.
(* Goal: forall _ : or (lt (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))) (lt (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)), not (@eq ascii (unit_digit x) c) *)
  assert (mod_fact : x mod 10 < 10).
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
  { apply Nat.mod_upper_bound; auto. }
(* Goal: forall _ : or (lt (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))) (lt (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)), not (@eq ascii (unit_digit x) c) *)
  intros H e.
(* Goal: False *)
  unfold unit_digit in e.
(* Goal: False *)
  apply (f_equal nat_of_ascii) in e.
(* Goal: False *)
  rewrite nat_ascii_embedding in e.
(* Goal: le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
  intuition.
(* Goal: le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
  intuition.
Qed.

Lemma unit_digit_ascii :
  forall n, digit_of_ascii (unit_digit n) = Some (n mod 10).
Proof.
(* Goal: forall s : string, @eq (option string) (read_string (@show string showString s)) (@Some string s) *)
  intro.
  assert (mod_fact : n mod 10 < 10).
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
  { apply Nat.mod_upper_bound; auto. }
  unfold unit_digit.
  unfold digit_of_ascii.
  rewrite nat_ascii_embedding.
  replace (48 <=? n mod 10 + 48) with true.
  replace (n mod 10 + 48 <=? 57) with true.
  rewrite Nat.add_sub.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
  auto.
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
  { symmetry. apply leb_correct. intuition. }
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
  { symmetry. apply leb_correct. intuition. }
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
  { intuition. }
Qed.

Lemma decimal_thousand : forall n,
    n < 256 ->
    (n / 100) mod 10 * 100 + (n / 10) mod 10 * 10 + n mod 10 = n.
Admitted.

Lemma ascii_256 : forall c, nat_of_ascii c < 256.
Admitted.

Lemma unthree_three_digit (c : ascii) :
  let n := nat_of_ascii c in
  unthree_digit
    (unit_digit (n / 100)) (unit_digit (n / 10)) (unit_digit n)
  = Some (ascii_of_nat n).
Proof.
(* Goal: let n := nat_of_ascii c in @eq (option ascii) (unthree_digit (unit_digit (Nat.div n (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (Nat.div n (S (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit n)) (@Some ascii (ascii_of_nat n)) *)
  unfold unthree_digit.
(* Goal: @eq (option ascii) match digit_of_ascii (unit_digit (Nat.div (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with | Some n2 => match digit_of_ascii (unit_digit (Nat.div (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S O)))))))))))) with | Some n1 => match digit_of_ascii (unit_digit (nat_of_ascii c)) with | Some n0 => @Some ascii (ascii_of_nat (Init.Nat.add (Init.Nat.add (Init.Nat.mul n2 (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Init.Nat.mul n1 (S (S (S (S (S (S (S (S (S (S O)))))))))))) n0)) | None => @None ascii end | None => @None ascii end | None => @None ascii end (@Some ascii (ascii_of_nat (nat_of_ascii c))) *)
  do 3 rewrite unit_digit_ascii.
(* Goal: @eq (option ascii) (@Some ascii (ascii_of_nat (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Nat.modulo (Nat.div (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S O))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Init.Nat.mul (Nat.modulo (Nat.div (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S O))))))))))) (S (S (S (S (S (S (S (S (S (S O))))))))))) (S (S (S (S (S (S (S (S (S (S O)))))))))))) (Nat.modulo (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S O)))))))))))))) (@Some ascii (ascii_of_nat (nat_of_ascii c))) *)
  rewrite decimal_thousand.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
  auto.
(* Goal: lt (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
  apply ascii_256.
Qed.

Lemma read_show_quoted_string : forall (s : string),
    read_quoted_string (show_quoted_string s) = Some s.
Proof.
(* Goal: forall s : string, @eq (option string) (read_quoted_string (show_quoted_string s)) (@Some string s) *)
  induction 0.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
  - auto.
  - unfold show_quoted_string.
(* Goal: @eq (option string) (read_quoted_string (if ascii_dec a (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if orb (Nat.ltb (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii a)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii a)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s)) else String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    destruct (ascii_dec a "009") as [is_tab | isn_tab].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    { fold show_quoted_string.
(* Goal: @eq (option string) (read_string (@show string showString s)) (@Some string s) *)
      simpl.
(* Goal: @eq (option string) (@option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      rewrite IHs.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
      rewrite is_tab; auto.
    }
(* Goal: @eq (option string) (read_quoted_string (if ascii_dec a (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if orb (Nat.ltb (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii a)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii a)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s)) else String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    destruct (ascii_dec a "010") as [is_nl | isn_nl].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    { fold show_quoted_string.
(* Goal: @eq (option string) (@option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      simpl; rewrite IHs.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
      rewrite is_nl; auto.
    }
(* Goal: @eq (option string) (read_quoted_string (if ascii_dec a (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if orb (Nat.ltb (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii a)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii a)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s)) else String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    destruct (ascii_dec a "013") as [is_cr | isn_cr].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    { fold show_quoted_string.
(* Goal: @eq (option string) (@option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      simpl; rewrite IHs.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
      rewrite is_cr; auto.
    }
(* Goal: @eq (option string) (read_quoted_string (if ascii_dec a (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if ascii_dec a (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if orb (Nat.ltb (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii a)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii a)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s)) else String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    destruct (ascii_dec a """") as [is_dq | isn_dq].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    { fold show_quoted_string.
(* Goal: @eq (option string) (@option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      simpl; rewrite IHs.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
      rewrite is_dq; auto.
    }
(* Goal: @eq (option string) (read_quoted_string (if ascii_dec a (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s) else if orb (Nat.ltb (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii a)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii a)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s)) else String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    destruct (ascii_dec a "\") as [is_bs | isn_bs].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    { fold show_quoted_string.
(* Goal: @eq (option string) (@option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      simpl; rewrite IHs.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
      rewrite is_bs; auto.
    }
(* Goal: @eq (option string) (read_quoted_string (if orb (Nat.ltb (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii a)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii a)) ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s)) else String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    destruct ((nat_of_ascii a <? 32) || (126 <? nat_of_ascii a))%bool.
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    { fold show_quoted_string.
(* Goal: @eq (option string) (read_string (@show string showString s)) (@Some string s) *)
      simpl.
(* Goal: @eq (option string) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else match unthree_digit (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end) (@Some string (String a s)) *)
      destruct (ascii_dec _ "n") as [is_n2 | isn_n2].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
      { apply not_digit_when in is_n2. contradict is_n2.
(* Goal: le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
        compute. right. intuition.
      }
(* Goal: @eq (option string) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else match unthree_digit (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end) (@Some string (String a s)) *)
      destruct (ascii_dec _ "r") as [is_r2 | isn_r2].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
      { apply not_digit_when in is_r2. contradict is_r2.
(* Goal: le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
        compute. right. intuition.
      }
(* Goal: @eq (option string) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else match unthree_digit (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end) (@Some string (String a s)) *)
      destruct (ascii_dec _ "t") as [is_t2 | isn_t2].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
      { apply not_digit_when in is_t2. contradict is_t2.
(* Goal: le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
        compute. right. intuition.
      }
(* Goal: @eq (option string) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else match unthree_digit (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end) (@Some string (String a s)) *)
      destruct (ascii_dec _ "\") as [is_bs2 | isn_bs2].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
      { apply not_digit_when in is_bs2. contradict is_bs2.
(* Goal: le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
        compute. right; intuition.
      }
(* Goal: @eq (option string) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false true false false false true false false) then @None string else if ascii_dec (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (Ascii false false true true true false true false) then if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string (show_quoted_string s)) else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string (show_quoted_string s)) else match show_quoted_string s with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit (unit_digit (nat_of_ascii a)) c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end else @option_map string string (String (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O))))))))))))) (if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec (unit_digit (nat_of_ascii a)) (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String (unit_digit (nat_of_ascii a))) (read_quoted_string (show_quoted_string s)))) else match unthree_digit (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end) (@Some string (String a s)) *)
      destruct (ascii_dec _ """") as [is_dq2 | isn_dq2].
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
      { apply not_digit_when in is_dq2. contradict is_dq2.
(* Goal: le (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
        compute. left; intuition.
      }
(* Goal: @eq (option string) match unthree_digit (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) O (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end (@Some string (String a s)) *)
      fold (Nat.div (nat_of_ascii a) 100).
(* Goal: @eq (option string) match unthree_digit (unit_digit (Nat.div (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (@fst nat nat (Nat.divmod (nat_of_ascii a) (S (S (S (S (S (S (S (S (S O))))))))) O (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end (@Some string (String a s)) *)
      fold (Nat.div (nat_of_ascii a) 10).
(* Goal: @eq (option string) match unthree_digit (unit_digit (Nat.div (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (unit_digit (Nat.div (nat_of_ascii a) (S (S (S (S (S (S (S (S (S (S O)))))))))))) (unit_digit (nat_of_ascii a)) with | Some c' => @option_map string string (String c') (read_quoted_string (show_quoted_string s)) | None => @None string end (@Some string (String a s)) *)
      rewrite unthree_three_digit.
(* Goal: @eq (option string) (@option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      rewrite IHs.
(* Goal: @eq (option string) (@option_map string string (String (ascii_of_nat (nat_of_ascii a))) (@Some string s)) (@Some string (String a s)) *)
      rewrite ascii_nat_embedding.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
      auto.
    }
(* Goal: @eq (option string) (read_quoted_string (String a ((fix show_quoted_string (s : string) : string := match s with | EmptyString => String (Ascii false true false false false true false false) EmptyString | String c s' => if ascii_dec c (Ascii true false false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true true true false true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii true false true true false false false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false true true true false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false true false false false true false false) then append (String (Ascii false false true true true false true false) (String (Ascii false true false false false true false false) EmptyString)) (show_quoted_string s') else if ascii_dec c (Ascii false false true true true false true false) then append (String (Ascii false false true true true false true false) (String (Ascii false false true true true false true false) EmptyString)) (show_quoted_string s') else if orb (Nat.ltb (nat_of_ascii c) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Nat.ltb (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (nat_of_ascii c)) then append (String (Ascii false false true true true false true false) EmptyString) (append (three_digit (nat_of_ascii c)) (show_quoted_string s')) else String c (show_quoted_string s') end) s))) (@Some string (String a s)) *)
    { fold show_quoted_string.
(* Goal: @eq (option string) (read_string (@show string showString s)) (@Some string s) *)
      simpl.
(* Goal: @eq (option string) (if ascii_dec a (Ascii false true false false false true false false) then match show_quoted_string s with | EmptyString => @Some string EmptyString | String a s => @None string end else if ascii_dec a (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      destruct (ascii_dec a """"); [contradiction |].
(* Goal: @eq (option string) (if ascii_dec a (Ascii false false true true true false true false) then match show_quoted_string s with | EmptyString => @None string | String c2 s'' => if ascii_dec c2 (Ascii false true true true false true true false) then @option_map string string (String (Ascii false true false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false true true true false) then @option_map string string (String (Ascii true false true true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true false true true true false) then @option_map string string (String (Ascii true false false true false false false false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false false true true true false true false) then @option_map string string (String (Ascii false false true true true false true false)) (read_quoted_string s'') else if ascii_dec c2 (Ascii false true false false false true false false) then @option_map string string (String (Ascii false true false false false true false false)) (read_quoted_string s'') else match s'' with | EmptyString => @None string | String c1 (EmptyString as s) => @None string | String c1 (String c0 s''' as s) => match unthree_digit c2 c1 c0 with | Some c' => @option_map string string (String c') (read_quoted_string s''') | None => @None string end end end else @option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      destruct (ascii_dec a "\"); [contradiction |].
(* Goal: @eq (option string) (@option_map string string (String a) (read_quoted_string (show_quoted_string s))) (@Some string (String a s)) *)
      rewrite IHs.
(* Goal: @eq (option string) (@option_map string string (String a) (@Some string s)) (@Some string (String a s)) *)
      auto.
    }
Qed.
                             
Lemma read_show_string : forall (s : string),
    read_string (show s) = Some s.
Proof.
(* Goal: forall s : string, @eq (option string) (read_string (@show string showString s)) (@Some string s) *)
  intro.
(* Goal: @eq (option string) (read_string (@show string showString s)) (@Some string s) *)
  simpl.
(* Goal: @eq (option string) (read_quoted_string (show_quoted_string s)) (@Some string s) *)
  apply read_show_quoted_string.
Qed.
