diff options
| author | Jubilee Young <workingjubilee@gmail.com> | 2024-03-18 18:35:49 -0700 |
|---|---|---|
| committer | Jubilee Young <workingjubilee@gmail.com> | 2024-03-18 21:35:18 -0700 |
| commit | cdeb170fc21dc9099c2a79ea8c36be58a7b405f4 (patch) | |
| tree | 03ae3aaa611e0f7783fd4f9497f71cbad69d8d64 | |
| parent | 3c85e56249b0b1942339a6a989a971bf6f1c9e0f (diff) | |
| download | rust-cdeb170fc21dc9099c2a79ea8c36be58a7b405f4.tar.gz rust-cdeb170fc21dc9099c2a79ea8c36be58a7b405f4.zip | |
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.
| -rw-r--r-- | compiler/rustc_parse/src/parser/expr.rs | 5 | ||||
| -rw-r--r-- | tests/ui/parser/survive-peano-lesson-queue.rs | 4907 |
2 files changed, 4911 insertions, 1 deletions
diff --git a/compiler/rustc_parse/src/parser/expr.rs b/compiler/rustc_parse/src/parser/expr.rs index e27a5f93799..136145dd182 100644 --- a/compiler/rustc_parse/src/parser/expr.rs +++ b/compiler/rustc_parse/src/parser/expr.rs @@ -943,7 +943,10 @@ impl<'a> Parser<'a> { // Stitch the list of outer attributes onto the return value. // A little bit ugly, but the best way given the current code // structure - let res = self.parse_expr_dot_or_call_with_(e0, lo); + let res = ensure_sufficient_stack( + // this expr demonstrates the recursion it guards against + || self.parse_expr_dot_or_call_with_(e0, lo), + ); if attrs.is_empty() { res } else { diff --git a/tests/ui/parser/survive-peano-lesson-queue.rs b/tests/ui/parser/survive-peano-lesson-queue.rs new file mode 100644 index 00000000000..3608728594e --- /dev/null +++ b/tests/ui/parser/survive-peano-lesson-queue.rs @@ -0,0 +1,4907 @@ +//@ 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()) +} |