rust/tests/ui/parser/survive-peano-lesson-queue.rs
Jubilee Young cdeb170fc2 Ensure stack before parsing dot-or-call
There are many cases where, due to codegen or a massively unruly codebase,
a deeply nested call(call(call(call(call(call(call(call(call(f())))))))))
can happen. This is a spot where it would be good to grow our stack, so that
we can survive to tell the programmer their code is dubiously written.
2024-03-18 21:35:18 -07:00

4908 lines
7.7 MiB

//@ build-pass
// ignore-tidy-filelength
// ignore-tidy-linelength
// some very lightly modified generated code from issue rust-lang/rust#122715
// the main differences are to strip the dependency on bumpalo so it can be tested separately
// the original purpose of this code was to implement a binomial queue, however it is extracted from Gallina
// which means that it uses an incredibly naive Peano representation of the natural numbers.
// this is fairly standard "someone did something very silly and we should try to gracefully handle it"
#![allow(dead_code)]
#![allow(non_camel_case_types)]
#![allow(unused_imports)]
#![allow(non_snake_case)]
#![allow(unused_variables)]
use std::marker::PhantomData;
fn __nat_succ(x: u64) -> u64 {
x.checked_add(1).unwrap()
}
macro_rules! __nat_elim {
($zcase:expr, $pred:ident, $scase:expr, $val:expr) => {
{ let v = $val;
if v == 0 { $zcase } else { let $pred = v - 1; $scase } }
}
}
macro_rules! __andb { ($b1:expr, $b2:expr) => { $b1 && $b2 } }
macro_rules! __orb { ($b1:expr, $b2:expr) => { $b1 || $b2 } }
fn __pos_onebit(x: u64) -> u64 {
x.checked_mul(2).unwrap() + 1
}
fn __pos_zerobit(x: u64) -> u64 {
x.checked_mul(2).unwrap()
}
macro_rules! __pos_elim {
($p:ident, $onebcase:expr, $p2:ident, $zerobcase:expr, $onecase:expr, $val:expr) => {
{
let n = $val;
if n == 1 {
$onecase
} else if (n & 1) == 0 {
let $p2 = n >> 1;
$zerobcase
} else {
let $p = n >> 1;
$onebcase
}
}
}
}
fn __Z_frompos(z: u64) -> i64 {
use std::convert::TryFrom;
i64::try_from(z).unwrap()
}
fn __Z_fromneg(z : u64) -> i64 {
use std::convert::TryFrom;
i64::try_from(z).unwrap().checked_neg().unwrap()
}
macro_rules! __Z_elim {
($zero_case:expr, $p:ident, $pos_case:expr, $p2:ident, $neg_case:expr, $val:expr) => {
{
let n = $val;
if n == 0 {
$zero_case
} else if n < 0 {
let $p2 = n.unsigned_abs();
$neg_case
} else {
let $p = n as u64;
$pos_case
}
}
}
}
fn __N_frompos(z: u64) -> u64 {
z
}
macro_rules! __N_elim {
($zero_case:expr, $p:ident, $pos_case:expr, $val:expr) => {
{ let $p = $val; if $p == 0 { $zero_case } else { $pos_case } }
}
}
type __pair<A, B> = (A, B);
macro_rules! __pair_elim {
($fst:ident, $snd:ident, $body:expr, $p:expr) => {
{ let ($fst, $snd) = $p; $body }
}
}
fn __mk_pair<A: Copy, B: Copy>(a: A, b: B) -> __pair<A, B> { (a, b) }
fn hint_app<TArg, TRet>(f: &dyn Fn(TArg) -> TRet) -> &dyn Fn(TArg) -> TRet {
f
}
#[derive(Debug, Clone)]
pub enum Coq_Init_Datatypes_list<'a, A> {
nil(PhantomData<&'a A>),
cons(PhantomData<&'a A>, A, &'a Coq_Init_Datatypes_list<'a, A>)
}
type CertiCoq_Benchmarks_lib_Binom_key<'a> = u64;
#[derive(Debug, Clone)]
pub enum CertiCoq_Benchmarks_lib_Binom_tree<'a> {
Node(PhantomData<&'a ()>, CertiCoq_Benchmarks_lib_Binom_key<'a>, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>),
Leaf(PhantomData<&'a ()>)
}
type CertiCoq_Benchmarks_lib_Binom_priqueue<'a> = &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>>;
struct Program {
}
impl<'a> Program {
fn new() -> Self {
Program {
}
}
fn alloc<T>(&'a self, t: T) -> &'a T {
let _alloc = Box::new(t);
Box::leak(_alloc)
}
fn closure<TArg, TRet>(&'a self, f: impl Fn(TArg) -> TRet + 'a) -> &'a dyn Fn(TArg) -> TRet {
let _alloc = Box::new(f);
Box::leak(_alloc)
}
fn Coq_Init_Nat_leb(&'a self, n: u64, m: u64) -> bool {
__nat_elim!(
{
true
},
n2, {
__nat_elim!(
{
false
},
m2, {
self.Coq_Init_Nat_leb(
n2,
m2)
},
m)
},
n)
}
fn Coq_Init_Nat_leb__curried(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> bool {
self.closure(move |n| {
self.closure(move |m| {
self.Coq_Init_Nat_leb(
n,
m)
})
})
}
fn Coq_Init_Nat_ltb(&'a self, n: u64, m: u64) -> bool {
self.Coq_Init_Nat_leb(
__nat_succ(
n),
m)
}
fn Coq_Init_Nat_ltb__curried(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> bool {
self.closure(move |n| {
self.closure(move |m| {
self.Coq_Init_Nat_ltb(
n,
m)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_smash(&'a self, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>, u: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a CertiCoq_Benchmarks_lib_Binom_tree<'a> {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t0) => {
match t0 {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t2, t3) => {
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
match u {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, y, u1, t2) => {
match t2 {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t3, t4) => {
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
match self.Coq_Init_Nat_ltb(
y,
x) {
true => {
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
x,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
y,
u1,
t1)),
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData))))
},
false => {
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
y,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
x,
t1,
u1)),
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData))))
},
}
},
}
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData))
},
}
},
}
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData))
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_smash__curried(&'a self) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a CertiCoq_Benchmarks_lib_Binom_tree<'a> {
self.closure(move |t| {
self.closure(move |u| {
self.CertiCoq_Benchmarks_lib_Binom_smash(
t,
u)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_carry(&'a self, q: &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>>, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>> {
match q {
&Coq_Init_Datatypes_list::nil(_) => {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t0, t1) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
t,
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))
},
}
},
&Coq_Init_Datatypes_list::cons(_, u, q2) => {
match u {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t0, t1) => {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t2, t3) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)),
self.CertiCoq_Benchmarks_lib_Binom_carry(
q2,
self.CertiCoq_Benchmarks_lib_Binom_smash(
t,
u))))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
u,
q2))
},
}
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
t,
q2))
},
}
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_carry__curried(&'a self) -> &'a dyn Fn(&'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>>) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>> {
self.closure(move |q| {
self.closure(move |t| {
self.CertiCoq_Benchmarks_lib_Binom_carry(
q,
t)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_insert(&'a self, x: CertiCoq_Benchmarks_lib_Binom_key<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.CertiCoq_Benchmarks_lib_Binom_carry(
q,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
x,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)),
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))))
}
fn CertiCoq_Benchmarks_lib_Binom_insert__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_key<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.closure(move |x| {
self.closure(move |q| {
self.CertiCoq_Benchmarks_lib_Binom_insert(
x,
q)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_insert_list(&'a self, l: &'a Coq_Init_Datatypes_list<'a, u64>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
match l {
&Coq_Init_Datatypes_list::nil(_) => {
q
},
&Coq_Init_Datatypes_list::cons(_, x, l2) => {
self.CertiCoq_Benchmarks_lib_Binom_insert_list(
l2,
self.CertiCoq_Benchmarks_lib_Binom_insert(
x,
q))
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_insert_list__curried(&'a self) -> &'a dyn Fn(&'a Coq_Init_Datatypes_list<'a, u64>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.closure(move |l| {
self.closure(move |q| {
self.CertiCoq_Benchmarks_lib_Binom_insert_list(
l,
q)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_make_list(&'a self, n: u64, l: &'a Coq_Init_Datatypes_list<'a, u64>) -> &'a Coq_Init_Datatypes_list<'a, u64> {
__nat_elim!(
{
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
0,
l))
},
n0, {
__nat_elim!(
{
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
__nat_succ(
0),
l))
},
n2, {
self.CertiCoq_Benchmarks_lib_Binom_make_list(
n2,
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
__nat_succ(
__nat_succ(
n2)),
l)))
},
n0)
},
n)
}
fn CertiCoq_Benchmarks_lib_Binom_make_list__curried(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(&'a Coq_Init_Datatypes_list<'a, u64>) -> &'a Coq_Init_Datatypes_list<'a, u64> {
self.closure(move |n| {
self.closure(move |l| {
self.CertiCoq_Benchmarks_lib_Binom_make_list(
n,
l)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_empty(&'a self) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))
}
fn CertiCoq_Benchmarks_lib_Binom_join(&'a self, p: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, c: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
match p {
&Coq_Init_Datatypes_list::nil(_) => {
self.CertiCoq_Benchmarks_lib_Binom_carry(
q,
c)
},
&Coq_Init_Datatypes_list::cons(_, p1, p2) => {
match p1 {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t, t0) => {
match q {
&Coq_Init_Datatypes_list::nil(_) => {
self.CertiCoq_Benchmarks_lib_Binom_carry(
p,
c)
},
&Coq_Init_Datatypes_list::cons(_, q1, q2) => {
match q1 {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t1, t2) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
c,
self.CertiCoq_Benchmarks_lib_Binom_join(
p2,
q2,
self.CertiCoq_Benchmarks_lib_Binom_smash(
p1,
q1))))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
match c {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t1, t2) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)),
self.CertiCoq_Benchmarks_lib_Binom_join(
p2,
q2,
self.CertiCoq_Benchmarks_lib_Binom_smash(
c,
p1))))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
p1,
self.CertiCoq_Benchmarks_lib_Binom_join(
p2,
q2,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))))
},
}
},
}
},
}
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
match q {
&Coq_Init_Datatypes_list::nil(_) => {
self.CertiCoq_Benchmarks_lib_Binom_carry(
p,
c)
},
&Coq_Init_Datatypes_list::cons(_, q1, q2) => {
match q1 {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t, t0) => {
match c {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t1, t2) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)),
self.CertiCoq_Benchmarks_lib_Binom_join(
p2,
q2,
self.CertiCoq_Benchmarks_lib_Binom_smash(
c,
q1))))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
q1,
self.CertiCoq_Benchmarks_lib_Binom_join(
p2,
q2,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))))
},
}
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
c,
self.CertiCoq_Benchmarks_lib_Binom_join(
p2,
q2,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))))
},
}
},
}
},
}
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_join__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.closure(move |p| {
self.closure(move |q| {
self.closure(move |c| {
self.CertiCoq_Benchmarks_lib_Binom_join(
p,
q,
c)
})
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_merge(&'a self, p: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.CertiCoq_Benchmarks_lib_Binom_join(
p,
q,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))
}
fn CertiCoq_Benchmarks_lib_Binom_merge__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.closure(move |p| {
self.closure(move |q| {
self.CertiCoq_Benchmarks_lib_Binom_merge(
p,
q)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_find_max_(&'a self, current: CertiCoq_Benchmarks_lib_Binom_key<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_key<'a> {
match q {
&Coq_Init_Datatypes_list::nil(_) => {
current
},
&Coq_Init_Datatypes_list::cons(_, t, q2) => {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t0, t1) => {
self.CertiCoq_Benchmarks_lib_Binom_find_max_(
match self.Coq_Init_Nat_ltb(
current,
x) {
true => {
x
},
false => {
current
},
},
q2)
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.CertiCoq_Benchmarks_lib_Binom_find_max_(
current,
q2)
},
}
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_find_max___curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_key<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_key<'a> {
self.closure(move |current| {
self.closure(move |q| {
self.CertiCoq_Benchmarks_lib_Binom_find_max_(
current,
q)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_find_max(&'a self, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<CertiCoq_Benchmarks_lib_Binom_key<'a>> {
match q {
&Coq_Init_Datatypes_list::nil(_) => {
None
},
&Coq_Init_Datatypes_list::cons(_, t, q2) => {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t0, t1) => {
Some(
self.CertiCoq_Benchmarks_lib_Binom_find_max_(
x,
q2))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.CertiCoq_Benchmarks_lib_Binom_find_max(
q2)
},
}
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_find_max__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<CertiCoq_Benchmarks_lib_Binom_key<'a>> {
self.closure(move |q| {
self.CertiCoq_Benchmarks_lib_Binom_find_max(
q)
})
}
fn CertiCoq_Benchmarks_lib_Binom_unzip(&'a self, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>, cont: &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t2) => {
self.CertiCoq_Benchmarks_lib_Binom_unzip(
t2,
self.closure(move |q| {
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
x,
t1,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))),
hint_app(cont)(q)))
}))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
hint_app(cont)(self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData)))
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_unzip__curried(&'a self) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a dyn Fn(&'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.closure(move |t| {
self.closure(move |cont| {
self.CertiCoq_Benchmarks_lib_Binom_unzip(
t,
cont)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_heap_delete_max(&'a self, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t0) => {
match t0 {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t2, t3) => {
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.CertiCoq_Benchmarks_lib_Binom_unzip(
t1,
self.closure(move |u| {
u
}))
},
}
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_heap_delete_max__curried(&'a self) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> {
self.closure(move |t| {
self.CertiCoq_Benchmarks_lib_Binom_heap_delete_max(
t)
})
}
fn CertiCoq_Benchmarks_lib_Binom_delete_max_aux(&'a self, m: CertiCoq_Benchmarks_lib_Binom_key<'a>, p: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> __pair<CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>> {
match p {
&Coq_Init_Datatypes_list::nil(_) => {
__mk_pair(
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData)),
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData)))
},
&Coq_Init_Datatypes_list::cons(_, t, p2) => {
match t {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t0) => {
match t0 {
&CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t2, t3) => {
__mk_pair(
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData)),
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData)))
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
match self.Coq_Init_Nat_ltb(
x,
m) {
true => {
__pair_elim!(
k, j, {
__mk_pair(
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
x,
t1,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))),
k)),
j)
},
self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux(
m,
p2))
},
false => {
__mk_pair(
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)),
p2)),
self.CertiCoq_Benchmarks_lib_Binom_heap_delete_max(
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Node(
PhantomData,
x,
t1,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData))))))
},
}
},
}
},
&CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => {
__pair_elim!(
k, j, {
__mk_pair(
self.alloc(
Coq_Init_Datatypes_list::cons(
PhantomData,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)),
k)),
j)
},
self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux(
m,
p2))
},
}
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_delete_max_aux__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_key<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> __pair<CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>> {
self.closure(move |m| {
self.closure(move |p| {
self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux(
m,
p)
})
})
}
fn CertiCoq_Benchmarks_lib_Binom_delete_max(&'a self, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<__pair<CertiCoq_Benchmarks_lib_Binom_key<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>>> {
match self.CertiCoq_Benchmarks_lib_Binom_find_max(
q) {
Some(m) => {
__pair_elim!(
q2, p, {
Some(
__mk_pair(
m,
self.CertiCoq_Benchmarks_lib_Binom_join(
q2,
p,
self.alloc(
CertiCoq_Benchmarks_lib_Binom_tree::Leaf(
PhantomData)))))
},
self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux(
m,
q))
},
None => {
None
},
}
}
fn CertiCoq_Benchmarks_lib_Binom_delete_max__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<__pair<CertiCoq_Benchmarks_lib_Binom_key<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>>> {
self.closure(move |q| {
self.CertiCoq_Benchmarks_lib_Binom_delete_max(
q)
})
}
fn CertiCoq_Benchmarks_lib_Binom_main(&'a self) -> CertiCoq_Benchmarks_lib_Binom_key<'a> {
let a =
self.CertiCoq_Benchmarks_lib_Binom_insert_list(
self.CertiCoq_Benchmarks_lib_Binom_make_list(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))),
self.CertiCoq_Benchmarks_lib_Binom_empty());
let b =
self.CertiCoq_Benchmarks_lib_Binom_insert_list(
self.CertiCoq_Benchmarks_lib_Binom_make_list(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))),
self.CertiCoq_Benchmarks_lib_Binom_empty());
let c =
self.CertiCoq_Benchmarks_lib_Binom_merge(
a,
b);
match self.CertiCoq_Benchmarks_lib_Binom_delete_max(
c) {
Some(p) => {
__pair_elim!(
p0, k, {
p0
},
p)
},
None => {
0
},
}
}
fn CertiCoq_Benchmarks_tests_binom(&'a self) -> CertiCoq_Benchmarks_lib_Binom_key<'a> {
self.CertiCoq_Benchmarks_lib_Binom_main()
}
}
fn main() {
println!("{:?}", Program::new().CertiCoq_Benchmarks_tests_binom())
}