%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM746^4 : TPTP v9.2.0. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.7f1EAoVaj8 true
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:48:12 PM UTC 2025
% Result : Theorem 83.83s 12.44s
% Output : Refutation 83.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM746^4 : TPTP v9.2.0. Released v7.1.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.7f1EAoVaj8 true
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 16:29:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in HO mode
% 0.55/0.64 % Total configuration time : 828
% 0.55/0.64 % Estimated wc time : 1656
% 0.55/0.64 % Estimated cpu time (8 cpus) : 207.0
% 0.55/0.73 % /export/starexec/sandbox2/solver/bin/lams/40_c.s.sh running for 80s
% 0.55/0.73 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.55/0.73 % /export/starexec/sandbox2/solver/bin/lams/40_c_ic.sh running for 80s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/lams/15_e_short1.sh running for 30s
% 0.55/0.75 % /export/starexec/sandbox2/solver/bin/lams/40_b.comb.sh running for 70s
% 0.55/0.75 % /export/starexec/sandbox2/solver/bin/lams/40_noforms.sh running for 90s
% 0.55/0.75 % /export/starexec/sandbox2/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.55/0.75 % /export/starexec/sandbox2/solver/bin/lams/30_sp5.sh running for 60s
% 83.83/12.44 % Solved by lams/40_b.comb.sh.
% 83.83/12.44 % done 616 iterations in 11.558s
% 83.83/12.44 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 83.83/12.44 % SZS output start Refutation
% 83.83/12.44 thf(moreq_type, type, moreq: $i > $i > $o).
% 83.83/12.44 thf(lessf_type, type, lessf: $i > $i > $o).
% 83.83/12.44 thf('#sk2_type', type, '#sk2': $i).
% 83.83/12.44 thf(nat_type, type, nat: $i).
% 83.83/12.44 thf(is_of_type, type, is_of: $i > ($i > $o) > $o).
% 83.83/12.44 thf(in_type, type, in: $i > $i > $o).
% 83.83/12.44 thf(lesseq_type, type, lesseq: $i > $i > $o).
% 83.83/12.44 thf(imp_type, type, imp: $o > $o > $o).
% 83.83/12.44 thf('#sk3_type', type, '#sk3': $i).
% 83.83/12.44 thf(frac_type, type, frac: $i).
% 83.83/12.44 thf(n_eq_type, type, n_eq: $i > $i > $o).
% 83.83/12.44 thf(pair1type_type, type, pair1type: $i > $i).
% 83.83/12.44 thf(all_of_type, type, all_of: ($i > $o) > ($i > $o) > $o).
% 83.83/12.44 thf(l_or_type, type, l_or: $o > $o > $o).
% 83.83/12.44 thf('#ty_enc5_type', type, '#ty_enc5': ($i > $i > $o) > $i > $i > $o).
% 83.83/12.44 thf(moref_type, type, moref: $i > $i > $o).
% 83.83/12.44 thf(d_not_type, type, d_not: $o > $o).
% 83.83/12.44 thf('#sk4_type', type, '#sk4': $i).
% 83.83/12.44 thf(s_comb_type, type, '#S': !>[A:$tType, B:$tType, C:$tType]: ((A > B > C) > (A > B) > A > C)).
% 83.83/12.44 thf(c_comb_type, type, '#C': !>[A:$tType, B:$tType, C:$tType]: ((A > B > C) > B > A > C)).
% 83.83/12.44 thf(b_comb_type, type, '#B': !>[A:$tType, B:$tType, C:$tType]: ((A > B) > (C > A) > C > B)).
% 83.83/12.44 thf(k_comb_type, type, '#K': !>[A:$tType, B:$tType]: (B > A > B)).
% 83.83/12.44 thf(i_comb_type, type, '#I': !>[A:$tType]: (A > A)).
% 83.83/12.44 thf(satz52, conjecture,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X2:$i]: ( in @ X2 @ frac ) ) @
% 83.83/12.44 ( ^[X2:$i]:
% 83.83/12.44 ( ( lesseq @ X0 @ X1 ) =>
% 83.83/12.44 ( ( lesseq @ X1 @ X2 ) => ( lesseq @ X0 @ X2 ) ) ) ) ) ) ) ))).
% 83.83/12.44 thf(zf_stmt_0, negated_conjecture,
% 83.83/12.44 (~( all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X2:$i]: ( in @ X2 @ frac ) ) @
% 83.83/12.44 ( ^[X2:$i]:
% 83.83/12.44 ( ( lesseq @ X0 @ X1 ) =>
% 83.83/12.44 ( ( lesseq @ X1 @ X2 ) => ( lesseq @ X0 @ X2 ) ) ) ) ) ) ) ) )),
% 83.83/12.44 inference('cnf.neg', [status(esa)], [satz52])).
% 83.83/12.44 thf(zip_derived_cl292, plain,
% 83.83/12.44 (~ (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]:
% 83.83/12.44 (all_of @ (^[Y2 : $i]: (in @ Y2 @ frac)) @
% 83.83/12.44 (^[Y2 : $i]:
% 83.83/12.44 (((lesseq @ Y0 @ Y1) =>
% 83.83/12.44 (((lesseq @ Y1 @ Y2) => (lesseq @ Y0 @ Y2)))))))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [zf_stmt_0])).
% 83.83/12.44 thf(zip_derived_cl293, plain,
% 83.83/12.44 (~ (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ frac))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))))) @
% 83.83/12.44 lesseq)))))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl292])).
% 83.83/12.44 thf(def_frac, axiom,(( frac ) = ((pair1type @ nat)))).
% 83.83/12.44 thf('0', plain, (( frac ) = ( pair1type @ nat )), define([status(thm)])).
% 83.83/12.44 thf(zip_derived_cl448, plain,
% 83.83/12.44 (~ (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))))) @
% 83.83/12.44 lesseq)))))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl293, '0'])).
% 83.83/12.44 thf(def_all_of, axiom, ~ (all_of @ X0 @ X1) =>
% 83.83/12.44 ((((!!) @ (^[Y0 : $i]: (((is_of @ Y0 @ X0) => (X1 @ Y0)))))) != ($true))).
% 83.83/12.44 thf('1', plain,
% 83.83/12.44 (![X0:( $i > $o ),X1:( $i > $o )]:
% 83.83/12.44 ( ( ~( all_of @ X0 @ X1 ) ) <=>
% 83.83/12.44 ( ~( ![X6:$i]: ( ( is_of @ X6 @ X0 ) => ( X1 @ X6 ) ) ) ) )),
% 83.83/12.44 inference('rw.lit', [status(esa)], [def_all_of])).
% 83.83/12.44 thf(zip_derived_cl449, plain,
% 83.83/12.44 (~ (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @
% 83.83/12.44 (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 lesseq)))))) @
% 83.83/12.44 lesseq)))))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl448, '1'])).
% 83.83/12.44 thf(zip_derived_cl450, plain,
% 83.83/12.44 (~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 lesseq)))))) @
% 83.83/12.44 lesseq))))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl449])).
% 83.83/12.44 thf(zip_derived_cl451, plain,
% 83.83/12.44 (~ (((is_of @ '#sk2' @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (lesseq @ '#sk2'))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 (lesseq @ '#sk2'))))))))))),
% 83.83/12.44 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl450])).
% 83.83/12.44 thf(zip_derived_cl453, plain,
% 83.83/12.44 (~ (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (lesseq @ '#sk2'))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 (lesseq @ '#sk2'))))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl451])).
% 83.83/12.44 thf(zip_derived_cl454, plain,
% 83.83/12.44 (~ (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (lesseq @ '#sk2'))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 (lesseq @ '#sk2'))))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl453, '1'])).
% 83.83/12.44 thf(zip_derived_cl455, plain,
% 83.83/12.44 (~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (lesseq @ '#sk2'))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 (lesseq @ '#sk2')))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl454])).
% 83.83/12.44 thf(zip_derived_cl456, plain,
% 83.83/12.44 (~ (((is_of @ '#sk3' @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (lesseq @ '#sk2' @ '#sk3'))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ '#sk3'))) @
% 83.83/12.44 (lesseq @ '#sk2'))))))))),
% 83.83/12.44 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl455])).
% 83.83/12.44 thf(def_d_not, axiom,(( d_not @ (X0)) = ((imp @ X0 @ ($false))))).
% 83.83/12.44 thf('2', plain, (![X0:$o]: ( ( d_not @ X0 ) = ( imp @ X0 @ $false ) )),
% 83.83/12.44 define([status(thm)])).
% 83.83/12.44 thf(def_l_or, axiom,(( l_or @ (X0)@ (X1)) = ((imp @ (d_not @ X0) @ X1)))).
% 83.83/12.44 thf('3', plain,
% 83.83/12.44 (![X1:$o,X0:$o]: ( ( l_or @ X0 @ X1 ) = ( imp @ ( d_not @ X0 ) @ X1 ) )),
% 83.83/12.44 define([status(thm)])).
% 83.83/12.44 thf(def_lesseq, axiom,(( lesseq @ (X0)@ (X1)) =
% 83.83/12.44 ((l_or @ (lessf @ X0 @ X1) @ (n_eq @ X0 @ X1))))).
% 83.83/12.44 thf('4', plain,
% 83.83/12.44 (![X1:$i,X0:$i]:
% 83.83/12.44 ( ( lesseq @ X0 @ X1 ) =
% 83.83/12.44 ( l_or @ ( lessf @ X0 @ X1 ) @ ( n_eq @ X0 @ X1 ) ) )),
% 83.83/12.44 define([status(thm)])).
% 83.83/12.44 thf(zip_derived_cl457, plain,
% 83.83/12.44 (~ (((is_of @ '#sk3' @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @
% 83.83/12.44 (imp @ (lessf @ '#sk2' @ '#sk3') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3')))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ '#sk3'))) @
% 83.83/12.44 (lesseq @ '#sk2'))))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl456, '2', '3', '4'])).
% 83.83/12.44 thf(zip_derived_cl459, plain,
% 83.83/12.44 (~ (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @
% 83.83/12.44 (imp @ (lessf @ '#sk2' @ '#sk3') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3')))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ '#sk3'))) @
% 83.83/12.44 (lesseq @ '#sk2'))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl457])).
% 83.83/12.44 thf(zip_derived_cl460, plain,
% 83.83/12.44 (~ (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @
% 83.83/12.44 (imp @ (lessf @ '#sk2' @ '#sk3') @
% 83.83/12.44 ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3')))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ '#sk3'))) @
% 83.83/12.44 (lesseq @ '#sk2'))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl459, '1'])).
% 83.83/12.44 thf(zip_derived_cl461, plain,
% 83.83/12.44 (~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @
% 83.83/12.44 (imp @ (lessf @ '#sk2' @ '#sk3') @
% 83.83/12.44 ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3')))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ '#sk3'))) @
% 83.83/12.44 (lesseq @ '#sk2')))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl460])).
% 83.83/12.44 thf(zip_derived_cl462, plain,
% 83.83/12.44 (~ (((is_of @ '#sk4' @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((imp @ (imp @ (lessf @ '#sk2' @ '#sk3') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3')) =>
% 83.83/12.44 (((lesseq @ '#sk3' @ '#sk4') => (lesseq @ '#sk2' @ '#sk4')))))))),
% 83.83/12.44 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl461])).
% 83.83/12.44 thf(zip_derived_cl463, plain,
% 83.83/12.44 (~ (((is_of @ '#sk4' @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((imp @ (imp @ (lessf @ '#sk2' @ '#sk3') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3')) =>
% 83.83/12.44 (((imp @ (imp @ (lessf @ '#sk3' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk3' @ '#sk4')) => (imp @
% 83.83/12.44 (imp @ (lessf @ '#sk2' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk4'))))))))),
% 83.83/12.44 inference('rw', [status(thm)],
% 83.83/12.44 [zip_derived_cl462, '2', '2', '3', '3', '4', '4'])).
% 83.83/12.44 thf(zip_derived_cl465, plain,
% 83.83/12.44 (~ (((imp @ (imp @ (lessf @ '#sk2' @ '#sk3') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3')) =>
% 83.83/12.44 (((imp @ (imp @ (lessf @ '#sk3' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk3' @ '#sk4')) => (imp @
% 83.83/12.44 (imp @ (lessf @ '#sk2' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk4'))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl463])).
% 83.83/12.44 thf(zip_derived_cl467, plain,
% 83.83/12.44 (~ (((imp @ (imp @ (lessf @ '#sk3' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk3' @ '#sk4')) => (imp @
% 83.83/12.44 (imp @ (lessf @ '#sk2' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk4'))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl465])).
% 83.83/12.44 thf(zip_derived_cl469, plain,
% 83.83/12.44 ( (imp @ (imp @ (lessf @ '#sk3' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk3' @ '#sk4'))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl467])).
% 83.83/12.44 thf(def_imp, axiom, (imp @ X0 @ X1) => ((((X0) => (X1))) = ($true))).
% 83.83/12.44 thf('5', plain,
% 83.83/12.44 (![X0:$o,X1:$o]: ( ( imp @ X0 @ X1 ) <=> ( ( X0 ) => ( X1 ) ) )),
% 83.83/12.44 inference('rw.lit', [status(esa)], [def_imp])).
% 83.83/12.44 thf(zip_derived_cl472, plain,
% 83.83/12.44 ( (((imp @ (lessf @ '#sk3' @ '#sk4') @ ($false)) => (n_eq @ '#sk3' @
% 83.83/12.44 '#sk4')))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl469, '5'])).
% 83.83/12.44 thf(zip_derived_cl475, plain,
% 83.83/12.44 ((~ (imp @ (lessf @ '#sk3' @ '#sk4') @ ($false))
% 83.83/12.44 | (n_eq @ '#sk3' @ '#sk4'))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl472])).
% 83.83/12.44 thf(def_imp, axiom, ~ (imp @ X0 @ X1) => ((((X0) => (X1))) != ($true))).
% 83.83/12.44 thf('6', plain,
% 83.83/12.44 (![X0:$o,X1:$o]: ( ( ~( imp @ X0 @ X1 ) ) <=> ( ~( ( X0 ) => ( X1 ) ) ) )),
% 83.83/12.44 inference('rw.lit', [status(esa)], [def_imp])).
% 83.83/12.44 thf(zip_derived_cl480, plain,
% 83.83/12.44 ((~ (((lessf @ '#sk3' @ '#sk4') => ($false))) | (n_eq @ '#sk3' @ '#sk4'))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl475, '6'])).
% 83.83/12.44 thf(zip_derived_cl482, plain,
% 83.83/12.44 ((~ (((~) @ (lessf @ '#sk3' @ '#sk4'))) | (n_eq @ '#sk3' @ '#sk4'))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl480])).
% 83.83/12.44 thf(zip_derived_cl483, plain,
% 83.83/12.44 (( (lessf @ '#sk3' @ '#sk4') | (n_eq @ '#sk3' @ '#sk4'))),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl482])).
% 83.83/12.44 thf(satz51c, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X2:$i]: ( in @ X2 @ frac ) ) @
% 83.83/12.44 ( ^[X2:$i]:
% 83.83/12.44 ( ( moreq @ X0 @ X1 ) =>
% 83.83/12.44 ( ( moref @ X1 @ X2 ) => ( moref @ X0 @ X2 ) ) ) ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl288, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]:
% 83.83/12.44 (all_of @ (^[Y2 : $i]: (in @ Y2 @ frac)) @
% 83.83/12.44 (^[Y2 : $i]:
% 83.83/12.44 (((moreq @ Y0 @ Y1) =>
% 83.83/12.44 (((moref @ Y1 @ Y2) => (moref @ Y0 @ Y2)))))))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz51c])).
% 83.83/12.44 thf(zip_derived_cl289, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ frac))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))))) @
% 83.83/12.44 moref)))))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl288])).
% 83.83/12.44 thf(zip_derived_cl1466, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))))) @
% 83.83/12.44 moref)))))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl289, '0'])).
% 83.83/12.44 thf(def_all_of, axiom, (all_of @ X0 @ X1) =>
% 83.83/12.44 ((((!!) @ (^[Y0 : $i]: (((is_of @ Y0 @ X0) => (X1 @ Y0)))))) = ($true))).
% 83.83/12.44 thf('7', plain,
% 83.83/12.44 (![X0:( $i > $o ),X1:( $i > $o )]:
% 83.83/12.44 ( ( all_of @ X0 @ X1 ) <=>
% 83.83/12.44 ( ![X6:$i]: ( ( is_of @ X6 @ X0 ) => ( X1 @ X6 ) ) ) )),
% 83.83/12.44 inference('rw.lit', [status(esa)], [def_all_of])).
% 83.83/12.44 thf(zip_derived_cl1467, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @
% 83.83/12.44 (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 moref)))))) @
% 83.83/12.44 moref)))))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1466, '7'])).
% 83.83/12.44 thf(zip_derived_cl1468, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 moref)))))) @
% 83.83/12.44 moref))))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1467])).
% 83.83/12.44 thf(zip_derived_cl1469, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @ ((('#B') @ (=>) @ (moreq @ X2))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 (moref @ X2))))))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1468])).
% 83.83/12.44 thf(zip_derived_cl1470, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @ ((('#B') @ (=>) @ (moreq @ X2))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 (moref @ X2)))))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1469])).
% 83.83/12.44 thf(zip_derived_cl1471, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (moreq @ X0))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 (moref @ X0))))) @
% 83.83/12.44 Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1470, '7'])).
% 83.83/12.44 thf(zip_derived_cl1472, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (moreq @ X0))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 (moref @ X0)))))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1471])).
% 83.83/12.44 thf(zip_derived_cl1473, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (moreq @ X0 @ X2))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X2))) @ (moref @ X0))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1472])).
% 83.83/12.44 thf(def_moreq, axiom,(( moreq @ (X0)@ (X1)) =
% 83.83/12.44 ((l_or @ (moref @ X0 @ X1) @ (n_eq @ X0 @ X1))))).
% 83.83/12.44 thf('8', plain,
% 83.83/12.44 (![X1:$i,X0:$i]:
% 83.83/12.44 ( ( moreq @ X0 @ X1 ) =
% 83.83/12.44 ( l_or @ ( moref @ X0 @ X1 ) @ ( n_eq @ X0 @ X1 ) ) )),
% 83.83/12.44 define([status(thm)])).
% 83.83/12.44 thf(zip_derived_cl1474, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @ (imp @ (moref @ X0 @ X2) @ ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X2)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X2))) @ (moref @ X0))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl1473, '2', '3', '8'])).
% 83.83/12.44 thf(zip_derived_cl1475, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @
% 83.83/12.44 (imp @ (moref @ X0 @ X2) @ ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X2)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X2))) @ (moref @ X0))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1474])).
% 83.83/12.44 thf(zip_derived_cl1476, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @
% 83.83/12.44 (imp @ (moref @ X0 @ X1) @
% 83.83/12.44 ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X1)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X1))) @
% 83.83/12.44 (moref @ X0))) @
% 83.83/12.44 Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1475, '7'])).
% 83.83/12.44 thf(zip_derived_cl1477, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (imp @
% 83.83/12.44 (imp @ (moref @ X0 @ X1) @ ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X1)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X1))) @
% 83.83/12.44 (moref @ X0)))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1476])).
% 83.83/12.44 thf(zip_derived_cl1478, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 ( (((is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((imp @ (imp @ (moref @ X0 @ X1) @ ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X1)) => (((moref @ X1 @ X3) => (moref @ X0 @ X3)))))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1477])).
% 83.83/12.44 thf(zip_derived_cl1479, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((imp @ (imp @ (moref @ X0 @ X1) @ ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X1)) => (((moref @ X1 @ X3) => (moref @ X0 @ X3)))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1478])).
% 83.83/12.44 thf(zip_derived_cl1480, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (imp @ (imp @ (moref @ X0 @ X1) @ ($false)) @ (n_eq @ X0 @ X1))
% 83.83/12.44 | (((moref @ X1 @ X3) => (moref @ X0 @ X3)))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1479])).
% 83.83/12.44 thf(zip_derived_cl1481, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (((imp @ (moref @ X1 @ X2) @ ($false)) => (n_eq @ X1 @ X2)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((moref @ X2 @ X0) => (moref @ X1 @ X0))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1480, '6'])).
% 83.83/12.44 thf(zip_derived_cl1482, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 ( (imp @ (moref @ X1 @ X2) @ ($false))
% 83.83/12.44 | (((moref @ X2 @ X0) => (moref @ X1 @ X0)))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1481])).
% 83.83/12.44 thf(zip_derived_cl1484, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 ( (((moref @ X1 @ X2) => ($false)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((moref @ X2 @ X0) => (moref @ X1 @ X0))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1482, '5'])).
% 83.83/12.44 thf(zip_derived_cl1486, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 ( (((~) @ (moref @ X1 @ X2)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((moref @ X2 @ X0) => (moref @ X1 @ X0))))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)],
% 83.83/12.44 [zip_derived_cl1484])).
% 83.83/12.44 thf(zip_derived_cl1487, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (moref @ X1 @ X2)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((moref @ X2 @ X0) => (moref @ X1 @ X0))))),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl1486])).
% 83.83/12.44 thf(zip_derived_cl1488, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (moref @ X2 @ X0)
% 83.83/12.44 | (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (moref @ X1 @ X2))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1487])).
% 83.83/12.44 thf(zip_derived_cl15398, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (moref @ X2 @ X0)
% 83.83/12.44 | (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X2 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X1 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (moref @ X1 @ X2))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl1488])).
% 83.83/12.44 thf(satz51d, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X2:$i]: ( in @ X2 @ frac ) ) @
% 83.83/12.44 ( ^[X2:$i]:
% 83.83/12.44 ( ( moref @ X0 @ X1 ) =>
% 83.83/12.44 ( ( moreq @ X1 @ X2 ) => ( moref @ X0 @ X2 ) ) ) ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl290, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]:
% 83.83/12.44 (all_of @ (^[Y2 : $i]: (in @ Y2 @ frac)) @
% 83.83/12.44 (^[Y2 : $i]:
% 83.83/12.44 (((moref @ Y0 @ Y1) =>
% 83.83/12.44 (((moreq @ Y1 @ Y2) => (moref @ Y0 @ Y2)))))))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz51d])).
% 83.83/12.44 thf(zip_derived_cl291, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ frac))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))))) @
% 83.83/12.44 moref)))))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl290])).
% 83.83/12.44 thf(zip_derived_cl1489, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))))) @
% 83.83/12.44 moref)))))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl291, '0'])).
% 83.83/12.44 thf(zip_derived_cl1490, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @
% 83.83/12.44 (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 moreq)))))) @
% 83.83/12.44 moref)))))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1489, '7'])).
% 83.83/12.44 thf(zip_derived_cl1491, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 moreq)))))) @
% 83.83/12.44 moref))))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1490])).
% 83.83/12.44 thf(zip_derived_cl1492, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @ ((('#B') @ (=>) @ (moref @ X2))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))) @
% 83.83/12.44 (moref @ X2))))))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1491])).
% 83.83/12.44 thf(zip_derived_cl1493, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @ ((('#B') @ (=>) @ (moref @ X2))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))) @
% 83.83/12.44 (moref @ X2)))))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1492])).
% 83.83/12.44 thf(zip_derived_cl1494, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (moref @ X0))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))) @
% 83.83/12.44 (moref @ X0))))) @
% 83.83/12.44 Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1493, '7'])).
% 83.83/12.44 thf(zip_derived_cl1495, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (moref @ X0))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moreq)))) @
% 83.83/12.44 (moref @ X0)))))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1494])).
% 83.83/12.44 thf(zip_derived_cl1496, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (moref @ X0 @ X2))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moreq @ X2))) @ (moref @ X0))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1495])).
% 83.83/12.44 thf(zip_derived_cl1497, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (moref @ X0 @ X2))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moreq @ X2))) @ (moref @ X0))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1496])).
% 83.83/12.44 thf(zip_derived_cl1498, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (((=>) @ (moref @ X0 @ X1))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moreq @ X1))) @
% 83.83/12.44 (moref @ X0))) @
% 83.83/12.44 Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1497, '7'])).
% 83.83/12.44 thf(zip_derived_cl1499, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (moref @ X0 @ X1))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moreq @ X1))) @
% 83.83/12.44 (moref @ X0)))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1498])).
% 83.83/12.44 thf(zip_derived_cl1500, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 ( (((is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((moref @ X0 @ X1) => (((moreq @ X1 @ X3) => (moref @ X0 @ X3)))))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1499])).
% 83.83/12.44 thf(zip_derived_cl1501, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 ( (((is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((moref @ X0 @ X1) =>
% 83.83/12.44 (((imp @ (imp @ (moref @ X1 @ X3) @ ($false)) @
% 83.83/12.44 (n_eq @ X1 @ X3)) => (moref @ X0 @ X3)))))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl1500, '2', '3', '8'])).
% 83.83/12.44 thf(zip_derived_cl1502, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((moref @ X0 @ X1) =>
% 83.83/12.44 (((imp @ (imp @ (moref @ X1 @ X3) @ ($false)) @
% 83.83/12.44 (n_eq @ X1 @ X3)) => (moref @ X0 @ X3)))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1501])).
% 83.83/12.44 thf(zip_derived_cl1503, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (moref @ X0 @ X1)
% 83.83/12.44 | (((imp @ (imp @ (moref @ X1 @ X3) @ ($false)) @
% 83.83/12.44 (n_eq @ X1 @ X3)) => (moref @ X0 @ X3)))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1502])).
% 83.83/12.44 thf(zip_derived_cl1504, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (imp @ (imp @ (moref @ X1 @ X3) @ ($false)) @ (n_eq @ X1 @ X3))
% 83.83/12.44 | (moref @ X0 @ X3)
% 83.83/12.44 | ~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (moref @ X0 @ X1))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1503])).
% 83.83/12.44 thf(zip_derived_cl1505, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (((imp @ (moref @ X0 @ X2) @ ($false)) => (n_eq @ X0 @ X2)))
% 83.83/12.44 | ~ (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (moref @ X1 @ X2))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1504, '6'])).
% 83.83/12.44 thf(zip_derived_cl1507, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (n_eq @ X0 @ X2)
% 83.83/12.44 | (moref @ X1 @ X2)
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (moref @ X1 @ X0))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1505])).
% 83.83/12.44 thf(zip_derived_cl15399, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (n_eq @ X0 @ X2)
% 83.83/12.44 | (moref @ X1 @ X2)
% 83.83/12.44 | ~ (is_of @ X2 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X1 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (moref @ X1 @ X0))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl1507])).
% 83.83/12.44 thf(zip_derived_cl466, plain,
% 83.83/12.44 ( (imp @ (imp @ (lessf @ '#sk2' @ '#sk3') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk3'))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl465])).
% 83.83/12.44 thf(zip_derived_cl468, plain,
% 83.83/12.44 ( (((imp @ (lessf @ '#sk2' @ '#sk3') @ ($false)) => (n_eq @ '#sk2' @
% 83.83/12.44 '#sk3')))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl466, '5'])).
% 83.83/12.44 thf(zip_derived_cl471, plain,
% 83.83/12.44 ((~ (imp @ (lessf @ '#sk2' @ '#sk3') @ ($false))
% 83.83/12.44 | (n_eq @ '#sk2' @ '#sk3'))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl468])).
% 83.83/12.44 thf(zip_derived_cl474, plain,
% 83.83/12.44 ((~ (((lessf @ '#sk2' @ '#sk3') => ($false))) | (n_eq @ '#sk2' @ '#sk3'))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl471, '6'])).
% 83.83/12.44 thf(zip_derived_cl478, plain,
% 83.83/12.44 ((~ (((~) @ (lessf @ '#sk2' @ '#sk3'))) | (n_eq @ '#sk2' @ '#sk3'))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl474])).
% 83.83/12.44 thf(zip_derived_cl479, plain,
% 83.83/12.44 (( (lessf @ '#sk2' @ '#sk3') | (n_eq @ '#sk2' @ '#sk3'))),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl478])).
% 83.83/12.44 thf(zip_derived_cl464, plain,
% 83.83/12.44 ( (is_of @ '#sk4' @ ((('#C') @ in @ (pair1type @ nat))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl463])).
% 83.83/12.44 thf(zip_derived_cl15349, plain,
% 83.83/12.44 ( (is_of @ '#sk4' @ ('#ty_enc5' @ in @ (pair1type @ nat)))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl464])).
% 83.83/12.44 thf(zip_derived_cl470, plain,
% 83.83/12.44 (~ (imp @ (imp @ (lessf @ '#sk2' @ '#sk4') @ ($false)) @
% 83.83/12.44 (n_eq @ '#sk2' @ '#sk4'))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl467])).
% 83.83/12.44 thf(zip_derived_cl473, plain,
% 83.83/12.44 (~ (((imp @ (lessf @ '#sk2' @ '#sk4') @ ($false)) => (n_eq @ '#sk2' @
% 83.83/12.44 '#sk4')))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl470, '6'])).
% 83.83/12.44 thf(zip_derived_cl477, plain, (~ (n_eq @ '#sk2' @ '#sk4')),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl473])).
% 83.83/12.44 thf(satz41e, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]:
% 83.83/12.44 ( ( d_not @ ( moref @ X0 @ X1 ) ) => ( lesseq @ X0 @ X1 ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl262, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]: (((d_not @ (moref @ Y0 @ Y1)) => (lesseq @ Y0 @ Y1)))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz41e])).
% 83.83/12.44 thf(zip_derived_cl263, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref)))))) @
% 83.83/12.44 lesseq)))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl262])).
% 83.83/12.44 thf(zip_derived_cl636, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref)))))) @
% 83.83/12.44 lesseq)))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl263, '0'])).
% 83.83/12.44 thf(zip_derived_cl637, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref)))))) @
% 83.83/12.44 lesseq)) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl636, '7'])).
% 83.83/12.44 thf(zip_derived_cl638, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref)))))) @
% 83.83/12.44 lesseq))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl637])).
% 83.83/12.44 thf(zip_derived_cl639, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ ((('#B') @ d_not @ (moref @ X2))))) @
% 83.83/12.44 (lesseq @ X2))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl638])).
% 83.83/12.44 thf(zip_derived_cl640, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ ((('#B') @ d_not @ (moref @ X2))))) @
% 83.83/12.44 (lesseq @ X2)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl639])).
% 83.83/12.44 thf(zip_derived_cl641, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#B') @ d_not @ (moref @ X0))))) @
% 83.83/12.44 (lesseq @ X0) @ Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl640, '7'])).
% 83.83/12.44 thf(zip_derived_cl642, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#B') @ d_not @ (moref @ X0))))) @
% 83.83/12.44 (lesseq @ X0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl641])).
% 83.83/12.44 thf(zip_derived_cl643, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((d_not @ (moref @ X0 @ X2)) => (lesseq @ X0 @ X2)))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl642])).
% 83.83/12.44 thf(zip_derived_cl644, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((imp @ (moref @ X0 @ X2) @ ($false)) => (imp @
% 83.83/12.44 (imp @ (lessf @ X0 @ X2) @ ($false)) @ (n_eq @ X0 @ X2))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl643, '2', '2', '3', '4'])).
% 83.83/12.44 thf(zip_derived_cl645, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((imp @ (moref @ X0 @ X2) @ ($false)) => (imp @
% 83.83/12.44 (imp @ (lessf @ X0 @ X2) @ ($false)) @ (n_eq @ X0 @ X2))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl644])).
% 83.83/12.44 thf(zip_derived_cl646, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (imp @ (moref @ X0 @ X2) @ ($false))
% 83.83/12.44 | (imp @ (imp @ (lessf @ X0 @ X2) @ ($false)) @ (n_eq @ X0 @ X2))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl645])).
% 83.83/12.44 thf(zip_derived_cl647, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (((moref @ X1 @ X0) => ($false)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (imp @ (imp @ (lessf @ X1 @ X0) @ ($false)) @ (n_eq @ X1 @ X0)))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl646, '6'])).
% 83.83/12.44 thf(zip_derived_cl648, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (((~) @ (moref @ X1 @ X0)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (imp @ (imp @ (lessf @ X1 @ X0) @ ($false)) @ (n_eq @ X1 @ X0)))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl647])).
% 83.83/12.44 thf(zip_derived_cl649, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (imp @ (imp @ (lessf @ X1 @ X0) @ ($false)) @ (n_eq @ X1 @ X0)))),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl648])).
% 83.83/12.44 thf(zip_derived_cl650, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((imp @ (lessf @ X0 @ X1) @ ($false)) => (n_eq @ X0 @ X1)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (moref @ X0 @ X1))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl649, '5'])).
% 83.83/12.44 thf(zip_derived_cl651, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (imp @ (lessf @ X0 @ X1) @ ($false))
% 83.83/12.44 | (n_eq @ X0 @ X1)
% 83.83/12.44 | (moref @ X0 @ X1)
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl650])).
% 83.83/12.44 thf(zip_derived_cl652, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (((lessf @ X0 @ X1) => ($false)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (moref @ X0 @ X1)
% 83.83/12.44 | (n_eq @ X0 @ X1))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl651, '6'])).
% 83.83/12.44 thf(zip_derived_cl653, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (((~) @ (lessf @ X0 @ X1)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (moref @ X0 @ X1)
% 83.83/12.44 | (n_eq @ X0 @ X1))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl652])).
% 83.83/12.44 thf(zip_derived_cl654, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (lessf @ X0 @ X1)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (moref @ X0 @ X1)
% 83.83/12.44 | (n_eq @ X0 @ X1))),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl653])).
% 83.83/12.44 thf(zip_derived_cl15359, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (lessf @ X0 @ X1)
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X1 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | (moref @ X0 @ X1)
% 83.83/12.44 | (n_eq @ X0 @ X1))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl654])).
% 83.83/12.44 thf(zip_derived_cl476, plain,
% 83.83/12.44 ( (imp @ (lessf @ '#sk2' @ '#sk4') @ ($false))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl473])).
% 83.83/12.44 thf(zip_derived_cl481, plain, ( (((lessf @ '#sk2' @ '#sk4') => ($false)))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl476, '5'])).
% 83.83/12.44 thf(zip_derived_cl484, plain, ( (((~) @ (lessf @ '#sk2' @ '#sk4')))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl481])).
% 83.83/12.44 thf(zip_derived_cl485, plain, (~ (lessf @ '#sk2' @ '#sk4')),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl484])).
% 83.83/12.44 thf(satz39, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X2:$i]: ( in @ X2 @ frac ) ) @
% 83.83/12.44 ( ^[X2:$i]:
% 83.83/12.44 ( ( n_eq @ X0 @ X1 ) =>
% 83.83/12.44 ( ( n_eq @ X1 @ X2 ) => ( n_eq @ X0 @ X2 ) ) ) ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl242, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]:
% 83.83/12.44 (all_of @ (^[Y2 : $i]: (in @ Y2 @ frac)) @
% 83.83/12.44 (^[Y2 : $i]:
% 83.83/12.44 (((n_eq @ Y0 @ Y1) =>
% 83.83/12.44 (((n_eq @ Y1 @ Y2) => (n_eq @ Y0 @ Y2)))))))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz39])).
% 83.83/12.44 thf(zip_derived_cl243, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ frac))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))))) @
% 83.83/12.44 n_eq)))))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl242])).
% 83.83/12.44 thf(zip_derived_cl1330, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))))) @
% 83.83/12.44 n_eq)))))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl243, '0'])).
% 83.83/12.44 thf(zip_derived_cl1331, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @
% 83.83/12.44 (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 n_eq)))))) @
% 83.83/12.44 n_eq)))))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1330, '7'])).
% 83.83/12.44 thf(zip_derived_cl1332, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat)))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ ('#B'))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))))) @
% 83.83/12.44 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @
% 83.83/12.44 n_eq)))))) @
% 83.83/12.44 n_eq))))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1331])).
% 83.83/12.44 thf(zip_derived_cl1333, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @ ((('#B') @ (=>) @ (n_eq @ X2))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 (n_eq @ X2))))))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1332])).
% 83.83/12.44 thf(zip_derived_cl1334, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @ ((('#B') @ (=>) @ (n_eq @ X2))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 (n_eq @ X2)))))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1333])).
% 83.83/12.44 thf(zip_derived_cl1335, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (n_eq @ X0))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 (n_eq @ X0))))) @
% 83.83/12.44 Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1334, '7'])).
% 83.83/12.44 thf(zip_derived_cl1336, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#B') @
% 83.83/12.44 ((('#B') @ (=>) @ (n_eq @ X0))))) @
% 83.83/12.44 ((('#C') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 (n_eq @ X0)))))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1335])).
% 83.83/12.44 thf(zip_derived_cl1337, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (n_eq @ X0 @ X2))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X2))) @ (n_eq @ X0))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1336])).
% 83.83/12.44 thf(zip_derived_cl1338, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (n_eq @ X0 @ X2))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X2))) @ (n_eq @ X0))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1337])).
% 83.83/12.44 thf(zip_derived_cl1339, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (((=>) @ (n_eq @ X0 @ X1))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X1))) @
% 83.83/12.44 (n_eq @ X0))) @
% 83.83/12.44 Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl1338, '7'])).
% 83.83/12.44 thf(zip_derived_cl1340, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (((=>) @ (n_eq @ X0 @ X1))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X1))) @
% 83.83/12.44 (n_eq @ X0)))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl1339])).
% 83.83/12.44 thf(zip_derived_cl1341, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 ( (((is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((n_eq @ X0 @ X1) => (((n_eq @ X1 @ X3) => (n_eq @ X0 @ X3)))))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1340])).
% 83.83/12.44 thf(zip_derived_cl1342, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((n_eq @ X0 @ X1) => (((n_eq @ X1 @ X3) => (n_eq @ X0 @ X3)))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1341])).
% 83.83/12.44 thf(zip_derived_cl1343, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (n_eq @ X0 @ X1)
% 83.83/12.44 | (((n_eq @ X1 @ X3) => (n_eq @ X0 @ X3)))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1342])).
% 83.83/12.44 thf(zip_derived_cl1344, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (n_eq @ X1 @ X3)
% 83.83/12.44 | (n_eq @ X0 @ X3)
% 83.83/12.44 | ~ (is_of @ X3 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (n_eq @ X0 @ X1))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1343])).
% 83.83/12.44 thf(zip_derived_cl15392, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X3 : $i]:
% 83.83/12.44 (~ (n_eq @ X1 @ X3)
% 83.83/12.44 | (n_eq @ X0 @ X3)
% 83.83/12.44 | ~ (is_of @ X3 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X1 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (n_eq @ X0 @ X1))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl1344])).
% 83.83/12.44 thf(zip_derived_cl1483, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (n_eq @ X1 @ X2)
% 83.83/12.44 | (((moref @ X2 @ X0) => (moref @ X1 @ X0)))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1481])).
% 83.83/12.44 thf(zip_derived_cl1485, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (moref @ X2 @ X0)
% 83.83/12.44 | (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (n_eq @ X1 @ X2))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1483])).
% 83.83/12.44 thf(zip_derived_cl15397, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i, X2 : $i]:
% 83.83/12.44 (~ (moref @ X2 @ X0)
% 83.83/12.44 | (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X1 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X2 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (n_eq @ X1 @ X2))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl1485])).
% 83.83/12.44 thf(satz38, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]: ( ( n_eq @ X0 @ X1 ) => ( n_eq @ X1 @ X0 ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl240, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]: (((n_eq @ Y0 @ Y1) => (n_eq @ Y1 @ Y0)))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz38])).
% 83.83/12.44 thf(zip_derived_cl241, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @ ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 ((('#C') @ n_eq)))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl240])).
% 83.83/12.44 thf(zip_derived_cl561, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @ ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 ((('#C') @ n_eq)))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl241, '0'])).
% 83.83/12.44 thf(zip_derived_cl562, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 ((('#C') @ n_eq)))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl561, '7'])).
% 83.83/12.44 thf(zip_derived_cl563, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ n_eq)))) @
% 83.83/12.44 ((('#C') @ n_eq))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl562])).
% 83.83/12.44 thf(zip_derived_cl564, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X2))) @ ((('#C') @ n_eq @ X2)))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl563])).
% 83.83/12.44 thf(zip_derived_cl565, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X2))) @
% 83.83/12.44 ((('#C') @ n_eq @ X2))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl564])).
% 83.83/12.44 thf(zip_derived_cl566, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X0))) @
% 83.83/12.44 ((('#C') @ n_eq @ X0)) @ Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl565, '7'])).
% 83.83/12.44 thf(zip_derived_cl567, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (n_eq @ X0))) @
% 83.83/12.44 ((('#C') @ n_eq @ X0))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl566])).
% 83.83/12.44 thf(zip_derived_cl568, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((n_eq @ X0 @ X2) => (n_eq @ X2 @ X0)))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl567])).
% 83.83/12.44 thf(zip_derived_cl569, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((n_eq @ X0 @ X2) => (n_eq @ X2 @ X0)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl568])).
% 83.83/12.44 thf(zip_derived_cl570, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (n_eq @ X0 @ X2)
% 83.83/12.44 | (n_eq @ X2 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl569])).
% 83.83/12.44 thf(zip_derived_cl15354, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (n_eq @ X0 @ X2)
% 83.83/12.44 | (n_eq @ X2 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X2 @ ('#ty_enc5' @ in @ (pair1type @ nat))))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl570])).
% 83.83/12.44 thf(zip_derived_cl458, plain,
% 83.83/12.44 ( (is_of @ '#sk3' @ ((('#C') @ in @ (pair1type @ nat))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl457])).
% 83.83/12.44 thf(zip_derived_cl15348, plain,
% 83.83/12.44 ( (is_of @ '#sk3' @ ('#ty_enc5' @ in @ (pair1type @ nat)))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl458])).
% 83.83/12.44 thf(zip_derived_cl452, plain,
% 83.83/12.44 ( (is_of @ '#sk2' @ ((('#C') @ in @ (pair1type @ nat))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl451])).
% 83.83/12.44 thf(zip_derived_cl15347, plain,
% 83.83/12.44 ( (is_of @ '#sk2' @ ('#ty_enc5' @ in @ (pair1type @ nat)))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl452])).
% 83.83/12.44 thf(satz41d, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]:
% 83.83/12.44 ( ( lesseq @ X0 @ X1 ) => ( d_not @ ( moref @ X0 @ X1 ) ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl260, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]: (((lesseq @ Y0 @ Y1) => (d_not @ (moref @ Y0 @ Y1))))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz41d])).
% 83.83/12.44 thf(zip_derived_cl261, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref)))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl260])).
% 83.83/12.44 thf(zip_derived_cl616, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref)))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl261, '0'])).
% 83.83/12.44 thf(zip_derived_cl617, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref)))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl616, '7'])).
% 83.83/12.44 thf(zip_derived_cl618, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lesseq)))) @
% 83.83/12.44 ((('#B') @ ((('#B') @ d_not)) @ moref))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl617])).
% 83.83/12.44 thf(zip_derived_cl619, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ X2))) @
% 83.83/12.44 ((('#B') @ d_not @ (moref @ X2))))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl618])).
% 83.83/12.44 thf(zip_derived_cl620, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ X2))) @
% 83.83/12.44 ((('#B') @ d_not @ (moref @ X2)))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl619])).
% 83.83/12.44 thf(zip_derived_cl621, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ X0))) @
% 83.83/12.44 ((('#B') @ d_not @ (moref @ X0))) @ Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl620, '7'])).
% 83.83/12.44 thf(zip_derived_cl622, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lesseq @ X0))) @
% 83.83/12.44 ((('#B') @ d_not @ (moref @ X0)))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl621])).
% 83.83/12.44 thf(zip_derived_cl623, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((lesseq @ X0 @ X2) => (d_not @ (moref @ X0 @ X2))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl622])).
% 83.83/12.44 thf(zip_derived_cl624, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((imp @ (imp @ (lessf @ X0 @ X2) @ ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X2)) => (imp @ (moref @ X0 @ X2) @ ($false))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl623, '2', '2', '3', '4'])).
% 83.83/12.44 thf(zip_derived_cl625, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((imp @ (imp @ (lessf @ X0 @ X2) @ ($false)) @
% 83.83/12.44 (n_eq @ X0 @ X2)) => (imp @ (moref @ X0 @ X2) @ ($false))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl624])).
% 83.83/12.44 thf(zip_derived_cl626, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (imp @ (imp @ (lessf @ X0 @ X2) @ ($false)) @ (n_eq @ X0 @ X2))
% 83.83/12.44 | (imp @ (moref @ X0 @ X2) @ ($false))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl625])).
% 83.83/12.44 thf(zip_derived_cl627, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (((imp @ (lessf @ X1 @ X0) @ ($false)) => (n_eq @ X1 @ X0)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (imp @ (moref @ X1 @ X0) @ ($false)))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl626, '6'])).
% 83.83/12.44 thf(zip_derived_cl628, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((moref @ X0 @ X1) => ($false)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (((imp @ (lessf @ X0 @ X1) @ ($false)) => (n_eq @ X0 @ X1))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl627, '5'])).
% 83.83/12.44 thf(zip_derived_cl629, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((~) @ (moref @ X0 @ X1)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (((imp @ (lessf @ X0 @ X1) @ ($false)) => (n_eq @ X0 @ X1))))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl628])).
% 83.83/12.44 thf(zip_derived_cl630, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (moref @ X0 @ X1)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (((imp @ (lessf @ X0 @ X1) @ ($false)) => (n_eq @ X0 @ X1))))),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl629])).
% 83.83/12.44 thf(zip_derived_cl632, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (n_eq @ X0 @ X1)
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (moref @ X0 @ X1))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl630])).
% 83.83/12.44 thf(zip_derived_cl15357, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (n_eq @ X0 @ X1)
% 83.83/12.44 | ~ (is_of @ X1 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (moref @ X0 @ X1))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl632])).
% 83.83/12.44 thf(satz42, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]: ( ( moref @ X0 @ X1 ) => ( lessf @ X1 @ X0 ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl250, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]: (((moref @ Y0 @ Y1) => (lessf @ Y1 @ Y0)))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz42])).
% 83.83/12.44 thf(zip_derived_cl251, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 ((('#C') @ lessf)))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl250])).
% 83.83/12.44 thf(zip_derived_cl571, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 ((('#C') @ lessf)))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl251, '0'])).
% 83.83/12.44 thf(zip_derived_cl572, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 ((('#C') @ lessf)))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl571, '7'])).
% 83.83/12.44 thf(zip_derived_cl573, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ moref)))) @
% 83.83/12.44 ((('#C') @ lessf))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl572])).
% 83.83/12.44 thf(zip_derived_cl574, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X2))) @
% 83.83/12.44 ((('#C') @ lessf @ X2)))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl573])).
% 83.83/12.44 thf(zip_derived_cl575, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X2))) @
% 83.83/12.44 ((('#C') @ lessf @ X2))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl574])).
% 83.83/12.44 thf(zip_derived_cl576, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X0))) @
% 83.83/12.44 ((('#C') @ lessf @ X0)) @ Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl575, '7'])).
% 83.83/12.44 thf(zip_derived_cl577, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (moref @ X0))) @
% 83.83/12.44 ((('#C') @ lessf @ X0))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl576])).
% 83.83/12.44 thf(zip_derived_cl578, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((moref @ X0 @ X2) => (lessf @ X2 @ X0)))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl577])).
% 83.83/12.44 thf(zip_derived_cl579, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((moref @ X0 @ X2) => (lessf @ X2 @ X0)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl578])).
% 83.83/12.44 thf(zip_derived_cl580, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (moref @ X0 @ X2)
% 83.83/12.44 | (lessf @ X2 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl579])).
% 83.83/12.44 thf(zip_derived_cl15355, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (moref @ X0 @ X2)
% 83.83/12.44 | (lessf @ X2 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X2 @ ('#ty_enc5' @ in @ (pair1type @ nat))))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl580])).
% 83.83/12.44 thf(satz43, axiom,
% 83.83/12.44 (all_of @
% 83.83/12.44 ( ^[X0:$i]: ( in @ X0 @ frac ) ) @
% 83.83/12.44 ( ^[X0:$i]:
% 83.83/12.44 ( all_of @
% 83.83/12.44 ( ^[X1:$i]: ( in @ X1 @ frac ) ) @
% 83.83/12.44 ( ^[X1:$i]: ( ( lessf @ X0 @ X1 ) => ( moref @ X1 @ X0 ) ) ) ) ))).
% 83.83/12.44 thf(zip_derived_cl252, plain,
% 83.83/12.44 ( (all_of @ (^[Y0 : $i]: (in @ Y0 @ frac)) @
% 83.83/12.44 (^[Y0 : $i]:
% 83.83/12.44 (all_of @ (^[Y1 : $i]: (in @ Y1 @ frac)) @
% 83.83/12.44 (^[Y1 : $i]: (((lessf @ Y0 @ Y1) => (moref @ Y1 @ Y0)))))))),
% 83.83/12.44 inference('cnf', [status(esa)], [satz43])).
% 83.83/12.44 thf(zip_derived_cl253, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ frac)) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ frac))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lessf)))) @
% 83.83/12.44 ((('#C') @ moref)))))))),
% 83.83/12.44 inference('lams2combs', [status(thm)], [zip_derived_cl252])).
% 83.83/12.44 thf(zip_derived_cl581, plain,
% 83.83/12.44 ( (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lessf)))) @
% 83.83/12.44 ((('#C') @ moref)))))))),
% 83.83/12.44 inference('rw', [status(thm)], [zip_derived_cl253, '0'])).
% 83.83/12.44 thf(zip_derived_cl582, plain,
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lessf)))) @
% 83.83/12.44 ((('#C') @ moref)))) @
% 83.83/12.44 Y0)))))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl581, '7'])).
% 83.83/12.44 thf(zip_derived_cl583, plain,
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#B') @ (all_of @ ((('#C') @ in @ (pair1type @ nat)))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ ('#S') @
% 83.83/12.44 ((('#B') @ ((('#B') @ (=>))) @ lessf)))) @
% 83.83/12.44 ((('#C') @ moref))))))))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl582])).
% 83.83/12.44 thf(zip_derived_cl584, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) => (all_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lessf @ X2))) @
% 83.83/12.44 ((('#C') @ moref @ X2)))))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl583])).
% 83.83/12.44 thf(zip_derived_cl585, plain,
% 83.83/12.44 (![X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (all_of @ ((('#C') @ in @ (pair1type @ nat))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lessf @ X2))) @
% 83.83/12.44 ((('#C') @ moref @ X2))))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl584])).
% 83.83/12.44 thf(zip_derived_cl586, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ (^[Y0 : $i]:
% 83.83/12.44 (((is_of @ Y0 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lessf @ X0))) @
% 83.83/12.44 ((('#C') @ moref @ X0)) @ Y0)))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl585, '7'])).
% 83.83/12.44 thf(zip_derived_cl587, plain,
% 83.83/12.44 (![X0 : $i]:
% 83.83/12.44 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 83.83/12.44 ((('#C') @ is_of @
% 83.83/12.44 ((('#C') @ in @ (pair1type @ nat))))))) @
% 83.83/12.44 ((('#S') @ ((('#B') @ (=>) @ (lessf @ X0))) @
% 83.83/12.44 ((('#C') @ moref @ X0))))))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('comb-normalize', [status(thm)], [zip_derived_cl586])).
% 83.83/12.44 thf(zip_derived_cl588, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 ( (((is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))) =>
% 83.83/12.44 (((lessf @ X0 @ X2) => (moref @ X2 @ X0)))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl587])).
% 83.83/12.44 thf(zip_derived_cl589, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | (((lessf @ X0 @ X2) => (moref @ X2 @ X0)))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl588])).
% 83.83/12.44 thf(zip_derived_cl590, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (lessf @ X0 @ X2)
% 83.83/12.44 | (moref @ X2 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X2 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl589])).
% 83.83/12.44 thf(zip_derived_cl15356, plain,
% 83.83/12.44 (![X0 : $i, X2 : $i]:
% 83.83/12.44 (~ (lessf @ X0 @ X2)
% 83.83/12.44 | (moref @ X2 @ X0)
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X2 @ ('#ty_enc5' @ in @ (pair1type @ nat))))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl590])).
% 83.83/12.44 thf(zip_derived_cl631, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (imp @ (lessf @ X0 @ X1) @ ($false))
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (moref @ X0 @ X1))),
% 83.83/12.44 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl630])).
% 83.83/12.44 thf(zip_derived_cl633, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((lessf @ X1 @ X0) => ($false)))
% 83.83/12.44 | ~ (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('rw_clause', [status(thm)], [zip_derived_cl631, '5'])).
% 83.83/12.44 thf(zip_derived_cl634, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 ( (((~) @ (lessf @ X1 @ X0)))
% 83.83/12.44 | ~ (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl633])).
% 83.83/12.44 thf(zip_derived_cl635, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (lessf @ X1 @ X0)
% 83.83/12.44 | ~ (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X1 @ ((('#C') @ in @ (pair1type @ nat))))
% 83.83/12.44 | ~ (is_of @ X0 @ ((('#C') @ in @ (pair1type @ nat)))))),
% 83.83/12.44 inference('simplify nested equalities', [status(thm)],
% 83.83/12.44 [zip_derived_cl634])).
% 83.83/12.44 thf(zip_derived_cl15358, plain,
% 83.83/12.44 (![X0 : $i, X1 : $i]:
% 83.83/12.44 (~ (lessf @ X1 @ X0)
% 83.83/12.44 | ~ (moref @ X1 @ X0)
% 83.83/12.44 | ~ (is_of @ X1 @ ('#ty_enc5' @ in @ (pair1type @ nat)))
% 83.83/12.44 | ~ (is_of @ X0 @ ('#ty_enc5' @ in @ (pair1type @ nat))))),
% 83.83/12.44 inference('remove_ty_args', [status(thm)], [zip_derived_cl635])).
% 83.83/12.44 thf(zip_derived_cl15453, plain, ($false),
% 83.83/12.44 inference('eprover', [status(thm)],
% 83.83/12.44 [zip_derived_cl483, zip_derived_cl15398, zip_derived_cl15399,
% 83.83/12.44 zip_derived_cl479, zip_derived_cl15349, zip_derived_cl477,
% 83.83/12.44 zip_derived_cl15359, zip_derived_cl485, zip_derived_cl15392,
% 83.83/12.44 zip_derived_cl15397, zip_derived_cl15354,
% 83.83/12.44 zip_derived_cl15348, zip_derived_cl15347,
% 83.83/12.44 zip_derived_cl15357, zip_derived_cl15355,
% 83.83/12.44 zip_derived_cl15356, zip_derived_cl15358])).
% 83.83/12.44
% 83.83/12.44 % SZS output end Refutation
% 83.83/12.44
% 83.83/12.44
% 83.83/12.44 % Terminating...
% 84.46/12.61 % Runner terminated.
% 84.46/12.62 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------