tt('const/Omega/MAP2', ty, ![A : $t, B : $t]: (B > ((B > (B > A)) > (('type/list/list' B) > (('type/list/list' B) > ('type/list/list' A)))))).
tt('const/Omega/MAP2_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) > ('type/list/list' A))).
tt('const/Omega/calc_nightmare', ty, ('type/integer/int' > ('type/num/num' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o)))).
tt('const/Omega/calc_nightmare_tupled', ty, (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o)).
tt('const/Omega/dark_shadow', ty, (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))).
tt('const/Omega/dark_shadow_cond_row', ty, (('type/pair/prod' 'type/num/num' 'type/integer/int') > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))).
tt('const/Omega/dark_shadow_cond_row_tupled', ty, (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o)).
tt('const/Omega/dark_shadow_condition', ty, (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))).
tt('const/Omega/dark_shadow_condition_tupled', ty, (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o)).
tt('const/Omega/dark_shadow_row', ty, ('type/num/num' > ('type/integer/int' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o)))).
tt('const/Omega/dark_shadow_row_tupled', ty, (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o)).
tt('const/Omega/dark_shadow_tupled', ty, (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o)).
tt('const/Omega/evallower', ty, ('type/integer/int' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))).
tt('const/Omega/evallower_tupled', ty, (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o)).
tt('const/Omega/evalupper', ty, ('type/integer/int' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))).
tt('const/Omega/evalupper_tupled', ty, (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o)).
tt('const/Omega/fst1', ty, ![A : $t]: (('type/pair/prod' 'type/num/num' A) > $o)).
tt('const/Omega/fst_nzero', ty, ![A : $t]: (('type/pair/prod' 'type/num/num' A) > $o)).
tt('const/Omega/modhat', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/Omega/nightmare', ty, ('type/integer/int' > ('type/num/num' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o)))))).
tt('const/Omega/nightmare_tupled', ty, (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) > $o)).
tt('const/Omega/real_shadow', ty, (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))).
tt('const/Omega/rshadow_row', ty, (('type/pair/prod' 'type/num/num' 'type/integer/int') > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))).
tt('const/Omega/rshadow_row_tupled', ty, (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o)).
tt('const/Omega/sumc', ty, (('type/list/list' 'type/integer/int') > (('type/list/list' 'type/integer/int') > 'type/integer/int'))).
tt('const/Omega/sumc_tupled', ty, (('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) > 'type/integer/int')).
tt('thm/Omega/MAP2_tupled_primitive_def_', def, ![B : $t, A : $t]: (('const/Omega/MAP2_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) ('type/list/list' A)) (('const/min/@' (('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) > (('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) > $o))) (^[R : (('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) > (('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) > $o))]: ((('const/relation/WF' ('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))))) R) & ((![y : B, ys : ('type/list/list' B), f : (B > (B > A)), pad : B]: (R (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) ('const/list/NIL' B) ys))) (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) ('const/list/NIL' B) (('const/list/CONS' B) y ys)))))) & ((![x : B, xs : ('type/list/list' B), f : (B > (B > A)), pad : B]: (R (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) xs ('const/list/NIL' B)))) (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) (('const/list/CONS' B) x xs) ('const/list/NIL' B)))))) & (![y : B, x : B, ys : ('type/list/list' B), xs : ('type/list/list' B), f : (B > (B > A)), pad : B]: (R (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) xs ys))) (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) (('const/list/CONS' B) x xs) (('const/list/CONS' B) y ys))))))))))) (^[MAP2_tupled : (('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) > ('type/list/list' A)), a : ('type/pair/prod' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))))]: (('const/pair/pair_CASE' ('type/list/list' A) B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) a (^[pad : B, v1 : ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))]: (('const/pair/pair_CASE' ('type/list/list' A) (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) v1 (^[f : (B > (B > A)), v3 : ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))]: (('const/pair/pair_CASE' ('type/list/list' A) ('type/list/list' B) ('type/list/list' B)) v3 (^[v4 : ('type/list/list' B), v5 : ('type/list/list' B)]: (('const/list/list_CASE' B ('type/list/list' A)) v4 (('const/list/list_CASE' B ('type/list/list' A)) v5 (('const/combin/I' ('type/list/list' A)) ('const/list/NIL' A)) (^[y : B, ys : ('type/list/list' B)]: (('const/combin/I' ('type/list/list' A)) (('const/list/CONS' A) (f pad y) (MAP2_tupled (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) ('const/list/NIL' B) ys)))))))) (^[x : B, xs : ('type/list/list' B)]: (('const/list/list_CASE' B ('type/list/list' A)) v5 (('const/combin/I' ('type/list/list' A)) (('const/list/CONS' A) (f x pad) (MAP2_tupled (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) xs ('const/list/NIL' B))))))) (^['y\'' : B, 'ys\'' : ('type/list/list' B)]: (('const/combin/I' ('type/list/list' A)) (('const/list/CONS' A) (f x 'y\'') (MAP2_tupled (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) pad (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) f (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) xs 'ys\'')))))))))))))))))))).
tt('thm/Omega/MAP2_curried_def_', def, ![B : $t, A : $t]: (![x : B, x1 : (B > (B > A)), x2 : ('type/list/list' B), x3 : ('type/list/list' B)]: ((('const/Omega/MAP2' A B) x x1 x2 x3) = (('const/Omega/MAP2_tupled' A B) (('const/pair/,' B ('type/pair/prod' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B)))) x (('const/pair/,' (B > (B > A)) ('type/pair/prod' ('type/list/list' B) ('type/list/list' B))) x1 (('const/pair/,' ('type/list/list' B) ('type/list/list' B)) x2 x3))))))).
tt('thm/Omega/MAP2_ind_', ax, ![B : $t, A : $t]: (![P : (B > ((B > (B > A)) > (('type/list/list' B) > (('type/list/list' B) > $o))))]: (((![pad : B, f : (B > (B > A))]: (P pad f ('const/list/NIL' B) ('const/list/NIL' B))) & ((![pad : B, f : (B > (B > A)), y : B, ys : ('type/list/list' B)]: ((P pad f ('const/list/NIL' B) ys) => (P pad f ('const/list/NIL' B) (('const/list/CONS' B) y ys)))) & ((![pad : B, f : (B > (B > A)), x : B, xs : ('type/list/list' B)]: ((P pad f xs ('const/list/NIL' B)) => (P pad f (('const/list/CONS' B) x xs) ('const/list/NIL' B)))) & (![pad : B, f : (B > (B > A)), x : B, xs : ('type/list/list' B), y : B, ys : ('type/list/list' B)]: ((P pad f xs ys) => (P pad f (('const/list/CONS' B) x xs) (('const/list/CONS' B) y ys))))))) => (![v : B, v1 : (B > (B > A)), v2 : ('type/list/list' B), v3 : ('type/list/list' B)]: (P v v1 v2 v3))))).
tt('thm/Omega/MAP2_def_0', ax, ![A : $t, B : $t]: (![pad : B, f : (B > (B > A))]: ((('const/Omega/MAP2' A B) pad f ('const/list/NIL' B) ('const/list/NIL' B)) = ('const/list/NIL' A)))).
tt('thm/Omega/MAP2_def_1', ax, ![B : $t, A : $t]: (![ys : ('type/list/list' B), y : B, pad : B, f : (B > (B > A))]: ((('const/Omega/MAP2' A B) pad f ('const/list/NIL' B) (('const/list/CONS' B) y ys)) = (('const/list/CONS' A) (f pad y) (('const/Omega/MAP2' A B) pad f ('const/list/NIL' B) ys))))).
tt('thm/Omega/MAP2_def_2', ax, ![B : $t, A : $t]: (![xs : ('type/list/list' B), x : B, pad : B, f : (B > (B > A))]: ((('const/Omega/MAP2' A B) pad f (('const/list/CONS' B) x xs) ('const/list/NIL' B)) = (('const/list/CONS' A) (f x pad) (('const/Omega/MAP2' A B) pad f xs ('const/list/NIL' B)))))).
tt('thm/Omega/MAP2_def_e3', ax, ![B : $t, A : $t]: (![ys : ('type/list/list' B), y : B, xs : ('type/list/list' B), x : B, pad : B, f : (B > (B > A))]: ((('const/Omega/MAP2' A B) pad f (('const/list/CONS' B) x xs) (('const/list/CONS' B) y ys)) = (('const/list/CONS' A) (f x y) (('const/Omega/MAP2' A B) pad f xs ys))))).
tt('thm/Omega/MAP2_zero_ADD_0', ax, (![xs : ('type/list/list' 'type/integer/int')]: ((('const/Omega/MAP2' 'type/integer/int' 'type/integer/int') ('const/integer/int_of_num' 'const/num/0') 'const/integer/int_add' ('const/list/NIL' 'type/integer/int') xs) = xs))).
tt('thm/Omega/MAP2_zero_ADD_e1', ax, (![xs : ('type/list/list' 'type/integer/int')]: ((('const/Omega/MAP2' 'type/integer/int' 'type/integer/int') ('const/integer/int_of_num' 'const/num/0') 'const/integer/int_add' xs ('const/list/NIL' 'type/integer/int')) = xs))).
tt('thm/Omega/sumc_tupled_primitive_def_', def, ('const/Omega/sumc_tupled' = (('const/relation/WFREC' ('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) 'type/integer/int') (('const/min/@' (('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) > (('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) > $o))) (^[R : (('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) > (('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int'))) R) & (![v : 'type/integer/int', c : 'type/integer/int', vs : ('type/list/list' 'type/integer/int'), cs : ('type/list/list' 'type/integer/int')]: (R (('const/pair/,' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) cs vs) (('const/pair/,' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) (('const/list/CONS' 'type/integer/int') c cs) (('const/list/CONS' 'type/integer/int') v vs))))))) (^[sumc_tupled : (('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) > 'type/integer/int'), a : ('type/pair/prod' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int'))]: (('const/pair/pair_CASE' 'type/integer/int' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) a (^[v0 : ('type/list/list' 'type/integer/int'), v3 : ('type/list/list' 'type/integer/int')]: (('const/list/list_CASE' 'type/integer/int' 'type/integer/int') v3 (('const/combin/I' 'type/integer/int') ('const/integer/int_of_num' 'const/num/0')) (^[v : 'type/integer/int', vs : ('type/list/list' 'type/integer/int')]: (('const/list/list_CASE' 'type/integer/int' 'type/integer/int') v0 (('const/combin/I' 'type/integer/int') ('const/integer/int_of_num' 'const/num/0')) (^[c : 'type/integer/int', cs : ('type/list/list' 'type/integer/int')]: (('const/combin/I' 'type/integer/int') ('const/integer/int_add' ('const/integer/int_mul' c v) (sumc_tupled (('const/pair/,' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) cs vs)))))))))))))).
tt('thm/Omega/sumc_curried_def_', def, (![x : ('type/list/list' 'type/integer/int'), x1 : ('type/list/list' 'type/integer/int')]: (('const/Omega/sumc' x x1) = ('const/Omega/sumc_tupled' (('const/pair/,' ('type/list/list' 'type/integer/int') ('type/list/list' 'type/integer/int')) x x1))))).
tt('thm/Omega/sumc_ind_', ax, (![P : (('type/list/list' 'type/integer/int') > (('type/list/list' 'type/integer/int') > $o))]: (((![v0 : ('type/list/list' 'type/integer/int')]: (P v0 ('const/list/NIL' 'type/integer/int'))) & ((![v4 : 'type/integer/int', v5 : ('type/list/list' 'type/integer/int')]: (P ('const/list/NIL' 'type/integer/int') (('const/list/CONS' 'type/integer/int') v4 v5))) & (![c : 'type/integer/int', cs : ('type/list/list' 'type/integer/int'), v : 'type/integer/int', vs : ('type/list/list' 'type/integer/int')]: ((P cs vs) => (P (('const/list/CONS' 'type/integer/int') c cs) (('const/list/CONS' 'type/integer/int') v vs)))))) => (![v : ('type/list/list' 'type/integer/int'), v1 : ('type/list/list' 'type/integer/int')]: (P v v1))))).
tt('thm/Omega/sumc_def_0', ax, (![v0 : ('type/list/list' 'type/integer/int')]: (('const/Omega/sumc' v0 ('const/list/NIL' 'type/integer/int')) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/Omega/sumc_def_1', ax, (![v5 : ('type/list/list' 'type/integer/int'), v4 : 'type/integer/int']: (('const/Omega/sumc' ('const/list/NIL' 'type/integer/int') (('const/list/CONS' 'type/integer/int') v4 v5)) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/Omega/sumc_def_e2', ax, (![vs : ('type/list/list' 'type/integer/int'), v : 'type/integer/int', cs : ('type/list/list' 'type/integer/int'), c : 'type/integer/int']: (('const/Omega/sumc' (('const/list/CONS' 'type/integer/int') c cs) (('const/list/CONS' 'type/integer/int') v vs)) = ('const/integer/int_add' ('const/integer/int_mul' c v) ('const/Omega/sumc' cs vs))))).
tt('thm/Omega/sumc_thm_0', ax, (![vs : ('type/list/list' 'type/integer/int')]: (('const/Omega/sumc' ('const/list/NIL' 'type/integer/int') vs) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/Omega/sumc_thm_1', ax, (![cs : ('type/list/list' 'type/integer/int')]: (('const/Omega/sumc' cs ('const/list/NIL' 'type/integer/int')) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/Omega/sumc_thm_e2', ax, (![vs : ('type/list/list' 'type/integer/int'), v : 'type/integer/int', cs : ('type/list/list' 'type/integer/int'), c : 'type/integer/int']: (('const/Omega/sumc' (('const/list/CONS' 'type/integer/int') c cs) (('const/list/CONS' 'type/integer/int') v vs)) = ('const/integer/int_add' ('const/integer/int_mul' c v) ('const/Omega/sumc' cs vs))))).
tt('thm/Omega/sumc_ADD_', ax, (![cs : ('type/list/list' 'type/integer/int'), vs : ('type/list/list' 'type/integer/int'), ds : ('type/list/list' 'type/integer/int')]: (('const/integer/int_add' ('const/Omega/sumc' cs vs) ('const/Omega/sumc' ds vs)) = ('const/Omega/sumc' (('const/Omega/MAP2' 'type/integer/int' 'type/integer/int') ('const/integer/int_of_num' 'const/num/0') 'const/integer/int_add' cs ds) vs)))).
tt('thm/Omega/sumc_MULT_', ax, (![cs : ('type/list/list' 'type/integer/int'), vs : ('type/list/list' 'type/integer/int'), f : 'type/integer/int']: (('const/integer/int_mul' f ('const/Omega/sumc' cs vs)) = ('const/Omega/sumc' (('const/list/MAP' 'type/integer/int' 'type/integer/int') (^[x : 'type/integer/int']: ('const/integer/int_mul' f x)) cs) vs)))).
tt('thm/Omega/sumc_singleton_', ax, (![f : ('type/integer/int' > 'type/integer/int'), c : 'type/integer/int']: (('const/Omega/sumc' (('const/list/MAP' 'type/integer/int' 'type/integer/int') f (('const/list/CONS' 'type/integer/int') c ('const/list/NIL' 'type/integer/int'))) (('const/list/CONS' 'type/integer/int') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/list/NIL' 'type/integer/int'))) = (f c)))).
tt('thm/Omega/sumc_nonsingle_', ax, (![f : ('type/integer/int' > 'type/integer/int'), cs : ('type/list/list' 'type/integer/int'), c : 'type/integer/int', v : 'type/integer/int', vs : ('type/list/list' 'type/integer/int')]: (('const/Omega/sumc' (('const/list/MAP' 'type/integer/int' 'type/integer/int') f (('const/list/CONS' 'type/integer/int') c cs)) (('const/list/CONS' 'type/integer/int') v vs)) = ('const/integer/int_add' ('const/integer/int_mul' (f c) v) ('const/Omega/sumc' (('const/list/MAP' 'type/integer/int' 'type/integer/int') f cs) vs))))).
tt('thm/Omega/modhat_def_', def, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/Omega/modhat' x y) = ('const/integer/int_sub' x ('const/integer/int_mul' y ('const/integer/int_div' ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x) y) ('const/integer/int_mul' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) y))))))).
tt('thm/Omega/equality_removal_', ax, (![c : 'type/integer/int', x : 'type/integer/int', cs : ('type/list/list' 'type/integer/int'), vs : ('type/list/list' 'type/integer/int')]: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') c) => ((('const/integer/int_of_num' 'const/num/0') = ('const/integer/int_add' ('const/integer/int_mul' c x) ('const/Omega/sumc' cs vs))) = (?[s : 'type/integer/int']: ((x = ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_add' c ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) s) ('const/Omega/sumc' (('const/list/MAP' 'type/integer/int' 'type/integer/int') (^[x0 : 'type/integer/int']: ('const/Omega/modhat' x0 ('const/integer/int_add' c ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) cs) vs))) & (('const/integer/int_of_num' 'const/num/0') = ('const/integer/int_add' ('const/integer/int_mul' c x) ('const/Omega/sumc' cs vs))))))))).
tt('thm/Omega/evalupper_tupled_primitive_def_', def, ('const/Omega/evalupper_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) $o) (('const/min/@' (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))) (^[R : (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) R) & (![y : 'type/integer/int', c : 'type/num/num', cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int']: (R (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x cs) (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c y) cs))))))) (^[evalupper_tupled : (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o), a : ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) a (^[x : 'type/integer/int', v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v1 (('const/combin/I' $o) $true) (^[v2 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v2 (^[c : 'type/num/num', y : 'type/integer/int']: (('const/combin/I' $o) (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) x) y) & (evalupper_tupled (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x cs)))))))))))))).
tt('thm/Omega/evalupper_curried_def_', def, (![x : 'type/integer/int', x1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/evalupper' x x1) = ('const/Omega/evalupper_tupled' (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x x1))))).
tt('thm/Omega/evalupper_ind_', ax, (![P : ('type/integer/int' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))]: (((![x : 'type/integer/int']: (P x ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & (![x : 'type/integer/int', c : 'type/num/num', y : 'type/integer/int', cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P x cs) => (P x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c y) cs))))) => (![v : 'type/integer/int', v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P v v1))))).
tt('thm/Omega/evalupper_def_0', ax, (![x : 'type/integer/int']: (('const/Omega/evalupper' x ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) = $true))).
tt('thm/Omega/evalupper_def_e1', ax, (![y : 'type/integer/int', x : 'type/integer/int', cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num']: (('const/Omega/evalupper' x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c y) cs)) = (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) x) y) & ('const/Omega/evalupper' x cs))))).
tt('thm/Omega/evallower_tupled_primitive_def_', def, ('const/Omega/evallower_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) $o) (('const/min/@' (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))) (^[R : (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) R) & (![y : 'type/integer/int', c : 'type/num/num', cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int']: (R (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x cs) (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c y) cs))))))) (^[evallower_tupled : (('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o), a : ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) a (^[x : 'type/integer/int', v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v1 (('const/combin/I' $o) $true) (^[v2 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v2 (^[c : 'type/num/num', y : 'type/integer/int']: (('const/combin/I' $o) (('const/integer/int_le' y ('const/integer/int_mul' ('const/integer/int_of_num' c) x)) & (evallower_tupled (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x cs)))))))))))))).
tt('thm/Omega/evallower_curried_def_', def, (![x : 'type/integer/int', x1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/evallower' x x1) = ('const/Omega/evallower_tupled' (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x x1))))).
tt('thm/Omega/evallower_ind_', ax, (![P : ('type/integer/int' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))]: (((![x : 'type/integer/int']: (P x ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & (![x : 'type/integer/int', c : 'type/num/num', y : 'type/integer/int', cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P x cs) => (P x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c y) cs))))) => (![v : 'type/integer/int', v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P v v1))))).
tt('thm/Omega/evallower_def_0', ax, (![x : 'type/integer/int']: (('const/Omega/evallower' x ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) = $true))).
tt('thm/Omega/evallower_def_e1', ax, (![y : 'type/integer/int', x : 'type/integer/int', cs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num']: (('const/Omega/evallower' x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c y) cs)) = (('const/integer/int_le' y ('const/integer/int_mul' ('const/integer/int_of_num' c) x)) & ('const/Omega/evallower' x cs))))).
tt('thm/Omega/smaller_satisfies_uppers_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int', y : 'type/integer/int']: ((('const/Omega/evalupper' x uppers) & ('const/integer/int_lt' y x)) => ('const/Omega/evalupper' y uppers)))).
tt('thm/Omega/bigger_satisfies_lowers_', ax, (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int', y : 'type/integer/int']: ((('const/Omega/evallower' x lowers) & ('const/integer/int_lt' x y)) => ('const/Omega/evallower' y lowers)))).
tt('thm/Omega/fst_nzero_def_', def, ![A : $t]: (![x : ('type/pair/prod' 'type/num/num' A)]: ((('const/Omega/fst_nzero' A) x) = ('const/prim_rec/<' 'const/num/0' (('const/pair/FST' 'type/num/num' A) x))))).
tt('thm/Omega/fst1_def_', def, ![A : $t]: (![x : ('type/pair/prod' 'type/num/num' A)]: ((('const/Omega/fst1' A) x) = ((('const/pair/FST' 'type/num/num' A) x) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/Omega/onlylowers_satisfiable_', ax, (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers) => (?[x : 'type/integer/int']: ('const/Omega/evallower' x lowers))))).
tt('thm/Omega/onlyuppers_satisfiable_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) => (?[x : 'type/integer/int']: ('const/Omega/evalupper' x uppers))))).
tt('thm/Omega/rshadow_row_tupled_primitive_def_', def, ('const/Omega/rshadow_row_tupled' = (('const/relation/WFREC' ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) $o) (('const/min/@' (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))) (^[R : (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) R) & (![lowery : 'type/integer/int', lowerc : 'type/num/num', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), uppery : 'type/integer/int', upperc : 'type/num/num']: (R (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) rs) (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') lowerc lowery) rs))))))) (^[rshadow_row_tupled : (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o), a : ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) a (^[v : ('type/pair/prod' 'type/num/num' 'type/integer/int'), v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v1 (('const/combin/I' $o) $true) (^[v2 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v2 (^[lowerc : 'type/num/num', lowery : 'type/integer/int']: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v (^[upperc : 'type/num/num', uppery : 'type/integer/int']: (('const/combin/I' $o) (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' upperc) lowery) ('const/integer/int_mul' ('const/integer/int_of_num' lowerc) uppery)) & (rshadow_row_tupled (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) rs)))))))))))))))).
tt('thm/Omega/rshadow_row_curried_def_', def, (![x : ('type/pair/prod' 'type/num/num' 'type/integer/int'), x1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/rshadow_row' x x1) = ('const/Omega/rshadow_row_tupled' (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x x1))))).
tt('thm/Omega/rshadow_row_ind_', ax, (![P : (('type/pair/prod' 'type/num/num' 'type/integer/int') > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))]: (((![upperc : 'type/num/num', uppery : 'type/integer/int']: (P (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & (![upperc : 'type/num/num', uppery : 'type/integer/int', lowerc : 'type/num/num', lowery : 'type/integer/int', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) rs) => (P (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') lowerc lowery) rs))))) => (![v : 'type/num/num', v1 : 'type/integer/int', v2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P (('const/pair/,' 'type/num/num' 'type/integer/int') v v1) v2))))).
tt('thm/Omega/rshadow_row_def_0', ax, (![uppery : 'type/integer/int', upperc : 'type/num/num']: (('const/Omega/rshadow_row' (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) = $true))).
tt('thm/Omega/rshadow_row_def_e1', ax, (![uppery : 'type/integer/int', upperc : 'type/num/num', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowery : 'type/integer/int', lowerc : 'type/num/num']: (('const/Omega/rshadow_row' (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') lowerc lowery) rs)) = (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' upperc) lowery) ('const/integer/int_mul' ('const/integer/int_of_num' lowerc) uppery)) & ('const/Omega/rshadow_row' (('const/pair/,' 'type/num/num' 'type/integer/int') upperc uppery) rs))))).
tt('thm/Omega/real_shadow_def_0', def, (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/real_shadow' ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers) = $true))).
tt('thm/Omega/real_shadow_def_e1', def, (![upper : ('type/pair/prod' 'type/num/num' 'type/integer/int'), ls : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/real_shadow' (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) upper ls) lowers) = (('const/Omega/rshadow_row' upper lowers) & ('const/Omega/real_shadow' ls lowers))))).
tt('thm/Omega/singleton_real_shadow_', ax, (![c : 'type/num/num', L : 'type/integer/int', x : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) x) L) & ('const/prim_rec/<' 'const/num/0' c)) => (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers) & ('const/Omega/evallower' x lowers)) => ('const/Omega/rshadow_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) lowers)))))).
tt('thm/Omega/real_shadow_revimp_uppers1_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), L : 'type/integer/int', x : 'type/integer/int']: ((('const/Omega/rshadow_row' (('const/pair/,' 'type/num/num' 'type/integer/int') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) L) lowers) & (('const/Omega/evallower' x lowers) & (('const/Omega/evalupper' x uppers) & ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers) & (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst1' 'type/integer/int') uppers))))) => (?[x0 : 'type/integer/int']: (('const/integer/int_le' x0 L) & (('const/Omega/evalupper' x0 uppers) & ('const/Omega/evallower' x0 lowers))))))).
tt('thm/Omega/real_shadow_revimp_lowers1_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num', L : 'type/integer/int', x : 'type/integer/int']: ((('const/prim_rec/<' 'const/num/0' c) & (('const/Omega/rshadow_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) lowers) & (('const/Omega/evalupper' x uppers) & (('const/Omega/evallower' x lowers) & ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) & (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst1' 'type/integer/int') lowers)))))) => (?[x0 : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) x0) L) & (('const/Omega/evalupper' x0 uppers) & ('const/Omega/evallower' x0 lowers))))))).
tt('thm/Omega/real_shadow_always_implied_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int']: ((('const/Omega/evalupper' x uppers) & (('const/Omega/evallower' x lowers) & ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) & (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers)))) => ('const/Omega/real_shadow' uppers lowers)))).
tt('thm/Omega/exact_shadow_case_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) & (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers)) => (((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst1' 'type/integer/int') uppers) | (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst1' 'type/integer/int') lowers)) => ((?[x : 'type/integer/int']: (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers))) = ('const/Omega/real_shadow' uppers lowers)))))).
tt('thm/Omega/dark_shadow_cond_row_tupled_primitive_def_', def, ('const/Omega/dark_shadow_cond_row_tupled' = (('const/relation/WFREC' ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) $o) (('const/min/@' (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))) (^['R\'' : (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) 'R\'') & (![R : 'type/integer/int', d : 'type/num/num', t : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), L : 'type/integer/int', c : 'type/num/num']: ('R\'' (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) t) (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) t))))))) (^[dark_shadow_cond_row_tupled : (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o), a : ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) a (^[v : ('type/pair/prod' 'type/num/num' 'type/integer/int'), v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v1 (('const/combin/I' $o) $true) (^[v2 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), t : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v2 (^[d : 'type/num/num', R : 'type/integer/int']: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v (^[c : 'type/num/num', L : 'type/integer/int']: (('const/combin/I' $o) ((~ (?[i : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_mul' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) i) ('const/integer/int_mul' ('const/integer/int_of_num' c) R)) & (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) R) ('const/integer/int_mul' ('const/integer/int_of_num' d) L)) & ('const/integer/int_lt' ('const/integer/int_mul' ('const/integer/int_of_num' d) L) ('const/integer/int_mul' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) ('const/integer/int_add' i ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) & (dark_shadow_cond_row_tupled (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) t)))))))))))))))).
tt('thm/Omega/dark_shadow_cond_row_curried_def_', def, (![x : ('type/pair/prod' 'type/num/num' 'type/integer/int'), x1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/dark_shadow_cond_row' x x1) = ('const/Omega/dark_shadow_cond_row_tupled' (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/integer/int') ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x x1))))).
tt('thm/Omega/dark_shadow_cond_row_ind_', ax, (![P : (('type/pair/prod' 'type/num/num' 'type/integer/int') > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))]: (((![c : 'type/num/num', L : 'type/integer/int']: (P (('const/pair/,' 'type/num/num' 'type/integer/int') c L) ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & (![c : 'type/num/num', L : 'type/integer/int', d : 'type/num/num', R : 'type/integer/int', t : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P (('const/pair/,' 'type/num/num' 'type/integer/int') c L) t) => (P (('const/pair/,' 'type/num/num' 'type/integer/int') c L) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) t))))) => (![v : 'type/num/num', v1 : 'type/integer/int', v2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P (('const/pair/,' 'type/num/num' 'type/integer/int') v v1) v2))))).
tt('thm/Omega/dark_shadow_cond_row_def_0', ax, (![c : 'type/num/num', L : 'type/integer/int']: (('const/Omega/dark_shadow_cond_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) = $true))).
tt('thm/Omega/dark_shadow_cond_row_def_e1', ax, (![t : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), d : 'type/num/num', c : 'type/num/num', R : 'type/integer/int', L : 'type/integer/int']: (('const/Omega/dark_shadow_cond_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) t)) = ((~ (?[i : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_mul' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) i) ('const/integer/int_mul' ('const/integer/int_of_num' c) R)) & (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) R) ('const/integer/int_mul' ('const/integer/int_of_num' d) L)) & ('const/integer/int_lt' ('const/integer/int_mul' ('const/integer/int_of_num' d) L) ('const/integer/int_mul' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) ('const/integer/int_add' i ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) & ('const/Omega/dark_shadow_cond_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) t))))).
tt('thm/Omega/dark_shadow_condition_tupled_primitive_def_', def, ('const/Omega/dark_shadow_condition_tupled' = (('const/relation/WFREC' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) $o) (('const/min/@' (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))) (^[R : (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) R) & (![L : 'type/integer/int', c : 'type/num/num', lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (R (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) uppers lowers) (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) uppers) lowers)))))) (^[dark_shadow_condition_tupled : (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o), a : ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) a (^[v : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v (('const/combin/I' $o) $true) (^[v2 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v2 (^[c : 'type/num/num', L : 'type/integer/int']: (('const/combin/I' $o) (('const/Omega/dark_shadow_cond_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) lowers) & (dark_shadow_condition_tupled (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) uppers lowers)))))))))))))).
tt('thm/Omega/dark_shadow_condition_curried_def_', def, (![x : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/dark_shadow_condition' x x1) = ('const/Omega/dark_shadow_condition_tupled' (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x x1))))).
tt('thm/Omega/dark_shadow_condition_ind_', ax, (![P : (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))]: (((![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers)) & (![c : 'type/num/num', L : 'type/integer/int', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P uppers lowers) => (P (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) uppers) lowers)))) => (![v : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P v v1))))).
tt('thm/Omega/dark_shadow_condition_def_0', ax, (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/dark_shadow_condition' ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers) = $true))).
tt('thm/Omega/dark_shadow_condition_def_e1', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num', L : 'type/integer/int']: (('const/Omega/dark_shadow_condition' (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) uppers) lowers) = (('const/Omega/dark_shadow_cond_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) lowers) & ('const/Omega/dark_shadow_condition' uppers lowers))))).
tt('thm/Omega/basic_shadow_equivalence_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) & (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers)) => ((?[x : 'type/integer/int']: (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers))) = (('const/Omega/real_shadow' uppers lowers) & ('const/Omega/dark_shadow_condition' uppers lowers)))))).
tt('thm/Omega/dark_shadow_row_tupled_primitive_def_', def, ('const/Omega/dark_shadow_row_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) $o) (('const/min/@' (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o))) (^['R\'' : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))) 'R\'') & (![R : 'type/integer/int', d : 'type/num/num', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), L : 'type/integer/int', c : 'type/num/num']: ('R\'' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) c (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) L rs)) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) c (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) L (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs)))))))) (^[dark_shadow_row_tupled : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o), a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))]: (('const/pair/pair_CASE' $o 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) a (^[c : 'type/num/num', v1 : ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) v1 (^[L : 'type/integer/int', v3 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v3 (('const/combin/I' $o) $true) (^[v4 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v4 (^[d : 'type/num/num', R : 'type/integer/int']: (('const/combin/I' $o) (('const/integer/int_ge' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' d) L) ('const/integer/int_mul' ('const/integer/int_of_num' c) R)) ('const/integer/int_mul' ('const/integer/int_sub' ('const/integer/int_of_num' c) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/integer/int_sub' ('const/integer/int_of_num' d) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & (dark_shadow_row_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) c (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) L rs))))))))))))))))).
tt('thm/Omega/dark_shadow_row_curried_def_', def, (![x : 'type/num/num', x1 : 'type/integer/int', x2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/dark_shadow_row' x x1 x2) = ('const/Omega/dark_shadow_row_tupled' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) x (('const/pair/,' 'type/integer/int' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x1 x2)))))).
tt('thm/Omega/dark_shadow_row_ind_', ax, (![P : ('type/num/num' > ('type/integer/int' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o)))]: (((![c : 'type/num/num', L : 'type/integer/int']: (P c L ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & (![c : 'type/num/num', L : 'type/integer/int', d : 'type/num/num', R : 'type/integer/int', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P c L rs) => (P c L (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs))))) => (![v : 'type/num/num', v1 : 'type/integer/int', v2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P v v1 v2))))).
tt('thm/Omega/dark_shadow_row_def_0', ax, (![c : 'type/num/num', L : 'type/integer/int']: (('const/Omega/dark_shadow_row' c L ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) = $true))).
tt('thm/Omega/dark_shadow_row_def_e1', ax, (![rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), d : 'type/num/num', c : 'type/num/num', R : 'type/integer/int', L : 'type/integer/int']: (('const/Omega/dark_shadow_row' c L (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs)) = (('const/integer/int_ge' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' d) L) ('const/integer/int_mul' ('const/integer/int_of_num' c) R)) ('const/integer/int_mul' ('const/integer/int_sub' ('const/integer/int_of_num' c) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/integer/int_sub' ('const/integer/int_of_num' d) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ('const/Omega/dark_shadow_row' c L rs))))).
tt('thm/Omega/dark_shadow_tupled_primitive_def_', def, ('const/Omega/dark_shadow_tupled' = (('const/relation/WFREC' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) $o) (('const/min/@' (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))) (^[R : (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) R) & (![L : 'type/integer/int', c : 'type/num/num', lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (R (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) uppers lowers) (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) uppers) lowers)))))) (^[dark_shadow_tupled : (('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) > $o), a : ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) a (^[v : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v (('const/combin/I' $o) $true) (^[v2 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v2 (^[c : 'type/num/num', L : 'type/integer/int']: (('const/combin/I' $o) (('const/Omega/dark_shadow_row' c L lowers) & (dark_shadow_tupled (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) uppers lowers)))))))))))))).
tt('thm/Omega/dark_shadow_curried_def_', def, (![x : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/dark_shadow' x x1) = ('const/Omega/dark_shadow_tupled' (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x x1))))).
tt('thm/Omega/dark_shadow_ind_', ax, (![P : (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o))]: (((![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers)) & (![c : 'type/num/num', L : 'type/integer/int', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P uppers lowers) => (P (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) uppers) lowers)))) => (![v : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), v1 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P v v1))))).
tt('thm/Omega/dark_shadow_def_0', ax, (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/dark_shadow' ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers) = $true))).
tt('thm/Omega/dark_shadow_def_e1', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num', L : 'type/integer/int']: (('const/Omega/dark_shadow' (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) uppers) lowers) = (('const/Omega/dark_shadow_row' c L lowers) & ('const/Omega/dark_shadow' uppers lowers))))).
tt('thm/Omega/nightmare_tupled_primitive_def_', def, ('const/Omega/nightmare_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) $o) (('const/min/@' (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) > (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) > $o))) (^['R\'' : (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) > (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))))) 'R\'') & (![R : 'type/integer/int', d : 'type/num/num', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num', x : 'type/integer/int']: ('R\'' (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) x (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))) c (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) uppers (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) lowers rs)))) (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) x (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))) c (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) uppers (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) lowers (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs)))))))))) (^[nightmare_tupled : (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) > $o), a : ('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))))]: (('const/pair/pair_CASE' $o 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) a (^[x : 'type/integer/int', v1 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))]: (('const/pair/pair_CASE' $o 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))) v1 (^[c : 'type/num/num', v3 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))]: (('const/pair/pair_CASE' $o ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) v3 (^[uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), v5 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) v5 (^[lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), v7 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v7 (('const/combin/I' $o) $false) (^[v8 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v8 (^[d : 'type/num/num', R : 'type/integer/int']: (('const/combin/I' $o) ((?[i : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) & ('const/integer/int_le' i ('const/integer/int_div' ('const/integer/int_sub' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)))) & ((('const/integer/int_mul' ('const/integer/int_of_num' d) x) = ('const/integer/int_add' R i)) & (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers))))) | (nightmare_tupled (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) x (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))) c (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) uppers (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) lowers rs))))))))))))))))))))))).
tt('thm/Omega/nightmare_curried_def_', def, (![x : 'type/integer/int', x1 : 'type/num/num', x2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x3 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x4 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/nightmare' x x1 x2 x3 x4) = ('const/Omega/nightmare_tupled' (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))))) x (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))) x1 (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/pair/prod' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) x2 (('const/pair/,' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x3 x4)))))))).
tt('thm/Omega/nightmare_ind_', ax, (![P : ('type/integer/int' > ('type/num/num' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o)))))]: (((![x : 'type/integer/int', c : 'type/num/num', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P x c uppers lowers ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & (![x : 'type/integer/int', c : 'type/num/num', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), d : 'type/num/num', R : 'type/integer/int', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P x c uppers lowers rs) => (P x c uppers lowers (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs))))) => (![v : 'type/integer/int', v1 : 'type/num/num', v2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), v3 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), v4 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P v v1 v2 v3 v4))))).
tt('thm/Omega/nightmare_def_0', ax, (![x : 'type/integer/int', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num']: (('const/Omega/nightmare' x c uppers lowers ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) = $false))).
tt('thm/Omega/nightmare_def_e1', ax, (![x : 'type/integer/int', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), d : 'type/num/num', c : 'type/num/num', R : 'type/integer/int']: (('const/Omega/nightmare' x c uppers lowers (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs)) = ((?[i : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) & ('const/integer/int_le' i ('const/integer/int_div' ('const/integer/int_sub' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)))) & ((('const/integer/int_mul' ('const/integer/int_of_num' d) x) = ('const/integer/int_add' R i)) & (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers))))) | ('const/Omega/nightmare' x c uppers lowers rs))))).
tt('thm/Omega/nightmare_implies_LHS_', ax, (![rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num']: (('const/Omega/nightmare' x c uppers lowers rs) => (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers))))).
tt('thm/Omega/dark_shadow_FORALL_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/dark_shadow' uppers lowers) = (![c : 'type/num/num', d : 'type/num/num', L : 'type/integer/int', R : 'type/integer/int']: (((('const/bool/IN' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' 'type/integer/int')) uppers)) & (('const/bool/IN' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers))) => ('const/integer/int_ge' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' d) L) ('const/integer/int_mul' ('const/integer/int_of_num' c) R)) ('const/integer/int_mul' ('const/integer/int_sub' ('const/integer/int_of_num' c) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/integer/int_sub' ('const/integer/int_of_num' d) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/Omega/real_shadow_FORALL_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/real_shadow' uppers lowers) = (![c : 'type/num/num', d : 'type/num/num', L : 'type/integer/int', R : 'type/integer/int']: (((('const/bool/IN' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' 'type/integer/int')) uppers)) & (('const/bool/IN' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers))) => ('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) R) ('const/integer/int_mul' ('const/integer/int_of_num' d) L))))))).
tt('thm/Omega/evalupper_FORALL_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int']: (('const/Omega/evalupper' x uppers) = (![c : 'type/num/num', L : 'type/integer/int']: ((('const/bool/IN' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c L) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' 'type/integer/int')) uppers)) => ('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) x) L)))))).
tt('thm/Omega/evallower_FORALL_', ax, (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int']: (('const/Omega/evallower' x lowers) = (![d : 'type/num/num', R : 'type/integer/int']: ((('const/bool/IN' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' 'type/integer/int')) lowers)) => ('const/integer/int_le' R ('const/integer/int_mul' ('const/integer/int_of_num' d) x))))))).
tt('thm/Omega/nightmare_EXISTS_', ax, (![rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), x : 'type/integer/int', c : 'type/num/num', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/nightmare' x c uppers lowers rs) = (?[i : 'type/integer/int', d : 'type/num/num', R : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) & (('const/integer/int_le' i ('const/integer/int_div' ('const/integer/int_sub' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' d) ('const/integer/int_of_num' c)) ('const/integer/int_of_num' c)) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c))) & ((('const/bool/IN' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' 'type/integer/int')) rs)) & (('const/Omega/evalupper' x uppers) & (('const/Omega/evallower' x lowers) & (('const/integer/int_mul' ('const/integer/int_of_num' d) x) = ('const/integer/int_add' R i))))))))))).
tt('thm/Omega/final_equivalence_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), m : 'type/num/num']: (((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) & ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers) & (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (^[p : ('type/pair/prod' 'type/num/num' 'type/integer/int')]: ('const/arithmetic/<=' (('const/pair/FST' 'type/num/num' 'type/integer/int') p) m)) uppers))) => ((?[x : 'type/integer/int']: (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers))) = (('const/Omega/real_shadow' uppers lowers) & (('const/Omega/dark_shadow' uppers lowers) | (?[x : 'type/integer/int']: ('const/Omega/nightmare' x m uppers lowers lowers)))))))).
tt('thm/Omega/darkrow_implies_realrow_', ax, (![lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num', L : 'type/integer/int']: ((('const/prim_rec/<' 'const/num/0' c) & ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers) & ('const/Omega/dark_shadow_row' c L lowers))) => ('const/Omega/rshadow_row' (('const/pair/,' 'type/num/num' 'type/integer/int') c L) lowers)))).
tt('thm/Omega/dark_implies_real_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) & ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers) & ('const/Omega/dark_shadow' uppers lowers))) => ('const/Omega/real_shadow' uppers lowers)))).
tt('thm/Omega/alternative_equivalence_', ax, (![uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), m : 'type/num/num']: (((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') uppers) & ((('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) ('const/Omega/fst_nzero' 'type/integer/int') lowers) & (('const/list/EVERY' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (^[p : ('type/pair/prod' 'type/num/num' 'type/integer/int')]: ('const/arithmetic/<=' (('const/pair/FST' 'type/num/num' 'type/integer/int') p) m)) uppers))) => ((?[x : 'type/integer/int']: (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers))) = (('const/Omega/dark_shadow' uppers lowers) | (?[x : 'type/integer/int']: ('const/Omega/nightmare' x m uppers lowers lowers))))))).
tt('thm/Omega/eval_base_', ax, (![x : 'type/integer/int', p : $o]: (p = (((('const/Omega/evalupper' x ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) & ('const/Omega/evallower' x ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & $true) & p)))).
tt('thm/Omega/eval_step_upper1_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), r : 'type/integer/int', lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), ex : $o, c : 'type/num/num']: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & ex) & ('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) x) r)) = ((('const/Omega/evalupper' x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c r) ups)) & ('const/Omega/evallower' x lows)) & ex)))).
tt('thm/Omega/eval_step_upper2_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), r : 'type/integer/int', p : $o, lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), ex : $o, c : 'type/num/num']: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & ex) & (('const/integer/int_le' ('const/integer/int_mul' ('const/integer/int_of_num' c) x) r) & p)) = (((('const/Omega/evalupper' x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c r) ups)) & ('const/Omega/evallower' x lows)) & ex) & p)))).
tt('thm/Omega/eval_step_lower1_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), r : 'type/integer/int', lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), ex : $o, c : 'type/num/num']: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & ex) & ('const/integer/int_le' r ('const/integer/int_mul' ('const/integer/int_of_num' c) x))) = ((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c r) lows))) & ex)))).
tt('thm/Omega/eval_step_lower2_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), r : 'type/integer/int', p : $o, lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), ex : $o, c : 'type/num/num']: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & ex) & (('const/integer/int_le' r ('const/integer/int_mul' ('const/integer/int_of_num' c) x)) & p)) = (((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') c r) lows))) & ex) & p)))).
tt('thm/Omega/eval_step_extra1_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), 'ex\'' : $o]: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & $true) & 'ex\'') = ((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & 'ex\'')))).
tt('thm/Omega/eval_step_extra2_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), 'ex\'' : $o, ex : $o]: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & ex) & 'ex\'') = ((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & (ex & 'ex\''))))).
tt('thm/Omega/eval_step_extra3_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), p : $o, lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), 'ex\'' : $o]: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & $true) & ('ex\'' & p)) = (((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & 'ex\'') & p)))).
tt('thm/Omega/eval_step_extra4_', ax, (![x : 'type/integer/int', ups : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), p : $o, lows : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), 'ex\'' : $o, ex : $o]: ((((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & ex) & ('ex\'' & p)) = (((('const/Omega/evalupper' x ups) & ('const/Omega/evallower' x lows)) & (ex & 'ex\'')) & p)))).
tt('thm/Omega/calc_nightmare_tupled_primitive_def_', def, ('const/Omega/calc_nightmare_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) $o) (('const/min/@' (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o))) (^['R\'' : (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))) 'R\'') & (![R : 'type/integer/int', d : 'type/num/num', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num', x : 'type/integer/int']: ('R\'' (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) x (('const/pair/,' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) c rs)) (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) x (('const/pair/,' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) c (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs)))))))) (^[calc_nightmare_tupled : (('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) > $o), a : ('type/pair/prod' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))))]: (('const/pair/pair_CASE' $o 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) a (^[x : 'type/integer/int', v1 : ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))]: (('const/pair/pair_CASE' $o 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) v1 (^[c : 'type/num/num', v3 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' 'type/integer/int') $o) v3 (('const/combin/I' $o) $false) (^[v4 : ('type/pair/prod' 'type/num/num' 'type/integer/int'), rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/pair/pair_CASE' $o 'type/num/num' 'type/integer/int') v4 (^[d : 'type/num/num', R : 'type/integer/int']: (('const/combin/I' $o) ((?[i : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) & ('const/integer/int_le' i ('const/integer/int_div' ('const/integer/int_sub' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)))) & (('const/integer/int_mul' ('const/integer/int_of_num' d) x) = ('const/integer/int_add' R i)))) | (calc_nightmare_tupled (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) x (('const/pair/,' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) c rs))))))))))))))))).
tt('thm/Omega/calc_nightmare_curried_def_', def, (![x : 'type/integer/int', x1 : 'type/num/num', x2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/calc_nightmare' x x1 x2) = ('const/Omega/calc_nightmare_tupled' (('const/pair/,' 'type/integer/int' ('type/pair/prod' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) x (('const/pair/,' 'type/num/num' ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) x1 x2)))))).
tt('thm/Omega/calc_nightmare_ind_', ax, (![P : ('type/integer/int' > ('type/num/num' > (('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')) > $o)))]: (((![x : 'type/integer/int', c : 'type/num/num']: (P x c ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int')))) & (![x : 'type/integer/int', c : 'type/num/num', d : 'type/num/num', R : 'type/integer/int', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: ((P x c rs) => (P x c (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs))))) => (![v : 'type/integer/int', v1 : 'type/num/num', v2 : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (P v v1 v2))))).
tt('thm/Omega/calc_nightmare_def_0', ax, (![x : 'type/integer/int', c : 'type/num/num']: (('const/Omega/calc_nightmare' x c ('const/list/NIL' ('type/pair/prod' 'type/num/num' 'type/integer/int'))) = $false))).
tt('thm/Omega/calc_nightmare_def_e1', ax, (![x : 'type/integer/int', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), d : 'type/num/num', c : 'type/num/num', R : 'type/integer/int']: (('const/Omega/calc_nightmare' x c (('const/list/CONS' ('type/pair/prod' 'type/num/num' 'type/integer/int')) (('const/pair/,' 'type/num/num' 'type/integer/int') d R) rs)) = ((?[i : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) & ('const/integer/int_le' i ('const/integer/int_div' ('const/integer/int_sub' ('const/integer/int_sub' ('const/integer/int_mul' ('const/integer/int_of_num' c) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)) ('const/integer/int_of_num' d)) ('const/integer/int_of_num' c)))) & (('const/integer/int_mul' ('const/integer/int_of_num' d) x) = ('const/integer/int_add' R i)))) | ('const/Omega/calc_nightmare' x c rs))))).
tt('thm/Omega/calculational_nightmare_', ax, (![x : 'type/integer/int', uppers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), lowers : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int')), c : 'type/num/num', rs : ('type/list/list' ('type/pair/prod' 'type/num/num' 'type/integer/int'))]: (('const/Omega/nightmare' x c uppers lowers rs) = (('const/Omega/calc_nightmare' x c rs) & (('const/Omega/evalupper' x uppers) & ('const/Omega/evallower' x lowers)))))).
