//@ 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); macro_rules! __pair_elim { ($fst:ident, $snd:ident, $body:expr, $p:expr) => { { let ($fst, $snd) = $p; $body } } } fn __mk_pair(a: A, b: B) -> __pair { (a, b) } fn hint_app(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(&'a self, t: T) -> &'a T { let _alloc = Box::new(t); Box::leak(_alloc) } fn closure(&'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> { 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> { 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>> { 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>> { 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_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_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()) }