Skip to content

Instantly share code, notes, and snippets.

@relrod

relrod/*response*.txt

Created May 25, 2016 18:02
Show Gist options
  • Save relrod/e684a8f38bf820f783d4aebd2c2f847d to your computer and use it in GitHub Desktop.
Save relrod/e684a8f38bf820f783d4aebd2c2f847d to your computer and use it in GitHub Desktop.
Download ZIP
Raw
*response*.txt
= fun i : string =>
match
match
match i with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x, i') =>
(if
if
match
match
(let (a0, a1, a2, a3, a4, a5, a6, a7) := x in
match
(if a0 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a3 then ... else BinNums.N0)
with
| BinNums.N0 =>
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match ...
...
...
end with
| BinNums.N0 =>
if a3
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (... p0 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match
match
match ... with
| BinNums.N0 => ...
...
...
end
| BinNums.Npos p1 =>
...
...
...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p1 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
with
add_carry
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p1 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
for add) p0 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 => ...
...
...
end
| BinNums.Npos p1 =>
...
...
...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ...
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix add ... :
BinNums.positive :=
...
with add_carry ... :
BinNums.positive := ...
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p1 q0)
| BinNums.xO q0 =>
BinNums.xO (add p1 q0)
| BinNums.xH => BinNums.xI p1
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH => BinNums.xO 1
end
end
with
add_carry
(x0 y : BinNums.positive) {struct
x0} : BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xH =>
BinNums.xI
((fix succ
... : BinNums.positive :=
...
...
...
...
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) p1)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix succ
... : BinNums.positive :=
...
...
...
...
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) q0)
| BinNums.xH => BinNums.xI 1
end
end
for add) p0 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q => BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match
match
match
(if a1 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 => ...
...
...
end
| BinNums.Npos p1 =>
...
...
...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ...
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix add ... :
BinNums.positive :=
...
with add_carry ... :
BinNums.positive := ...
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match (...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ...
end
| BinNums.Npos p2 =>
match ... with
| BinNums.N0 => ... ... ...
| BinNums.Npos q =>
BinNums.Npos ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO (...)
| BinNums.xO q0 =>
BinNums.xI (...)
| BinNums.xH =>
BinNums.xO (...)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (...)
| BinNums.xO q0 =>
BinNums.xO (...)
| BinNums.xH =>
BinNums.xI p2
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO (...)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x0 y : BinNums.positive) {struct
x0} : BinNums.positive :=
match x0 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (...)
| BinNums.xO q0 =>
BinNums.xO (...)
| BinNums.xH =>
BinNums.xI (...)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO (...)
| BinNums.xO q0 =>
BinNums.xI (...)
| BinNums.xH =>
BinNums.xO (...)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI (...)
| BinNums.xO q0 =>
BinNums.xO (...)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q => BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0 then BinNums.Npos 1 else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x0 y : BinNums.positive) {struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO (add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p1 q0)
| BinNums.xO q0 =>
BinNums.xO (add p1 q0)
| BinNums.xH => BinNums.xI p1
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (succ p1)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 => BinNums.xI q0
| BinNums.xH => BinNums.xO 1
end
end
with
add_carry (x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xO (add_carry p1 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO (add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (succ p1)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (succ p1)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xH => BinNums.xI 1
end
end
for add) p0 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p0 =>
(fix
iter (p1 : BinNums.positive) (a : nat) {struct p1} :
nat :=
match p1 with
| BinNums.xI p2 =>
(fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p3 => S (add p3 m)
end) a
(iter p2
((fix add (n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p3 => S (add p3 m)
end) a a))
| BinNums.xO p2 =>
iter p2
((fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p3 => S (add p3 m)
end) a a)
| BinNums.xH => a
end) p0 1
end
with
| 0 => false
| 1 => false
| 2 => false
| 3 => false
| 4 => false
| 5 => false
| 6 => false
| 7 => false
| 8 => false
| 9 => false
| 10 => false
| 11 => false
| 12 => false
| 13 => false
| 14 => false
| 15 => false
| 16 => false
| 17 => false
| 18 => false
| 19 => false
| 20 => false
| 21 => false
| 22 => false
| 23 => false
| 24 => false
| 25 => false
| 26 => false
| 27 => false
| 28 => false
| 29 => false
| 30 => false
| 31 => false
| 32 => false
| 33 => false
| 34 => false
| 35 => false
| 36 => false
| 37 => false
| 38 => false
| 39 => false
| 40 => false
| 41 => false
| 42 => false
| 43 => false
| 44 => false
| 45 => false
| 46 => false
| 47 => false
| S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S (S (S (S (S (S (S ...)))))))))))))))))))))))))))))))) =>
true
end
then
(fix leb (n m : nat) {struct n} : bool :=
match n with
| 0 => true
| S n' =>
match m with
| 0 => false
| S m' => leb n' m'
end
end)
match
(let (a0, a1, a2, a3, a4, a5, a6, a7) := x in
match
(if a0 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a3
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p0 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
with
| BinNums.N0 =>
if a3
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
... {struct x0} :
BinNums.positive :=
...
...
...
...
end
with
add_carry
... {struct x0} :
BinNums.positive :=
...
...
...
...
end
for add) p0 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match
match
match (... ... ...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
| BinNums.Npos p1 =>
match ... with
| BinNums.N0 =>
if a3
then ...
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO (... p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p1 q0)
| BinNums.xO q0 =>
BinNums.xO (add p1 q0)
| BinNums.xH =>
BinNums.xI p1
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO (... q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xH =>
BinNums.xI (... p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO (... p1)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI (... q0)
| BinNums.xO q0 =>
BinNums.xO (... q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p0 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match (... ... ...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
| BinNums.Npos p1 =>
match ... with
| BinNums.N0 =>
if a3
then ...
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match ... with
| ... ...
| ... ...
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match ... with
| BinNums.xI p2 =>
...
...
...
...
end
| BinNums.xO p2 =>
...
...
...
...
end
| BinNums.xH =>
...
...
...
...
end
end
with
add_carry
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match ... with
| BinNums.xI p2 =>
...
...
...
...
end
| BinNums.xO p2 =>
...
...
...
...
end
| BinNums.xH =>
...
...
...
...
end
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (...)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p1 q0)
| BinNums.xO q0 =>
BinNums.xO (add p1 q0)
| BinNums.xH => BinNums.xI p1
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (...)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH => BinNums.xO 1
end
end
with
add_carry
(x0 y : BinNums.positive) {struct
x0} : BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (...)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (...)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (...)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (...)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xH => BinNums.xI 1
end
end
for add) p0 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q => BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p0 =>
match
match
match
(if a1 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match (... ... ...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
| BinNums.Npos p1 =>
match ... with
| BinNums.N0 =>
if a3
then ...
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match ... with
| ... ...
| ... ...
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match ... with
| BinNums.xI p2 =>
...
...
...
...
end
| BinNums.xO p2 =>
...
...
...
...
end
| BinNums.xH =>
...
...
...
...
end
end
with
add_carry
(x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match ... with
| BinNums.xI p2 =>
...
...
...
...
end
| BinNums.xO p2 =>
...
...
...
...
end
| BinNums.xH =>
...
...
...
...
end
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| ... ...
| ... ...
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p2 =>
match
match ... with
| ... BinNums.N0
| ... ...
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ((...) p2 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix succ ... :
BinNums.positive := ...)
p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p2 q0)
| BinNums.xO q0 =>
BinNums.xO (add p2 q0)
| BinNums.xH =>
BinNums.xI p2
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix succ ... :
BinNums.positive := ...)
q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x0 y : BinNums.positive) {struct
x0} : BinNums.positive :=
match x0 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xH =>
BinNums.xI
((fix succ ... :
BinNums.positive := ...)
p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix succ ... :
BinNums.positive := ...)
p2)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix succ ... :
BinNums.positive := ...)
q0)
| BinNums.xO q0 =>
BinNums.xO
((fix succ ... :
BinNums.positive := ...)
q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q => BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0 then BinNums.Npos 1 else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x0 y : BinNums.positive) {struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO (add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p1 q0)
| BinNums.xO q0 =>
BinNums.xO (add p1 q0)
| BinNums.xH => BinNums.xI p1
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (succ p1)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 => BinNums.xI q0
| BinNums.xH => BinNums.xO 1
end
end
with
add_carry (x0 y : BinNums.positive)
{struct x0} :
BinNums.positive :=
match x0 with
| BinNums.xI p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xO (add_carry p1 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xO p1 =>
match y with
| BinNums.xI q0 =>
BinNums.xO (add_carry p1 q0)
| BinNums.xO q0 =>
BinNums.xI (add p1 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) p1)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (succ p1)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x1 : BinNums.positive) :
BinNums.positive :=
match x1 with
| BinNums.xI p1 =>
BinNums.xO (succ p1)
| BinNums.xO p1 =>
BinNums.xI p1
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xH => BinNums.xI 1
end
end
for add) p0 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p0 =>
(fix
iter (p1 : BinNums.positive) (a : nat) {struct p1} :
nat :=
match p1 with
| BinNums.xI p2 =>
(fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p3 => S (add p3 m)
end) a
(iter p2
((fix add (n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p3 => S (add p3 m)
end) a a))
| BinNums.xO p2 =>
iter p2
((fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p3 => S (add p3 m)
end) a a)
| BinNums.xH => a
end) p0 1
end 57
else false
then fun inp : string => Some (x, inp)
else fun _ : string => None) i'
| None => None
end
with
| Some (_, i') =>
match
match
match i' with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x0, i'0) =>
(if
if
match
match
(let (a0, a1, a2, a3, a4, a5, a6, a7) := x0 in
match
(if a0 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match (...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ...
end
| BinNums.Npos p1 =>
match ... with
| BinNums.N0 => ... ... ...
| BinNums.Npos q =>
BinNums.Npos ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end
with
add_carry
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match
(if a2 then ... else BinNums.N0)
with
| BinNums.N0 =>
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p2 =>
match ...
...
...
end with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (... p2 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO ((...) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p2 q0)
| BinNums.xO q0 =>
BinNums.xO (add p2 q0)
| BinNums.xH =>
BinNums.xI p2
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO ((...) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xH =>
BinNums.xI ((...) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO ((...) p2)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI ((...) q0)
| BinNums.xO q0 =>
BinNums.xO ((...) q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2 then ... else BinNums.N0)
with
| BinNums.N0 =>
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p2 =>
match ...
...
...
end with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (... p2 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p2 =>
match
match
match ... with
| BinNums.N0 => ...
...
...
end
| BinNums.Npos p3 =>
...
...
...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p3 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p3 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
with
add_carry
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p3 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p3 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
for add) p2 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0 then BinNums.Npos 1 else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x1 y : BinNums.positive) {struct
x1} : BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p3 =>
BinNums.xO (succ p3)
| BinNums.xO p3 =>
BinNums.xI p3
| BinNums.xH =>
BinNums.xO 1
end) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p2 q0)
| BinNums.xO q0 =>
BinNums.xO (add p2 q0)
| BinNums.xH => BinNums.xI p2
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH => BinNums.xO 1
end
end
with
add_carry (x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p3 =>
BinNums.xO (succ p3)
| BinNums.xO p3 =>
BinNums.xI p3
| BinNums.xH =>
BinNums.xO 1
end) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p3 =>
BinNums.xO (succ p3)
| BinNums.xO p3 =>
BinNums.xI p3
| BinNums.xH =>
BinNums.xO 1
end) p2)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xH => BinNums.xI 1
end
end
for add) p1 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p1 =>
(fix
iter (p2 : BinNums.positive)
(a : nat) {struct p2} : nat :=
match p2 with
| BinNums.xI p3 =>
(fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p4 => S (add p4 m)
end) a
(iter p3
((fix add (n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p4 => S (add p4 m)
end) a a))
| BinNums.xO p3 =>
iter p3
((fix add (n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p4 => S (add p4 m)
end) a a)
| BinNums.xH => a
end) p1 1
end
with
| 0 => false
| 1 => false
| 2 => false
| 3 => false
| 4 => false
| 5 => false
| 6 => false
| 7 => false
| 8 => false
| 9 => false
| 10 => false
| 11 => false
| 12 => false
| 13 => false
| 14 => false
| 15 => false
| 16 => false
| 17 => false
| 18 => false
| 19 => false
| 20 => false
| 21 => false
| 22 => false
| 23 => false
| 24 => false
| 25 => false
| 26 => false
| 27 => false
| 28 => false
| 29 => false
| 30 => false
| 31 => false
| 32 => false
| 33 => false
| 34 => false
| 35 => false
| 36 => false
| 37 => false
| 38 => false
| 39 => false
| 40 => false
| 41 => false
| 42 => false
| 43 => false
| 44 => false
| 45 => false
| 46 => false
| 47 => false
| S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S (S (S (S (S (S ...)))))))))))))))))))))))))))))) =>
true
end
then
(fix leb (n m : nat) {struct n} : bool :=
match n with
| 0 => true
| S n' =>
match m with
| 0 => false
| S m' => leb n' m'
end
end)
match
(let (a0, a1, a2, a3, a4, a5, a6, a7) := x0 in
match
(if a0 then BinNums.Npos 1 else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a3
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| ... ...
| ... ...
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match ... with
| ... BinNums.N0
| ... ...
end
with
| BinNums.N0 =>
if a3
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ((...) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p2 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI ...
| BinNums.xH =>
BinNums.xO ...
end
| BinNums.xO p2 =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI p2
end
| BinNums.xH =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI ...
end
| BinNums.xO p2 =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI ...
| BinNums.xH =>
BinNums.xO ...
end
| BinNums.xH =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p2 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p2 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
... {struct x1} :
BinNums.positive :=
...
...
...
...
end
with
add_carry
... {struct x1} :
BinNums.positive :=
...
...
...
...
end
for add) p2 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p2 q0)
| BinNums.xO q0 =>
BinNums.xO (add p2 q0)
| BinNums.xH =>
BinNums.xI p2
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) p2)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p1 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p1 =>
match
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p2 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p2 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
... {struct x1} :
BinNums.positive :=
...
...
...
...
end
with
add_carry
... {struct x1} :
BinNums.positive :=
...
...
...
...
end
for add) p2 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p2 =>
match
match
match (... ... ...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
| BinNums.Npos p3 =>
match ... with
| BinNums.N0 =>
if a2
then ...
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p3 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p3 q0)
| BinNums.xO q0 =>
BinNums.xI (add p3 q0)
| BinNums.xH =>
BinNums.xO (... p3)
end
| BinNums.xO p3 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p3 q0)
| BinNums.xO q0 =>
BinNums.xO (add p3 q0)
| BinNums.xH =>
BinNums.xI p3
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO (... q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p3 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p3 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p3 q0)
| BinNums.xH =>
BinNums.xI (... p3)
end
| BinNums.xO p3 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p3 q0)
| BinNums.xO q0 =>
BinNums.xI (add p3 q0)
| BinNums.xH =>
BinNums.xO (... p3)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI (... q0)
| BinNums.xO q0 =>
BinNums.xO (... q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p2 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0 then BinNums.Npos 1 else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add (x1 y : BinNums.positive) {struct
x1} : BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p3 =>
BinNums.xO (succ p3)
| BinNums.xO p3 =>
BinNums.xI p3
| BinNums.xH =>
BinNums.xO 1
end) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p2 q0)
| BinNums.xO q0 =>
BinNums.xO (add p2 q0)
| BinNums.xH => BinNums.xI p2
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH => BinNums.xO 1
end
end
with
add_carry (x1 y : BinNums.positive)
{struct x1} :
BinNums.positive :=
match x1 with
| BinNums.xI p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p3 =>
BinNums.xO (succ p3)
| BinNums.xO p3 =>
BinNums.xI p3
| BinNums.xH =>
BinNums.xO 1
end) p2)
end
| BinNums.xO p2 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p2 q0)
| BinNums.xO q0 =>
BinNums.xI (add p2 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p3 =>
BinNums.xO (succ p3)
| BinNums.xO p3 =>
BinNums.xI p3
| BinNums.xH =>
BinNums.xO 1
end) p2)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x2 : BinNums.positive) :
BinNums.positive :=
match x2 with
| BinNums.xI p2 =>
BinNums.xO (succ p2)
| BinNums.xO p2 =>
BinNums.xI p2
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xH => BinNums.xI 1
end
end
for add) p1 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p1 =>
(fix
iter (p2 : BinNums.positive)
(a : nat) {struct p2} : nat :=
match p2 with
| BinNums.xI p3 =>
(fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p4 => S (add p4 m)
end) a
(iter p3
((fix add (n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p4 => S (add p4 m)
end) a a))
| BinNums.xO p3 =>
iter p3
((fix add (n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p4 => S (add p4 m)
end) a a)
| BinNums.xH => a
end) p1 1
end 57
else false
then fun inp : string => Some (x0, inp)
else fun _ : string => None) i'0
| None => None
end
with
| Some (_, i'0) =>
match
match
match i'0 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x1, i'1) =>
(if
if
match
x1 as a
return
({":"%char = a} + {":"%char = a -> False})
with
| Ascii b8 b9 b10 b11 b12 b13 b14 b15 =>
match
(if b8 as b
return
({false = b} + {false = b -> False})
then
right
(fun H : false = true =>
match
match
H in (_ = y)
return (if y then False else True)
with
| eq_refl => I
end return False
with
end)
else left eq_refl)
with
| left a0 =>
match
(if b9 as b
return
({true = b} + {true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
match
H in (_ = y)
return
(if y then True else False)
with
| eq_refl => I
end return False
with
end))
with
| left a1 =>
match
(if b10 as b
return
({false = b} +
{false = b -> False})
then
right
(fun H : false = true =>
match
match
H in (_ = y)
return
(if y then False else True)
with
| eq_refl => I
end
return False
with
end)
else left eq_refl)
with
| left a2 =>
match
(if b11 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
match
H in (_ = y)
return
(if y then True else False)
with
| eq_refl => I
end
return False
with
end))
with
| left a3 =>
match
(if b12 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
match
H in (_ = y)
return
(if y then True else False)
with
| eq_refl => I
end
return False
with
end))
with
| left a4 =>
match
(if b13 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
match
H in (...) return (...)
with
| eq_refl => I
end
return False
with
end))
with
| left a5 =>
match
(if b14 as b
return
({false = b} +
{false = b -> False})
then
right
(fun H : false = true =>
match
match ... ... with
| eq_refl => I
end
return False
with
end)
else left eq_refl)
with
| left a6 =>
match
(if b15 as b
return
({false = b} +
{false = b -> False})
then
right
(fun H : false = true =>
match
...
...
end return False
with
end)
else left eq_refl)
with
| left a7 =>
left
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15)
with
| eq_refl =>
match
match
a2 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15)
with
| eq_refl =>
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... = ...)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a2 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a2 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a3 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 b10 y true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
fun ... => diseq ...
end
end
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a2 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a3 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 b10 y true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a4 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 b10 b11 y
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 b9 b10 b11 b12
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in ... return ...
with
| eq_refl => eq_refl
end
end
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a2 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a3 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 b10 y true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 b9 b10 b11 true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(true =
match ... with
| ... b3
end)
with
| eq_refl => eq_refl
end
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a2 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 b9 b10 true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(true =
match y with
| Ascii _ _ _ b2 _ _ _
_ => b2
end)
with
| eq_refl => eq_refl
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12 b13
b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 b9 false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(false =
match y with
| Ascii _ _ b1 _ _ _ _
_ => b1
end)
with
| eq_refl => eq_refl
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y) return (y = false)
with
| eq_refl => eq_refl
end in (_ = y)
return
(Ascii y true false true true
true false false =
Ascii b8 b9 b10 b11 b12 b13 b14
b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 true false true true
true false false =
Ascii b8 b9 b10 b11 b12 b13
b14 b15 =>
diseq
match
absurd in (_ = y)
return
(true =
match y with
| Ascii _ b0 _ _ _ _ _
_ => b0
end)
with
| eq_refl => eq_refl
end
end
end
| right diseq =>
right
(fun
absurd : ":"%char =
Ascii b8 b9 b10 b11 b12 b13
b14 b15 =>
diseq
match
absurd in (_ = y)
return
(false =
match y with
| Ascii b _ _ _ _ _ _ _ => b
end)
with
| eq_refl => eq_refl
end)
end
end
then true
else false
then fun inp : string => Some (x1, inp)
else fun _ : string => None) i'1
| None => None
end
with
| Some (_, i'1) =>
match
match
match i'1 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x2, i'2) =>
(if
if
match
match
(let (a0, a1, a2, a3, a4, a5, a6, a7) :=
x2 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then ...
else BinNums.N0)
with
| BinNums.N0 =>
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p3 =>
match ...
...
...
end with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (... p3 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p3 =>
match
match
match ... with
| BinNums.N0 =>
...
...
...
end
| BinNums.Npos p4 =>
...
...
...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p4 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
with
add_carry
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p4 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
for add) p3 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p3 =>
match
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 =>
...
...
...
end
| BinNums.Npos p4 =>
...
...
...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p4 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ...
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix add ... :
BinNums.positive :=
...
with add_carry ... :
BinNums.positive := ...
for add) p4 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xI (add p4 q0)
| BinNums.xH =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) p4)
end
| BinNums.xO p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p4 q0)
| BinNums.xO q0 =>
BinNums.xO (add p4 q0)
| BinNums.xH =>
BinNums.xI p4
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xH =>
BinNums.xI
((fix succ
... : BinNums.positive :=
...
...
...
...
end) p4)
end
| BinNums.xO p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xI (add p4 q0)
| BinNums.xH =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) p4)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix succ
... : BinNums.positive :=
...
...
...
...
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix succ
... : BinNums.positive :=
...
...
...
...
end) q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p3 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p3 =>
(fix
iter (p4 : BinNums.positive)
(a : nat) {struct p4} : nat :=
match p4 with
| BinNums.xI p5 =>
(fix add
(n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p6 => S (add p6 m)
end) a
(iter p5
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p6 => S (add p6 m)
end) a a))
| BinNums.xO p5 =>
iter p5
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p6 => S (add p6 m)
end) a a)
| BinNums.xH => a
end) p3 1
end
with
| 0 => false
| 1 => false
| 2 => false
| 3 => false
| 4 => false
| 5 => false
| 6 => false
| 7 => false
| 8 => false
| 9 => false
| 10 => false
| 11 => false
| 12 => false
| 13 => false
| 14 => false
| 15 => false
| 16 => false
| 17 => false
| 18 => false
| 19 => false
| 20 => false
| 21 => false
| 22 => false
| 23 => false
| 24 => false
| 25 => false
| 26 => false
| 27 => false
| 28 => false
| 29 => false
| 30 => false
| 31 => false
| 32 => false
| 33 => false
| 34 => false
| 35 => false
| 36 => false
| 37 => false
| 38 => false
| 39 => false
| 40 => false
| 41 => false
| 42 => false
| 43 => false
| 44 => false
| 45 => false
| 46 => false
| 47 => false
| S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S (S (S (S (S ...)))))))))))))))))))))))))) =>
true
end
then
(fix leb (n m : nat) {struct n} : bool :=
match n with
| 0 => true
| S n' =>
match m with
| 0 => false
| S m' => leb n' m'
end
end)
match
(let (a0, a1, a2, a3, a4, a5, a6, a7) :=
x2 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p3 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p3 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
... {struct x3} :
BinNums.positive :=
...
...
...
...
end
with
add_carry
... {struct x3} :
BinNums.positive :=
...
...
...
...
end
for add) p3 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p3 =>
match
match
match (... ... ...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
| BinNums.Npos p4 =>
match ... with
| BinNums.N0 =>
if a2
then ...
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xI (add p4 q0)
| BinNums.xH =>
BinNums.xO (... p4)
end
| BinNums.xO p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p4 q0)
| BinNums.xO q0 =>
BinNums.xO (add p4 q0)
| BinNums.xH =>
BinNums.xI p4
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO (... q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xH =>
BinNums.xI (... p4)
end
| BinNums.xO p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xI (add p4 q0)
| BinNums.xH =>
BinNums.xO (... p4)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI (... q0)
| BinNums.xO q0 =>
BinNums.xO (... q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p3 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p3 =>
match
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match (... ... ...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
| BinNums.Npos p4 =>
match ... with
| BinNums.N0 =>
if a2
then ...
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p4 =>
match
match
match ... with
| ... ...
| ... ...
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match ... with
| BinNums.xI p5 =>
...
...
...
...
end
| BinNums.xO p5 =>
...
...
...
...
end
| BinNums.xH =>
...
...
...
...
end
end
with
add_carry
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match ... with
| BinNums.xI p5 =>
...
...
...
...
end
| BinNums.xO p5 =>
...
...
...
...
end
| BinNums.xH =>
...
...
...
...
end
end
for add) p4 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xI (add p4 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x4 : BinNums.positive) :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
BinNums.xO (...)
| BinNums.xO p5 =>
BinNums.xI p5
| BinNums.xH =>
BinNums.xO 1
end) p4)
end
| BinNums.xO p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p4 q0)
| BinNums.xO q0 =>
BinNums.xO (add p4 q0)
| BinNums.xH =>
BinNums.xI p4
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x4 : BinNums.positive) :
BinNums.positive :=
match x4 with
| BinNums.xI p4 =>
BinNums.xO (...)
| BinNums.xO p4 =>
BinNums.xI p4
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x3 y : BinNums.positive)
{struct x3} :
BinNums.positive :=
match x3 with
| BinNums.xI p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x4 : BinNums.positive) :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
BinNums.xO (...)
| BinNums.xO p5 =>
BinNums.xI p5
| BinNums.xH =>
BinNums.xO 1
end) p4)
end
| BinNums.xO p4 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p4 q0)
| BinNums.xO q0 =>
BinNums.xI (add p4 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x4 : BinNums.positive) :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
BinNums.xO (...)
| BinNums.xO p5 =>
BinNums.xI p5
| BinNums.xH =>
BinNums.xO 1
end) p4)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x4 : BinNums.positive) :
BinNums.positive :=
match x4 with
| BinNums.xI p4 =>
BinNums.xO (...)
| BinNums.xO p4 =>
BinNums.xI p4
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x4 : BinNums.positive) :
BinNums.positive :=
match x4 with
| BinNums.xI p4 =>
BinNums.xO (...)
| BinNums.xO p4 =>
BinNums.xI p4
| BinNums.xH =>
BinNums.xO 1
end) q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p3 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p3 =>
(fix
iter (p4 : BinNums.positive)
(a : nat) {struct p4} : nat :=
match p4 with
| BinNums.xI p5 =>
(fix add
(n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p6 => S (add p6 m)
end) a
(iter p5
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p6 => S (add p6 m)
end) a a))
| BinNums.xO p5 =>
iter p5
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p6 => S (add p6 m)
end) a a)
| BinNums.xH => a
end) p3 1
end 57
else false
then fun inp : string => Some (x2, inp)
else fun _ : string => None) i'2
| None => None
end
with
| Some (_, i'2) =>
match
match
match i'2 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x3, i'3) =>
(if
if
match
match
(let
(a0, a1, a2, a3, a4, a5, a6, a7) :=
x3 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match (...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ...
end
| BinNums.Npos p4 =>
match ... with
| BinNums.N0 =>
... ... ...
| BinNums.Npos q =>
BinNums.Npos ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p4 =>
match
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end
with
add_carry
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end
for add) p4 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p4 =>
match
match
match
(if a1
then ...
else BinNums.N0)
with
| BinNums.N0 =>
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p5 =>
match ...
...
...
end with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (... p5 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p5 q0)
| BinNums.xO q0 =>
BinNums.xI (add p5 q0)
| BinNums.xH =>
BinNums.xO ((...) p5)
end
| BinNums.xO p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p5 q0)
| BinNums.xO q0 =>
BinNums.xO (add p5 q0)
| BinNums.xH =>
BinNums.xI p5
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO ((...) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p5 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p5 q0)
| BinNums.xH =>
BinNums.xI ((...) p5)
end
| BinNums.xO p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p5 q0)
| BinNums.xO q0 =>
BinNums.xI (add p5 q0)
| BinNums.xH =>
BinNums.xO ((...) p5)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI ((...) q0)
| BinNums.xO q0 =>
BinNums.xO ((...) q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p4 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p4 =>
(fix
iter (p5 : BinNums.positive)
(a : nat) {struct p5} : nat :=
match p5 with
| BinNums.xI p6 =>
(fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p7 => S (add p7 m)
end) a
(iter p6
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p7 => S (add p7 m)
end) a a))
| BinNums.xO p6 =>
iter p6
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p7 => S (add p7 m)
end) a a)
| BinNums.xH => a
end) p4 1
end
with
| 0 => false
| 1 => false
| 2 => false
| 3 => false
| 4 => false
| 5 => false
| 6 => false
| 7 => false
| 8 => false
| 9 => false
| 10 => false
| 11 => false
| 12 => false
| 13 => false
| 14 => false
| 15 => false
| 16 => false
| 17 => false
| 18 => false
| 19 => false
| 20 => false
| 21 => false
| 22 => false
| 23 => false
| 24 => false
| 25 => false
| 26 => false
| 27 => false
| 28 => false
| 29 => false
| 30 => false
| 31 => false
| 32 => false
| 33 => false
| 34 => false
| 35 => false
| 36 => false
| 37 => false
| 38 => false
| 39 => false
| 40 => false
| 41 => false
| 42 => false
| 43 => false
| 44 => false
| 45 => false
| 46 => false
| 47 => false
| S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S (S (S (S (S ...)))))))))))))))))))))))) =>
true
end
then
(fix leb (n m : nat) {struct n} : bool :=
match n with
| 0 => true
| S n' =>
match m with
| 0 => false
| S m' => leb n' m'
end
end)
match
(let
(a0, a1, a2, a3, a4, a5, a6, a7) :=
x3 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a2
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| ... ...
| ... ...
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p4 =>
match
match ... with
| ... BinNums.N0
| ... ...
end
with
| BinNums.N0 =>
if a2
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ((...) p4 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p4 =>
match
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p5 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI ...
| BinNums.xH =>
BinNums.xO ...
end
| BinNums.xO p5 =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI p5
end
| BinNums.xH =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI ...
end
| BinNums.xO p5 =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI ...
| BinNums.xH =>
BinNums.xO ...
end
| BinNums.xH =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p4 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
| BinNums.Npos p4 =>
match
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p5 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p5 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
... {struct x4} :
BinNums.positive :=
...
...
...
...
end
with
add_carry
... {struct x4} :
BinNums.positive :=
...
...
...
...
end
for add) p5 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p5 q0)
| BinNums.xO q0 =>
BinNums.xI (add p5 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x5 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) p5)
end
| BinNums.xO p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p5 q0)
| BinNums.xO q0 =>
BinNums.xO (add p5 q0)
| BinNums.xH =>
BinNums.xI p5
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO
((fix
succ
(x5 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x4 y : BinNums.positive)
{struct x4} :
BinNums.positive :=
match x4 with
| BinNums.xI p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p5 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p5 q0)
| BinNums.xH =>
BinNums.xI
((fix
succ
(x5 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) p5)
end
| BinNums.xO p5 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p5 q0)
| BinNums.xO q0 =>
BinNums.xI (add p5 q0)
| BinNums.xH =>
BinNums.xO
((fix
succ
(x5 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) p5)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI
((fix
succ
(x5 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) q0)
| BinNums.xO q0 =>
BinNums.xO
((fix
succ
(x5 : BinNums.positive) :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end) q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p4 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p4 =>
(fix
iter (p5 : BinNums.positive)
(a : nat) {struct p5} : nat :=
match p5 with
| BinNums.xI p6 =>
(fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p7 => S (add p7 m)
end) a
(iter p6
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p7 => S (add p7 m)
end) a a))
| BinNums.xO p6 =>
iter p6
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p7 => S (add p7 m)
end) a a)
| BinNums.xH => a
end) p4 1
end 57
else false
then fun inp : string => Some (x3, inp)
else fun _ : string => None) i'3
| None => None
end
with
| Some (_, i'3) =>
match
match
match i'3 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x4, i'4) =>
(if
if
match
x4 as a
return
({":"%char = a} +
{":"%char = a -> False})
with
| Ascii b8 b9 b10 b11 b12 b13 b14
b15 =>
match
(if b8 as b
return
({false = b} +
{false = b -> False})
then
right
(fun H : false = true =>
match
match
H in (_ = y)
return
(if y then False else True)
with
| eq_refl => I
end
return False
with
end)
else left eq_refl)
with
| left a0 =>
match
(if b9 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
match
H in (_ = y)
return
(if y then True else False)
with
| eq_refl => I
end
return False
with
end))
with
| left a1 =>
match
(if b10 as b
return
({false = b} +
{false = b -> False})
then
right
(fun H : false = true =>
match
match
H in (...) return (...)
with
| eq_refl => I
end
return False
with
end)
else left eq_refl)
with
| left a2 =>
match
(if b11 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
match ... ... with
| eq_refl => I
end
return False
with
end))
with
| left a3 =>
match
(if b12 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
...
...
end return False
with
end))
with
| left a4 =>
match
(if b13 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match ... ... with
end))
with
| left a5 =>
match
(if b14 as b
return ({...} + {...})
then
right (fun ... => ...
end)
else left eq_refl)
with
| left a6 =>
match
(if b15 as b return (...)
then right (...)
else left eq_refl)
with
| left a7 =>
left
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... = ...)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
| right diseq =>
right
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
end
| right diseq =>
right
match
match
a0 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a2 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
fun absurd : ... = ... =>
diseq
match ... with
| ... eq_refl
end
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a2 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 b9 y true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 b9 b10 true true
true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return (true = ...)
with
| eq_refl => eq_refl
end
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match
a1 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii b8 y false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 b9 false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(false =
match y with
| Ascii _ _ b1 _ _ _ _
_ => b1
end)
with
| eq_refl => eq_refl
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = false)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 true false true
true true false false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(true =
match y with
| Ascii _ b0 _ _ _ _ _
_ => b0
end)
with
| eq_refl => eq_refl
end
end
end
| right diseq =>
right
(fun
absurd :
":"%char =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(false =
match y with
| Ascii b _ _ _ _ _ _ _ =>
b
end)
with
| eq_refl => eq_refl
end)
end
end
then true
else false
then fun inp : string => Some (x4, inp)
else fun _ : string => None) i'4
| None => None
end
with
| Some (_, i'4) =>
match
match
match i'4 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x5, i'5) =>
(if
if
match
match
(let
(a0, a1, a2, a3, a4, a5,
a6, a7) := x5 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then ...
else BinNums.N0)
with
| BinNums.N0 =>
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p6 =>
match ...
...
...
end with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (... p6 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p6 =>
match
match
match ... with
| BinNums.N0 =>
...
...
...
end
| BinNums.Npos p7 =>
...
...
...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x6 y : BinNums.positive)
{struct x6} :
BinNums.positive :=
match x6 with
| BinNums.xI p7 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p7 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
with
add_carry
(x6 y : BinNums.positive)
{struct x6} :
BinNums.positive :=
match x6 with
| BinNums.xI p7 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xO p7 =>
match ... with
| ... ...
| ... ...
| ... ...
end
| BinNums.xH =>
match ... with
| ... ...
| ... ...
| ... ...
end
end
for add) p6 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p6 =>
(fix
iter
(p7 : BinNums.positive)
(a : nat) {struct p7} :
nat :=
match p7 with
| BinNums.xI p8 =>
(fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p9 => S (add p9 m)
end) a
(iter p8
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p9 => S (add p9 m)
end) a a))
| BinNums.xO p8 =>
iter p8
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p9 => S (add p9 m)
end) a a)
| BinNums.xH => a
end) p6 1
end
with
| 0 => false
| 1 => false
| 2 => false
| 3 => false
| 4 => false
| 5 => false
| 6 => false
| 7 => false
| 8 => false
| 9 => false
| 10 => false
| 11 => false
| 12 => false
| 13 => false
| 14 => false
| 15 => false
| 16 => false
| 17 => false
| 18 => false
| 19 => false
| 20 => false
| 21 => false
| 22 => false
| 23 => false
| 24 => false
| 25 => false
| 26 => false
| 27 => false
| 28 => false
| 29 => false
| 30 => false
| 31 => false
| 32 => false
| 33 => false
| 34 => false
| 35 => false
| 36 => false
| 37 => false
| 38 => false
| 39 => false
| 40 => false
| 41 => false
| 42 => false
| 43 => false
| 44 => false
| 45 => false
| 46 => false
| 47 => false
| S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S (S (S (S (S ...)))))))))))))))))))) =>
true
end
then
(fix leb
(n m : nat) {struct n} : bool :=
match n with
| 0 => true
| S n' =>
match m with
| 0 => false
| S m' => leb n' m'
end
end)
match
(let
(a0, a1, a2, a3, a4, a5,
a6, a7) := x5 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p6 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p6 =>
match
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
... {struct x6} :
BinNums.positive :=
...
...
...
...
end
with
add_carry
... {struct x6} :
BinNums.positive :=
...
...
...
...
end
for add) p6 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p6 =>
match
match
match (... ... ...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
| BinNums.Npos p7 =>
match ... with
| BinNums.N0 =>
if a1
then ...
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos (...)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x6 y : BinNums.positive)
{struct x6} :
BinNums.positive :=
match x6 with
| BinNums.xI p7 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p7 q0)
| BinNums.xO q0 =>
BinNums.xI (add p7 q0)
| BinNums.xH =>
BinNums.xO (... p7)
end
| BinNums.xO p7 =>
match y with
| BinNums.xI q0 =>
BinNums.xI (add p7 q0)
| BinNums.xO q0 =>
BinNums.xO (add p7 q0)
| BinNums.xH =>
BinNums.xI p7
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xO (... q0)
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x6 y : BinNums.positive)
{struct x6} :
BinNums.positive :=
match x6 with
| BinNums.xI p7 =>
match y with
| BinNums.xI q0 =>
BinNums.xI
(add_carry p7 q0)
| BinNums.xO q0 =>
BinNums.xO
(add_carry p7 q0)
| BinNums.xH =>
BinNums.xI (... p7)
end
| BinNums.xO p7 =>
match y with
| BinNums.xI q0 =>
BinNums.xO
(add_carry p7 q0)
| BinNums.xO q0 =>
BinNums.xI (add p7 q0)
| BinNums.xH =>
BinNums.xO (... p7)
end
| BinNums.xH =>
match y with
| BinNums.xI q0 =>
BinNums.xI (... q0)
| BinNums.xO q0 =>
BinNums.xO (... q0)
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p6 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p6 =>
(fix
iter
(p7 : BinNums.positive)
(a : nat) {struct p7} :
nat :=
match p7 with
| BinNums.xI p8 =>
(fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p9 => S (add p9 m)
end) a
(iter p8
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p9 => S (add p9 m)
end) a a))
| BinNums.xO p8 =>
iter p8
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p9 => S (add p9 m)
end) a a)
| BinNums.xH => a
end) p6 1
end 57
else false
then
fun inp : string => Some (x5, inp)
else fun _ : string => None) i'5
| None => None
end
with
| Some (_, i'5) =>
match
match
match i'5 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x6, i'6) =>
(if
if
match
match
(let
(a0, a1, a2, a3, a4, a5,
a6, a7) := x6 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match (...) with
| BinNums.N0 =>
match ... with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ...
end
| BinNums.Npos p7 =>
match ... with
| BinNums.N0 =>
... ... ...
| BinNums.Npos q =>
BinNums.Npos ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p7 =>
match
match ...
...
...
end with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x7 y : BinNums.positive)
{struct x7} :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end
with
add_carry
(x7 y : BinNums.positive)
{struct x7} :
BinNums.positive :=
match ... with
| ... ...
| ... ...
| ... ...
end
for add) p7 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p7 =>
(fix
iter
(p8 : BinNums.positive)
(a : nat) {struct p8} :
nat :=
match p8 with
| BinNums.xI p9 =>
(fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p10 => S (add p10 m)
end) a
(iter p9
((fix
add
(n m : nat) {struct n} :
nat :=
match ... with
| 0 => m
| S p10 => S ...
end) a a))
| BinNums.xO p9 =>
iter p9
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p10 => S (add p10 m)
end) a a)
| BinNums.xH => a
end) p7 1
end
with
| 0 => false
| 1 => false
| 2 => false
| 3 => false
| 4 => false
| 5 => false
| 6 => false
| 7 => false
| 8 => false
| 9 => false
| 10 => false
| 11 => false
| 12 => false
| 13 => false
| 14 => false
| 15 => false
| 16 => false
| 17 => false
| 18 => false
| 19 => false
| 20 => false
| 21 => false
| 22 => false
| 23 => false
| 24 => false
| 25 => false
| 26 => false
| 27 => false
| 28 => false
| 29 => false
| 30 => false
| 31 => false
| 32 => false
| 33 => false
| 34 => false
| 35 => false
| 36 => false
| 37 => false
| 38 => false
| 39 => false
| 40 => false
| 41 => false
| 42 => false
| 43 => false
| 44 => false
| 45 => false
| 46 => false
| 47 => false
| S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S
(S (S (S (S (S ...)))))))))))))))))) =>
true
end
then
(fix
leb
(n m : nat) {struct n} :
bool :=
match n with
| 0 => true
| S n' =>
match m with
| 0 => false
| S m' => leb n' m'
end
end)
match
(let
(a0, a1, a2, a3, a4, a5,
a6, a7) := x6 in
match
(if a0
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match
(if a1
then BinNums.Npos 1
else BinNums.N0)
with
| BinNums.N0 =>
match
match ... with
| ... ...
| ... ...
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p7 =>
match
match ... with
| ... BinNums.N0
| ... ...
end
with
| BinNums.N0 =>
if a1
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos ((...) p7 q)
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
| BinNums.Npos p7 =>
match
match
match ... with
| BinNums.N0 =>
match ... with
| ... BinNums.N0
| ... ...
end
| BinNums.Npos p8 =>
match ... with
| ... ...
| ... ...
end
end
with
| BinNums.N0 => BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
(BinNums.xO q)
end
with
| BinNums.N0 =>
if a0
then BinNums.Npos 1
else BinNums.N0
| BinNums.Npos q =>
BinNums.Npos
((fix
add
(x7 y : BinNums.positive)
{struct x7} :
BinNums.positive :=
match x7 with
| BinNums.xI p8 =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI ...
| BinNums.xH =>
BinNums.xO ...
end
| BinNums.xO p8 =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI p8
end
| BinNums.xH =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI q0
| BinNums.xH =>
BinNums.xO 1
end
end
with
add_carry
(x7 y : BinNums.positive)
{struct x7} :
BinNums.positive :=
match x7 with
| BinNums.xI p8 =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI ...
end
| BinNums.xO p8 =>
match ... with
| BinNums.xI q0 =>
BinNums.xO ...
| BinNums.xO q0 =>
BinNums.xI ...
| BinNums.xH =>
BinNums.xO ...
end
| BinNums.xH =>
match ... with
| BinNums.xI q0 =>
BinNums.xI ...
| BinNums.xO q0 =>
BinNums.xO ...
| BinNums.xH =>
BinNums.xI 1
end
end
for add) p7 q)
end
end)
with
| BinNums.N0 => 0
| BinNums.Npos p7 =>
(fix
iter
(p8 : BinNums.positive)
(a : nat) {struct p8} :
nat :=
match p8 with
| BinNums.xI p9 =>
(fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p10 => S (add p10 m)
end) a
(iter p9
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p10 => S (add p10 m)
end) a a))
| BinNums.xO p9 =>
iter p9
((fix
add
(n m : nat) {struct n} :
nat :=
match n with
| 0 => m
| S p10 => S (add p10 m)
end) a a)
| BinNums.xH => a
end) p7 1
end 57
else false
then
fun inp : string =>
Some (x6, inp)
else fun _ : string => None) i'6
| None => None
end
with
| Some (_, i'6) =>
match
match
match
match i'6 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x7, i'7) =>
(if
if
match
x7 as a
return
({"p"%char = a} +
{"p"%char = a -> False})
with
| Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
match
(if b8 as b
return
({false = b} +
{false = b -> False})
then
right
(fun H : false = true =>
match ... ... with
end)
else left eq_refl)
with
| left a0 =>
match
(if b9 as b
return ({...} + {...})
then
right (fun ... => ...
end)
else left eq_refl)
with
| left a1 =>
match
(if b10 as b return (...)
then right (...)
else left eq_refl)
with
| left a2 =>
match
(if b11 as b ...
then ...
else ...)
with
| left a3 =>
match (...) with
| left a4 =>
match ... with
| left a5 =>
...
...
...
end
| right diseq => right ...
end
| right diseq =>
right
match ... with
| ... ...
end
end
| right diseq =>
right
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
| right diseq =>
right
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
fun ... => diseq ...
end
end
end
| right diseq =>
right
match
match
a0 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y false false false
true true true false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 false false false
true true true false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in ... return ...
with
| eq_refl => eq_refl
end
end
end
| right diseq =>
right
(fun
absurd :
"p"%char =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(false = ...
...
end)
with
| eq_refl => eq_refl
end)
end
end
then true
else false
then
fun inp : string =>
Some (x7, inp)
else
fun _ : string => None)
i'7
| None => None
end
with
| Some (_, i'7) =>
match
match
match
match i'7 with
| "" => None
| String h t =>
Some (h, t)
end
with
| Some (x8, i'8) =>
(if
if
match
x8 as a
return
({"m"%char = a} +
{"m"%char = a -> False})
with
| Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
match
(if b8 as b ...
then ...
else ...)
with
| left a0 =>
match (...) with
| left a1 =>
match ... with
| left a2 =>
...
...
...
end
| right diseq => right ...
end
| right diseq =>
right
match ... with
| ... ...
end
end
| right diseq =>
right
(fun absurd : ... =>
diseq ...
...
end)
end
end
then true
else false
then
fun inp : string =>
Some (x8, inp)
else
fun _ : string => None)
i'8
| None => None
end
with
| Some (_, i'8) =>
Some ("m", i'8)
| None => None
end
with
| Some (_, i'8) =>
Some ("pm", i'8)
| None => None
end
| None => None
end
with
| Some p7 => Some p7
| None =>
match
match
match i'6 with
| "" => None
| String h t => Some (h, t)
end
with
| Some (x7, i'7) =>
(if
if
match
x7 as a
return
({"a"%char = a} +
{"a"%char = a -> False})
with
| Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
match
(if b8 as b
return
({true = b} +
{true = b -> False})
then left eq_refl
else
right
(fun H : true = false =>
match
...
...
end return False
with
end))
with
| left a0 =>
match
(if b9 as b
return
({false = b} +
{false = b -> False})
then
right
(fun H : false = true =>
match ... ... with
end)
else left eq_refl)
with
| left a1 =>
match
(if b10 as b
return ({...} + {...})
then
right (fun ... => ...
end)
else left eq_refl)
with
| left a2 =>
match
(if b11 as b return (...)
then right (...)
else left eq_refl)
with
| left a3 =>
match
(if b12 as b ...
then ...
else ...)
with
| left a4 =>
match (...) with
| left a5 =>
match ... with
| left a6 =>
...
...
...
end
| right diseq => right ...
end
| right diseq =>
right
match ... with
| ... ...
end
end
| right diseq =>
right
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
| right diseq =>
right
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
match
... in ... return ...
with
| eq_refl =>
match ... with
| ... ...
end
end
end
end
| right diseq =>
right
match
match
a0 in ... return ...
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y false false false
false true true false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
match
match ... with
| ... eq_refl
end in
(_ = y)
return (... -> False)
with
| eq_refl =>
fun absurd : ... = ... =>
diseq
match ... with
| ... eq_refl
end
end
end
end
| right diseq =>
right
match
match
a0 in (_ = y)
return (y = true)
with
| eq_refl => eq_refl
end in
(_ = y)
return
(Ascii y false false false
false true true false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 -> False)
with
| eq_refl =>
fun
absurd :
Ascii b8 false false false
false true true false =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return (false = ...)
with
| eq_refl => eq_refl
end
end
end
| right diseq =>
right
(fun
absurd :
"a"%char =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match
absurd in (_ = y)
return
(true =
match ... with
| Ascii b _ _ _ _ _ _ _ =>
b
end)
with
| eq_refl => eq_refl
end)
end
end
then true
else false
then
fun inp : string =>
Some (x7, inp)
else
fun _ : string => None)
i'7
| None => None
end
with
| Some (_, i'7) =>
match
match
match
match i'7 with
| "" => None
| String h t =>
Some (h, t)
end
with
| Some (x8, i'8) =>
(if
if
match
x8 as a
return
({"m"%char = a} +
{"m"%char = a -> False})
with
| Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
match
(if b8 as b return (...)
then left eq_refl
else right (...))
with
| left a0 =>
match
(if b9 as b ...
then ...
else ...)
with
| left a1 =>
match (...) with
| left a2 =>
match ... with
| left a3 =>
...
...
...
end
| right diseq => right ...
end
| right diseq =>
right
match ... with
| ... ...
end
end
| right diseq =>
right
match
... in ... return ...
with
| eq_refl =>
fun ... => diseq ...
end
end
| right diseq =>
right
(fun
absurd :
"m"%char =
Ascii b8 b9 b10 b11 b12
b13 b14 b15 =>
diseq
match ... ... with
| eq_refl => eq_refl
end)
end
end
then true
else false
then
fun inp : string =>
Some (x8, inp)
else
fun _ : string => None)
i'8
| None => None
end
with
| Some (_, i'8) =>
Some ("m", i'8)
| None => None
end
with
| Some (_, i'8) =>
Some ("am", i'8)
| None => None
end
| None => None
end
end
| None => None
end
| None => None
end
| None => None
end
| None => None
end
| None => None
end
| None => None
end
| None => None
end
| None => None
end
: parser string
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment