diff --git a/theories/Grammar.v b/theories/Grammar.v
index e822987..4009671 100644
--- a/theories/Grammar.v
+++ b/theories/Grammar.v
@@ -1,6 +1,15 @@
 (* Defines regular "grammars" in terms of regular expressions. *)
 
-From Stdlib Require Import Ascii List Strings.String Setoid Program.Equality.
+From Ltac2 Require Import Ltac2 List Printf.
+Set Default Proof Mode "Classic".
+
+From Stdlib Require Import
+  Ascii
+  List
+  Strings.String
+  Setoid
+  Program.Equality
+  ZArith.
 From Temporal Require Import StringUtil.
 Open Scope string_scope.
 
@@ -17,7 +26,7 @@ Inductive grammar :=
     generated by the grammar `g` *)
 Inductive generates : grammar -> string -> Prop :=
 | gen_empty : generates empty EmptyString
-| gen_char : forall c s, generates (char c) (String c s)
+| gen_char : forall c, generates (char c) (String c EmptyString)
 | gen_alt_l : forall s a b, generates a s -> generates (alternative a b) s
 | gen_alt_r : forall s a b, generates b s -> generates (alternative a b) s
 | gen_seq : forall s0 s1 a b, generates a s0 -> generates b s1 -> generates (sequence a b) (s0 ++ s1)
@@ -26,7 +35,7 @@ Inductive generates : grammar -> string -> Prop :=
 
 Fixpoint ntimes (n : nat) (a : grammar) :=
   match n with
-  | 0 => a
+  | 0 => empty
   | S n' => sequence a (ntimes n' a)
   end.
 
@@ -44,6 +53,13 @@ Fixpoint alt (gs : list grammar) :=
 
 Definition maybe a := alternative empty a.
 
+Definition digit : grammar :=
+  alt (
+    char "0" :: char "1" :: char "2" :: char "3" :: char "4" ::
+    char "5" :: char "6" :: char "7" :: char "8" :: char "9" ::
+    nil
+  ).
+
 Module Grammar.
   (* two grammars are equivalent if they generate the same strings *)
   Definition Equiv (a b : grammar) := forall s, generates a s <-> generates b s.
@@ -257,4 +273,433 @@ Module Grammar.
         assumption.
         assumption.
   Qed.
+
+  Lemma equiv_elim {g0 g1 s} :
+    generates g0 s -> Equiv g0 g1 -> generates g1 s.
+  Proof.
+    intros.
+    specialize (H0 s).
+    apply H0.
+    assumption.
+  Qed.
+
+  Lemma sequence_string :
+    forall a s g0 g1,
+    generates g0 (String a EmptyString) -> generates g1 s ->
+    generates (sequence g0 g1) (String a s).
+  Proof.
+    intros.
+    rewrite <- append_char_l.
+    apply gen_seq; assumption.
+  Qed.
+
+  Fixpoint star_append :
+    forall g s0 s1,
+    generates (star g) s0 -> generates (star g) s1 ->
+    generates (star g) (s0 ++ s1).
+  Proof.
+    intros.
+    dependent induction H.
+    - assumption.
+    - apply unfold_star.
+      apply gen_alt_r.
+      rewrite append_assoc.
+      apply gen_seq.
+      + assumption.
+      + apply star_append; assumption.
+  Qed.
 End Grammar.
+
+Set Default Proof Mode "Ltac2".
+
+(** Apply the given thunk to the first goal. *)
+Ltac2 first f := Control.focus 1 1 f.
+
+Ltac2 Notation "either" f(constr) g(constr) :=
+  Control.plus (fun () => f) (fun _ex => g).
+
+(** Applying a particular tactic by looping over the digit characters. *)
+Ltac2 rec char_loop f cs :=
+  match cs with
+  | [] => ()
+  | c :: cs' =>
+      f c;
+      char_loop f cs'
+  end.
+
+Ltac2 digits () :=
+  '"0"%char :: '"1"%char :: '"2"%char :: '"3"%char :: '"4"%char :: '"5"%char ::
+  '"6"%char :: '"7"%char :: '"8"%char :: '"9"%char :: [].
+
+Ltac2 on_digits f := char_loop f (digits ()).
+
+(** if we know a string to be generated by either a given character `c`, or
+   something else, case split on that hypothesis *)
+Ltac2 split_alt c :=
+  match! goal with
+  | [ h : generates (alternative (char ?c0) _) _ |- _ ] =>
+      let h := Control.hyp h in
+      if Constr.equal (Std.eval_hnf c0) c then
+        inversion $h
+      else
+        fail
+  end.
+
+(** if we know a string to be generated by a particular character, then we can
+   substitute that character for the string. *)
+Ltac2 split_digit () :=
+  lazy_match! goal with
+  | [ h : generates (char _) _ |- _ ] =>
+      let h := Control.hyp h in
+      inversion $h;
+      reflexivity
+  end.
+
+(** given hypotheses `s0 ++ s1 = String a s` and `generates (char c) s0`, we can
+    can derive `a = c` and `s1 = s`. *)
+Ltac2 rewrite_char () :=
+  let apply_rewrite () :=
+    lazy_match! goal with
+    | [ h0 : ?_s0 ++ _ = String _ _, h1 : ?_c = ?_s0 |- _ ] =>
+        let h1 := Control.hyp h1 in
+        rewrite <- $h1 in $h0;
+        let h0 := Control.hyp h0 in
+        inversion $h0
+    end
+  in
+  lazy_match! goal with
+  | [ _h : ?_s0 ++ _ = String _ _, h : generates (char ?_c) ?_s0 |- _ ] =>
+      let h := Control.hyp h in
+      inversion $h as [];
+      apply_rewrite ()
+  end.
+
+Ltac2 rewrite_string () :=
+  lazy_match! goal with
+  | [ h0 : generates (star digit) ?_s1,
+      h1 : ?_s1 = ?_s
+      |- generates (star digit) ?_s ] =>
+    let h1 := Control.hyp h1 in
+    rewrite $h1 in $h0;
+    assumption
+  end.
+
+(** apply the appropriate constructor when proving 
+    generates digit (String c "")` *)
+Ltac2 construct_digit () :=
+  let rec again cs :=
+    match cs with
+    | [] => Control.zero (Tactic_failure (Some (fprintf "not a digit!")))
+    | _ :: cs' =>
+      Control.plus
+        (fun () => apply gen_alt_l, gen_char)
+        (fun _ex => apply gen_alt_r; again cs')
+    end
+  in
+  again (digits ()).
+
+Lemma digit_length_1 : forall s, generates digit s -> length s = 1.
+Proof.
+  intros.
+  inversion H.
+  split_digit ().
+  on_digits (fun c => try (split_alt c; first split_digit)).
+  inversion H39.
+Qed.
+
+Lemma digit_char :
+  forall a s,
+  generates (star digit) (String a s) -> generates digit (String a EmptyString).
+Proof.
+  intros.
+  inversion H as [].
+  unfold digit in H0.
+  simpl in H0.
+
+  on_digits (fun c =>
+    split_alt c;
+    first (fun () => rewrite_char (); construct_digit ())
+  ).
+
+  inversion H43.
+Qed.
+
+Lemma digit_string :
+  forall a s,
+  generates (star digit) (String a s) -> generates (star digit) s.
+Proof.
+  intros.
+  inversion H as [].
+  unfold digit in H0.
+  simpl in H0.
+
+  on_digits (fun c =>
+    split_alt c;
+    Control.focus 1 1 (fun () => rewrite_char (); rewrite_string ())
+  ).
+  
+  inversion H43.
+Qed.
+
+Lemma ntimes_append_char :
+  forall n a s,
+  generates digit (String a EmptyString) -> generates (ntimes n digit) s ->
+  generates (ntimes (S n) digit) (String a s).
+Proof.
+  intros.
+  rewrite <- append_char_l.
+  apply gen_seq; assumption.
+Qed.
+
+(** If `s` has length `n`, and is a sequence of zero or more digits, then it is
+    a sequence of `n` digits. *)
+Fixpoint ntimes_digits :
+  forall n s,
+  generates (star digit) s -> length s = n -> generates (ntimes n digit) s.
+Proof.
+  refine open_constr:(
+    fun n s h l =>
+      match s as s' return (s = s' -> generates (ntimes n digit) s') with
+      | EmptyString => fun H => _
+      | String a s => fun H => _
+      end eq_refl
+  ).
+
+  - rewrite H in l.
+    rewrite <- l.
+    constructor.
+  
+  - rewrite H in l.
+    rewrite <- l.
+    apply ntimes_append_char.
+    + rewrite H in h.
+      apply (digit_char _ _ h).
+    + apply ntimes_digits.
+      * rewrite H in h.
+        apply (digit_string _ _ h).
+      * reflexivity.
+Qed.
+
+Ltac2 decimal_digit () :=
+  rewrite <- append_char_l;
+  apply gen_star_r;
+  Control.enter (fun () => orelse construct_digit (fun _ex => assumption)).
+
+Lemma string_of_int_some_digits :
+  forall n, (0 <= n)%Z ->
+  generates
+    (sequence digit (star digit))
+    (DecimalString.NilEmpty.string_of_int (Z.to_int n)).
+Admitted.
+
+Lemma string_of_int_digits :
+  forall n, (0 <= n)%Z ->
+  generates (star digit) (DecimalString.NilEmpty.string_of_int (Z.to_int n)).
+Proof.
+  intros.
+  unfold DecimalString.NilEmpty.string_of_int, Z.to_int.
+  destruct n eqn: n_def.
+  - apply Grammar.unfold_star.
+    apply gen_alt_r.
+    rewrite <- append_empty_r.
+    apply gen_seq.
+    + construct_digit ().
+    + apply gen_star_l.
+  - induction (Pos.to_uint p); simpl.
+    apply gen_star_l.
+    all: decimal_digit ().
+  - destruct H.
+    reflexivity.
+Qed.
+
+Lemma string_of_int_length_2 :
+  forall n, (0 <= n <= 99)%Z ->
+  length (DecimalString.NilEmpty.string_of_int (Z.to_int n)) <= 2.
+Proof.
+  intros.
+  destruct H.
+  unfold Z.to_int.
+  destruct n eqn: n_def.
+  - auto.
+  - admit.
+  - destruct H.
+    reflexivity.
+Admitted.
+
+Lemma string_of_int_length_4 :
+  forall n, (0 <= n <= 9999)%Z ->
+  length (DecimalString.NilEmpty.string_of_int (Z.to_int n)) <= 4.
+Proof.
+  intros.
+  destruct H.
+  unfold Z.to_int.
+  destruct n eqn: n_def.
+  - auto.
+  - admit.
+  - destruct H.
+    reflexivity.
+Admitted.
+
+Lemma Z_to_string_2_digits :
+  forall n, (0 <= n <= 99)%Z -> length (Z_to_string n) <= 2.
+Proof.
+  now apply string_of_int_length_2.
+Qed.
+
+Lemma Z_to_string_4_digits :
+  forall n, (0 <= n <= 9999)%Z -> length (Z_to_string n) <= 4.
+Proof.
+  now apply string_of_int_length_4.
+Qed.
+
+Lemma Z_to_string_some_digits :
+  forall n, (0 <= n)%Z ->
+  generates (sequence digit (star digit)) (Z_to_string n).
+Proof.
+  now apply string_of_int_some_digits.
+Qed.
+
+Lemma Z_to_string_digits :
+  forall n, (0 <= n)%Z -> generates (star digit) (Z_to_string n).
+Proof.
+  intros.
+  now apply string_of_int_digits.
+Qed.
+
+Lemma RepeatString_digits :
+  forall n, generates (star digit) (RepeatString "0" n).
+Proof.
+  induction n.
+  - constructor.
+  - simpl.
+    rewrite <- append_char_l.
+    apply gen_star_r.
+    + construct_digit ().
+    + assumption.
+Qed.
+
+Lemma RepeatString_some_digits :
+  forall n, 0 < n ->
+  generates (sequence digit (star digit)) (RepeatString "0" n).
+Proof.
+  intros.
+  destruct n.
+  - auto with *.
+  - simpl.
+    rewrite <- append_char_l.
+    apply gen_seq.
+    + construct_digit ().
+    + apply RepeatString_digits.
+Qed.
+
+Lemma length_nonnegative_z : forall s, (0 <= Z.of_nat (length s))%Z.
+Proof.
+  intros.
+  now destruct s.
+Qed.
+
+Lemma ToZeroPaddedDecimalString_4_digits :
+  forall n nv h, (0 <= n <= 9999)%Z ->
+  generates (ntimes 4 digit) (ToZeroPaddedDecimalString n 4 nv h).
+Proof.
+  assert (z4 : 4%Z = Z.of_nat 4). { ltac1:(easy). }
+  intros.
+  unfold ToZeroPaddedDecimalString, StringPad.
+  destruct ("0" =? EmptyString) eqn: h'. {
+    rewrite eqb_eq in h'.
+    discriminate.
+  }
+  destruct (4 <=? Z.of_nat (length (Z_to_string n)))%Z eqn: n_len.
+  - unfold Z_to_string.
+    apply ntimes_digits.
+    + now apply string_of_int_digits.
+    + rewrite Z.leb_le in n_len.
+      rewrite z4 in n_len.
+      rewrite <- Nat2Z.inj_le in n_len.
+      apply Nat.le_antisymm.
+      * apply string_of_int_length_4.
+        assumption.
+      * assumption.
+  - apply ntimes_digits.
+    + apply Grammar.star_append.
+      * apply RepeatString_digits.
+      * now apply Z_to_string_digits.
+    + rewrite append_length.
+      rewrite RepeatString_length.
+      * rewrite z4.
+        rewrite Z2Nat.inj_sub.
+        rewrite Nat2Z.id, Nat2Z.id.
+        apply Nat.sub_add.
+        rewrite z4 in n_len.
+        rewrite Z.leb_gt in n_len.
+        rewrite Z2Nat.inj_lt in n_len.
+        rewrite Nat2Z.id, Nat2Z.id in n_len.
+        apply Nat.lt_le_incl.
+        assumption.
+        apply length_nonnegative_z.
+        ltac1:(easy).
+        apply length_nonnegative_z.
+      * apply Nat.lt_0_1.
+Qed.
+
+Lemma ToZeroPaddedDecimalString_2_digits :
+  forall n nv h, (0 <= n <= 99)%Z ->
+  generates (ntimes 2 digit) (ToZeroPaddedDecimalString n 2 nv h).
+Proof.
+  intros.
+  unfold ToZeroPaddedDecimalString, StringPad.
+Proof.
+  assert (z2 : 2%Z = Z.of_nat 2). { ltac1:(easy). }
+  intros.
+  unfold ToZeroPaddedDecimalString, StringPad.
+  destruct ("0" =? EmptyString) eqn: h'. {
+    rewrite eqb_eq in h'.
+    discriminate.
+  }
+  destruct (2 <=? Z.of_nat (length (Z_to_string n)))%Z eqn: n_len.
+  - unfold Z_to_string.
+    apply ntimes_digits.
+    + now apply string_of_int_digits.
+    + rewrite Z.leb_le in n_len.
+      rewrite z2 in n_len.
+      rewrite <- Nat2Z.inj_le in n_len.
+      apply Nat.le_antisymm.
+      * apply string_of_int_length_2.
+        assumption.
+      * assumption.
+  - apply ntimes_digits.
+    + apply Grammar.star_append.
+      * apply RepeatString_digits.
+      * now apply Z_to_string_digits.
+    + rewrite append_length.
+      rewrite RepeatString_length.
+      * rewrite z2.
+        rewrite Z2Nat.inj_sub.
+        rewrite Nat2Z.id, Nat2Z.id.
+        apply Nat.sub_add.
+        rewrite z2 in n_len.
+        rewrite Z.leb_gt in n_len.
+        rewrite Z2Nat.inj_lt in n_len.
+        rewrite Nat2Z.id, Nat2Z.id in n_len.
+        apply Nat.lt_le_incl.
+        assumption.
+        apply length_nonnegative_z.
+        ltac1:(easy).
+        apply length_nonnegative_z.
+      * apply Nat.lt_0_1.
+Qed.
+
+Lemma ToZeroPaddedDecimalString_gt_0_digits :
+  forall n m nv mv, (0 < m)%Z ->
+  generates (sequence digit (star digit)) (ToZeroPaddedDecimalString n m nv mv).
+Proof.
+  intros.
+  unfold ToZeroPaddedDecimalString, StringPad.
+  destruct ("0" =? EmptyString) eqn: h'. {
+    rewrite eqb_eq in h'.
+    discriminate.
+  }
+  destruct (m <=? Z.of_nat (length (Z_to_string n)))%Z.
+  - now apply Z_to_string_some_digits.
+  - admit.
+Admitted.
diff --git a/theories/RFC3339.v b/theories/RFC3339.v
index f700ef2..cab70d3 100644
--- a/theories/RFC3339.v
+++ b/theories/RFC3339.v
@@ -5,13 +5,6 @@ Open Scope char_scope.
 (* Defines the grammar from RFC 33339 *)
 (* https://www.rfc-editor.org/rfc/rfc3339#section-5.6 *)
 
-Definition digit : grammar :=
-  alt (
-    char "0" :: char "1" :: char "2" :: char "3" :: char "4" ::
-    char "5" :: char "6" :: char "7" :: char "8" :: char "9" ::
-    nil
-  ).
-
 Definition date_fullyear := ntimes 4 digit.
 Definition date_month    := ntimes 2 digit.
 Definition date_mday     := ntimes 2 digit.
@@ -25,8 +18,7 @@ Definition time_numoffset :=
     alternative (char "+") (char "-") :: time_hour :: char ":" :: time_minute :: nil
   ).
 Definition time_offset :=
-  sequence (alternative (char "Z") (char "z"))
-  time_numoffset.
+  alternative (alternative (char "Z") (char "z")) time_numoffset.
 
 Definition partial_time :=
   seq (
@@ -41,3 +33,6 @@ Definition full_time := sequence partial_time time_offset.
 
 Definition date_time :=
   seq (full_date :: alternative (char "T") (char "t") :: full_time :: nil).
+
+Definition date_time_without_offset :=
+  seq (full_date :: alternative (char "T") (char "t") :: partial_time :: nil).
diff --git a/theories/Section12/FormatCalendarAnnotation.v b/theories/Section12/FormatCalendarAnnotation.v
index 8a1df5a..7a921a6 100644
--- a/theories/Section12/FormatCalendarAnnotation.v
+++ b/theories/Section12/FormatCalendarAnnotation.v
@@ -1,5 +1,6 @@
 From Stdlib Require Import Strings.String.
 From Temporal Require Import
+  Grammar
   Section12.CalendarType
   Section12.ShowCalendar.
 Open Scope string_scope.
@@ -23,3 +24,10 @@ Definition FormatCalendarAnnotation (id' : CalendarType) (showCalendar : ShowCal
     end in
     "[" ++ flag ++ "u-ca=" ++ idStringValue ++ "]"
   end.
+
+Lemma FormatCalendarAnnotation_never :
+  forall id', generates empty (FormatCalendarAnnotation id' SC_NEVER).
+Proof.
+  intros.
+  constructor.
+Qed.
diff --git a/theories/Section13/FormatFractionalSeconds.v b/theories/Section13/FormatFractionalSeconds.v
index 368d3d4..596185f 100644
--- a/theories/Section13/FormatFractionalSeconds.v
+++ b/theories/Section13/FormatFractionalSeconds.v
@@ -3,8 +3,10 @@ From Stdlib Require Import
   Strings.String
   Ascii.
 From Temporal Require Import
+  Grammar
   StringUtil
   Section13.Precision.
+From Temporal Require RFC3339.
 Open Scope string_scope.
 Open Scope Z.
 
@@ -16,7 +18,14 @@ Fixpoint RemoveTrailingZero (s : string) : string :=
     | EmptyString => if eqb c "0"%char then EmptyString else String c EmptyString
     | s'' => String c EmptyString ++ s''
     end
-  end. 
+  end.
+
+Lemma RemoveTrailingZero_some_digits :
+  forall n m nsv mv, 0 < n ->
+  generates
+    (sequence digit (star digit))
+    (RemoveTrailingZero (ToZeroPaddedDecimalString n m nsv mv)).
+Admitted.
 
 (* 13.25 FormatFractionalSeconds *)
 Program Definition FormatFractionalSeconds (subSecondNanoseconds : Z) (precision : Precision) (subSecondNanoseconds_valid : 0 <= subSecondNanoseconds <= 999999999) : string :=
@@ -42,3 +51,52 @@ Program Definition FormatFractionalSeconds (subSecondNanoseconds : Z) (precision
   (*>> 3. Return the string-concatenation of the code unit 0x002E (FULL STOP) and fractionString. <<*)
     "." ++ fractionString'
   end.
+
+Lemma FormatFractionalSeconds_rfc3339 :
+  forall ns p nsv,
+  generates (maybe RFC3339.time_secfrac) (FormatFractionalSeconds ns p nsv).
+Proof.
+  intros.
+  unfold FormatFractionalSeconds.
+  destruct p.
+  - destruct (ns =? 0) eqn: ns_eq_0.
+    + apply gen_alt_l.
+      constructor.
+    + apply gen_alt_r.
+      apply gen_seq.
+      * constructor.
+      * rewrite Z.eqb_neq in ns_eq_0.
+        destruct nsv.
+        assert (l' : 0 < ns). {
+          apply Z.le_neq.
+          split.
+          - assumption.
+          - symmetry.
+            assumption.
+        }
+        eapply Grammar.equiv_elim.
+        apply RemoveTrailingZero_some_digits.
+        assumption.
+        rewrite <- Grammar.sequence_assoc.
+        apply Grammar.sequence_empty_r.
+  - destruct (p =? 0) eqn: p_eq_0.
+    + apply gen_alt_l.
+      constructor.
+    + apply gen_alt_r.
+      apply gen_seq.
+      * constructor.
+      * rewrite Z.eqb_neq in p_eq_0.
+        destruct a.
+        assert (a' : 0 < p). {
+          apply Z.le_neq.
+          split.
+          - assumption.
+          - symmetry.
+            assumption.
+        }
+        eapply Grammar.equiv_elim.
+        apply ToZeroPaddedDecimalString_gt_0_digits.
+        assumption.
+        rewrite <- Grammar.sequence_assoc.
+        apply Grammar.sequence_empty_r.
+Qed.
diff --git a/theories/Section13/FormatTimeString.v b/theories/Section13/FormatTimeString.v
index e2b00bf..8993e3a 100644
--- a/theories/Section13/FormatTimeString.v
+++ b/theories/Section13/FormatTimeString.v
@@ -3,10 +3,12 @@ From Stdlib Require Import
   Strings.String.
 From Temporal Require Import
   Basic
+  Grammar
   StringUtil
   Section13.FormatFractionalSeconds
   Section13.PrecisionPrime
   Section13.Style.
+From Temporal Require RFC3339.
 Open Scope Z.
 
 (* 13.26 FormatTimeString *)
@@ -36,3 +38,31 @@ Definition FormatTimeString (hour minute second subSecondNanoseconds : Z) (preci
   (*>> 7. Return the string-concatenation of hh, separator, mm, separator, ss, and subSecondsPart. <<*)
   hh ++ separator ++ mm ++ separator ++ ss ++ subSecondsPart
   end.
+
+Lemma FormatTimeString_rfc3339 :
+  forall h min s ns precision h0 h1 h2 h3,
+  generates RFC3339.partial_time (FormatTimeString h min s ns (NormalPrecision precision) None h0 h1 h2 h3).
+Proof.
+  intros.
+  unfold FormatTimeString.
+  repeat (apply gen_seq).
+  - apply ToZeroPaddedDecimalString_2_digits.
+    destruct h0.
+    split.
+    * assumption.
+    * now (apply Z.le_trans with (m := 23); try assumption).
+  - constructor.
+  - apply ToZeroPaddedDecimalString_2_digits.
+    destruct h1.
+    split.
+    + assumption.
+    + now (apply Z.le_trans with (m := 59); try assumption).
+  - constructor.
+  - apply ToZeroPaddedDecimalString_2_digits.
+    destruct h2.
+    split.
+    + assumption.
+    + now (apply Z.le_trans with (m := 59); try assumption).
+  - refine (proj1 (Grammar.sequence_empty_r _ _) _).
+    apply FormatFractionalSeconds_rfc3339.
+Qed.
diff --git a/theories/Section3/PadISOYear.v b/theories/Section3/PadISOYear.v
index 64cc953..e28646d 100644
--- a/theories/Section3/PadISOYear.v
+++ b/theories/Section3/PadISOYear.v
@@ -1,8 +1,10 @@
 From Stdlib Require Import
   ZArith
   Strings.String
-  Lia.
-From Temporal Require Import StringUtil.
+  Lia
+  Program.Equality.
+From Temporal Require Import Grammar StringUtil.
+From Temporal Require RFC3339.
 Open Scope bool_scope.
 Open Scope string_scope.
 Open Scope Z.
@@ -53,3 +55,28 @@ Proof.
       apply ToZeroPaddedDecimalString_length.
       lia.
 Qed.
+
+Lemma PadISOYear_satisfies_rfc3339 :
+  forall y, 0 <= y <= 9999 -> generates RFC3339.date_fullyear (PadISOYear y).
+Proof.
+  intros.
+  unfold PadISOYear.
+  unfold PadISOYear_obligation_1.
+  
+  destruct H.
+  rewrite <- Z.leb_le in H.
+  rewrite <- Z.leb_le in H0.
+  rewrite <- Z.geb_leb in H.
+
+  generalize (Bool.andb_true_iff (y >=? 0) (y <=? 9999)).
+  destruct ((y >=? 0) && (y <=? 9999)).
+  - intros.
+    rewrite Z.geb_leb in H.
+    rewrite Z.leb_le in H.
+    rewrite Z.leb_le in H0.
+    apply ToZeroPaddedDecimalString_4_digits.
+    split; assumption.
+  - rewrite H, H0.
+    intuition auto.
+    discriminate.
+Qed.
diff --git a/theories/Section5/ISODateTimeToString.v b/theories/Section5/ISODateTimeToString.v
index f80b7fc..9589031 100644
--- a/theories/Section5/ISODateTimeToString.v
+++ b/theories/Section5/ISODateTimeToString.v
@@ -43,7 +43,59 @@ Next Obligation. destruct isoDateTime. destruct Time. simpl. lia. Qed.
 Next Obligation. destruct isoDateTime. destruct Time. simpl. lia. Qed.
 Next Obligation. destruct isoDateTime. destruct Time. simpl. lia. Qed.
 
+Lemma month_rfc3339 :
+  forall isoDate h,
+  generates RFC3339.date_month (ToZeroPaddedDecimalString (month isoDate) 2 h zero_le_two).
+Proof.
+  intros.
+  apply ToZeroPaddedDecimalString_2_digits.
+  split.
+  - assumption.
+  - destruct (month_valid isoDate).
+    apply Z.le_trans with (m := 12).
+    + assumption.
+    + easy.
+Qed.
+
+Lemma mday_rfc3339 :
+  forall isoDate h,
+  generates RFC3339.date_mday (ToZeroPaddedDecimalString (day isoDate) 2 h zero_le_two).
+Proof.
+  intros.
+  apply ToZeroPaddedDecimalString_2_digits.
+  split.
+  - assumption.
+  - destruct (day_valid isoDate).
+    apply Z.le_trans with (m := 31).
+    + assumption.
+    + easy.
+Qed.
+
 Theorem ISODateTimeToString_without_calendar_satisfies_rfc3339 :
-  forall isoDateTime calendar precision',
-  generates RFC3339.date_time (ISODateTimeToString isoDateTime calendar precision' SC_NEVER).
-Admitted.
+  forall isoDateTime calendar precision,
+  0 <= year (ISODate isoDateTime) <= 9999 ->
+  generates RFC3339.date_time_without_offset (ISODateTimeToString isoDateTime calendar (NormalPrecision precision) SC_NEVER).
+Proof.
+  intros.
+  unfold ISODateTimeToString.
+  rewrite <- append_assoc.
+  rewrite <- append_assoc.
+  rewrite <- append_assoc.
+  rewrite <- append_assoc.
+  apply gen_seq.
+  - repeat (rewrite append_assoc).
+    repeat (try apply gen_seq).
+    + apply PadISOYear_satisfies_rfc3339.
+      assumption.
+    + constructor.
+    + apply month_rfc3339.
+    + constructor.
+    + refine (Grammar.equiv_elim _ (Grammar.sequence_empty_r _)).
+      apply mday_rfc3339.
+  - apply gen_seq.
+    + apply gen_alt_l.
+      constructor.
+    + apply gen_seq.
+      * apply FormatTimeString_rfc3339.
+      * apply FormatCalendarAnnotation_never.
+Qed.
diff --git a/theories/StringUtil.v b/theories/StringUtil.v
index feb2ae1..5b0c924 100644
--- a/theories/StringUtil.v
+++ b/theories/StringUtil.v
@@ -80,6 +80,12 @@ Proof.
     reflexivity.
 Qed.
 
+Lemma append_char_l : forall a s0, String a EmptyString ++ s0 = String a s0.
+Proof.
+  intros.
+  reflexivity.
+Qed.
+
 Lemma length_char_eq :
   forall a a', length (String a EmptyString) = length (String a' EmptyString).
 Proof.
@@ -116,6 +122,18 @@ Proof.
     now inversion H.
 Qed.
 
+Lemma length_empty : forall s, length s = 0 <-> s = EmptyString.
+Proof.
+  split.
+  - intros.
+    destruct s.
+    + reflexivity.
+    + discriminate.
+  - intros.
+    rewrite H.
+    reflexivity.
+Qed.
+
 Lemma length_nonempty : forall s, s <> EmptyString -> 0 < length s.
 Proof.
   intros.