proposition: Lemma decode_encode_word' : forall {n} w ext, decode_word' n (mappend (encode_word' n w mempty) ext) = Some (w, ext).
proof: Proof. induction n; simpl; intros; try shatter_word w; simpl in *. - rewrite mempty_left; reflexivity. - destruct (shatter_word_S w) as (?, (?, ?)); subst; simpl. rewrite enqueue_opt_format_word. rewrite <- !mappend_assoc. destruct n. + shatter_word x0; simpl. rewrite mempty_left. erewrite dequeue_mappend_opt; eauto using dequeue_head_opt. simpl. rewrite mempty_left; auto. + rewrite dequeue_opt_Some'. unfold DecodeBindOpt, BindOpt at 1; unfold If_Opt_Then_Else. assert (decode_word' (S n) (mappend (encode_word' n (word_split_tl x0) mempty) (mappend (enqueue_opt x mempty) ext)) = Some (WS x (word_split_tl x0), ext)). { simpl. pose proof (IHn (WS x (word_split_tl x0)) ext). simpl in H. rewrite enqueue_opt_format_word in H. rewrite <- mappend_assoc in H. rewrite H. eauto. } unfold BindOpt. rewrite H; simpl; rewrite <- (word_split_SW x0); auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats