Data.SHA256Schedule

44def sha256ReadWord =
45  (lambda unrestricted input : Bytes .
46    (nat-eliminate
47      (lambda unrestricted sufficient : Nat . (family SHA256WordReadResult))
48      (constructor
49        SHA256WordReadResult
50        SHA256WordReadFailed
51        (constructor SHA256ErrorCode SHA256BlockLengthInvalid))
52      (lambda unrestricted predecessor : Nat .
53        (lambda unrestricted induction : (family SHA256WordReadResult) .
54          (app
55            (lambda unrestricted tail1 : Bytes .
56              (app
57                (lambda unrestricted tail2 : Bytes .
58                  (app
59                    (lambda unrestricted tail3 : Bytes .
60                      (app
61                        (lambda unrestricted tail4 : Bytes .
62                          (constructor
63                            SHA256WordReadResult
64                            SHA256WordReadSucceeded
65                            (constructor
66                              ModelWord32
67                              ModelWord32Value
68                              (bytes-head tail3)
69                              (bytes-head tail2)
70                              (bytes-head tail1)
71                              (bytes-head input))
72                            tail4))
73                        (bytes-tail tail3)))
74                    (bytes-tail tail2)))
75                (bytes-tail tail1)))
76            (bytes-tail input))))
77      (naturalLessOrEqual sha256NaturalFour (bytes-length input))))