proposition: Lemma ByteString_into_word_eq : forall bs, bs = word_into_ByteString (paddingOK bs) (ByteString_into_word bs).
proof: Proof. destruct bs; simpl. unfold word_into_ByteString, ByteString_into_word. f_equal. - destruct padding0 as [ | [ | [ | [ | [ | [ | [ | [ | ] ] ] ] ] ] ] ]. + pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; eauto. + pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; eauto. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; eauto. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; eauto. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; eauto. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl front0)))))) as H'; simpl in H'; rewrite H'; eauto. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl front0)))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl front0))))))) as H'; simpl in H'; rewrite H'; eauto. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl front0)))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl front0))))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl (wtl front0)))))))) as H'; simpl in H'; rewrite H'; eauto. + omega. - destruct padding0 as [ | [ | [ | [ | [ | [ | [ | [ | ] ] ] ] ] ] ] ]. + pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; subst; simpl; eauto using ByteString_into_word'_eq. + pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; simpl; eauto using ByteString_into_word'_eq. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; simpl; eauto using ByteString_into_word'_eq. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; simpl; eauto using ByteString_into_word'_eq. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; simpl; eauto using ByteString_into_word'_eq. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl front0)))))) as H'; simpl in H'; rewrite H'; simpl; eauto using ByteString_into_word'_eq. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl front0)))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl front0))))))) as H'; simpl in H'; rewrite H'; simpl; eauto using ByteString_into_word'_eq. + let H' := fresh in pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; let H'' := fresh in pose proof (shatter_word (wtl front0)) as H''; simpl in H''; rewrite H''; let H' := fresh in pose proof (shatter_word (wtl (wtl front0))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl front0)))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl front0))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl front0)))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl front0))))))) as H'; simpl in H'; rewrite H'; let H' := fresh in pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl (wtl front0)))))))) as H'; simpl in H'; rewrite H'; simpl; eauto using ByteString_into_word'_eq. + omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs