%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.RJnWiSd46W true
% Computer : n002.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 : Tue May 5 07:08:43 PM UTC 2026
% Result : Theorem 138.51s 18.08s
% Output : Refutation 138.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.RJnWiSd46W true
% 0.17/0.34 % Computer : n002.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue May 5 08:57:46 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 % Running portfolio for 300 s
% 0.17/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Number of cores: 8
% 0.17/0.35 % Python version: Python 3.6.8
% 0.17/0.35 % Running in HO mode
% 0.57/0.67 % Total configuration time : 828
% 0.57/0.67 % Estimated wc time : 1656
% 0.57/0.67 % Estimated cpu time (8 cpus) : 207.0
% 0.57/0.72 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.57/0.73 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.57/0.73 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.57/0.73 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.57/0.75 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.57/0.77 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 0.58/0.80 % /export/starexec/sandbox/solver/bin/lams/30_b.l.sh running for 90s
% 0.58/0.80 % /export/starexec/sandbox/solver/bin/lams/35_full_unif.sh running for 56s
% 138.51/18.08 % Solved by lams/40_c.s.sh.
% 138.51/18.08 % done 661 iterations in 17.311s
% 138.51/18.08 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 138.51/18.08 % SZS output start Refutation
% 138.51/18.08 thf(term_type, type, term: $tType).
% 138.51/18.08 thf(subst_type, type, subst: $tType).
% 138.51/18.08 thf(d_subst_type, type, d_subst: $tType).
% 138.51/18.08 thf(d_term_type, type, d_term: $tType).
% 138.51/18.08 thf(axmap_type, type, axmap: $o).
% 138.51/18.08 thf(zip_tseitin_40_type, type, zip_tseitin_40: term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_8_type, type, zip_tseitin_8: subst > term > (term > $o) > $o).
% 138.51/18.08 thf(hoasinduction_lem3a_type, type, hoasinduction_lem3a: $o).
% 138.51/18.08 thf(hoasapnotvar_gthm_type, type, hoasapnotvar_gthm: $o).
% 138.51/18.08 thf(sk__247_type, type, sk__247: term).
% 138.51/18.08 thf(zip_tseitin_24_type, type, zip_tseitin_24: (subst > term > term) >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_29_type, type, zip_tseitin_29: $o).
% 138.51/18.08 thf(pushprop_lthm_orig_type, type, pushprop_lthm_orig: $o).
% 138.51/18.08 thf(termmset_gthm_type, type, termmset_gthm: $o).
% 138.51/18.08 thf(axclos_type, type, axclos: $o).
% 138.51/18.08 thf(lam_type, type, lam: term > term).
% 138.51/18.08 thf(lamnotap_type, type, lamnotap: $o).
% 138.51/18.08 thf(hoasinduction_lem3aa_type, type, hoasinduction_lem3aa: $o).
% 138.51/18.08 thf(zip_tseitin_38_type, type, zip_tseitin_38: term > subst >
% 138.51/18.08 (subst > term > term) >
% 138.51/18.08 (subst > term > term) > $o).
% 138.51/18.08 thf(sk__331_type, type, sk__331: subst).
% 138.51/18.08 thf(zip_tseitin_2_type, type, zip_tseitin_2: subst > term > (term > $o) >
% 138.51/18.08 (term > $o) > $o).
% 138.51/18.08 thf(hoaslamnotvar_gthm_type, type, hoaslamnotvar_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_71_type, type, zip_tseitin_71: $o).
% 138.51/18.08 thf(axvarcons_type, type, axvarcons: $o).
% 138.51/18.08 thf(zip_tseitin_34_type, type, zip_tseitin_34: $o).
% 138.51/18.08 thf(hoaslamnotvar_lthm_type, type, hoaslamnotvar_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_19_type, type, zip_tseitin_19: subst > subst > term >
% 138.51/18.08 subst >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(d2term_type, type, d2term: d_term > term).
% 138.51/18.08 thf(zip_tseitin_18_type, type, zip_tseitin_18: term > (term > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_9_type, type, zip_tseitin_9: term > term > term > term > $o).
% 138.51/18.08 thf(hoasinduction_no_psi_cond_lthm_type, type, hoasinduction_no_psi_cond_lthm:
% 138.51/18.08 $o).
% 138.51/18.08 thf(zip_tseitin_28_type, type, zip_tseitin_28: term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_35_type, type, zip_tseitin_35: $o).
% 138.51/18.08 thf(zip_tseitin_64_type, type, zip_tseitin_64: $o).
% 138.51/18.08 thf(substmonoid_type, type, substmonoid: $o).
% 138.51/18.08 thf(zip_tseitin_59_type, type, zip_tseitin_59: $o).
% 138.51/18.08 thf(zip_tseitin_37_type, type, zip_tseitin_37: $o).
% 138.51/18.08 thf(hoasinduction_lem3a_gthm_type, type, hoasinduction_lem3a_gthm: $o).
% 138.51/18.08 thf(substmonoid_gthm_type, type, substmonoid_gthm: $o).
% 138.51/18.08 thf(d_id_type, type, d_id: d_subst).
% 138.51/18.08 thf(pushprop_gthm_type, type, pushprop_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_20_type, type, zip_tseitin_20: subst > subst > term >
% 138.51/18.08 subst >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(hoasinduction_lem3v2_type, type, hoasinduction_lem3v2: $o).
% 138.51/18.08 thf(pushprop_lem1v2_type, type, pushprop_lem1v2: $o).
% 138.51/18.08 thf(zip_tseitin_72_type, type, zip_tseitin_72: $o).
% 138.51/18.08 thf(push_type, type, push: term > subst > subst).
% 138.51/18.08 thf(zip_tseitin_45_type, type, zip_tseitin_45: $o).
% 138.51/18.08 thf(zip_tseitin_69_type, type, zip_tseitin_69: $o).
% 138.51/18.08 thf(zip_tseitin_73_type, type, zip_tseitin_73: $o).
% 138.51/18.08 thf(zip_tseitin_22_type, type, zip_tseitin_22: term > term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(hoaslamnotap_lthm_type, type, hoaslamnotap_lthm: $o).
% 138.51/18.08 thf(axshiftcons_type, type, axshiftcons: $o).
% 138.51/18.08 thf(zip_tseitin_47_type, type, zip_tseitin_47: term > term > (term > $o) >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_16_type, type, zip_tseitin_16: $o).
% 138.51/18.08 thf(zip_tseitin_27_type, type, zip_tseitin_27: term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_68_type, type, zip_tseitin_68: $o).
% 138.51/18.08 thf(zip_tseitin_39_type, type, zip_tseitin_39: term >
% 138.51/18.08 (subst > term > term) >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_6_type, type, zip_tseitin_6: term > (term > $o) > $o).
% 138.51/18.08 thf(hoasinduction_lem1v2_type, type, hoasinduction_lem1v2: $o).
% 138.51/18.08 thf(sk__245_type, type, sk__245: subst > term > (term > $o) > term > $o).
% 138.51/18.08 thf(hoasapinj1_lthm_type, type, hoasapinj1_lthm: $o).
% 138.51/18.08 thf(hoasapinj1_type, type, hoasapinj1: $o).
% 138.51/18.08 thf(hoasinduction_p_and_p_prime_type, type, hoasinduction_p_and_p_prime:
% 138.51/18.08 (subst > term > subst > $o) > (term > $o) > $o).
% 138.51/18.08 thf(axapp_type, type, axapp: $o).
% 138.51/18.08 thf(hoasinduction_lem3_lthm_type, type, hoasinduction_lem3_lthm: $o).
% 138.51/18.08 thf(hoasinduction_lem3v2_lthm_type, type, hoasinduction_lem3v2_lthm: $o).
% 138.51/18.08 thf(pushprop_lem1v2_gthm_type, type, pushprop_lem1v2_gthm: $o).
% 138.51/18.08 thf(shinj_type, type, shinj: $o).
% 138.51/18.08 thf(zip_tseitin_12_type, type, zip_tseitin_12: term > (term > $o) > $o).
% 138.51/18.08 thf(hoasap_type, type, hoasap: subst > term > subst > term > term).
% 138.51/18.08 thf(hoasinduction_gthm_type, type, hoasinduction_gthm: $o).
% 138.51/18.08 thf(hoasinduction_lem3b_type, type, hoasinduction_lem3b: $o).
% 138.51/18.08 thf(hoaslaminj_type, type, hoaslaminj: $o).
% 138.51/18.08 thf(induction2_lthm_type, type, induction2_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_50_type, type, zip_tseitin_50: $o).
% 138.51/18.08 thf(zip_tseitin_4_type, type, zip_tseitin_4: term > term > (term > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_25_type, type, zip_tseitin_25: term > term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_14_type, type, zip_tseitin_14: $o).
% 138.51/18.08 thf(induction2_gthm_type, type, induction2_gthm: $o).
% 138.51/18.08 thf(hoasinduction_lem2_gthm_type, type, hoasinduction_lem2_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_3_type, type, zip_tseitin_3: term > term > $o).
% 138.51/18.08 thf(one_type, type, one: term).
% 138.51/18.08 thf(pushprop_lem2v2_lthm_type, type, pushprop_lem2v2_lthm: $o).
% 138.51/18.08 thf(id_type, type, id: subst).
% 138.51/18.08 thf(comp_type, type, comp: subst > subst > subst).
% 138.51/18.08 thf(hoaslamnotap_type, type, hoaslamnotap: $o).
% 138.51/18.08 thf(zip_tseitin_54_type, type, zip_tseitin_54: $o).
% 138.51/18.08 thf(induction2_type, type, induction2: $o).
% 138.51/18.08 thf(axvarid_type, type, axvarid: $o).
% 138.51/18.08 thf(axvarshift_type, type, axvarshift: $o).
% 138.51/18.08 thf(hoaslamnotap_gthm_type, type, hoaslamnotap_gthm: $o).
% 138.51/18.08 thf(induction2lem_type, type, induction2lem: $o).
% 138.51/18.08 thf(hoasinduction_lem1_gthm_type, type, hoasinduction_lem1_gthm: $o).
% 138.51/18.08 thf(sh_type, type, sh: subst).
% 138.51/18.08 thf(hoasinduction_lem2v2_type, type, hoasinduction_lem2v2: $o).
% 138.51/18.08 thf(sk__332_type, type, sk__332: subst > term > (term > $o) > term > $o).
% 138.51/18.08 thf(zip_tseitin_7_type, type, zip_tseitin_7: term > subst > (term > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_70_type, type, zip_tseitin_70: term > (term > $o) >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(laminj_type, type, laminj: $o).
% 138.51/18.08 thf(zip_tseitin_60_type, type, zip_tseitin_60: $o).
% 138.51/18.08 thf(hoasinduction_lem3aa_lthm_type, type, hoasinduction_lem3aa_lthm: $o).
% 138.51/18.08 thf(ulamvarind_type, type, ulamvarind: $o).
% 138.51/18.08 thf(sk__249_type, type, sk__249: (term > $o) > term).
% 138.51/18.08 thf(pushprop_lem2v2_type, type, pushprop_lem2v2: $o).
% 138.51/18.08 thf(zip_tseitin_62_type, type, zip_tseitin_62: $o).
% 138.51/18.08 thf(zip_tseitin_53_type, type, zip_tseitin_53: term > term > $o).
% 138.51/18.08 thf(hoasinduction_lthm_3_type, type, hoasinduction_lthm_3: $o).
% 138.51/18.08 thf(zip_tseitin_15_type, type, zip_tseitin_15: $o).
% 138.51/18.08 thf(zip_tseitin_65_type, type, zip_tseitin_65: $o).
% 138.51/18.08 thf(hoasinduction_lem3v2_f_lthm_type, type, hoasinduction_lem3v2_f_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_61_type, type, zip_tseitin_61: $o).
% 138.51/18.08 thf(apinj2_type, type, apinj2: $o).
% 138.51/18.08 thf(hoasapinj2_lthm_type, type, hoasapinj2_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_30_type, type, zip_tseitin_30: $o).
% 138.51/18.08 thf(ulamvarsh_type, type, ulamvarsh: $o).
% 138.51/18.08 thf(hoasinduction_lem3v2a_lthm_type, type, hoasinduction_lem3v2a_lthm: $o).
% 138.51/18.08 thf(sk__329_type, type, sk__329: term > $o).
% 138.51/18.08 thf(hoasinduction_lem3a_lthm_type, type, hoasinduction_lem3a_lthm: $o).
% 138.51/18.08 thf(pushprop_lthm_type, type, pushprop_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_48_type, type, zip_tseitin_48: term > term > term > term > $o).
% 138.51/18.08 thf(hoasapinj1_gthm_type, type, hoasapinj1_gthm: $o).
% 138.51/18.08 thf(hoasinduction_lem0_lthm_type, type, hoasinduction_lem0_lthm: $o).
% 138.51/18.08 thf(hoasinduction_lem3b_lthm_type, type, hoasinduction_lem3b_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_10_type, type, zip_tseitin_10: term > term > term > term > $o).
% 138.51/18.08 thf(zip_tseitin_58_type, type, zip_tseitin_58: $o).
% 138.51/18.08 thf(zip_tseitin_11_type, type, zip_tseitin_11: term > (term > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_74_type, type, zip_tseitin_74: $o).
% 138.51/18.08 thf(lamnotvar_type, type, lamnotvar: $o).
% 138.51/18.08 thf(apnotvar_type, type, apnotvar: $o).
% 138.51/18.08 thf(zip_tseitin_52_type, type, zip_tseitin_52: $o).
% 138.51/18.08 thf(pushprop_p_and_p_prime_type, type, pushprop_p_and_p_prime: term >
% 138.51/18.08 subst >
% 138.51/18.08 (term > $o) >
% 138.51/18.08 (term > $o) > $o).
% 138.51/18.08 thf(hoasapinj2_gthm_type, type, hoasapinj2_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_56_type, type, zip_tseitin_56: $o).
% 138.51/18.08 thf(d_one_type, type, d_one: d_term).
% 138.51/18.08 thf(pushprop_lem1_type, type, pushprop_lem1: $o).
% 138.51/18.08 thf(pushprop_type, type, pushprop: $o).
% 138.51/18.08 thf(hoasinduction_lem1_lthm_type, type, hoasinduction_lem1_lthm: $o).
% 138.51/18.08 thf(hoasinduction_lem3_gthm_type, type, hoasinduction_lem3_gthm: $o).
% 138.51/18.08 thf(sub_type, type, sub: term > subst > term).
% 138.51/18.08 thf(zip_tseitin_51_type, type, zip_tseitin_51: $o).
% 138.51/18.08 thf(zip_tseitin_33_type, type, zip_tseitin_33: term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(apinj1_type, type, apinj1: $o).
% 138.51/18.08 thf(axidl_type, type, axidl: $o).
% 138.51/18.08 thf(hoasinduction_type, type, hoasinduction: $o).
% 138.51/18.08 thf(ap_type, type, ap: term > term > term).
% 138.51/18.08 thf(termmset_type, type, termmset: $o).
% 138.51/18.08 thf(zip_tseitin_31_type, type, zip_tseitin_31: $o).
% 138.51/18.08 thf(zip_tseitin_57_type, type, zip_tseitin_57: term > subst > term >
% 138.51/18.08 (term > $o) > (term > $o) > $o).
% 138.51/18.08 thf(hoasapinj2_type, type, hoasapinj2: $o).
% 138.51/18.08 thf(zip_tseitin_32_type, type, zip_tseitin_32: term > (term > $o) >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(hoasinduction_lem1_type, type, hoasinduction_lem1: $o).
% 138.51/18.08 thf(pushprop_lem3v2_lthm_type, type, pushprop_lem3v2_lthm: $o).
% 138.51/18.08 thf(hoasinduction_lem3v2a_type, type, hoasinduction_lem3v2a: $o).
% 138.51/18.08 thf(hoasapnotvar_type, type, hoasapnotvar: $o).
% 138.51/18.08 thf(var_type, type, var: term > $o).
% 138.51/18.08 thf(pushprop_lem1_lthm_type, type, pushprop_lem1_lthm: $o).
% 138.51/18.08 thf(induction2lem_lthm_type, type, induction2lem_lthm: $o).
% 138.51/18.08 thf(pushprop_lem0_lthm_type, type, pushprop_lem0_lthm: $o).
% 138.51/18.08 thf(axassoc_type, type, axassoc: $o).
% 138.51/18.08 thf(hoaslamnotvar_type, type, hoaslamnotvar: $o).
% 138.51/18.08 thf(hoaslam_type, type, hoaslam: subst > (subst > term > term) > term).
% 138.51/18.08 thf(hoasinduction_lem2_lthm_type, type, hoasinduction_lem2_lthm: $o).
% 138.51/18.08 thf(pushprop_lem3v2_type, type, pushprop_lem3v2: $o).
% 138.51/18.08 thf(hoasinduction_lem3b_gthm_type, type, hoasinduction_lem3b_gthm: $o).
% 138.51/18.08 thf(pushprop_lem0_type, type, pushprop_lem0: $o).
% 138.51/18.08 thf(hoaslaminj_gthm_type, type, hoaslaminj_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_67_type, type, zip_tseitin_67: term > term >
% 138.51/18.08 (subst > term > term) > $o).
% 138.51/18.08 thf(hoasinduction_lem3_type, type, hoasinduction_lem3: $o).
% 138.51/18.08 thf(hoasinduction_lem2_type, type, hoasinduction_lem2: $o).
% 138.51/18.08 thf(hoasinduction_lem0_type, type, hoasinduction_lem0: $o).
% 138.51/18.08 thf(zip_tseitin_26_type, type, zip_tseitin_26: term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(hoaslaminj_lthm_type, type, hoaslaminj_lthm: $o).
% 138.51/18.08 thf(hoasinduction_lem3aaa_type, type, hoasinduction_lem3aaa: $o).
% 138.51/18.08 thf(axidr_type, type, axidr: $o).
% 138.51/18.08 thf(zip_tseitin_63_type, type, zip_tseitin_63: $o).
% 138.51/18.08 thf(sk__330_type, type, sk__330: term).
% 138.51/18.08 thf(hoasapnotvar_lthm_type, type, hoasapnotvar_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_5_type, type, zip_tseitin_5: term > term > (term > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_46_type, type, zip_tseitin_46: $o).
% 138.51/18.08 thf(sk__248_type, type, sk__248: subst).
% 138.51/18.08 thf(zip_tseitin_75_type, type, zip_tseitin_75: $o).
% 138.51/18.08 thf(hoasinduction_lem3v2_f_type, type, hoasinduction_lem3v2_f: $o).
% 138.51/18.08 thf(zip_tseitin_36_type, type, zip_tseitin_36: $o).
% 138.51/18.08 thf(pushprop_lem2v2_gthm_type, type, pushprop_lem2v2_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_0_type, type, zip_tseitin_0: term > (term > $o) >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(substmonoid_lthm_type, type, substmonoid_lthm: $o).
% 138.51/18.08 thf(axabs_type, type, axabs: $o).
% 138.51/18.08 thf(hoasinduction_lem3v2_gthm_type, type, hoasinduction_lem3v2_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_23_type, type, zip_tseitin_23: term >
% 138.51/18.08 (subst > term > term) >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_41_type, type, zip_tseitin_41: term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(hoasvar_type, type, hoasvar: subst > term > subst > $o).
% 138.51/18.08 thf(hoasinduction_lem2v2_gthm_type, type, hoasinduction_lem2v2_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_43_type, type, zip_tseitin_43: $o).
% 138.51/18.08 thf(ulamvar1_type, type, ulamvar1: $o).
% 138.51/18.08 thf(zip_tseitin_17_type, type, zip_tseitin_17: $o).
% 138.51/18.08 thf(hoasinduction_lem1v2_gthm_type, type, hoasinduction_lem1v2_gthm: $o).
% 138.51/18.08 thf(induction_type, type, induction: $o).
% 138.51/18.08 thf(zip_tseitin_13_type, type, zip_tseitin_13: term > (term > $o) > $o).
% 138.51/18.08 thf(pushprop_lem1v2_lthm_type, type, pushprop_lem1v2_lthm: $o).
% 138.51/18.08 thf(axscons_type, type, axscons: $o).
% 138.51/18.08 thf(zip_tseitin_49_type, type, zip_tseitin_49: term > term > term > term > $o).
% 138.51/18.08 thf(zip_tseitin_55_type, type, zip_tseitin_55: $o).
% 138.51/18.08 thf(sk__325_type, type, sk__325: (term > $o) > (term > $o) > subst > term > term).
% 138.51/18.08 thf(pushprop_lem1_gthm_type, type, pushprop_lem1_gthm: $o).
% 138.51/18.08 thf(zip_tseitin_21_type, type, zip_tseitin_21: term > term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(zip_tseitin_66_type, type, zip_tseitin_66: $o).
% 138.51/18.08 thf(induction2lem_gthm_type, type, induction2lem_gthm: $o).
% 138.51/18.08 thf(pushprop_lem0_gthm_type, type, pushprop_lem0_gthm: $o).
% 138.51/18.08 thf(termmset_lthm_type, type, termmset_lthm: $o).
% 138.51/18.08 thf(zip_tseitin_1_type, type, zip_tseitin_1: term > (term > $o) >
% 138.51/18.08 (term > $o) > subst > term > $o).
% 138.51/18.08 thf(d2subst_type, type, d2subst: d_subst > subst).
% 138.51/18.08 thf(hoasinduction_lthm_type, type, hoasinduction_lthm: $o).
% 138.51/18.08 thf(hoasinduction_no_psi_cond_type, type, hoasinduction_no_psi_cond: $o).
% 138.51/18.08 thf(zip_tseitin_42_type, type, zip_tseitin_42: $o).
% 138.51/18.08 thf(zip_tseitin_44_type, type, zip_tseitin_44: term >
% 138.51/18.08 (subst > term > subst > $o) > $o).
% 138.51/18.08 thf(sk__246_type, type, sk__246: term > $o).
% 138.51/18.08 thf(alg444_1, axiom,
% 138.51/18.08 (( ![T:term]: ( ?[DT:d_term]: ( ( T ) = ( d2term @ DT ) ) ) ) &
% 138.51/18.08 ( ![DT:d_term]: ( ( DT ) = ( d_one ) ) ) &
% 138.51/18.08 ( ![DT1:d_term,DT2:d_term]:
% 138.51/18.08 ( ( ( d2term @ DT1 ) = ( d2term @ DT2 ) ) => ( ( DT1 ) = ( DT2 ) ) ) ) &
% 138.51/18.08 ( ![S:subst]: ( ?[DS:d_subst]: ( ( S ) = ( d2subst @ DS ) ) ) ) &
% 138.51/18.08 ( ![DS:d_subst]: ( ( DS ) = ( d_id ) ) ) &
% 138.51/18.08 ( ![DS1:d_subst,DS2:d_subst]:
% 138.51/18.08 ( ( ( d2subst @ DS1 ) = ( d2subst @ DS2 ) ) => ( ( DS1 ) = ( DS2 ) ) ) ) &
% 138.51/18.08 ( ( one ) = ( d2term @ d_one ) ) &
% 138.51/18.08 ( ( ap @ ( d2term @ d_one ) @ ( d2term @ d_one ) ) = ( d2term @ d_one ) ) &
% 138.51/18.08 ( ( lam @ ( d2term @ d_one ) ) = ( d2term @ d_one ) ) &
% 138.51/18.08 ( ( sub @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) = ( d2term @ d_one ) ) &
% 138.51/18.08 ( ( id ) = ( d2subst @ d_id ) ) & ( ( sh ) = ( d2subst @ d_id ) ) &
% 138.51/18.08 ( ( push @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) = ( d2subst @ d_id ) ) &
% 138.51/18.08 ( ( comp @ ( d2subst @ d_id ) @ ( d2subst @ d_id ) ) = ( d2subst @ d_id ) ) &
% 138.51/18.08 ( ( hoasap @
% 138.51/18.08 ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) @
% 138.51/18.08 ( d2term @ d_one ) ) =
% 138.51/18.08 ( d2term @ d_one ) ) &
% 138.51/18.08 ( ![Bound_variable_4913:subst,Bound_variable_4915:( subst > term > term )]:
% 138.51/18.08 ( ( hoaslam @ Bound_variable_4913 @ Bound_variable_4915 ) =
% 138.51/18.08 ( d2term @ d_one ) ) ) &
% 138.51/18.08 ( ![P:( subst > term > subst > $o ),Q:( term > $o )]:
% 138.51/18.08 ( ( hoasinduction_p_and_p_prime @ P @ Q ) <=>
% 138.51/18.08 ( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) ) &
% 138.51/18.08 ( ![A:term,M:subst,P:( term > $o ),Q:( term > $o )]:
% 138.51/18.08 ( ( pushprop_p_and_p_prime @ A @ M @ P @ Q ) <=>
% 138.51/18.08 ( ![X:term]: ( ( Q @ X ) <=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ) ) ) &
% 138.51/18.08 ( ~( var @ ( d2term @ d_one ) ) ) &
% 138.51/18.08 ( ( pushprop_lem1v2 ) <=>
% 138.51/18.08 ( ![P:( term > $o ),Q:( term > $o ),A:term,M:subst]:
% 138.51/18.08 ( ( ~( P @ A ) ) |
% 138.51/18.08 ( ~( ![X:term]:
% 138.51/18.08 ( ( Q @ X ) <=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ) ) |
% 138.51/18.08 ( Q @ one ) ) ) ) &
% 138.51/18.08 ( pushprop_lem1_gthm ) & ( axmap ) & ( pushprop_lem0_gthm ) &
% 138.51/18.08 ( ( shinj ) <=>
% 138.51/18.08 ( ![A:term,B:term]:
% 138.51/18.08 ( ( ( sub @ A @ sh ) != ( sub @ B @ sh ) ) | ( ( A ) = ( B ) ) ) ) ) &
% 138.51/18.08 ( hoasinduction_lem1v2 ) & ( hoasinduction_lem1v2_gthm ) &
% 138.51/18.08 ( ( induction2lem ) <=>
% 138.51/18.08 ( ![P:( term > $o ),Bound_variable_2340:term,Bound_variable_2342:subst]:
% 138.51/18.08 ( ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( P @ B ) ) |
% 138.51/18.08 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.08 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.08 ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( var @ B ) ) | ( P @ ( sub @ B @ Bound_variable_2342 ) ) ) ) ) |
% 138.51/18.08 ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) ) ) ) &
% 138.51/18.08 ( ( hoasinduction_lem3v2_f ) <=>
% 138.51/18.08 ( ![B:term]:
% 138.51/18.08 ( ~( ![F:( subst > term > term )]:
% 138.51/18.08 ( ~( ![A:term,M:subst]:
% 138.51/18.08 ( ( sub @ B @ ( push @ A @ M ) ) = ( F @ M @ A ) ) ) ) ) ) ) ) &
% 138.51/18.08 ( axvarshift ) &
% 138.51/18.08 ( ( hoasapinj2 ) <=>
% 138.51/18.08 ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.08 ( ( ( ap @ ( sub @ A @ id ) @ C ) != ( ap @ ( sub @ B @ id ) @ D ) ) |
% 138.51/18.08 ( ( C ) = ( D ) ) ) ) ) &
% 138.51/18.08 ( hoasapnotvar_gthm ) &
% 138.51/18.08 ( ( hoasapinj1 ) <=>
% 138.51/18.08 ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.08 ( ( ( ap @ ( sub @ A @ id ) @ C ) != ( ap @ ( sub @ B @ id ) @ D ) ) |
% 138.51/18.08 ( ( A ) = ( B ) ) ) ) ) &
% 138.51/18.08 ( ~( ulamvar1 ) ) &
% 138.51/18.08 ( ( induction2lem_lthm ) <=>
% 138.51/18.08 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.08 ( ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.08 ( ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) =>
% 138.51/18.08 ( ( ![P:( term > $o ),Bound_variable_2140:term]:
% 138.51/18.08 ( ( ~( ![A:term]: ( ( ~( var @ A ) ) | ( P @ A ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) |
% 138.51/18.08 ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]: ( ( ~( P @ A ) ) | ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.08 ( P @ Bound_variable_2140 ) ) ) =>
% 138.51/18.08 ( ![P:( term > $o ),Bound_variable_2340:term,
% 138.51/18.08 Bound_variable_2342:subst]:
% 138.51/18.08 ( ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) |
% 138.51/18.08 ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( P @ B ) ) |
% 138.51/18.08 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.08 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.08 ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( var @ B ) ) |
% 138.51/18.08 ( P @ ( sub @ B @ Bound_variable_2342 ) ) ) ) ) |
% 138.51/18.08 ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) ) ) ) ) ) ) ) &
% 138.51/18.08 ( hoasinduction_lem3v2_gthm ) & ( apnotvar ) & ( pushprop_lthm_orig ) &
% 138.51/18.08 ( ( hoasinduction_lem3v2_f_lthm ) <=>
% 138.51/18.08 ( ![B:term]:
% 138.51/18.08 ( ~( ![F:( subst > term > term )]:
% 138.51/18.08 ( ~( ![A:term,M:subst]:
% 138.51/18.08 ( ( sub @ B @ ( push @ A @ M ) ) = ( F @ M @ A ) ) ) ) ) ) ) ) &
% 138.51/18.08 ( ( hoasinduction_lthm ) <=>
% 138.51/18.08 ( ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.08 ( ( ~( ![A:term]: ( ( ~( var @ A ) ) | ( P @ A ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( P @ B ) ) |
% 138.51/18.08 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.08 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.08 ( P @ Bound_variable_2367 ) ) ) =>
% 138.51/18.08 ( ( ![P:( subst > term > subst > $o ),Bound_variable_2999:term,
% 138.51/18.08 Bound_variable_3001:term]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.08 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.08 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.08 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.08 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.08 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) | ( ~( P @ id @ B @ id ) ) |
% 138.51/18.08 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.08 ( ~( P @ id @ Bound_variable_2999 @ id ) ) |
% 138.51/18.08 ( ~( P @ id @ Bound_variable_3001 @ id ) ) |
% 138.51/18.08 ( P @
% 138.51/18.08 id @ ( ap @ Bound_variable_2999 @ Bound_variable_3001 ) @ id ) ) ) =>
% 138.51/18.08 ( ( ![P:( subst > term > subst > $o ),Bound_variable_3211:term]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.08 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.08 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.08 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.08 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.08 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![F:( subst > term > term )]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.08 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.08 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.08 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.08 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.08 ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.08 ( P @
% 138.51/18.08 id @
% 138.51/18.08 ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @
% 138.51/18.08 id ) ) ) ) |
% 138.51/18.08 ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) ) ) =>
% 138.51/18.08 ( ![P:( subst > term > subst > $o ),Bound_variable_3283:term]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.08 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.08 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.08 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.08 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.08 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( var @ ( sub @ A @ id ) ) ) | ( P @ id @ A @ id ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) | ( ~( P @ id @ B @ id ) ) |
% 138.51/18.08 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.08 ( ~( ![F:( subst > term > term )]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.08 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.08 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.08 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.08 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.08 ( P @ id @ Bound_variable_3283 @ id ) ) ) ) ) ) ) &
% 138.51/18.08 ( ( hoasinduction_no_psi_cond_lthm ) <=>
% 138.51/18.08 ( ( ![P:( subst > term > subst > $o )]:
% 138.51/18.08 ( ~( ![Q:( term > $o )]:
% 138.51/18.08 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) ) ) ) =>
% 138.51/18.08 ( ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.08 ( ( ~( ![A:term]: ( ( ~( var @ A ) ) | ( P @ A ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( P @ B ) ) |
% 138.51/18.08 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.08 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.08 ( P @ Bound_variable_2367 ) ) ) =>
% 138.51/18.08 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.08 ( ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.08 Bound_variable_2931:term]:
% 138.51/18.08 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.08 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.08 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.08 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.08 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.08 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) |
% 138.51/18.08 ( ~( ![B:term]:
% 138.51/18.08 ( ( ~( Q @ B ) ) |
% 138.51/18.08 ( Q @
% 138.51/18.08 ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.08 ( Q @ ( lam @ Bound_variable_2931 ) ) ) ) =>
% 138.51/18.08 ( ![P:( subst > term > subst > $o ),Bound_variable_3295:term]:
% 138.51/18.08 ( ( ~( ![A:term,B:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.08 ( ~( P @ id @ B @ id ) ) |
% 138.51/18.08 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.08 ( ~( ![F:( subst > term > term )]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.08 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.08 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.08 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.08 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.08 ( P @ id @ Bound_variable_3295 @ id ) ) ) ) ) ) ) ) &
% 138.51/18.08 ( ( hoaslaminj ) <=>
% 138.51/18.08 ( ![F:( subst > term > term ),
% 138.51/18.08 Bound_variable_2547:( subst > term > term ),
% 138.51/18.08 Bound_variable_2549:subst,Bound_variable_2551:term]:
% 138.51/18.08 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.08 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.08 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.08 ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.08 ( ( sub @ ( Bound_variable_2547 @ M @ A ) @ N ) =
% 138.51/18.08 ( Bound_variable_2547 @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.08 ( ( lam @ ( F @ sh @ one ) ) !=
% 138.51/18.08 ( lam @ ( Bound_variable_2547 @ sh @ one ) ) ) |
% 138.51/18.08 ( ( F @ Bound_variable_2549 @ Bound_variable_2551 ) =
% 138.51/18.08 ( Bound_variable_2547 @ Bound_variable_2549 @ Bound_variable_2551 ) ) ) ) ) &
% 138.51/18.08 ( ( hoasinduction_lem3aaa ) <=>
% 138.51/18.08 ( ![P:( subst > term > subst > $o ),Bound_variable_3171:term]:
% 138.51/18.08 ( ( ~( ![F:( subst > term > term ),Bound_variable_3149:term]:
% 138.51/18.08 ( ( ~( ![A:term]:
% 138.51/18.08 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.08 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.08 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) |
% 138.51/18.08 ( ~( ![Bound_variable_3072:subst,Bound_variable_3074:term,
% 138.51/18.08 Bound_variable_3076:subst]:
% 138.51/18.08 ( ( sub @
% 138.51/18.08 ( F @ Bound_variable_3072 @ Bound_variable_3074 ) @
% 138.51/18.08 Bound_variable_3076 ) =
% 138.51/18.08 ( sub @
% 138.51/18.08 ( sub @
% 138.51/18.08 Bound_variable_3149 @
% 138.51/18.08 ( push @ Bound_variable_3074 @ Bound_variable_3072 ) ) @
% 138.51/18.08 Bound_variable_3076 ) ) ) ) |
% 138.51/18.08 ( ~( ![Bound_variable_3090:subst,Bound_variable_3092:term,
% 138.51/18.08 Bound_variable_3094:subst]:
% 138.51/18.08 ( ( F @
% 138.51/18.08 ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) @
% 138.51/18.08 ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) ) =
% 138.51/18.09 ( sub @
% 138.51/18.09 Bound_variable_3149 @
% 138.51/18.09 ( push @
% 138.51/18.09 ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) @
% 138.51/18.09 ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) ) ) ) ) ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @ ( sub @ Bound_variable_3171 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( lam @ ( sub @ Bound_variable_3171 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) &
% 138.51/18.09 ( induction2lem_gthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3aa_lthm ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3211:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem2 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_2999:term,
% 138.51/18.09 Bound_variable_3001:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) | ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( P @ id @ Bound_variable_2999 @ id ) ) |
% 138.51/18.09 ( ~( P @ id @ Bound_variable_3001 @ id ) ) |
% 138.51/18.09 ( P @ id @ ( ap @ Bound_variable_2999 @ Bound_variable_3001 ) @ id ) ) ) ) &
% 138.51/18.09 ( ( termmset_lthm ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) ) ) &
% 138.51/18.09 ( hoasinduction_lem1 ) & ( hoaslamnotap_lthm ) &
% 138.51/18.09 ( ( pushprop_lem1v2_lthm ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( ![P:( term > $o ),Q:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( ( ~( P @ A ) ) |
% 138.51/18.09 ( ~( ![X:term]:
% 138.51/18.09 ( ( Q @ X ) <=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ) ) |
% 138.51/18.09 ( Q @ one ) ) ) ) ) &
% 138.51/18.09 ( hoasapnotvar ) &
% 138.51/18.09 ( ( hoasinduction_lem0 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3283:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( var @ ( sub @ A @ id ) ) ) | ( P @ id @ A @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) | ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ Bound_variable_3283 @ id ) ) ) ) &
% 138.51/18.09 ( hoasinduction_gthm ) & ( axapp ) & ( hoaslamnotvar_lthm ) &
% 138.51/18.09 ( pushprop_lem3v2_lthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3b_lthm ) <=>
% 138.51/18.09 ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( F @ sh @ one ) != ( sub @ B @ ( push @ one @ sh ) ) ) ) ) ) ) &
% 138.51/18.09 ( ulamvarind ) &
% 138.51/18.09 ( ( induction ) <=>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2140:term]:
% 138.51/18.09 ( ( ~( ![A:term]: ( ( ~( var @ A ) ) | ( P @ A ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]: ( ( ~( P @ A ) ) | ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.09 ( P @ Bound_variable_2140 ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3a_lthm ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @
% 138.51/18.09 id ) ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3232:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( sub @ Bound_variable_3232 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ Bound_variable_3232 ) @ id ) ) ) ) ) ) &
% 138.51/18.09 ( termmset_gthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3aa ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) &
% 138.51/18.09 ( pushprop_lem1v2_gthm ) & ( hoaslamnotap_gthm ) &
% 138.51/18.09 ( hoaslamnotvar_gthm ) & ( hoasinduction_lem3b_gthm ) &
% 138.51/18.09 ( pushprop_lem2v2 ) & ( hoasinduction_lem3a_gthm ) & ( axclos ) &
% 138.51/18.09 ( axassoc ) &
% 138.51/18.09 ( ( hoasinduction_lem2v2 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2820:term,Bound_variable_2822:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) | ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) |
% 138.51/18.09 ( ~( Q @ Bound_variable_2820 ) ) |
% 138.51/18.09 ( ~( Q @ Bound_variable_2822 ) ) |
% 138.51/18.09 ( Q @ ( ap @ Bound_variable_2820 @ Bound_variable_2822 ) ) ) ) ) &
% 138.51/18.09 ( pushprop_lthm ) &
% 138.51/18.09 ( ( apinj2 ) <=>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.09 ( ( ( ap @ A @ C ) != ( ap @ B @ D ) ) | ( ( C ) = ( D ) ) ) ) ) &
% 138.51/18.09 ( ( apinj1 ) <=>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.09 ( ( ( ap @ A @ C ) != ( ap @ B @ D ) ) | ( ( A ) = ( B ) ) ) ) ) &
% 138.51/18.09 ( ( hoasapinj2_lthm ) <=>
% 138.51/18.09 ( ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.09 ( ( ( ap @ A @ C ) != ( ap @ B @ D ) ) | ( ( C ) = ( D ) ) ) ) =>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.09 ( ( ( ap @ ( sub @ A @ id ) @ C ) != ( ap @ ( sub @ B @ id ) @ D ) ) |
% 138.51/18.09 ( ( C ) = ( D ) ) ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2a ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2931:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( Q @ B ) ) |
% 138.51/18.09 ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( Q @ ( lam @ Bound_variable_2931 ) ) ) ) ) &
% 138.51/18.09 ( ( hoasapinj1_lthm ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.09 ( ( ( ap @ A @ C ) != ( ap @ B @ D ) ) | ( ( A ) = ( B ) ) ) ) =>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]:
% 138.51/18.09 ( ( ( ap @ ( sub @ A @ id ) @ C ) != ( ap @ ( sub @ B @ id ) @ D ) ) |
% 138.51/18.09 ( ( A ) = ( B ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( hoaslaminj_lthm ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( ( ![A:term,B:term]:
% 138.51/18.09 ( ( ( lam @ A ) != ( lam @ B ) ) | ( ( A ) = ( B ) ) ) ) =>
% 138.51/18.09 ( ![F:( subst > term > term ),
% 138.51/18.09 Bound_variable_2547:( subst > term > term ),
% 138.51/18.09 Bound_variable_2549:subst,Bound_variable_2551:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( Bound_variable_2547 @ M @ A ) @ N ) =
% 138.51/18.09 ( Bound_variable_2547 @
% 138.51/18.09 ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ( lam @ ( F @ sh @ one ) ) !=
% 138.51/18.09 ( lam @ ( Bound_variable_2547 @ sh @ one ) ) ) |
% 138.51/18.09 ( ( F @ Bound_variable_2549 @ Bound_variable_2551 ) =
% 138.51/18.09 ( Bound_variable_2547 @
% 138.51/18.09 Bound_variable_2549 @ Bound_variable_2551 ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( axvarcons ) <=>
% 138.51/18.09 ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) ) &
% 138.51/18.09 ( ( axscons ) <=>
% 138.51/18.09 ( ![M:subst]:
% 138.51/18.09 ( ( M ) = ( push @ ( sub @ one @ M ) @ ( comp @ sh @ M ) ) ) ) ) &
% 138.51/18.09 ( hoasinduction_lem2v2_gthm ) &
% 138.51/18.09 ( ( axidr ) <=> ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) ) &
% 138.51/18.09 ( ( pushprop_lem1 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),K:( term > $o ),A:term,M:subst,B:term]:
% 138.51/18.09 ( ( ~( P @ A ) ) | ( K @ ( sub @ A @ ( push @ B @ M ) ) ) ) ) ) &
% 138.51/18.09 ( ( laminj ) <=>
% 138.51/18.09 ( ![A:term,B:term]:
% 138.51/18.09 ( ( ( lam @ A ) != ( lam @ B ) ) | ( ( A ) = ( B ) ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3_lthm ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @
% 138.51/18.09 id ) ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3211:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) ) ) ) ) ) &
% 138.51/18.09 ( ( pushprop_lem0 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]:
% 138.51/18.09 ( ( Q @ X ) <=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( pushprop_gthm ) & ( axabs ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2a_lthm ) <=>
% 138.51/18.09 ( ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ~( ![A:term,M:subst]:
% 138.51/18.09 ( ( sub @ B @ ( push @ A @ M ) ) = ( F @ M @ A ) ) ) ) ) ) ) =>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2931:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( Q @ B ) ) |
% 138.51/18.09 ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( Q @ ( lam @ Bound_variable_2931 ) ) ) ) ) ) ) &
% 138.51/18.09 ( hoasinduction_lem2_lthm ) & ( hoasapinj2_gthm ) &
% 138.51/18.09 ( hoasinduction_lem1_lthm ) & ( ~( lamnotap ) ) & ( hoasapinj1_gthm ) &
% 138.51/18.09 ( hoaslamnotvar ) &
% 138.51/18.09 ( ( axidl ) <=> ( ![M:subst]: ( ( M ) = ( comp @ id @ M ) ) ) ) &
% 138.51/18.09 ( hoaslaminj_gthm ) &
% 138.51/18.09 ( ( induction2_lthm ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ( ![P:( term > $o ),Bound_variable_2340:term,
% 138.51/18.09 Bound_variable_2342:subst]:
% 138.51/18.09 ( ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ B ) ) |
% 138.51/18.09 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( var @ B ) ) |
% 138.51/18.09 ( P @ ( sub @ B @ Bound_variable_2342 ) ) ) ) ) |
% 138.51/18.09 ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) ) ) =>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( ( ~( ![A:term]: ( ( ~( var @ A ) ) | ( P @ A ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ B ) ) |
% 138.51/18.09 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.09 ( P @ Bound_variable_2367 ) ) ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem0_lthm ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( substmonoid_lthm ) <=>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ id @ M ) ) ) =>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) =>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) &
% 138.51/18.09 ( ![M:subst]: ( ( M ) = ( comp @ id @ M ) ) ) ) ) ) ) &
% 138.51/18.09 ( pushprop ) & ( hoasinduction_lem3_gthm ) &
% 138.51/18.09 ( hoasinduction_lem2_gthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3b ) <=>
% 138.51/18.09 ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( F @ sh @ one ) != ( sub @ B @ ( push @ one @ sh ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( substmonoid ) <=>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) &
% 138.51/18.09 ( ![M:subst]: ( ( M ) = ( comp @ id @ M ) ) ) ) ) &
% 138.51/18.09 ( lamnotvar ) &
% 138.51/18.09 ( ( hoasinduction_lem3a ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3232:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @
% 138.51/18.09 id @ ( sub @ Bound_variable_3232 @ ( push @ B @ id ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ Bound_variable_3232 ) @ id ) ) ) ) &
% 138.51/18.09 ( hoasinduction_lem1_gthm ) &
% 138.51/18.09 ( ( hoasinduction_no_psi_cond ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3295:term]:
% 138.51/18.09 ( ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) | ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ Bound_variable_3295 @ id ) ) ) ) &
% 138.51/18.09 ( induction2_gthm ) & ( pushprop_lem2v2_lthm ) &
% 138.51/18.09 ( ~( hoasvar @
% 138.51/18.09 ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) ) &
% 138.51/18.09 ( ( hoaslamnotap ) <=>
% 138.51/18.09 ( ![F:( subst > term > term ),Bound_variable_2603:term,
% 138.51/18.09 Bound_variable_2605:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ( lam @ ( F @ sh @ one ) ) !=
% 138.51/18.09 ( ap @ ( sub @ Bound_variable_2603 @ id ) @ Bound_variable_2605 ) ) ) ) ) &
% 138.51/18.09 ( substmonoid_gthm ) & ( ulamvarsh ) &
% 138.51/18.09 ( ( induction2 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( ( ~( ![A:term]: ( ( ~( var @ A ) ) | ( P @ A ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ B ) ) |
% 138.51/18.09 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.09 ( P @ Bound_variable_2367 ) ) ) ) &
% 138.51/18.09 ( pushprop_lem3v2 ) & ( pushprop_lem2v2_gthm ) &
% 138.51/18.09 ( ( pushprop_lem1_lthm ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( ![P:( term > $o ),K:( term > $o ),A:term,M:subst,B:term]:
% 138.51/18.09 ( ( ~( P @ A ) ) | ( K @ ( sub @ A @ ( push @ B @ M ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2910:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( Q @ B ) ) |
% 138.51/18.09 ( Q @ ( sub @ Bound_variable_2910 @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( Q @ ( lam @ Bound_variable_2910 ) ) ) ) ) &
% 138.51/18.09 ( ( axshiftcons ) <=>
% 138.51/18.09 ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) ) &
% 138.51/18.09 ( ( termmset ) <=> ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) ) &
% 138.51/18.09 ( ( pushprop_lem0_lthm ) <=>
% 138.51/18.09 ( ![P:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]:
% 138.51/18.09 ( ( Q @ X ) <=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( hoasapnotvar_lthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2_lthm ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2910:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( Q @ B ) ) |
% 138.51/18.09 ( Q @ ( sub @ Bound_variable_2910 @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( Q @ ( lam @ Bound_variable_2910 ) ) ) ) ) ) &
% 138.51/18.09 ( ( axvarid ) <=> ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lthm_3 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) ) ) ) =>
% 138.51/18.09 ( ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( ( ~( ![A:term]: ( ( ~( var @ A ) ) | ( P @ A ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ A ) ) | ( ~( P @ B ) ) | ( P @ ( ap @ A @ B ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( P @ B ) ) |
% 138.51/18.09 ( P @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( P @ ( lam @ A ) ) ) ) ) |
% 138.51/18.09 ( P @ Bound_variable_2367 ) ) ) =>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2931:term]:
% 138.51/18.09 ( ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![B:term]:
% 138.51/18.09 ( ( ~( Q @ B ) ) |
% 138.51/18.09 ( Q @
% 138.51/18.09 ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) ) ) ) |
% 138.51/18.09 ( Q @ ( lam @ Bound_variable_2931 ) ) ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3283:term]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) |
% 138.51/18.09 ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) |
% 138.51/18.09 ( P @ M @ A @ ( comp @ K @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( var @ ( sub @ A @ id ) ) ) | ( P @ id @ A @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( ~( P @ id @ B @ id ) ) |
% 138.51/18.09 ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![A:term]:
% 138.51/18.09 ( ( ~( P @ id @ A @ id ) ) |
% 138.51/18.09 ( P @ id @ ( F @ id @ A ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) ) ) ) |
% 138.51/18.09 ( P @ id @ Bound_variable_3283 @ id ) ) ) ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_0, type, zip_tseitin_75 : $o).
% 138.51/18.09 thf(zf_stmt_1, axiom,
% 138.51/18.09 (( zip_tseitin_75 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_74 ) ))).thf(zf_stmt_2, type, zip_tseitin_74 : $o).
% 138.51/18.09 thf(zf_stmt_3, axiom,
% 138.51/18.09 (( zip_tseitin_74 ) <=>
% 138.51/18.09 ( ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( zip_tseitin_18 @ Bound_variable_2367 @ P ) ) =>
% 138.51/18.09 ( zip_tseitin_73 ) ))).thf(zf_stmt_4, type, zip_tseitin_73 : $o).
% 138.51/18.09 thf(zf_stmt_5, axiom,
% 138.51/18.09 (( zip_tseitin_73 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) => ( zip_tseitin_72 ) ))).
% 138.51/18.09 thf(zf_stmt_6, type, zip_tseitin_72 : $o).
% 138.51/18.09 thf(zf_stmt_7, axiom,
% 138.51/18.09 (( zip_tseitin_72 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2931:term]:
% 138.51/18.09 ( zip_tseitin_32 @ Bound_variable_2931 @ Q @ P ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3283:term]:
% 138.51/18.09 ( zip_tseitin_28 @ Bound_variable_3283 @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_8, type, zip_tseitin_71 : $o).
% 138.51/18.09 thf(zf_stmt_9, axiom,
% 138.51/18.09 (( zip_tseitin_71 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2910:term]:
% 138.51/18.09 ( zip_tseitin_70 @ Bound_variable_2910 @ Q @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_10, type, zip_tseitin_70 :
% 138.51/18.09 term > ( term > $o ) > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_11, axiom,
% 138.51/18.09 (![Bound_variable_2910:term,Q:( term > $o ),P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_70 @ Bound_variable_2910 @ Q @ P ) <=>
% 138.51/18.09 ( ( Q @ ( lam @ Bound_variable_2910 ) ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_5 @ B @ Bound_variable_2910 @ Q ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]: ( zip_tseitin_24 @ F @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_20 @ K @ N @ A @ M @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_19 @ K @ N @ A @ M @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_12, type, zip_tseitin_69 : $o).
% 138.51/18.09 thf(zf_stmt_13, axiom,
% 138.51/18.09 (( zip_tseitin_69 ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_68 ) ))).thf(zf_stmt_14, type, zip_tseitin_68 : $o).
% 138.51/18.09 thf(zf_stmt_15, axiom,
% 138.51/18.09 (( zip_tseitin_68 ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( ![P:( term > $o ),K:( term > $o ),A:term,M:subst,B:term]:
% 138.51/18.09 ( zip_tseitin_57 @ B @ M @ A @ K @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_16, type, zip_tseitin_67 :
% 138.51/18.09 term > term > ( subst > term > term ) > $o).
% 138.51/18.09 thf(zf_stmt_17, axiom,
% 138.51/18.09 (![Bound_variable_2605:term,Bound_variable_2603:term,
% 138.51/18.09 F:( subst > term > term )]:
% 138.51/18.09 ( ( zip_tseitin_67 @ Bound_variable_2605 @ Bound_variable_2603 @ F ) <=>
% 138.51/18.09 ( ( ( lam @ ( F @ sh @ one ) ) !=
% 138.51/18.09 ( ap @ ( sub @ Bound_variable_2603 @ id ) @ Bound_variable_2605 ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_18, type, zip_tseitin_66 : $o).
% 138.51/18.09 thf(zf_stmt_19, axiom,
% 138.51/18.09 (( zip_tseitin_66 ) <=>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ id @ M ) ) ) => ( zip_tseitin_65 ) ))).
% 138.51/18.09 thf(zf_stmt_20, type, zip_tseitin_65 : $o).
% 138.51/18.09 thf(zf_stmt_21, axiom,
% 138.51/18.09 (( zip_tseitin_65 ) <=>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) => ( zip_tseitin_64 ) ))).
% 138.51/18.09 thf(zf_stmt_22, type, zip_tseitin_64 : $o).
% 138.51/18.09 thf(zf_stmt_23, axiom,
% 138.51/18.09 (( zip_tseitin_64 ) <=>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ id @ M ) ) ) &
% 138.51/18.09 ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_24, type, zip_tseitin_63 : $o).
% 138.51/18.09 thf(zf_stmt_25, axiom,
% 138.51/18.09 (( zip_tseitin_63 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) => ( zip_tseitin_62 ) ))).
% 138.51/18.09 thf(zf_stmt_26, type, zip_tseitin_62 : $o).
% 138.51/18.09 thf(zf_stmt_27, axiom,
% 138.51/18.09 (( zip_tseitin_62 ) <=>
% 138.51/18.09 ( ( ![P:( term > $o ),Bound_variable_2340:term,Bound_variable_2342:subst]:
% 138.51/18.09 ( zip_tseitin_8 @ Bound_variable_2342 @ Bound_variable_2340 @ P ) ) =>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( zip_tseitin_18 @ Bound_variable_2367 @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_28, type, zip_tseitin_61 : $o).
% 138.51/18.09 thf(zf_stmt_29, axiom,
% 138.51/18.09 (( zip_tseitin_61 ) <=>
% 138.51/18.09 ( ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ~( ![A:term,M:subst]:
% 138.51/18.09 ( ( sub @ B @ ( push @ A @ M ) ) = ( F @ M @ A ) ) ) ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_60 ) ))).thf(zf_stmt_30, type, zip_tseitin_60 : $o).
% 138.51/18.09 thf(zf_stmt_31, axiom,
% 138.51/18.09 (( zip_tseitin_60 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2931:term]:
% 138.51/18.09 ( zip_tseitin_32 @ Bound_variable_2931 @ Q @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_32, type, zip_tseitin_59 : $o).
% 138.51/18.09 thf(zf_stmt_33, axiom,
% 138.51/18.09 (( zip_tseitin_59 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) => ( zip_tseitin_58 ) ))).
% 138.51/18.09 thf(zf_stmt_34, type, zip_tseitin_58 : $o).
% 138.51/18.09 thf(zf_stmt_35, axiom,
% 138.51/18.09 (( zip_tseitin_58 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( zip_tseitin_41 @ Bound_variable_3046 @ P ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3211:term]:
% 138.51/18.09 ( zip_tseitin_26 @ Bound_variable_3211 @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_36, type, zip_tseitin_57 :
% 138.51/18.09 term > subst > term > ( term > $o ) > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_37, axiom,
% 138.51/18.09 (![B:term,M:subst,A:term,K:( term > $o ),P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_57 @ B @ M @ A @ K @ P ) <=>
% 138.51/18.09 ( ( K @ ( sub @ A @ ( push @ B @ M ) ) ) | ( ~( P @ A ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_38, type, zip_tseitin_56 : $o).
% 138.51/18.09 thf(zf_stmt_39, axiom,
% 138.51/18.09 (( zip_tseitin_56 ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_55 ) ))).thf(zf_stmt_40, type, zip_tseitin_55 : $o).
% 138.51/18.09 thf(zf_stmt_41, axiom,
% 138.51/18.09 (( zip_tseitin_55 ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_54 ) ))).thf(zf_stmt_42, type, zip_tseitin_54 : $o).
% 138.51/18.09 thf(zf_stmt_43, axiom,
% 138.51/18.09 (( zip_tseitin_54 ) <=>
% 138.51/18.09 ( ( ![A:term,B:term]: ( zip_tseitin_53 @ B @ A ) ) =>
% 138.51/18.09 ( ![F:( subst > term > term ),
% 138.51/18.09 Bound_variable_2547:( subst > term > term ),
% 138.51/18.09 Bound_variable_2549:subst,Bound_variable_2551:term]:
% 138.51/18.09 ( zip_tseitin_38 @
% 138.51/18.09 Bound_variable_2551 @ Bound_variable_2549 @ Bound_variable_2547 @ F ) ) ))).
% 138.51/18.09 thf(zf_stmt_44, type, zip_tseitin_53 : term > term > $o).
% 138.51/18.09 thf(zf_stmt_45, axiom,
% 138.51/18.09 (![B:term,A:term]:
% 138.51/18.09 ( ( zip_tseitin_53 @ B @ A ) <=>
% 138.51/18.09 ( ( ( A ) = ( B ) ) | ( ( lam @ A ) != ( lam @ B ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_46, type, zip_tseitin_52 : $o).
% 138.51/18.09 thf(zf_stmt_47, axiom,
% 138.51/18.09 (( zip_tseitin_52 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) => ( zip_tseitin_51 ) ))).
% 138.51/18.09 thf(zf_stmt_48, type, zip_tseitin_51 : $o).
% 138.51/18.09 thf(zf_stmt_49, axiom,
% 138.51/18.09 (( zip_tseitin_51 ) <=>
% 138.51/18.09 ( ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_49 @ D @ C @ B @ A ) ) =>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_10 @ D @ C @ B @ A ) ) ))).
% 138.51/18.09 thf(zf_stmt_50, type, zip_tseitin_50 : $o).
% 138.51/18.09 thf(zf_stmt_51, axiom,
% 138.51/18.09 (( zip_tseitin_50 ) <=>
% 138.51/18.09 ( ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_48 @ D @ C @ B @ A ) ) =>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_9 @ D @ C @ B @ A ) ) ))).
% 138.51/18.09 thf(zf_stmt_52, type, zip_tseitin_49 : term > term > term > term > $o).
% 138.51/18.09 thf(zf_stmt_53, axiom,
% 138.51/18.09 (![D:term,C:term,B:term,A:term]:
% 138.51/18.09 ( ( zip_tseitin_49 @ D @ C @ B @ A ) <=>
% 138.51/18.09 ( ( ( A ) = ( B ) ) | ( ( ap @ A @ C ) != ( ap @ B @ D ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_54, type, zip_tseitin_48 : term > term > term > term > $o).
% 138.51/18.09 thf(zf_stmt_55, axiom,
% 138.51/18.09 (![D:term,C:term,B:term,A:term]:
% 138.51/18.09 ( ( zip_tseitin_48 @ D @ C @ B @ A ) <=>
% 138.51/18.09 ( ( ( C ) = ( D ) ) | ( ( ap @ A @ C ) != ( ap @ B @ D ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_56, type, zip_tseitin_47 :
% 138.51/18.09 term > term > ( term > $o ) > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_57, axiom,
% 138.51/18.09 (![Bound_variable_2822:term,Bound_variable_2820:term,Q:( term > $o ),
% 138.51/18.09 P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_47 @ Bound_variable_2822 @ Bound_variable_2820 @ Q @ P ) <=>
% 138.51/18.09 ( ( Q @ ( ap @ Bound_variable_2820 @ Bound_variable_2822 ) ) |
% 138.51/18.09 ( ~( Q @ Bound_variable_2822 ) ) | ( ~( Q @ Bound_variable_2820 ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]: ( zip_tseitin_21 @ B @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_20 @ K @ N @ A @ M @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_19 @ K @ N @ A @ M @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_58, type, zip_tseitin_46 : $o).
% 138.51/18.09 thf(zf_stmt_59, axiom,
% 138.51/18.09 (( zip_tseitin_46 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) => ( zip_tseitin_45 ) ))).
% 138.51/18.09 thf(zf_stmt_60, type, zip_tseitin_45 : $o).
% 138.51/18.09 thf(zf_stmt_61, axiom,
% 138.51/18.09 (( zip_tseitin_45 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( zip_tseitin_41 @ Bound_variable_3046 @ P ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3232:term]:
% 138.51/18.09 ( zip_tseitin_44 @ Bound_variable_3232 @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_62, type, zip_tseitin_44 :
% 138.51/18.09 term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_63, axiom,
% 138.51/18.09 (![Bound_variable_3232:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_44 @ Bound_variable_3232 @ P ) <=>
% 138.51/18.09 ( ( P @ id @ ( lam @ Bound_variable_3232 ) @ id ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_25 @ B @ Bound_variable_3232 @ P ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]: ( zip_tseitin_24 @ F @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_64, type, zip_tseitin_43 : $o).
% 138.51/18.09 thf(zf_stmt_65, axiom,
% 138.51/18.09 (( zip_tseitin_43 ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( ![P:( term > $o ),Q:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( zip_tseitin_2 @ M @ A @ Q @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_66, type, zip_tseitin_42 : $o).
% 138.51/18.09 thf(zf_stmt_67, axiom,
% 138.51/18.09 (( zip_tseitin_42 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) =>
% 138.51/18.09 ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_68, type, zip_tseitin_41 :
% 138.51/18.09 term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_69, axiom,
% 138.51/18.09 (![Bound_variable_3046:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_41 @ Bound_variable_3046 @ P ) <=>
% 138.51/18.09 ( ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_25 @ B @ Bound_variable_3046 @ P ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]: ( zip_tseitin_24 @ F @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_70, type, zip_tseitin_40 :
% 138.51/18.09 term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_71, axiom,
% 138.51/18.09 (![Bound_variable_3171:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_40 @ Bound_variable_3171 @ P ) <=>
% 138.51/18.09 ( ( P @
% 138.51/18.09 id @
% 138.51/18.09 ( lam @ ( sub @ Bound_variable_3171 @ ( push @ one @ sh ) ) ) @ id ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_25 @ B @ Bound_variable_3171 @ P ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term ),Bound_variable_3149:term]:
% 138.51/18.09 ( zip_tseitin_39 @ Bound_variable_3149 @ F @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_72, type, zip_tseitin_39 :
% 138.51/18.09 term > ( subst > term > term ) > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_73, axiom,
% 138.51/18.09 (![Bound_variable_3149:term,F:( subst > term > term ),
% 138.51/18.09 P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_39 @ Bound_variable_3149 @ F @ P ) <=>
% 138.51/18.09 ( ( ~( ![Bound_variable_3090:subst,Bound_variable_3092:term,
% 138.51/18.09 Bound_variable_3094:subst]:
% 138.51/18.09 ( ( F @
% 138.51/18.09 ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) @
% 138.51/18.09 ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) ) =
% 138.51/18.09 ( sub @
% 138.51/18.09 Bound_variable_3149 @
% 138.51/18.09 ( push @
% 138.51/18.09 ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) @
% 138.51/18.09 ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) ) ) ) ) ) |
% 138.51/18.09 ( ~( ![Bound_variable_3072:subst,Bound_variable_3074:term,
% 138.51/18.09 Bound_variable_3076:subst]:
% 138.51/18.09 ( ( sub @
% 138.51/18.09 ( F @ Bound_variable_3072 @ Bound_variable_3074 ) @
% 138.51/18.09 Bound_variable_3076 ) =
% 138.51/18.09 ( sub @
% 138.51/18.09 ( sub @
% 138.51/18.09 Bound_variable_3149 @
% 138.51/18.09 ( push @ Bound_variable_3074 @ Bound_variable_3072 ) ) @
% 138.51/18.09 Bound_variable_3076 ) ) ) ) |
% 138.51/18.09 ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_23 @ A @ F @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_74, type, zip_tseitin_38 :
% 138.51/18.09 term > subst > ( subst > term > term ) > ( subst > term > term ) > $o).
% 138.51/18.09 thf(zf_stmt_75, axiom,
% 138.51/18.09 (![Bound_variable_2551:term,Bound_variable_2549:subst,
% 138.51/18.09 Bound_variable_2547:( subst > term > term ),F:( subst > term > term )]:
% 138.51/18.09 ( ( zip_tseitin_38 @
% 138.51/18.09 Bound_variable_2551 @ Bound_variable_2549 @ Bound_variable_2547 @ F ) <=>
% 138.51/18.09 ( ( ( F @ Bound_variable_2549 @ Bound_variable_2551 ) =
% 138.51/18.09 ( Bound_variable_2547 @ Bound_variable_2549 @ Bound_variable_2551 ) ) |
% 138.51/18.09 ( ( lam @ ( F @ sh @ one ) ) !=
% 138.51/18.09 ( lam @ ( Bound_variable_2547 @ sh @ one ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( Bound_variable_2547 @ M @ A ) @ N ) =
% 138.51/18.09 ( Bound_variable_2547 @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_76, type, zip_tseitin_37 : $o).
% 138.51/18.09 thf(zf_stmt_77, axiom,
% 138.51/18.09 (( zip_tseitin_37 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_36 ) ))).thf(zf_stmt_78, type, zip_tseitin_36 : $o).
% 138.51/18.09 thf(zf_stmt_79, axiom,
% 138.51/18.09 (( zip_tseitin_36 ) <=>
% 138.51/18.09 ( ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( zip_tseitin_18 @ Bound_variable_2367 @ P ) ) =>
% 138.51/18.09 ( zip_tseitin_35 ) ))).thf(zf_stmt_80, type, zip_tseitin_35 : $o).
% 138.51/18.09 thf(zf_stmt_81, axiom,
% 138.51/18.09 (( zip_tseitin_35 ) <=>
% 138.51/18.09 ( ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) => ( zip_tseitin_34 ) ))).
% 138.51/18.09 thf(zf_stmt_82, type, zip_tseitin_34 : $o).
% 138.51/18.09 thf(zf_stmt_83, axiom,
% 138.51/18.09 (( zip_tseitin_34 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2931:term]:
% 138.51/18.09 ( zip_tseitin_32 @ Bound_variable_2931 @ Q @ P ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3295:term]:
% 138.51/18.09 ( zip_tseitin_33 @ Bound_variable_3295 @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_84, type, zip_tseitin_33 :
% 138.51/18.09 term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_85, axiom,
% 138.51/18.09 (![Bound_variable_3295:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_33 @ Bound_variable_3295 @ P ) <=>
% 138.51/18.09 ( ( P @ id @ Bound_variable_3295 @ id ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]: ( zip_tseitin_24 @ F @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]: ( zip_tseitin_21 @ B @ A @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_86, type, zip_tseitin_32 :
% 138.51/18.09 term > ( term > $o ) > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_87, axiom,
% 138.51/18.09 (![Bound_variable_2931:term,Q:( term > $o ),P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_32 @ Bound_variable_2931 @ Q @ P ) <=>
% 138.51/18.09 ( ( Q @ ( lam @ Bound_variable_2931 ) ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_5 @ B @ Bound_variable_2931 @ Q ) ) ) |
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]: ( zip_tseitin_24 @ F @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_88, type, zip_tseitin_31 : $o).
% 138.51/18.09 thf(zf_stmt_89, axiom,
% 138.51/18.09 (( zip_tseitin_31 ) <=>
% 138.51/18.09 ( ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( zip_tseitin_18 @ Bound_variable_2367 @ P ) ) =>
% 138.51/18.09 ( zip_tseitin_30 ) ))).thf(zf_stmt_90, type, zip_tseitin_30 : $o).
% 138.51/18.09 thf(zf_stmt_91, axiom,
% 138.51/18.09 (( zip_tseitin_30 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Bound_variable_2999:term,
% 138.51/18.09 Bound_variable_3001:term]:
% 138.51/18.09 ( zip_tseitin_22 @ Bound_variable_3001 @ Bound_variable_2999 @ P ) ) =>
% 138.51/18.09 ( zip_tseitin_29 ) ))).thf(zf_stmt_92, type, zip_tseitin_29 : $o).
% 138.51/18.09 thf(zf_stmt_93, axiom,
% 138.51/18.09 (( zip_tseitin_29 ) <=>
% 138.51/18.09 ( ( ![P:( subst > term > subst > $o ),Bound_variable_3211:term]:
% 138.51/18.09 ( zip_tseitin_26 @ Bound_variable_3211 @ P ) ) =>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3283:term]:
% 138.51/18.09 ( zip_tseitin_28 @ Bound_variable_3283 @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_94, type, zip_tseitin_28 :
% 138.51/18.09 term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_95, axiom,
% 138.51/18.09 (![Bound_variable_3283:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_28 @ Bound_variable_3283 @ P ) <=>
% 138.51/18.09 ( ( P @ id @ Bound_variable_3283 @ id ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]: ( zip_tseitin_24 @ F @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]: ( zip_tseitin_21 @ B @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_27 @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_20 @ K @ N @ A @ M @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_19 @ K @ N @ A @ M @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_96, type, zip_tseitin_27 :
% 138.51/18.09 term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_97, axiom,
% 138.51/18.09 (![A:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_27 @ A @ P ) <=>
% 138.51/18.09 ( ( P @ id @ A @ id ) | ( ~( var @ ( sub @ A @ id ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_98, type, zip_tseitin_26 :
% 138.51/18.09 term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_99, axiom,
% 138.51/18.09 (![Bound_variable_3211:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_26 @ Bound_variable_3211 @ P ) <=>
% 138.51/18.09 ( ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_25 @ B @ Bound_variable_3211 @ P ) ) ) |
% 138.51/18.09 ( ~( ![F:( subst > term > term )]: ( zip_tseitin_24 @ F @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_20 @ K @ N @ A @ M @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_19 @ K @ N @ A @ M @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_100, type, zip_tseitin_25 :
% 138.51/18.09 term > term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_101, axiom,
% 138.51/18.09 (![B:term,Bound_variable_3211:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_25 @ B @ Bound_variable_3211 @ P ) <=>
% 138.51/18.09 ( ( P @ id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) |
% 138.51/18.09 ( ~( P @ id @ B @ id ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_102, type, zip_tseitin_24 :
% 138.51/18.09 ( subst > term > term ) > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_103, axiom,
% 138.51/18.09 (![F:( subst > term > term ),P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_24 @ F @ P ) <=>
% 138.51/18.09 ( ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_23 @ A @ F @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst]:
% 138.51/18.09 ( ( sub @ ( F @ M @ A ) @ N ) =
% 138.51/18.09 ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_104, type, zip_tseitin_23 :
% 138.51/18.09 term > ( subst > term > term ) > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_105, axiom,
% 138.51/18.09 (![A:term,F:( subst > term > term ),P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_23 @ A @ F @ P ) <=>
% 138.51/18.09 ( ( P @ id @ ( F @ id @ A ) @ id ) | ( ~( P @ id @ A @ id ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_106, type, zip_tseitin_22 :
% 138.51/18.09 term > term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_107, axiom,
% 138.51/18.09 (![Bound_variable_3001:term,Bound_variable_2999:term,
% 138.51/18.09 P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_22 @ Bound_variable_3001 @ Bound_variable_2999 @ P ) <=>
% 138.51/18.09 ( ( P @ id @ ( ap @ Bound_variable_2999 @ Bound_variable_3001 ) @ id ) |
% 138.51/18.09 ( ~( P @ id @ Bound_variable_3001 @ id ) ) |
% 138.51/18.09 ( ~( P @ id @ Bound_variable_2999 @ id ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]: ( zip_tseitin_21 @ B @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_20 @ K @ N @ A @ M @ P ) ) ) |
% 138.51/18.09 ( ~( ![M:subst,A:term,N:subst,K:subst]:
% 138.51/18.09 ( zip_tseitin_19 @ K @ N @ A @ M @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_108, type, zip_tseitin_21 :
% 138.51/18.09 term > term > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_109, axiom,
% 138.51/18.09 (![B:term,A:term,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_21 @ B @ A @ P ) <=>
% 138.51/18.09 ( ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) |
% 138.51/18.09 ( ~( P @ id @ B @ id ) ) | ( ~( P @ id @ A @ id ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_110, type, zip_tseitin_20 :
% 138.51/18.09 subst > subst > term > subst > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_111, axiom,
% 138.51/18.09 (![K:subst,N:subst,A:term,M:subst,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_20 @ K @ N @ A @ M @ P ) <=>
% 138.51/18.09 ( ( P @ M @ A @ ( comp @ K @ N ) ) |
% 138.51/18.09 ( ~( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_112, type, zip_tseitin_19 :
% 138.51/18.09 subst > subst > term > subst > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_113, axiom,
% 138.51/18.09 (![K:subst,N:subst,A:term,M:subst,P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_19 @ K @ N @ A @ M @ P ) <=>
% 138.51/18.09 ( ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) |
% 138.51/18.09 ( ~( P @ M @ A @ ( comp @ K @ N ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_114, type, zip_tseitin_18 : term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_115, axiom,
% 138.51/18.09 (![Bound_variable_2367:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_18 @ Bound_variable_2367 @ P ) <=>
% 138.51/18.09 ( ( P @ Bound_variable_2367 ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_6 @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]: ( zip_tseitin_4 @ B @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_11 @ A @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_116, type, zip_tseitin_17 : $o).
% 138.51/18.09 thf(zf_stmt_117, axiom,
% 138.51/18.09 (( zip_tseitin_17 ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_16 ) ))).thf(zf_stmt_118, type, zip_tseitin_16 : $o).
% 138.51/18.09 thf(zf_stmt_119, axiom,
% 138.51/18.09 (( zip_tseitin_16 ) <=>
% 138.51/18.09 ( ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) =>
% 138.51/18.09 ( zip_tseitin_15 ) ))).thf(zf_stmt_120, type, zip_tseitin_15 : $o).
% 138.51/18.09 thf(zf_stmt_121, axiom,
% 138.51/18.09 (( zip_tseitin_15 ) <=>
% 138.51/18.09 ( ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) => ( zip_tseitin_14 ) ))).
% 138.51/18.09 thf(zf_stmt_122, type, zip_tseitin_14 : $o).
% 138.51/18.09 thf(zf_stmt_123, axiom,
% 138.51/18.09 (( zip_tseitin_14 ) <=>
% 138.51/18.09 ( ( ![P:( term > $o ),Bound_variable_2140:term]:
% 138.51/18.09 ( zip_tseitin_13 @ Bound_variable_2140 @ P ) ) =>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2340:term,Bound_variable_2342:subst]:
% 138.51/18.09 ( zip_tseitin_8 @ Bound_variable_2342 @ Bound_variable_2340 @ P ) ) ))).
% 138.51/18.09 thf(zf_stmt_124, type, zip_tseitin_13 : term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_125, axiom,
% 138.51/18.09 (![Bound_variable_2140:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_13 @ Bound_variable_2140 @ P ) <=>
% 138.51/18.09 ( ( P @ Bound_variable_2140 ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_12 @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]: ( zip_tseitin_4 @ B @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_11 @ A @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_126, type, zip_tseitin_12 : term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_127, axiom,
% 138.51/18.09 (![A:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_12 @ A @ P ) <=> ( ( P @ ( lam @ A ) ) | ( ~( P @ A ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_128, type, zip_tseitin_11 : term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_129, axiom,
% 138.51/18.09 (![A:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_11 @ A @ P ) <=> ( ( P @ A ) | ( ~( var @ A ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_130, type, zip_tseitin_10 : term > term > term > term > $o).
% 138.51/18.09 thf(zf_stmt_131, axiom,
% 138.51/18.09 (![D:term,C:term,B:term,A:term]:
% 138.51/18.09 ( ( zip_tseitin_10 @ D @ C @ B @ A ) <=>
% 138.51/18.09 ( ( ( A ) = ( B ) ) |
% 138.51/18.09 ( ( ap @ ( sub @ A @ id ) @ C ) != ( ap @ ( sub @ B @ id ) @ D ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_132, type, zip_tseitin_9 : term > term > term > term > $o).
% 138.51/18.09 thf(zf_stmt_133, axiom,
% 138.51/18.09 (![D:term,C:term,B:term,A:term]:
% 138.51/18.09 ( ( zip_tseitin_9 @ D @ C @ B @ A ) <=>
% 138.51/18.09 ( ( ( C ) = ( D ) ) |
% 138.51/18.09 ( ( ap @ ( sub @ A @ id ) @ C ) != ( ap @ ( sub @ B @ id ) @ D ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_134, type, zip_tseitin_8 : subst > term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_135, axiom,
% 138.51/18.09 (![Bound_variable_2342:subst,Bound_variable_2340:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_8 @ Bound_variable_2342 @ Bound_variable_2340 @ P ) <=>
% 138.51/18.09 ( ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_7 @ B @ Bound_variable_2342 @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term]: ( zip_tseitin_6 @ A @ P ) ) ) |
% 138.51/18.09 ( ~( ![A:term,B:term]: ( zip_tseitin_4 @ B @ A @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_136, type, zip_tseitin_7 : term > subst > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_137, axiom,
% 138.51/18.09 (![B:term,Bound_variable_2342:subst,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_7 @ B @ Bound_variable_2342 @ P ) <=>
% 138.51/18.09 ( ( P @ ( sub @ B @ Bound_variable_2342 ) ) | ( ~( var @ B ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_138, type, zip_tseitin_6 : term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_139, axiom,
% 138.51/18.09 (![A:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_6 @ A @ P ) <=>
% 138.51/18.09 ( ( P @ ( lam @ A ) ) |
% 138.51/18.09 ( ~( ![B:term]: ( zip_tseitin_5 @ B @ A @ P ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_140, type, zip_tseitin_5 : term > term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_141, axiom,
% 138.51/18.09 (![B:term,A:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_5 @ B @ A @ P ) <=>
% 138.51/18.09 ( ( P @ ( sub @ A @ ( push @ B @ id ) ) ) | ( ~( P @ B ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_142, type, zip_tseitin_4 : term > term > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_143, axiom,
% 138.51/18.09 (![B:term,A:term,P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_4 @ B @ A @ P ) <=>
% 138.51/18.09 ( ( P @ ( ap @ A @ B ) ) | ( ~( P @ B ) ) | ( ~( P @ A ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_144, type, zip_tseitin_3 : term > term > $o).
% 138.51/18.09 thf(zf_stmt_145, axiom,
% 138.51/18.09 (![B:term,A:term]:
% 138.51/18.09 ( ( zip_tseitin_3 @ B @ A ) <=>
% 138.51/18.09 ( ( ( A ) = ( B ) ) | ( ( sub @ A @ sh ) != ( sub @ B @ sh ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_146, type, zip_tseitin_2 :
% 138.51/18.09 subst > term > ( term > $o ) > ( term > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_147, axiom,
% 138.51/18.09 (![M:subst,A:term,Q:( term > $o ),P:( term > $o )]:
% 138.51/18.09 ( ( zip_tseitin_2 @ M @ A @ Q @ P ) <=>
% 138.51/18.09 ( ( Q @ one ) |
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_1 @ X @ Q @ P @ M @ A ) ) ) |
% 138.51/18.09 ( ~( P @ A ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_148, type, zip_tseitin_1 :
% 138.51/18.09 term > ( term > $o ) > ( term > $o ) > subst > term > $o).
% 138.51/18.09 thf(zf_stmt_149, axiom,
% 138.51/18.09 (![X:term,Q:( term > $o ),P:( term > $o ),M:subst,A:term]:
% 138.51/18.09 ( ( zip_tseitin_1 @ X @ Q @ P @ M @ A ) <=>
% 138.51/18.09 ( ( Q @ X ) <=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ))).
% 138.51/18.09 thf(zf_stmt_150, type, zip_tseitin_0 :
% 138.51/18.09 term > ( term > $o ) > ( subst > term > subst > $o ) > $o).
% 138.51/18.09 thf(zf_stmt_151, axiom,
% 138.51/18.09 (![X:term,Q:( term > $o ),P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ( zip_tseitin_0 @ X @ Q @ P ) <=> ( ( Q @ X ) <=> ( P @ id @ X @ id ) ) ))).
% 138.51/18.09 thf(zf_stmt_152, axiom,
% 138.51/18.09 (( ( hoasinduction_lthm_3 ) <=> ( zip_tseitin_75 ) ) &
% 138.51/18.09 ( ( axvarid ) <=> ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2_lthm ) <=> ( zip_tseitin_71 ) ) &
% 138.51/18.09 ( hoasapnotvar_lthm ) &
% 138.51/18.09 ( ( pushprop_lem0_lthm ) <=>
% 138.51/18.09 ( ![P:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_1 @ X @ Q @ P @ M @ A ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( termmset ) <=> ( ![A:term]: ( ( A ) = ( sub @ A @ id ) ) ) ) &
% 138.51/18.09 ( ( axshiftcons ) <=>
% 138.51/18.09 ( ![A:term,M:subst]: ( ( M ) = ( comp @ sh @ ( push @ A @ M ) ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2910:term]:
% 138.51/18.09 ( zip_tseitin_70 @ Bound_variable_2910 @ Q @ P ) ) ) &
% 138.51/18.09 ( ( pushprop_lem1_lthm ) <=> ( zip_tseitin_69 ) ) &
% 138.51/18.09 ( pushprop_lem2v2_gthm ) & ( pushprop_lem3v2 ) &
% 138.51/18.09 ( ( induction2 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2367:term]:
% 138.51/18.09 ( zip_tseitin_18 @ Bound_variable_2367 @ P ) ) ) &
% 138.51/18.09 ( ulamvarsh ) & ( substmonoid_gthm ) &
% 138.51/18.09 ( ( hoaslamnotap ) <=>
% 138.51/18.09 ( ![F:( subst > term > term ),Bound_variable_2603:term,
% 138.51/18.09 Bound_variable_2605:term]:
% 138.51/18.09 ( zip_tseitin_67 @ Bound_variable_2605 @ Bound_variable_2603 @ F ) ) ) &
% 138.51/18.09 ( ~( hoasvar @
% 138.51/18.09 ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) ) &
% 138.51/18.09 ( pushprop_lem2v2_lthm ) & ( induction2_gthm ) &
% 138.51/18.09 ( ( hoasinduction_no_psi_cond ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3295:term]:
% 138.51/18.09 ( zip_tseitin_33 @ Bound_variable_3295 @ P ) ) ) &
% 138.51/18.09 ( hoasinduction_lem1_gthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3a ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3232:term]:
% 138.51/18.09 ( zip_tseitin_44 @ Bound_variable_3232 @ P ) ) ) &
% 138.51/18.09 ( lamnotvar ) & ( ( substmonoid ) <=> ( zip_tseitin_64 ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3b ) <=>
% 138.51/18.09 ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( F @ sh @ one ) != ( sub @ B @ ( push @ one @ sh ) ) ) ) ) ) ) &
% 138.51/18.09 ( hoasinduction_lem2_gthm ) & ( hoasinduction_lem3_gthm ) &
% 138.51/18.09 ( pushprop ) & ( ( substmonoid_lthm ) <=> ( zip_tseitin_66 ) ) &
% 138.51/18.09 ( ( hoasinduction_lem0_lthm ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( induction2_lthm ) <=> ( zip_tseitin_63 ) ) & ( hoaslaminj_gthm ) &
% 138.51/18.09 ( ( axidl ) <=> ( ![M:subst]: ( ( M ) = ( comp @ id @ M ) ) ) ) &
% 138.51/18.09 ( hoaslamnotvar ) & ( hoasapinj1_gthm ) & ( ~( lamnotap ) ) &
% 138.51/18.09 ( hoasinduction_lem1_lthm ) & ( hoasapinj2_gthm ) &
% 138.51/18.09 ( hoasinduction_lem2_lthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2a_lthm ) <=> ( zip_tseitin_61 ) ) & ( axabs ) &
% 138.51/18.09 ( pushprop_gthm ) &
% 138.51/18.09 ( ( pushprop_lem0 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_1 @ X @ Q @ P @ M @ A ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3_lthm ) <=> ( zip_tseitin_59 ) ) &
% 138.51/18.09 ( ( laminj ) <=> ( ![A:term,B:term]: ( zip_tseitin_53 @ B @ A ) ) ) &
% 138.51/18.09 ( ( pushprop_lem1 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),K:( term > $o ),A:term,M:subst,B:term]:
% 138.51/18.09 ( zip_tseitin_57 @ B @ M @ A @ K @ P ) ) ) &
% 138.51/18.09 ( ( axidr ) <=> ( ![M:subst]: ( ( M ) = ( comp @ M @ id ) ) ) ) &
% 138.51/18.09 ( hoasinduction_lem2v2_gthm ) &
% 138.51/18.09 ( ( axscons ) <=>
% 138.51/18.09 ( ![M:subst]:
% 138.51/18.09 ( ( M ) = ( push @ ( sub @ one @ M ) @ ( comp @ sh @ M ) ) ) ) ) &
% 138.51/18.09 ( ( axvarcons ) <=>
% 138.51/18.09 ( ![A:term,M:subst]: ( ( A ) = ( sub @ one @ ( push @ A @ M ) ) ) ) ) &
% 138.51/18.09 ( ( hoaslaminj_lthm ) <=> ( zip_tseitin_56 ) ) &
% 138.51/18.09 ( ( hoasapinj1_lthm ) <=> ( zip_tseitin_52 ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2a ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2931:term]:
% 138.51/18.09 ( zip_tseitin_32 @ Bound_variable_2931 @ Q @ P ) ) ) &
% 138.51/18.09 ( ( hoasapinj2_lthm ) <=> ( zip_tseitin_50 ) ) &
% 138.51/18.09 ( ( apinj1 ) <=>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_49 @ D @ C @ B @ A ) ) ) &
% 138.51/18.09 ( ( apinj2 ) <=>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_48 @ D @ C @ B @ A ) ) ) &
% 138.51/18.09 ( pushprop_lthm ) &
% 138.51/18.09 ( ( hoasinduction_lem2v2 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o ),
% 138.51/18.09 Bound_variable_2820:term,Bound_variable_2822:term]:
% 138.51/18.09 ( zip_tseitin_47 @ Bound_variable_2822 @ Bound_variable_2820 @ Q @ P ) ) ) &
% 138.51/18.09 ( axassoc ) & ( axclos ) & ( hoasinduction_lem3a_gthm ) &
% 138.51/18.09 ( pushprop_lem2v2 ) & ( hoasinduction_lem3b_gthm ) &
% 138.51/18.09 ( hoaslamnotvar_gthm ) & ( hoaslamnotap_gthm ) &
% 138.51/18.09 ( pushprop_lem1v2_gthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3aa ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( zip_tseitin_41 @ Bound_variable_3046 @ P ) ) ) &
% 138.51/18.09 ( termmset_gthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3a_lthm ) <=> ( zip_tseitin_46 ) ) &
% 138.51/18.09 ( ( induction ) <=>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2140:term]:
% 138.51/18.09 ( zip_tseitin_13 @ Bound_variable_2140 @ P ) ) ) &
% 138.51/18.09 ( ulamvarind ) &
% 138.51/18.09 ( ( hoasinduction_lem3b_lthm ) <=>
% 138.51/18.09 ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ( F @ sh @ one ) != ( sub @ B @ ( push @ one @ sh ) ) ) ) ) ) ) &
% 138.51/18.09 ( pushprop_lem3v2_lthm ) & ( hoaslamnotvar_lthm ) & ( axapp ) &
% 138.51/18.09 ( hoasinduction_gthm ) &
% 138.51/18.09 ( ( hoasinduction ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3283:term]:
% 138.51/18.09 ( zip_tseitin_28 @ Bound_variable_3283 @ P ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem0 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o )]:
% 138.51/18.09 ( ~( ![Q:( term > $o )]:
% 138.51/18.09 ( ~( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) ) ) ) ) &
% 138.51/18.09 ( hoasapnotvar ) & ( ( pushprop_lem1v2_lthm ) <=> ( zip_tseitin_43 ) ) &
% 138.51/18.09 ( hoaslamnotap_lthm ) & ( hoasinduction_lem1 ) &
% 138.51/18.09 ( ( termmset_lthm ) <=> ( zip_tseitin_42 ) ) &
% 138.51/18.09 ( ( hoasinduction_lem2 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_2999:term,
% 138.51/18.09 Bound_variable_3001:term]:
% 138.51/18.09 ( zip_tseitin_22 @ Bound_variable_3001 @ Bound_variable_2999 @ P ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3 ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3211:term]:
% 138.51/18.09 ( zip_tseitin_26 @ Bound_variable_3211 @ P ) ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3aa_lthm ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3046:term]:
% 138.51/18.09 ( zip_tseitin_41 @ Bound_variable_3046 @ P ) ) ) &
% 138.51/18.09 ( induction2lem_gthm ) &
% 138.51/18.09 ( ( hoasinduction_lem3aaa ) <=>
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Bound_variable_3171:term]:
% 138.51/18.09 ( zip_tseitin_40 @ Bound_variable_3171 @ P ) ) ) &
% 138.51/18.09 ( ( hoaslaminj ) <=>
% 138.51/18.09 ( ![F:( subst > term > term ),
% 138.51/18.09 Bound_variable_2547:( subst > term > term ),
% 138.51/18.09 Bound_variable_2549:subst,Bound_variable_2551:term]:
% 138.51/18.09 ( zip_tseitin_38 @
% 138.51/18.09 Bound_variable_2551 @ Bound_variable_2549 @ Bound_variable_2547 @ F ) ) ) &
% 138.51/18.09 ( ( hoasinduction_no_psi_cond_lthm ) <=> ( zip_tseitin_37 ) ) &
% 138.51/18.09 ( ( hoasinduction_lthm ) <=> ( zip_tseitin_31 ) ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2_f_lthm ) <=>
% 138.51/18.09 ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ~( ![A:term,M:subst]:
% 138.51/18.09 ( ( sub @ B @ ( push @ A @ M ) ) = ( F @ M @ A ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( pushprop_lthm_orig ) & ( apnotvar ) & ( hoasinduction_lem3v2_gthm ) &
% 138.51/18.09 ( ( induction2lem_lthm ) <=> ( zip_tseitin_17 ) ) & ( ~( ulamvar1 ) ) &
% 138.51/18.09 ( ( hoasapinj1 ) <=>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_10 @ D @ C @ B @ A ) ) ) &
% 138.51/18.09 ( hoasapnotvar_gthm ) &
% 138.51/18.09 ( ( hoasapinj2 ) <=>
% 138.51/18.09 ( ![A:term,B:term,C:term,D:term]: ( zip_tseitin_9 @ D @ C @ B @ A ) ) ) &
% 138.51/18.09 ( axvarshift ) &
% 138.51/18.09 ( ( hoasinduction_lem3v2_f ) <=>
% 138.51/18.09 ( ![B:term]:
% 138.51/18.09 ( ~( ![F:( subst > term > term )]:
% 138.51/18.09 ( ~( ![A:term,M:subst]:
% 138.51/18.09 ( ( sub @ B @ ( push @ A @ M ) ) = ( F @ M @ A ) ) ) ) ) ) ) ) &
% 138.51/18.09 ( ( induction2lem ) <=>
% 138.51/18.09 ( ![P:( term > $o ),Bound_variable_2340:term,Bound_variable_2342:subst]:
% 138.51/18.09 ( zip_tseitin_8 @ Bound_variable_2342 @ Bound_variable_2340 @ P ) ) ) &
% 138.51/18.09 ( hoasinduction_lem1v2_gthm ) & ( hoasinduction_lem1v2 ) &
% 138.51/18.09 ( ( shinj ) <=> ( ![A:term,B:term]: ( zip_tseitin_3 @ B @ A ) ) ) &
% 138.51/18.09 ( pushprop_lem0_gthm ) & ( axmap ) & ( pushprop_lem1_gthm ) &
% 138.51/18.09 ( ( pushprop_lem1v2 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),Q:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( zip_tseitin_2 @ M @ A @ Q @ P ) ) ) &
% 138.51/18.09 ( ~( var @ ( d2term @ d_one ) ) ) &
% 138.51/18.09 ( ![A:term,M:subst,P:( term > $o ),Q:( term > $o )]:
% 138.51/18.09 ( ( pushprop_p_and_p_prime @ A @ M @ P @ Q ) <=>
% 138.51/18.09 ( ![X:term]: ( zip_tseitin_1 @ X @ Q @ P @ M @ A ) ) ) ) &
% 138.51/18.09 ( ![P:( subst > term > subst > $o ),Q:( term > $o )]:
% 138.51/18.09 ( ( hoasinduction_p_and_p_prime @ P @ Q ) <=>
% 138.51/18.09 ( ![X:term]: ( zip_tseitin_0 @ X @ Q @ P ) ) ) ) &
% 138.51/18.09 ( ![Bound_variable_4913:subst,Bound_variable_4915:( subst > term > term )]:
% 138.51/18.09 ( ( hoaslam @ Bound_variable_4913 @ Bound_variable_4915 ) =
% 138.51/18.09 ( d2term @ d_one ) ) ) &
% 138.51/18.09 ( ( hoasap @
% 138.51/18.09 ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) @
% 138.51/18.09 ( d2term @ d_one ) ) =
% 138.51/18.09 ( d2term @ d_one ) ) &
% 138.51/18.09 ( ( comp @ ( d2subst @ d_id ) @ ( d2subst @ d_id ) ) = ( d2subst @ d_id ) ) &
% 138.51/18.09 ( ( push @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) = ( d2subst @ d_id ) ) &
% 138.51/18.09 ( ( sh ) = ( d2subst @ d_id ) ) & ( ( id ) = ( d2subst @ d_id ) ) &
% 138.51/18.09 ( ( sub @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) = ( d2term @ d_one ) ) &
% 138.51/18.09 ( ( lam @ ( d2term @ d_one ) ) = ( d2term @ d_one ) ) &
% 138.51/18.09 ( ( ap @ ( d2term @ d_one ) @ ( d2term @ d_one ) ) = ( d2term @ d_one ) ) &
% 138.51/18.09 ( ( one ) = ( d2term @ d_one ) ) &
% 138.51/18.09 ( ![DS1:d_subst,DS2:d_subst]:
% 138.51/18.09 ( ( ( d2subst @ DS1 ) = ( d2subst @ DS2 ) ) => ( ( DS1 ) = ( DS2 ) ) ) ) &
% 138.51/18.09 ( ![DS:d_subst]: ( ( DS ) = ( d_id ) ) ) &
% 138.51/18.09 ( ![S:subst]: ( ?[DS:d_subst]: ( ( S ) = ( d2subst @ DS ) ) ) ) &
% 138.51/18.09 ( ![DT1:d_term,DT2:d_term]:
% 138.51/18.09 ( ( ( d2term @ DT1 ) = ( d2term @ DT2 ) ) => ( ( DT1 ) = ( DT2 ) ) ) ) &
% 138.51/18.09 ( ![DT:d_term]: ( ( DT ) = ( d_one ) ) ) &
% 138.51/18.09 ( ![T:term]: ( ?[DT:d_term]: ( ( T ) = ( d2term @ DT ) ) ) ))).
% 138.51/18.09 thf(zip_derived_cl288, plain,
% 138.51/18.09 (![X0 : term, X1 : subst, X2 : term > $o, X3 : term > $o]:
% 138.51/18.09 ( (pushprop_p_and_p_prime @ X0 @ X1 @ X2 @ X3)
% 138.51/18.09 | ~ (zip_tseitin_1 @ (sk__325 @ X3 @ X2 @ X1 @ X0) @ X3 @ X2 @ X1 @
% 138.51/18.09 X0))),
% 138.51/18.09 inference('cnf', [status(esa)], [zf_stmt_152])).
% 138.51/18.09 thf(pushprop_lem0, conjecture,
% 138.51/18.09 (( pushprop_lem0 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( ?[Q:( term > $o )]: ( pushprop_p_and_p_prime @ A @ M @ P @ Q ) ) ))).
% 138.51/18.09 thf(zf_stmt_153, negated_conjecture,
% 138.51/18.09 (~( ( pushprop_lem0 ) <=>
% 138.51/18.09 ( ![P:( term > $o ),A:term,M:subst]:
% 138.51/18.09 ( ?[Q:( term > $o )]: ( pushprop_p_and_p_prime @ A @ M @ P @ Q ) ) ) )),
% 138.51/18.09 inference('cnf.neg', [status(esa)], [pushprop_lem0])).
% 138.51/18.09 thf(zip_derived_cl457, plain,
% 138.51/18.09 (![X3 : term > $o]:
% 138.51/18.09 (~ (pushprop_p_and_p_prime @ sk__330 @ sk__331 @ sk__329 @ X3)
% 138.51/18.09 | ~ (pushprop_lem0))),
% 138.51/18.09 inference('cnf', [status(esa)], [zf_stmt_153])).
% 138.51/18.09 thf(zip_derived_cl456, plain,
% 138.51/18.09 (![X0 : term, X1 : subst, X2 : term > $o]:
% 138.51/18.09 ( (pushprop_p_and_p_prime @ X0 @ X1 @ X2 @ (sk__332 @ X1 @ X0 @ X2))
% 138.51/18.09 | (pushprop_lem0))),
% 138.51/18.09 inference('cnf', [status(esa)], [zf_stmt_153])).
% 138.51/18.09 thf(zip_derived_cl395, plain,
% 138.51/18.09 (![X0 : term, X1 : subst, X2 : term, X3 : term > $o]:
% 138.51/18.09 ( (zip_tseitin_1 @ X0 @ (sk__245 @ X1 @ X2 @ X3) @ X3 @ X1 @ X2)
% 138.51/18.09 | ~ (pushprop_lem0))),
% 138.51/18.09 inference('cnf', [status(esa)], [zf_stmt_152])).
% 138.51/18.09 thf(zip_derived_cl289, plain,
% 138.51/18.09 (![X0 : term, X1 : term > $o, X2 : term > $o, X3 : subst, X4 : term]:
% 138.51/18.09 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3 @ X4)
% 138.51/18.09 | ~ (pushprop_p_and_p_prime @ X4 @ X3 @ X2 @ X1))),
% 138.51/18.09 inference('cnf', [status(esa)], [zf_stmt_152])).
% 138.51/18.09 thf(zip_derived_cl394, plain,
% 138.51/18.09 (![X0 : term > $o]:
% 138.51/18.09 ( (pushprop_lem0)
% 138.51/18.09 | ~ (zip_tseitin_1 @ (sk__249 @ X0) @ X0 @ sk__246 @ sk__248 @
% 138.51/18.09 sk__247))),
% 138.51/18.09 inference('cnf', [status(esa)], [zf_stmt_152])).
% 138.51/18.09 thf(zip_derived_cl8614, plain, ($false),
% 138.51/18.09 inference('eprover', [status(thm)],
% 138.51/18.09 [zip_derived_cl288, zip_derived_cl457, zip_derived_cl456,
% 138.51/18.09 zip_derived_cl395, zip_derived_cl289, zip_derived_cl394])).
% 138.51/18.09
% 138.51/18.09 % SZS output end Refutation
% 138.51/18.09
% 138.51/18.09
% 138.51/18.09 % Terminating...
% 18.78/18.22 % Runner terminated.
% 18.78/18.25 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------