%------------------------------------------------------------------------------
% 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.oCcQSEFHhv true
% Computer : n013.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 50.14s 7.36s
% Output : Refutation 50.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 2
% Syntax : Number of formulae : 68 ( 30 unt; 0 typ; 0 def)
% Number of atoms : 2625 ( 356 equ; 648 cnn)
% Maximal formula atoms : 1090 ( 38 avg)
% Number of connectives : 11041 (1058 ~; 963 |; 387 &;7136 @)
% ( 236 <=>; 130 =>; 0 <=; 0 <~>)
% Maximal formula depth : 155 ( 13 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 593 ( 593 >; 0 *; 0 +; 0 <<)
% Number of symbols : 140 ( 135 usr; 121 con; 0-4 aty)
% (1125 !!; 6 ??; 0 @@+; 0 @@-)
% Number of variables : 1773 (1167 ^; 604 !; 2 ?;1773 :)
% Comments :
%------------------------------------------------------------------------------
thf(term_type,type,
term: $tType ).
thf(subst_type,type,
subst: $tType ).
thf(d_subst_type,type,
d_subst: $tType ).
thf(d_term_type,type,
d_term: $tType ).
thf(axmap_type,type,
axmap: $o ).
thf(hoasinduction_lem3a_type,type,
hoasinduction_lem3a: $o ).
thf(hoasapnotvar_gthm_type,type,
hoasapnotvar_gthm: $o ).
thf(pushprop_lthm_orig_type,type,
pushprop_lthm_orig: $o ).
thf(termmset_gthm_type,type,
termmset_gthm: $o ).
thf(axclos_type,type,
axclos: $o ).
thf(lam_type,type,
lam: term > term ).
thf(lamnotap_type,type,
lamnotap: $o ).
thf(hoasinduction_lem3aa_type,type,
hoasinduction_lem3aa: $o ).
thf('#sk10494_type',type,
'#sk10494': term ).
thf(hoaslamnotvar_gthm_type,type,
hoaslamnotvar_gthm: $o ).
thf(axvarcons_type,type,
axvarcons: $o ).
thf(hoaslamnotvar_lthm_type,type,
hoaslamnotvar_lthm: $o ).
thf(d2term_type,type,
d2term: d_term > term ).
thf(hoasinduction_no_psi_cond_lthm_type,type,
hoasinduction_no_psi_cond_lthm: $o ).
thf(substmonoid_type,type,
substmonoid: $o ).
thf(hoasinduction_lem3a_gthm_type,type,
hoasinduction_lem3a_gthm: $o ).
thf(substmonoid_gthm_type,type,
substmonoid_gthm: $o ).
thf(d_id_type,type,
d_id: d_subst ).
thf(pushprop_gthm_type,type,
pushprop_gthm: $o ).
thf(hoasinduction_lem3v2_type,type,
hoasinduction_lem3v2: $o ).
thf(pushprop_lem1v2_type,type,
pushprop_lem1v2: $o ).
thf(push_type,type,
push: term > subst > subst ).
thf('#sk3141_type',type,
'#sk3141': subst ).
thf('#sk3138_type',type,
'#sk3138': term > $o ).
thf(hoaslamnotap_lthm_type,type,
hoaslamnotap_lthm: $o ).
thf('#sk1_type',type,
'#sk1': term > d_term ).
thf(axshiftcons_type,type,
axshiftcons: $o ).
thf(hoasinduction_lem1v2_type,type,
hoasinduction_lem1v2: $o ).
thf(hoasapinj1_lthm_type,type,
hoasapinj1_lthm: $o ).
thf(hoasapinj1_type,type,
hoasapinj1: $o ).
thf(hoasinduction_p_and_p_prime_type,type,
hoasinduction_p_and_p_prime: ( subst > term > subst > $o ) > ( term > $o ) > $o ).
thf(axapp_type,type,
axapp: $o ).
thf(hoasinduction_lem3_lthm_type,type,
hoasinduction_lem3_lthm: $o ).
thf(hoasinduction_lem3v2_lthm_type,type,
hoasinduction_lem3v2_lthm: $o ).
thf(pushprop_lem1v2_gthm_type,type,
pushprop_lem1v2_gthm: $o ).
thf(shinj_type,type,
shinj: $o ).
thf(hoasap_type,type,
hoasap: subst > term > subst > term > term ).
thf(hoasinduction_gthm_type,type,
hoasinduction_gthm: $o ).
thf(hoasinduction_lem3b_type,type,
hoasinduction_lem3b: $o ).
thf(hoaslaminj_type,type,
hoaslaminj: $o ).
thf(induction2_lthm_type,type,
induction2_lthm: $o ).
thf(induction2_gthm_type,type,
induction2_gthm: $o ).
thf(hoasinduction_lem2_gthm_type,type,
hoasinduction_lem2_gthm: $o ).
thf(one_type,type,
one: term ).
thf(pushprop_lem2v2_lthm_type,type,
pushprop_lem2v2_lthm: $o ).
thf(id_type,type,
id: subst ).
thf(comp_type,type,
comp: subst > subst > subst ).
thf(hoaslamnotap_type,type,
hoaslamnotap: $o ).
thf(induction2_type,type,
induction2: $o ).
thf(axvarid_type,type,
axvarid: $o ).
thf(axvarshift_type,type,
axvarshift: $o ).
thf(hoaslamnotap_gthm_type,type,
hoaslamnotap_gthm: $o ).
thf(induction2lem_type,type,
induction2lem: $o ).
thf(hoasinduction_lem1_gthm_type,type,
hoasinduction_lem1_gthm: $o ).
thf(sh_type,type,
sh: subst ).
thf(hoasinduction_lem2v2_type,type,
hoasinduction_lem2v2: $o ).
thf(laminj_type,type,
laminj: $o ).
thf(hoasinduction_lem3aa_lthm_type,type,
hoasinduction_lem3aa_lthm: $o ).
thf(ulamvarind_type,type,
ulamvarind: $o ).
thf(pushprop_lem2v2_type,type,
pushprop_lem2v2: $o ).
thf(hoasinduction_lthm_3_type,type,
hoasinduction_lthm_3: $o ).
thf(hoasinduction_lem3v2_f_lthm_type,type,
hoasinduction_lem3v2_f_lthm: $o ).
thf(apinj2_type,type,
apinj2: $o ).
thf(hoasapinj2_lthm_type,type,
hoasapinj2_lthm: $o ).
thf(ulamvarsh_type,type,
ulamvarsh: $o ).
thf(hoasinduction_lem3v2a_lthm_type,type,
hoasinduction_lem3v2a_lthm: $o ).
thf(hoasinduction_lem3a_lthm_type,type,
hoasinduction_lem3a_lthm: $o ).
thf(pushprop_lthm_type,type,
pushprop_lthm: $o ).
thf(hoasapinj1_gthm_type,type,
hoasapinj1_gthm: $o ).
thf('#sk10492_type',type,
'#sk10492': term > $o ).
thf(hoasinduction_lem0_lthm_type,type,
hoasinduction_lem0_lthm: $o ).
thf(hoasinduction_lem3b_lthm_type,type,
hoasinduction_lem3b_lthm: $o ).
thf(lamnotvar_type,type,
lamnotvar: $o ).
thf(apnotvar_type,type,
apnotvar: $o ).
thf(pushprop_p_and_p_prime_type,type,
pushprop_p_and_p_prime: term > subst > ( term > $o ) > ( term > $o ) > $o ).
thf(hoasapinj2_gthm_type,type,
hoasapinj2_gthm: $o ).
thf('#sk10495_type',type,
'#sk10495': subst ).
thf(d_one_type,type,
d_one: d_term ).
thf(pushprop_lem1_type,type,
pushprop_lem1: $o ).
thf(pushprop_type,type,
pushprop: $o ).
thf(hoasinduction_lem1_lthm_type,type,
hoasinduction_lem1_lthm: $o ).
thf(hoasinduction_lem3_gthm_type,type,
hoasinduction_lem3_gthm: $o ).
thf(sub_type,type,
sub: term > subst > term ).
thf(apinj1_type,type,
apinj1: $o ).
thf(axidl_type,type,
axidl: $o ).
thf(hoasinduction_type,type,
hoasinduction: $o ).
thf(ap_type,type,
ap: term > term > term ).
thf(termmset_type,type,
termmset: $o ).
thf(hoasapinj2_type,type,
hoasapinj2: $o ).
thf('#sk3139_type',type,
'#sk3139': term > $o ).
thf(hoasinduction_lem1_type,type,
hoasinduction_lem1: $o ).
thf(pushprop_lem3v2_lthm_type,type,
pushprop_lem3v2_lthm: $o ).
thf(hoasinduction_lem3v2a_type,type,
hoasinduction_lem3v2a: $o ).
thf(hoasapnotvar_type,type,
hoasapnotvar: $o ).
thf(var_type,type,
var: term > $o ).
thf(pushprop_lem1_lthm_type,type,
pushprop_lem1_lthm: $o ).
thf(induction2lem_lthm_type,type,
induction2lem_lthm: $o ).
thf(pushprop_lem0_lthm_type,type,
pushprop_lem0_lthm: $o ).
thf(axassoc_type,type,
axassoc: $o ).
thf(hoaslamnotvar_type,type,
hoaslamnotvar: $o ).
thf(hoaslam_type,type,
hoaslam: subst > ( subst > term > term ) > term ).
thf(hoasinduction_lem2_lthm_type,type,
hoasinduction_lem2_lthm: $o ).
thf(pushprop_lem3v2_type,type,
pushprop_lem3v2: $o ).
thf(hoasinduction_lem3b_gthm_type,type,
hoasinduction_lem3b_gthm: $o ).
thf(pushprop_lem0_type,type,
pushprop_lem0: $o ).
thf(hoaslaminj_gthm_type,type,
hoaslaminj_gthm: $o ).
thf(hoasinduction_lem3_type,type,
hoasinduction_lem3: $o ).
thf(hoasinduction_lem2_type,type,
hoasinduction_lem2: $o ).
thf(hoasinduction_lem0_type,type,
hoasinduction_lem0: $o ).
thf(hoaslaminj_lthm_type,type,
hoaslaminj_lthm: $o ).
thf(hoasinduction_lem3aaa_type,type,
hoasinduction_lem3aaa: $o ).
thf(axidr_type,type,
axidr: $o ).
thf(hoasapnotvar_lthm_type,type,
hoasapnotvar_lthm: $o ).
thf('#sk3140_type',type,
'#sk3140': term ).
thf(hoasinduction_lem3v2_f_type,type,
hoasinduction_lem3v2_f: $o ).
thf(pushprop_lem2v2_gthm_type,type,
pushprop_lem2v2_gthm: $o ).
thf(substmonoid_lthm_type,type,
substmonoid_lthm: $o ).
thf(axabs_type,type,
axabs: $o ).
thf(hoasinduction_lem3v2_gthm_type,type,
hoasinduction_lem3v2_gthm: $o ).
thf(hoasvar_type,type,
hoasvar: subst > term > subst > $o ).
thf(hoasinduction_lem2v2_gthm_type,type,
hoasinduction_lem2v2_gthm: $o ).
thf('#sk10493_type',type,
'#sk10493': term > $o ).
thf(ulamvar1_type,type,
ulamvar1: $o ).
thf(hoasinduction_lem1v2_gthm_type,type,
hoasinduction_lem1v2_gthm: $o ).
thf(induction_type,type,
induction: $o ).
thf(pushprop_lem1v2_lthm_type,type,
pushprop_lem1v2_lthm: $o ).
thf(axscons_type,type,
axscons: $o ).
thf(pushprop_lem1_gthm_type,type,
pushprop_lem1_gthm: $o ).
thf(induction2lem_gthm_type,type,
induction2lem_gthm: $o ).
thf(pushprop_lem0_gthm_type,type,
pushprop_lem0_gthm: $o ).
thf(termmset_lthm_type,type,
termmset_lthm: $o ).
thf(d2subst_type,type,
d2subst: d_subst > subst ).
thf(hoasinduction_lthm_type,type,
hoasinduction_lthm: $o ).
thf(hoasinduction_no_psi_cond_type,type,
hoasinduction_no_psi_cond: $o ).
thf(alg444_1,axiom,
( ! [T: term] :
? [DT: d_term] :
( T
= ( d2term @ DT ) )
& ! [DT: d_term] : ( DT = d_one )
& ! [DT1: d_term,DT2: d_term] :
( ( ( d2term @ DT1 )
= ( d2term @ DT2 ) )
=> ( DT1 = DT2 ) )
& ! [S: subst] :
? [DS: d_subst] :
( S
= ( d2subst @ DS ) )
& ! [DS: d_subst] : ( DS = d_id )
& ! [DS1: d_subst,DS2: d_subst] :
( ( ( d2subst @ DS1 )
= ( d2subst @ DS2 ) )
=> ( DS1 = DS2 ) )
& ( one
= ( d2term @ d_one ) )
& ( ( ap @ ( d2term @ d_one ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( lam @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( sub @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2term @ d_one ) )
& ( id
= ( d2subst @ d_id ) )
& ( sh
= ( d2subst @ d_id ) )
& ( ( push @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( comp @ ( d2subst @ d_id ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( hoasap @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( hoaslam
= ( ^ [Bound_variable_4913: subst,Bound_variable_4915: subst > term > term] : ( d2term @ d_one ) ) )
& ( hoasinduction_p_and_p_prime
= ( ^ [P: subst > term > subst > $o,Q: term > $o] :
! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) ) ) )
& ( pushprop_p_and_p_prime
= ( ^ [A: term,M: subst,P: term > $o,Q: term > $o] :
! [X: term] :
( ( Q @ X )
<=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ) )
& ~ ( var @ ( d2term @ d_one ) )
& ( pushprop_lem1v2
<=> ! [P: term > $o,Q: term > $o,A: term,M: subst] :
( ~ ( P @ A )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) )
| ( Q @ one ) ) )
& pushprop_lem1_gthm
& axmap
& pushprop_lem0_gthm
& ( shinj
<=> ! [A: term,B: term] :
( ( ( sub @ A @ sh )
!= ( sub @ B @ sh ) )
| ( A = B ) ) )
& hoasinduction_lem1v2
& hoasinduction_lem1v2_gthm
& ( induction2lem
<=> ! [P: term > $o,Bound_variable_2340: term,Bound_variable_2342: subst] :
( ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ~ ! [B: term] :
( ~ ( var @ B )
| ( P @ ( sub @ B @ Bound_variable_2342 ) ) )
| ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) ) )
& ( hoasinduction_lem3v2_f
<=> ! [B: term] :
~ ! [F: subst > term > term] :
~ ! [A: term,M: subst] :
( ( sub @ B @ ( push @ A @ M ) )
= ( F @ M @ A ) ) )
& axvarshift
& ( hoasapinj2
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( C = D ) ) )
& hoasapnotvar_gthm
& ( hoasapinj1
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( A = B ) ) )
& ~ ulamvar1
& ( induction2lem_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ( ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) )
=> ( ! [M: subst] :
( M
= ( comp @ M @ id ) )
=> ( ! [P: term > $o,Bound_variable_2140: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ( P @ A )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2140 ) )
=> ! [P: term > $o,Bound_variable_2340: term,Bound_variable_2342: subst] :
( ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ~ ! [B: term] :
( ~ ( var @ B )
| ( P @ ( sub @ B @ Bound_variable_2342 ) ) )
| ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) ) ) ) ) ) )
& hoasinduction_lem3v2_gthm
& apnotvar
& pushprop_lthm_orig
& ( hoasinduction_lem3v2_f_lthm
<=> ! [B: term] :
~ ! [F: subst > term > term] :
~ ! [A: term,M: subst] :
( ( sub @ B @ ( push @ A @ M ) )
= ( F @ M @ A ) ) )
& ( hoasinduction_lthm
<=> ( ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_2999: term,Bound_variable_3001: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ( P @ id @ Bound_variable_2999 @ id )
| ~ ( P @ id @ Bound_variable_3001 @ id )
| ( P @ id @ ( ap @ Bound_variable_2999 @ Bound_variable_3001 ) @ id ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_3211: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3283: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term] :
( ~ ( var @ ( sub @ A @ id ) )
| ( P @ id @ A @ id ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3283 @ id ) ) ) ) ) )
& ( hoasinduction_no_psi_cond_lthm
<=> ( ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
=> ( ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3295: term] :
( ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3295 @ id ) ) ) ) ) ) )
& ( hoaslaminj
<=> ! [F: subst > term > term,Bound_variable_2547: subst > term > term,Bound_variable_2549: subst,Bound_variable_2551: term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( Bound_variable_2547 @ M @ A ) @ N )
= ( Bound_variable_2547 @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ( ( lam @ ( F @ sh @ one ) )
!= ( lam @ ( Bound_variable_2547 @ sh @ one ) ) )
| ( ( F @ Bound_variable_2549 @ Bound_variable_2551 )
= ( Bound_variable_2547 @ Bound_variable_2549 @ Bound_variable_2551 ) ) ) )
& ( hoasinduction_lem3aaa
<=> ! [P: subst > term > subst > $o,Bound_variable_3171: term] :
( ~ ! [F: subst > term > term,Bound_variable_3149: term] :
( ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id )
| ~ ! [Bound_variable_3072: subst,Bound_variable_3074: term,Bound_variable_3076: subst] :
( ( sub @ ( F @ Bound_variable_3072 @ Bound_variable_3074 ) @ Bound_variable_3076 )
= ( sub @ ( sub @ Bound_variable_3149 @ ( push @ Bound_variable_3074 @ Bound_variable_3072 ) ) @ Bound_variable_3076 ) )
| ~ ! [Bound_variable_3090: subst,Bound_variable_3092: term,Bound_variable_3094: subst] :
( ( F @ ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) @ ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) )
= ( sub @ Bound_variable_3149 @ ( push @ ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) @ ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) ) ) ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3171 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3171 @ ( push @ one @ sh ) ) ) @ id ) ) )
& induction2lem_gthm
& ( hoasinduction_lem3aa_lthm
<=> ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) ) )
& ( hoasinduction_lem3
<=> ! [P: subst > term > subst > $o,Bound_variable_3211: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) ) )
& ( hoasinduction_lem2
<=> ! [P: subst > term > subst > $o,Bound_variable_2999: term,Bound_variable_3001: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ( P @ id @ Bound_variable_2999 @ id )
| ~ ( P @ id @ Bound_variable_3001 @ id )
| ( P @ id @ ( ap @ Bound_variable_2999 @ Bound_variable_3001 ) @ id ) ) )
& ( termmset_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [A: term] :
( A
= ( sub @ A @ id ) ) ) )
& hoasinduction_lem1
& hoaslamnotap_lthm
& ( pushprop_lem1v2_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ! [P: term > $o,Q: term > $o,A: term,M: subst] :
( ~ ( P @ A )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) )
| ( Q @ one ) ) ) )
& hoasapnotvar
& ( hoasinduction_lem0
<=> ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) ) )
& ( hoasinduction
<=> ! [P: subst > term > subst > $o,Bound_variable_3283: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term] :
( ~ ( var @ ( sub @ A @ id ) )
| ( P @ id @ A @ id ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3283 @ id ) ) )
& hoasinduction_gthm
& axapp
& hoaslamnotvar_lthm
& pushprop_lem3v2_lthm
& ( hoasinduction_lem3b_lthm
<=> ! [B: term] :
~ ! [F: subst > term > term] :
( ( F @ sh @ one )
!= ( sub @ B @ ( push @ one @ sh ) ) ) )
& ulamvarind
& ( induction
<=> ! [P: term > $o,Bound_variable_2140: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ( P @ A )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2140 ) ) )
& ( hoasinduction_lem3a_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3232: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3232 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3232 ) @ id ) ) ) ) )
& termmset_gthm
& ( hoasinduction_lem3aa
<=> ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) ) )
& pushprop_lem1v2_gthm
& hoaslamnotap_gthm
& hoaslamnotvar_gthm
& hoasinduction_lem3b_gthm
& pushprop_lem2v2
& hoasinduction_lem3a_gthm
& axclos
& axassoc
& ( hoasinduction_lem2v2
<=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2820: term,Bound_variable_2822: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
| ~ ( Q @ Bound_variable_2820 )
| ~ ( Q @ Bound_variable_2822 )
| ( Q @ ( ap @ Bound_variable_2820 @ Bound_variable_2822 ) ) ) )
& pushprop_lthm
& ( apinj2
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( C = D ) ) )
& ( apinj1
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( A = B ) ) )
& ( hoasapinj2_lthm
<=> ( ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( C = D ) )
=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( C = D ) ) ) )
& ( hoasinduction_lem3v2a
<=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) ) )
& ( hoasapinj1_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( A = B ) )
=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( A = B ) ) ) ) )
& ( hoaslaminj_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ( ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) )
=> ( ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) )
=> ! [F: subst > term > term,Bound_variable_2547: subst > term > term,Bound_variable_2549: subst,Bound_variable_2551: term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( Bound_variable_2547 @ M @ A ) @ N )
= ( Bound_variable_2547 @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ( ( lam @ ( F @ sh @ one ) )
!= ( lam @ ( Bound_variable_2547 @ sh @ one ) ) )
| ( ( F @ Bound_variable_2549 @ Bound_variable_2551 )
= ( Bound_variable_2547 @ Bound_variable_2549 @ Bound_variable_2551 ) ) ) ) ) ) )
& ( axvarcons
<=> ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) ) )
& ( axscons
<=> ! [M: subst] :
( M
= ( push @ ( sub @ one @ M ) @ ( comp @ sh @ M ) ) ) )
& hoasinduction_lem2v2_gthm
& ( axidr
<=> ! [M: subst] :
( M
= ( comp @ M @ id ) ) )
& ( pushprop_lem1
<=> ! [P: term > $o,K: term > $o,A: term,M: subst,B: term] :
( ~ ( P @ A )
| ( K @ ( sub @ A @ ( push @ B @ M ) ) ) ) )
& ( laminj
<=> ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) ) )
& ( hoasinduction_lem3_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3211: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) ) ) ) )
& ( pushprop_lem0
<=> ! [P: term > $o,A: term,M: subst] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
<=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) )
& pushprop_gthm
& axabs
& ( hoasinduction_lem3v2a_lthm
<=> ( ! [B: term] :
~ ! [F: subst > term > term] :
~ ! [A: term,M: subst] :
( ( sub @ B @ ( push @ A @ M ) )
= ( F @ M @ A ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) ) ) ) )
& hoasinduction_lem2_lthm
& hoasapinj2_gthm
& hoasinduction_lem1_lthm
& ~ lamnotap
& hoasapinj1_gthm
& hoaslamnotvar
& ( axidl
<=> ! [M: subst] :
( M
= ( comp @ id @ M ) ) )
& hoaslaminj_gthm
& ( induction2_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: term > $o,Bound_variable_2340: term,Bound_variable_2342: subst] :
( ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ~ ! [B: term] :
( ~ ( var @ B )
| ( P @ ( sub @ B @ Bound_variable_2342 ) ) )
| ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) )
=> ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) ) ) ) )
& ( hoasinduction_lem0_lthm
<=> ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) ) )
& ( substmonoid_lthm
<=> ( ! [M: subst] :
( M
= ( comp @ id @ M ) )
=> ( ! [M: subst] :
( M
= ( comp @ M @ id ) )
=> ( ! [M: subst] :
( M
= ( comp @ M @ id ) )
& ! [M: subst] :
( M
= ( comp @ id @ M ) ) ) ) ) )
& pushprop
& hoasinduction_lem3_gthm
& hoasinduction_lem2_gthm
& ( hoasinduction_lem3b
<=> ! [B: term] :
~ ! [F: subst > term > term] :
( ( F @ sh @ one )
!= ( sub @ B @ ( push @ one @ sh ) ) ) )
& ( substmonoid
<=> ( ! [M: subst] :
( M
= ( comp @ M @ id ) )
& ! [M: subst] :
( M
= ( comp @ id @ M ) ) ) )
& lamnotvar
& ( hoasinduction_lem3a
<=> ! [P: subst > term > subst > $o,Bound_variable_3232: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3232 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3232 ) @ id ) ) )
& hoasinduction_lem1_gthm
& ( hoasinduction_no_psi_cond
<=> ! [P: subst > term > subst > $o,Bound_variable_3295: term] :
( ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3295 @ id ) ) )
& induction2_gthm
& pushprop_lem2v2_lthm
& ~ ( hoasvar @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
& ( hoaslamnotap
<=> ! [F: subst > term > term,Bound_variable_2603: term,Bound_variable_2605: term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ( ( lam @ ( F @ sh @ one ) )
!= ( ap @ ( sub @ Bound_variable_2603 @ id ) @ Bound_variable_2605 ) ) ) )
& substmonoid_gthm
& ulamvarsh
& ( induction2
<=> ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) ) )
& pushprop_lem3v2
& pushprop_lem2v2_gthm
& ( pushprop_lem1_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ( ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) )
=> ! [P: term > $o,K: term > $o,A: term,M: subst,B: term] :
( ~ ( P @ A )
| ( K @ ( sub @ A @ ( push @ B @ M ) ) ) ) ) ) )
& ( hoasinduction_lem3v2
<=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2910: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2910 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2910 ) ) ) )
& ( axshiftcons
<=> ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) ) )
& ( termmset
<=> ! [A: term] :
( A
= ( sub @ A @ id ) ) )
& ( pushprop_lem0_lthm
<=> ! [P: term > $o,A: term,M: subst] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
<=> ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) )
& hoasapnotvar_lthm
& ( hoasinduction_lem3v2_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2910: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2910 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2910 ) ) ) ) )
& ( axvarid
<=> ! [A: term] :
( A
= ( sub @ A @ id ) ) )
& ( hoasinduction_lthm_3
<=> ( ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
=> ( ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
<=> ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3283: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term] :
( ~ ( var @ ( sub @ A @ id ) )
| ( P @ id @ A @ id ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3283 @ id ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl0,plain,
( ( !!
@ ^ [Y0: term] :
( ??
@ ^ [Y1: d_term] :
( Y0
= ( d2term @ Y1 ) ) ) )
& ( !!
@ ^ [Y0: d_term] : ( Y0 = d_one ) )
& ( !!
@ ^ [Y0: d_term] :
( !!
@ ^ [Y1: d_term] :
( ( ( d2term @ Y0 )
= ( d2term @ Y1 ) )
=> ( Y0 = Y1 ) ) ) )
& ( !!
@ ^ [Y0: subst] :
( ??
@ ^ [Y1: d_subst] :
( Y0
= ( d2subst @ Y1 ) ) ) )
& ( !!
@ ^ [Y0: d_subst] : ( Y0 = d_id ) )
& ( !!
@ ^ [Y0: d_subst] :
( !!
@ ^ [Y1: d_subst] :
( ( ( d2subst @ Y0 )
= ( d2subst @ Y1 ) )
=> ( Y0 = Y1 ) ) ) )
& ( one
= ( d2term @ d_one ) )
& ( ( ap @ ( d2term @ d_one ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( lam @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( sub @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2term @ d_one ) )
& ( id
= ( d2subst @ d_id ) )
& ( sh
= ( d2subst @ d_id ) )
& ( ( push @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( comp @ ( d2subst @ d_id ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( hoasap @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( hoaslam
= ( ^ [Y0: subst,Y1: subst > term > term] : ( d2term @ d_one ) ) )
& ( hoasinduction_p_and_p_prime
= ( ^ [Y0: subst > term > subst > $o,Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) )
& ( pushprop_p_and_p_prime
= ( ^ [Y0: term,Y1: subst,Y2: term > $o,Y3: term > $o] :
( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y2 @ ( sub @ Y4 @ ( push @ Y0 @ Y1 ) ) ) ) ) ) )
& ( (~) @ ( var @ ( d2term @ d_one ) ) )
& ( pushprop_lem1v2
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y2 @ Y3 ) ) ) ) ) )
| ( Y1 @ one ) ) ) ) ) ) )
& pushprop_lem1_gthm
& axmap
& pushprop_lem0_gthm
& ( shinj
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( ( ( sub @ Y0 @ sh )
!= ( sub @ Y1 @ sh ) )
| ( Y0 = Y1 ) ) ) ) )
& hoasinduction_lem1v2
& hoasinduction_lem1v2_gthm
& ( induction2lem
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( ap @ Y3 @ Y4 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( sub @ Y3 @ ( push @ Y4 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y3 ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( var @ Y3 ) )
| ( Y0 @ ( sub @ Y3 @ Y2 ) ) ) ) )
| ( Y0 @ ( sub @ Y1 @ Y2 ) ) ) ) ) ) )
& ( hoasinduction_lem3v2_f
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( sub @ Y0 @ ( push @ Y2 @ Y3 ) )
= ( Y1 @ Y3 @ Y2 ) ) ) ) ) ) ) ) )
& axvarshift
& ( hoasapinj2
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) ) )
& hoasapnotvar_gthm
& ( hoasapinj1
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) ) )
& ( (~) @ ulamvar1 )
& ( induction2lem_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( ap @ Y3 @ Y4 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( sub @ Y3 @ ( push @ Y4 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y3 ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( var @ Y3 ) )
| ( Y0 @ ( sub @ Y3 @ Y2 ) ) ) ) )
| ( Y0 @ ( sub @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) )
& hoasinduction_lem3v2_gthm
& apnotvar
& pushprop_lthm_orig
& ( hoasinduction_lem3v2_f_lthm
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( sub @ Y0 @ ( push @ Y2 @ Y3 ) )
= ( Y1 @ Y3 @ Y2 ) ) ) ) ) ) ) ) )
& ( hoasinduction_lthm
<=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y3 @ id ) @ Y4 ) @ id ) ) ) ) )
| ( (~) @ ( Y0 @ id @ Y1 @ id ) )
| ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( ap @ Y1 @ Y2 ) @ id ) ) ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ ( sub @ Y2 @ id ) ) )
| ( Y0 @ id @ Y2 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) ) ) ) )
& ( hoasinduction_no_psi_cond_lthm
<=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) ) ) ) ) )
& ( hoaslaminj
<=> ( !!
@ ^ [Y0: subst > term > term] :
( !!
@ ^ [Y1: subst > term > term] :
( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y0 @ Y4 @ Y5 ) @ Y6 )
= ( Y0 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y1 @ Y4 @ Y5 ) @ Y6 )
= ( Y1 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( ( lam @ ( Y0 @ sh @ one ) )
!= ( lam @ ( Y1 @ sh @ one ) ) )
| ( ( Y0 @ Y2 @ Y3 )
= ( Y1 @ Y2 @ Y3 ) ) ) ) ) ) ) )
& ( hoasinduction_lem3aaa
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y2 @ Y4 @ Y5 ) @ Y6 )
= ( sub @ ( sub @ Y3 @ ( push @ Y5 @ Y4 ) ) @ Y6 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( Y2 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) )
= ( sub @ Y3 @ ( push @ ( sub @ Y5 @ Y6 ) @ ( comp @ Y4 @ Y6 ) ) ) ) ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) )
& induction2lem_gthm
& ( hoasinduction_lem3aa_lthm
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) )
& ( hoasinduction_lem3
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) )
& ( hoasinduction_lem2
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y3 @ id ) @ Y4 ) @ id ) ) ) ) )
| ( (~) @ ( Y0 @ id @ Y1 @ id ) )
| ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( ap @ Y1 @ Y2 ) @ id ) ) ) ) ) )
& ( termmset_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) ) ) )
& hoasinduction_lem1
& hoaslamnotap_lthm
& ( pushprop_lem1v2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y2 @ Y3 ) ) ) ) ) )
| ( Y1 @ one ) ) ) ) ) ) ) )
& hoasapnotvar
& ( hoasinduction_lem0
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) ) )
& ( hoasinduction
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ ( sub @ Y2 @ id ) ) )
| ( Y0 @ id @ Y2 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) )
& hoasinduction_gthm
& axapp
& hoaslamnotvar_lthm
& pushprop_lem3v2_lthm
& ( hoasinduction_lem3b_lthm
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( ( Y1 @ sh @ one )
!= ( sub @ Y0 @ ( push @ one @ sh ) ) ) ) ) ) )
& ulamvarind
& ( induction
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) ) )
& ( hoasinduction_lem3a_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) ) ) )
& termmset_gthm
& ( hoasinduction_lem3aa
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) )
& pushprop_lem1v2_gthm
& hoaslamnotap_gthm
& hoaslamnotvar_gthm
& hoasinduction_lem3b_gthm
& pushprop_lem2v2
& hoasinduction_lem3a_gthm
& axclos
& axassoc
& ( hoasinduction_lem2v2
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( !!
@ ^ [Y7: subst] :
( ( (~) @ ( Y0 @ Y4 @ Y5 @ ( comp @ Y7 @ Y6 ) ) )
| ( Y0 @ ( comp @ Y4 @ Y7 ) @ ( sub @ Y5 @ Y7 ) @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( !!
@ ^ [Y7: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y4 @ Y7 ) @ ( sub @ Y5 @ Y7 ) @ Y6 ) )
| ( Y0 @ Y4 @ Y5 @ ( comp @ Y7 @ Y6 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( (~) @ ( Y0 @ id @ Y5 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y4 @ id ) @ Y5 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ id @ Y4 @ id ) ) ) )
| ( (~) @ ( Y1 @ Y2 ) )
| ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( ap @ Y2 @ Y3 ) ) ) ) ) ) ) )
& pushprop_lthm
& ( apinj2
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) ) )
& ( apinj1
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) ) )
& ( hoasapinj2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) ) ) )
& ( hoasinduction_lem3v2a
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) )
& ( hoasapinj1_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) ) ) ) )
& ( hoaslaminj_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( ( ( lam @ Y0 )
!= ( lam @ Y1 ) )
| ( Y0 = Y1 ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > term] :
( !!
@ ^ [Y1: subst > term > term] :
( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y0 @ Y4 @ Y5 ) @ Y6 )
= ( Y0 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y1 @ Y4 @ Y5 ) @ Y6 )
= ( Y1 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( ( lam @ ( Y0 @ sh @ one ) )
!= ( lam @ ( Y1 @ sh @ one ) ) )
| ( ( Y0 @ Y2 @ Y3 )
= ( Y1 @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) )
& ( axvarcons
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) ) )
& ( axscons
<=> ( !!
@ ^ [Y0: subst] :
( Y0
= ( push @ ( sub @ one @ Y0 ) @ ( comp @ sh @ Y0 ) ) ) ) )
& hoasinduction_lem2v2_gthm
& ( axidr
<=> ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) ) )
& ( pushprop_lem1
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y4 @ Y3 ) ) ) ) ) ) ) ) ) )
& ( laminj
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( ( ( lam @ Y0 )
!= ( lam @ Y1 ) )
| ( Y0 = Y1 ) ) ) ) )
& ( hoasinduction_lem3_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) ) ) )
& ( pushprop_lem0
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( (~)
@ ( !!
@ ^ [Y3: term > $o] :
( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) ) )
& pushprop_gthm
& axabs
& ( hoasinduction_lem3v2a_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( sub @ Y0 @ ( push @ Y2 @ Y3 ) )
= ( Y1 @ Y3 @ Y2 ) ) ) ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) ) ) )
& hoasinduction_lem2_lthm
& hoasapinj2_gthm
& hoasinduction_lem1_lthm
& ( (~) @ lamnotap )
& hoasapinj1_gthm
& hoaslamnotvar
& ( axidl
<=> ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) ) )
& hoaslaminj_gthm
& ( induction2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( ap @ Y3 @ Y4 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( sub @ Y3 @ ( push @ Y4 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y3 ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( var @ Y3 ) )
| ( Y0 @ ( sub @ Y3 @ Y2 ) ) ) ) )
| ( Y0 @ ( sub @ Y1 @ Y2 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) ) ) ) )
& ( hoasinduction_lem0_lthm
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) ) )
& ( substmonoid_lthm
<=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) )
=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
& ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) ) ) ) ) )
& pushprop
& hoasinduction_lem3_gthm
& hoasinduction_lem2_gthm
& ( hoasinduction_lem3b
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( ( Y1 @ sh @ one )
!= ( sub @ Y0 @ ( push @ one @ sh ) ) ) ) ) ) )
& ( substmonoid
<=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
& ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) ) ) )
& lamnotvar
& ( hoasinduction_lem3a
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) )
& hoasinduction_lem1_gthm
& ( hoasinduction_no_psi_cond
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) )
& induction2_gthm
& pushprop_lem2v2_lthm
& ( (~) @ ( hoasvar @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) )
& ( hoaslamnotap
<=> ( !!
@ ^ [Y0: subst > term > term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y0 @ Y3 @ Y4 ) @ Y5 )
= ( Y0 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( ( lam @ ( Y0 @ sh @ one ) )
!= ( ap @ ( sub @ Y1 @ id ) @ Y2 ) ) ) ) ) ) )
& substmonoid_gthm
& ulamvarsh
& ( induction2
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) ) )
& pushprop_lem3v2
& pushprop_lem2v2_gthm
& ( pushprop_lem1_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y4 @ Y3 ) ) ) ) ) ) ) ) ) ) ) )
& ( hoasinduction_lem3v2
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) )
& ( axshiftcons
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) ) )
& ( termmset
<=> ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) ) )
& ( pushprop_lem0_lthm
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( (~)
@ ( !!
@ ^ [Y3: term > $o] :
( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) ) )
& hoasapnotvar_lthm
& ( hoasinduction_lem3v2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) ) )
& ( axvarid
<=> ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) ) )
& ( hoasinduction_lthm_3
<=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ ( sub @ Y2 @ id ) ) )
| ( Y0 @ id @ Y2 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[alg444_1]) ).
thf(zip_derived_cl2,plain,
( ( !!
@ ^ [Y0: term] :
( ??
@ ^ [Y1: d_term] :
( Y0
= ( d2term @ Y1 ) ) ) )
& ( !!
@ ^ [Y0: d_term] : ( Y0 = d_one ) )
& ( !!
@ ^ [Y0: d_term] :
( !!
@ ^ [Y1: d_term] :
( ( ( d2term @ Y0 )
= ( d2term @ Y1 ) )
=> ( Y0 = Y1 ) ) ) )
& ( !!
@ ^ [Y0: subst] :
( ??
@ ^ [Y1: d_subst] :
( Y0
= ( d2subst @ Y1 ) ) ) )
& ( !!
@ ^ [Y0: d_subst] : ( Y0 = d_id ) )
& ( !!
@ ^ [Y0: d_subst] :
( !!
@ ^ [Y1: d_subst] :
( ( ( d2subst @ Y0 )
= ( d2subst @ Y1 ) )
=> ( Y0 = Y1 ) ) ) )
& ( one
= ( d2term @ d_one ) )
& ( ( ap @ ( d2term @ d_one ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( lam @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( sub @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2term @ d_one ) )
& ( id
= ( d2subst @ d_id ) )
& ( sh
= ( d2subst @ d_id ) )
& ( ( push @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( comp @ ( d2subst @ d_id ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( hoasap @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( hoaslam
= ( ^ [Y0: subst,Y1: subst > term > term] : ( d2term @ d_one ) ) )
& ( hoasinduction_p_and_p_prime
= ( ^ [Y0: subst > term > subst > $o,Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) )
& ( pushprop_p_and_p_prime
= ( ^ [Y0: term,Y1: subst,Y2: term > $o,Y3: term > $o] :
( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y2 @ ( sub @ Y4 @ ( push @ Y0 @ Y1 ) ) ) ) ) ) )
& ( (~) @ ( var @ ( d2term @ d_one ) ) )
& ( pushprop_lem1v2
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y2 @ Y3 ) ) ) ) ) )
| ( Y1 @ one ) ) ) ) ) ) )
& pushprop_lem1_gthm
& axmap
& pushprop_lem0_gthm
& ( shinj
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( ( ( sub @ Y0 @ sh )
!= ( sub @ Y1 @ sh ) )
| ( Y0 = Y1 ) ) ) ) )
& hoasinduction_lem1v2
& hoasinduction_lem1v2_gthm
& ( induction2lem
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( ap @ Y3 @ Y4 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( sub @ Y3 @ ( push @ Y4 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y3 ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( var @ Y3 ) )
| ( Y0 @ ( sub @ Y3 @ Y2 ) ) ) ) )
| ( Y0 @ ( sub @ Y1 @ Y2 ) ) ) ) ) ) )
& ( hoasinduction_lem3v2_f
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( sub @ Y0 @ ( push @ Y2 @ Y3 ) )
= ( Y1 @ Y3 @ Y2 ) ) ) ) ) ) ) ) )
& axvarshift
& ( hoasapinj2
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) ) )
& hoasapnotvar_gthm
& ( hoasapinj1
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) ) )
& ( (~) @ ulamvar1 )
& ( induction2lem_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( ap @ Y3 @ Y4 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( sub @ Y3 @ ( push @ Y4 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y3 ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( var @ Y3 ) )
| ( Y0 @ ( sub @ Y3 @ Y2 ) ) ) ) )
| ( Y0 @ ( sub @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) )
& hoasinduction_lem3v2_gthm
& apnotvar
& pushprop_lthm_orig
& ( hoasinduction_lem3v2_f_lthm
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( sub @ Y0 @ ( push @ Y2 @ Y3 ) )
= ( Y1 @ Y3 @ Y2 ) ) ) ) ) ) ) ) )
& ( hoasinduction_lthm
<=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y3 @ id ) @ Y4 ) @ id ) ) ) ) )
| ( (~) @ ( Y0 @ id @ Y1 @ id ) )
| ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( ap @ Y1 @ Y2 ) @ id ) ) ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ ( sub @ Y2 @ id ) ) )
| ( Y0 @ id @ Y2 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) ) ) ) )
& ( hoasinduction_no_psi_cond_lthm
<=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) ) ) ) ) )
& ( hoaslaminj
<=> ( !!
@ ^ [Y0: subst > term > term] :
( !!
@ ^ [Y1: subst > term > term] :
( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y0 @ Y4 @ Y5 ) @ Y6 )
= ( Y0 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y1 @ Y4 @ Y5 ) @ Y6 )
= ( Y1 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( ( lam @ ( Y0 @ sh @ one ) )
!= ( lam @ ( Y1 @ sh @ one ) ) )
| ( ( Y0 @ Y2 @ Y3 )
= ( Y1 @ Y2 @ Y3 ) ) ) ) ) ) ) )
& ( hoasinduction_lem3aaa
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y2 @ Y4 @ Y5 ) @ Y6 )
= ( sub @ ( sub @ Y3 @ ( push @ Y5 @ Y4 ) ) @ Y6 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( Y2 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) )
= ( sub @ Y3 @ ( push @ ( sub @ Y5 @ Y6 ) @ ( comp @ Y4 @ Y6 ) ) ) ) ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) )
& induction2lem_gthm
& ( hoasinduction_lem3aa_lthm
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) )
& ( hoasinduction_lem3
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) )
& ( hoasinduction_lem2
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y3 @ id ) @ Y4 ) @ id ) ) ) ) )
| ( (~) @ ( Y0 @ id @ Y1 @ id ) )
| ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( ap @ Y1 @ Y2 ) @ id ) ) ) ) ) )
& termmset_lthm
& hoasinduction_lem1
& hoaslamnotap_lthm
& ( pushprop_lem1v2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y2 @ Y3 ) ) ) ) ) )
| ( Y1 @ one ) ) ) ) ) ) ) )
& hoasapnotvar
& ( hoasinduction_lem0
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) ) )
& ( hoasinduction
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ ( sub @ Y2 @ id ) ) )
| ( Y0 @ id @ Y2 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) )
& hoasinduction_gthm
& axapp
& hoaslamnotvar_lthm
& pushprop_lem3v2_lthm
& ( hoasinduction_lem3b_lthm
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( ( Y1 @ sh @ one )
!= ( sub @ Y0 @ ( push @ one @ sh ) ) ) ) ) ) )
& ulamvarind
& ( induction
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) ) )
& ( hoasinduction_lem3a_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) ) ) )
& termmset_gthm
& ( hoasinduction_lem3aa
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) ) )
& pushprop_lem1v2_gthm
& hoaslamnotap_gthm
& hoaslamnotvar_gthm
& hoasinduction_lem3b_gthm
& pushprop_lem2v2
& hoasinduction_lem3a_gthm
& axclos
& axassoc
& ( hoasinduction_lem2v2
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( !!
@ ^ [Y7: subst] :
( ( (~) @ ( Y0 @ Y4 @ Y5 @ ( comp @ Y7 @ Y6 ) ) )
| ( Y0 @ ( comp @ Y4 @ Y7 ) @ ( sub @ Y5 @ Y7 ) @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( !!
@ ^ [Y7: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y4 @ Y7 ) @ ( sub @ Y5 @ Y7 ) @ Y6 ) )
| ( Y0 @ Y4 @ Y5 @ ( comp @ Y7 @ Y6 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( (~) @ ( Y0 @ id @ Y5 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y4 @ id ) @ Y5 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ id @ Y4 @ id ) ) ) )
| ( (~) @ ( Y1 @ Y2 ) )
| ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( ap @ Y2 @ Y3 ) ) ) ) ) ) ) )
& pushprop_lthm
& ( apinj2
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) ) )
& ( apinj1
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) ) )
& ( hoasapinj2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y2 = Y3 ) ) ) ) ) ) ) )
& ( hoasinduction_lem3v2a
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) )
& ( hoasapinj1_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ Y0 @ Y2 )
!= ( ap @ Y1 @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( ( ap @ ( sub @ Y0 @ id ) @ Y2 )
!= ( ap @ ( sub @ Y1 @ id ) @ Y3 ) )
| ( Y0 = Y1 ) ) ) ) ) ) ) ) )
& ( hoaslaminj_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( ( ( lam @ Y0 )
!= ( lam @ Y1 ) )
| ( Y0 = Y1 ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > term] :
( !!
@ ^ [Y1: subst > term > term] :
( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y0 @ Y4 @ Y5 ) @ Y6 )
= ( Y0 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y1 @ Y4 @ Y5 ) @ Y6 )
= ( Y1 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( ( lam @ ( Y0 @ sh @ one ) )
!= ( lam @ ( Y1 @ sh @ one ) ) )
| ( ( Y0 @ Y2 @ Y3 )
= ( Y1 @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) )
& ( axvarcons
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) ) )
& ( axscons
<=> ( !!
@ ^ [Y0: subst] :
( Y0
= ( push @ ( sub @ one @ Y0 ) @ ( comp @ sh @ Y0 ) ) ) ) )
& hoasinduction_lem2v2_gthm
& ( axidr
<=> ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) ) )
& ( pushprop_lem1
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y4 @ Y3 ) ) ) ) ) ) ) ) ) )
& ( laminj
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: term] :
( ( ( lam @ Y0 )
!= ( lam @ Y1 ) )
| ( Y0 = Y1 ) ) ) ) )
& ( hoasinduction_lem3_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( sub @ Y1 @ ( push @ one @ sh ) ) ) @ id ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) ) ) )
& ( pushprop_lem0
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( (~)
@ ( !!
@ ^ [Y3: term > $o] :
( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) ) )
& pushprop_gthm
& axabs
& ( hoasinduction_lem3v2a_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( sub @ Y0 @ ( push @ Y2 @ Y3 ) )
= ( Y1 @ Y3 @ Y2 ) ) ) ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) ) ) )
& hoasinduction_lem2_lthm
& hoasapinj2_gthm
& hoasinduction_lem1_lthm
& ( (~) @ lamnotap )
& hoasapinj1_gthm
& hoaslamnotvar
& ( axidl
<=> ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) ) )
& hoaslaminj_gthm
& ( induction2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( ap @ Y3 @ Y4 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y4 ) )
| ( Y0 @ ( sub @ Y3 @ ( push @ Y4 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y3 ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( var @ Y3 ) )
| ( Y0 @ ( sub @ Y3 @ Y2 ) ) ) ) )
| ( Y0 @ ( sub @ Y1 @ Y2 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) ) ) ) )
& ( hoasinduction_lem0_lthm
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) ) )
& ( substmonoid_lthm
<=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) )
=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
& ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) ) ) ) ) )
& pushprop
& hoasinduction_lem3_gthm
& hoasinduction_lem2_gthm
& ( hoasinduction_lem3b
<=> ( !!
@ ^ [Y0: term] :
( (~)
@ ( !!
@ ^ [Y1: subst > term > term] :
( ( Y1 @ sh @ one )
!= ( sub @ Y0 @ ( push @ one @ sh ) ) ) ) ) ) )
& ( substmonoid
<=> ( ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ Y0 @ id ) ) )
& ( !!
@ ^ [Y0: subst] :
( Y0
= ( comp @ id @ Y0 ) ) ) ) )
& lamnotvar
& ( hoasinduction_lem3a
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( Y0 @ id @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ Y1 ) @ id ) ) ) ) )
& hoasinduction_lem1_gthm
& ( hoasinduction_no_psi_cond
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) )
& induction2_gthm
& pushprop_lem2v2_lthm
& ( (~) @ ( hoasvar @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) ) )
& ( hoaslamnotap
<=> ( !!
@ ^ [Y0: subst > term > term] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y0 @ Y3 @ Y4 ) @ Y5 )
= ( Y0 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( ( lam @ ( Y0 @ sh @ one ) )
!= ( ap @ ( sub @ Y1 @ id ) @ Y2 ) ) ) ) ) ) )
& substmonoid_gthm
& ulamvarsh
& ( induction2
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) ) )
& pushprop_lem3v2
& pushprop_lem2v2_gthm
& ( pushprop_lem1_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y0
= ( sub @ one @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) )
=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y4 @ Y3 ) ) ) ) ) ) ) ) ) ) ) )
& ( hoasinduction_lem3v2
<=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) )
& ( axshiftcons
<=> ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( Y1
= ( comp @ sh @ ( push @ Y0 @ Y1 ) ) ) ) ) )
& ( termmset
<=> ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) ) )
& ( pushprop_lem0_lthm
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( (~)
@ ( !!
@ ^ [Y3: term > $o] :
( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) ) )
& hoasapnotvar_lthm
& ( hoasinduction_lem3v2_lthm
<=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) )
| ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( !!
@ ^ [Y6: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y3 @ Y6 ) @ ( sub @ Y4 @ Y6 ) @ Y5 ) )
| ( Y0 @ Y3 @ Y4 @ ( comp @ Y6 @ Y5 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) ) ) )
& ( axvarid
<=> ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) ) )
& ( hoasinduction_lthm_3
<=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( (~)
@ ( !!
@ ^ [Y1: term > $o] :
( (~)
@ ( !!
@ ^ [Y2: term] :
( ( Y1 @ Y2 )
<=> ( Y0 @ id @ Y2 @ id ) ) ) ) ) ) )
=> ( ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ Y2 ) )
| ( Y0 @ Y2 ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( ap @ Y2 @ Y3 ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ Y3 ) )
| ( Y0 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y0 @ ( lam @ Y2 ) ) ) ) )
| ( Y0 @ Y1 ) ) ) )
=> ( ( !!
@ ^ [Y0: term] :
( Y0
= ( sub @ Y0 @ id ) ) )
=> ( ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: term] :
( !!
@ ^ [Y6: subst] :
( ( sub @ ( Y3 @ Y4 @ Y5 ) @ Y6 )
= ( Y3 @ ( comp @ Y4 @ Y6 ) @ ( sub @ Y5 @ Y6 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( (~) @ ( Y0 @ id @ Y4 @ id ) )
| ( Y0 @ id @ ( Y3 @ id @ Y4 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y3 @ sh @ one ) ) @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y1 @ Y3 )
<=> ( Y0 @ id @ Y3 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y1 @ Y3 ) )
| ( Y1 @ ( sub @ Y2 @ ( push @ Y3 @ id ) ) ) ) ) )
| ( Y1 @ ( lam @ Y2 ) ) ) ) ) )
=> ( !!
@ ^ [Y0: subst > term > subst > $o] :
( !!
@ ^ [Y1: term] :
( ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) )
| ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst] :
( !!
@ ^ [Y3: term] :
( !!
@ ^ [Y4: subst] :
( !!
@ ^ [Y5: subst] :
( ( (~) @ ( Y0 @ ( comp @ Y2 @ Y5 ) @ ( sub @ Y3 @ Y5 ) @ Y4 ) )
| ( Y0 @ Y2 @ Y3 @ ( comp @ Y5 @ Y4 ) ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( (~) @ ( var @ ( sub @ Y2 @ id ) ) )
| ( Y0 @ id @ Y2 @ id ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y2 @ id ) )
| ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( ap @ ( sub @ Y2 @ id ) @ Y3 ) @ id ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y2: subst > term > term] :
( ( (~)
@ ( !!
@ ^ [Y3: subst] :
( !!
@ ^ [Y4: term] :
( !!
@ ^ [Y5: subst] :
( ( sub @ ( Y2 @ Y3 @ Y4 ) @ Y5 )
= ( Y2 @ ( comp @ Y3 @ Y5 ) @ ( sub @ Y4 @ Y5 ) ) ) ) ) ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( (~) @ ( Y0 @ id @ Y3 @ id ) )
| ( Y0 @ id @ ( Y2 @ id @ Y3 ) @ id ) ) ) )
| ( Y0 @ id @ ( lam @ ( Y2 @ sh @ one ) ) @ id ) ) ) )
| ( Y0 @ id @ Y1 @ id ) ) ) ) ) ) ) ) ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl0]) ).
thf(zip_derived_cl3,plain,
( !!
@ ^ [Y0: term] :
( ??
@ ^ [Y1: d_term] :
( Y0
= ( d2term @ Y1 ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl2]) ).
thf(zip_derived_cl131,plain,
! [X2: term] :
( ??
@ ^ [Y0: d_term] :
( X2
= ( d2term @ Y0 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl3]) ).
thf(zip_derived_cl204,plain,
! [X2: term] :
( X2
= ( d2term @ ( '#sk1' @ X2 ) ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl131]) ).
thf(zip_derived_cl210,plain,
! [X2: term] :
( X2
= ( d2term @ ( '#sk1' @ X2 ) ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl204]) ).
thf(zip_derived_cl4,plain,
( !!
@ ^ [Y0: d_term] : ( Y0 = d_one ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl2]) ).
thf(zip_derived_cl132,plain,
! [X2: d_term] : ( X2 = d_one ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl4]) ).
thf(zip_derived_cl205,plain,
! [X2: d_term] : ( X2 = d_one ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl132]) ).
thf(zip_derived_cl9,plain,
( one
= ( d2term @ d_one ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl2]) ).
thf(zip_derived_cl137,plain,
( one
= ( d2term @ d_one ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl9]) ).
thf(zip_derived_cl221,plain,
! [X2: term] : ( X2 = one ),
inference(demod,[status(thm)],[zip_derived_cl210,zip_derived_cl205,zip_derived_cl137]) ).
thf(zip_derived_cl221_001,plain,
! [X2: term] : ( X2 = one ),
inference(demod,[status(thm)],[zip_derived_cl210,zip_derived_cl205,zip_derived_cl137]) ).
thf(zip_derived_cl236,plain,
! [X0: term,X1: term] : ( X1 = X0 ),
inference('sup+',[status(thm)],[zip_derived_cl221,zip_derived_cl221]) ).
thf(zip_derived_cl22,plain,
( pushprop_lem1v2
<=> ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y2 @ Y3 ) ) ) ) ) )
| ( Y1 @ one ) ) ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl2]) ).
thf(zip_derived_cl149,plain,
( pushprop_lem1v2
= ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y2 @ Y3 ) ) ) ) ) )
| ( Y1 @ one ) ) ) ) ) ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl22]) ).
thf(zip_derived_cl790,plain,
( pushprop_lem1v2
| ~ ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( (~) @ ( Y0 @ Y2 ) )
| ( (~)
@ ( !!
@ ^ [Y4: term] :
( ( Y1 @ Y4 )
<=> ( Y0 @ ( sub @ Y4 @ ( push @ Y2 @ Y3 ) ) ) ) ) )
| ( Y1 @ one ) ) ) ) ) ) ),
inference(eq_elim,[status(thm)],[zip_derived_cl149]) ).
thf(zip_derived_cl3018,plain,
( ~ ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( (~) @ ( '#sk10492' @ Y1 ) )
| ( (~)
@ ( !!
@ ^ [Y3: term] :
( ( Y0 @ Y3 )
<=> ( '#sk10492' @ ( sub @ Y3 @ ( push @ Y1 @ Y2 ) ) ) ) ) )
| ( Y0 @ one ) ) ) ) )
| pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl790]) ).
thf(zip_derived_cl3019,plain,
( ~ ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( ( (~) @ ( '#sk10492' @ Y0 ) )
| ( (~)
@ ( !!
@ ^ [Y2: term] :
( ( '#sk10493' @ Y2 )
<=> ( '#sk10492' @ ( sub @ Y2 @ ( push @ Y0 @ Y1 ) ) ) ) ) )
| ( '#sk10493' @ one ) ) ) )
| pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl3018]) ).
thf(zip_derived_cl3020,plain,
( ~ ( !!
@ ^ [Y0: subst] :
( ( (~) @ ( '#sk10492' @ '#sk10494' ) )
| ( (~)
@ ( !!
@ ^ [Y1: term] :
( ( '#sk10493' @ Y1 )
<=> ( '#sk10492' @ ( sub @ Y1 @ ( push @ '#sk10494' @ Y0 ) ) ) ) ) )
| ( '#sk10493' @ one ) ) )
| pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl3019]) ).
thf(zip_derived_cl3021,plain,
( ~ ( ( (~) @ ( '#sk10492' @ '#sk10494' ) )
| ( (~)
@ ( !!
@ ^ [Y0: term] :
( ( '#sk10493' @ Y0 )
<=> ( '#sk10492' @ ( sub @ Y0 @ ( push @ '#sk10494' @ '#sk10495' ) ) ) ) ) )
| ( '#sk10493' @ one ) )
| pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl3020]) ).
thf(zip_derived_cl3023,plain,
( ( !!
@ ^ [Y0: term] :
( ( '#sk10493' @ Y0 )
<=> ( '#sk10492' @ ( sub @ Y0 @ ( push @ '#sk10494' @ '#sk10495' ) ) ) ) )
| pushprop_lem1v2 ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl3021]) ).
thf(zip_derived_cl3025,plain,
! [X2: term] :
( ( ( '#sk10493' @ X2 )
<=> ( '#sk10492' @ ( sub @ X2 @ ( push @ '#sk10494' @ '#sk10495' ) ) ) )
| pushprop_lem1v2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl3023]) ).
thf(zip_derived_cl3026,plain,
! [X2: term] :
( ( ( '#sk10493' @ X2 )
= ( '#sk10492' @ ( sub @ X2 @ ( push @ '#sk10494' @ '#sk10495' ) ) ) )
| pushprop_lem1v2 ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl3025]) ).
thf(zip_derived_cl236_002,plain,
! [X0: term,X1: term] : ( X1 = X0 ),
inference('sup+',[status(thm)],[zip_derived_cl221,zip_derived_cl221]) ).
thf(pushprop_lem1v2,conjecture,
( pushprop_lem1v2
<=> ! [P: term > $o,Q: term > $o,A: term,M: subst] :
( ( P @ A )
=> ( ( pushprop_p_and_p_prime @ A @ M @ P @ Q )
=> ( Q @ one ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ( pushprop_lem1v2
<=> ! [P: term > $o,Q: term > $o,A: term,M: subst] :
( ( P @ A )
=> ( ( pushprop_p_and_p_prime @ A @ M @ P @ Q )
=> ( Q @ one ) ) ) ),
inference('cnf.neg',[status(esa)],[pushprop_lem1v2]) ).
thf(zip_derived_cl1,plain,
( pushprop_lem1v2
!= ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( Y0 @ Y2 )
=> ( ( pushprop_p_and_p_prime @ Y2 @ Y3 @ Y0 @ Y1 )
=> ( Y1 @ one ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl233,plain,
( ~ pushprop_lem1v2
| ~ ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term > $o] :
( !!
@ ^ [Y2: term] :
( !!
@ ^ [Y3: subst] :
( ( Y0 @ Y2 )
=> ( ( pushprop_p_and_p_prime @ Y2 @ Y3 @ Y0 @ Y1 )
=> ( Y1 @ one ) ) ) ) ) ) ) ),
inference(eq_elim,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl639,plain,
( ~ ( !!
@ ^ [Y0: term > $o] :
( !!
@ ^ [Y1: term] :
( !!
@ ^ [Y2: subst] :
( ( '#sk3138' @ Y1 )
=> ( ( pushprop_p_and_p_prime @ Y1 @ Y2 @ '#sk3138' @ Y0 )
=> ( Y0 @ one ) ) ) ) ) )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl233]) ).
thf(zip_derived_cl640,plain,
( ~ ( !!
@ ^ [Y0: term] :
( !!
@ ^ [Y1: subst] :
( ( '#sk3138' @ Y0 )
=> ( ( pushprop_p_and_p_prime @ Y0 @ Y1 @ '#sk3138' @ '#sk3139' )
=> ( '#sk3139' @ one ) ) ) ) )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl639]) ).
thf(zip_derived_cl641,plain,
( ~ ( !!
@ ^ [Y0: subst] :
( ( '#sk3138' @ '#sk3140' )
=> ( ( pushprop_p_and_p_prime @ '#sk3140' @ Y0 @ '#sk3138' @ '#sk3139' )
=> ( '#sk3139' @ one ) ) ) )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl640]) ).
thf(zip_derived_cl642,plain,
( ~ ( ( '#sk3138' @ '#sk3140' )
=> ( ( pushprop_p_and_p_prime @ '#sk3140' @ '#sk3141' @ '#sk3138' @ '#sk3139' )
=> ( '#sk3139' @ one ) ) )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl641]) ).
thf(zip_derived_cl644,plain,
( ~ ( ( pushprop_p_and_p_prime @ '#sk3140' @ '#sk3141' @ '#sk3138' @ '#sk3139' )
=> ( '#sk3139' @ one ) )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl642]) ).
thf(zip_derived_cl646,plain,
( ~ ( '#sk3139' @ one )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl644]) ).
thf(zip_derived_cl656,plain,
! [X0: term] :
( ~ ( '#sk3139' @ X0 )
| ~ pushprop_lem1v2 ),
inference('sup-',[status(thm)],[zip_derived_cl236,zip_derived_cl646]) ).
thf(zip_derived_cl236_003,plain,
! [X0: term,X1: term] : ( X1 = X0 ),
inference('sup+',[status(thm)],[zip_derived_cl221,zip_derived_cl221]) ).
thf(zip_derived_cl645,plain,
( ( pushprop_p_and_p_prime @ '#sk3140' @ '#sk3141' @ '#sk3138' @ '#sk3139' )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl644]) ).
thf(zip_derived_cl658,plain,
! [X0: term] :
( ( pushprop_p_and_p_prime @ X0 @ '#sk3141' @ '#sk3138' @ '#sk3139' )
| ~ pushprop_lem1v2 ),
inference('sup+',[status(thm)],[zip_derived_cl236,zip_derived_cl645]) ).
thf(zip_derived_cl20,plain,
( pushprop_p_and_p_prime
= ( ^ [Y0: term,Y1: subst,Y2: term > $o,Y3: term > $o] :
( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y2 @ ( sub @ Y4 @ ( push @ Y0 @ Y1 ) ) ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl2]) ).
thf(zip_derived_cl148,plain,
( pushprop_p_and_p_prime
= ( ^ [Y0: term,Y1: subst,Y2: term > $o,Y3: term > $o] :
( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y2 @ ( sub @ Y4 @ ( push @ Y0 @ Y1 ) ) ) ) ) ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl20]) ).
thf(zip_derived_cl461,plain,
! [X1: term,X2: subst,X3: term > $o,X4: term > $o] :
( ( pushprop_p_and_p_prime @ X1 @ X2 @ X3 @ X4 )
= ( ^ [Y0: term,Y1: subst,Y2: term > $o,Y3: term > $o] :
( !!
@ ^ [Y4: term] :
( ( Y3 @ Y4 )
<=> ( Y2 @ ( sub @ Y4 @ ( push @ Y0 @ Y1 ) ) ) ) )
@ X1
@ X2
@ X3
@ X4 ) ),
inference(ho_complete_eq,[status(thm)],[zip_derived_cl148]) ).
thf(zip_derived_cl465,plain,
! [X1: term,X2: subst,X3: term > $o,X4: term > $o] :
( ( pushprop_p_and_p_prime @ X1 @ X2 @ X3 @ X4 )
= ( !!
@ ^ [Y0: term] :
( ( X4 @ Y0 )
<=> ( X3 @ ( sub @ Y0 @ ( push @ X1 @ X2 ) ) ) ) ) ),
inference(ho_norm,[status(thm)],[zip_derived_cl461]) ).
thf(zip_derived_cl3009,plain,
! [X1: term,X2: subst,X3: term > $o,X4: term > $o] :
( ~ ( pushprop_p_and_p_prime @ X1 @ X2 @ X3 @ X4 )
| ( !!
@ ^ [Y0: term] :
( ( X4 @ Y0 )
<=> ( X3 @ ( sub @ Y0 @ ( push @ X1 @ X2 ) ) ) ) ) ),
inference(eq_elim,[status(thm)],[zip_derived_cl465]) ).
thf(zip_derived_cl4326,plain,
! [X1: term,X2: subst,X3: term > $o,X4: term > $o,X6: term] :
( ( ( X4 @ X6 )
<=> ( X3 @ ( sub @ X6 @ ( push @ X1 @ X2 ) ) ) )
| ~ ( pushprop_p_and_p_prime @ X1 @ X2 @ X3 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl3009]) ).
thf(zip_derived_cl4327,plain,
! [X1: term,X2: subst,X3: term > $o,X4: term > $o,X6: term] :
( ( ( X4 @ X6 )
= ( X3 @ ( sub @ X6 @ ( push @ X1 @ X2 ) ) ) )
| ~ ( pushprop_p_and_p_prime @ X1 @ X2 @ X3 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl4326]) ).
thf(zip_derived_cl4542,plain,
! [X0: term,X1: term] :
( ~ pushprop_lem1v2
| ( ( '#sk3139' @ X1 )
= ( '#sk3138' @ ( sub @ X1 @ ( push @ X0 @ '#sk3141' ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl658,zip_derived_cl4327]) ).
thf(zip_derived_cl236_004,plain,
! [X0: term,X1: term] : ( X1 = X0 ),
inference('sup+',[status(thm)],[zip_derived_cl221,zip_derived_cl221]) ).
thf(zip_derived_cl4567,plain,
! [X1: term] :
( ~ pushprop_lem1v2
| ( ( '#sk3139' @ X1 )
= ( '#sk3138' @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4542,zip_derived_cl236]) ).
thf(zip_derived_cl4603,plain,
! [X0: term] :
( ~ ( '#sk3138' @ X0 )
| ~ pushprop_lem1v2
| ~ pushprop_lem1v2 ),
inference('sup+',[status(thm)],[zip_derived_cl656,zip_derived_cl4567]) ).
thf(zip_derived_cl4618,plain,
! [X0: term] :
( ~ pushprop_lem1v2
| ~ ( '#sk3138' @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl4603]) ).
thf(zip_derived_cl236_005,plain,
! [X0: term,X1: term] : ( X1 = X0 ),
inference('sup+',[status(thm)],[zip_derived_cl221,zip_derived_cl221]) ).
thf(zip_derived_cl643,plain,
( ( '#sk3138' @ '#sk3140' )
| ~ pushprop_lem1v2 ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl642]) ).
thf(zip_derived_cl647,plain,
! [X0: term] :
( ( '#sk3138' @ X0 )
| ~ pushprop_lem1v2 ),
inference('sup+',[status(thm)],[zip_derived_cl236,zip_derived_cl643]) ).
thf(zip_derived_cl4703,plain,
~ pushprop_lem1v2,
inference(clc,[status(thm)],[zip_derived_cl4618,zip_derived_cl647]) ).
thf(zip_derived_cl4707,plain,
! [X2: term] :
( ( '#sk10493' @ X2 )
= ( '#sk10492' @ ( sub @ X2 @ ( push @ '#sk10494' @ '#sk10495' ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3026,zip_derived_cl4703]) ).
thf(zip_derived_cl236_006,plain,
! [X0: term,X1: term] : ( X1 = X0 ),
inference('sup+',[status(thm)],[zip_derived_cl221,zip_derived_cl221]) ).
thf(zip_derived_cl3024,plain,
( ~ ( '#sk10493' @ one )
| pushprop_lem1v2 ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl3021]) ).
thf(zip_derived_cl3033,plain,
! [X0: term] :
( ~ ( '#sk10493' @ X0 )
| pushprop_lem1v2 ),
inference('sup-',[status(thm)],[zip_derived_cl236,zip_derived_cl3024]) ).
thf(zip_derived_cl4703_007,plain,
~ pushprop_lem1v2,
inference(clc,[status(thm)],[zip_derived_cl4618,zip_derived_cl647]) ).
thf(zip_derived_cl4708,plain,
! [X0: term] :
~ ( '#sk10493' @ X0 ),
inference(demod,[status(thm)],[zip_derived_cl3033,zip_derived_cl4703]) ).
thf(zip_derived_cl4819,plain,
! [X2: term] :
~ ( '#sk10492' @ ( sub @ X2 @ ( push @ '#sk10494' @ '#sk10495' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4707,zip_derived_cl4708]) ).
thf(zip_derived_cl4826,plain,
! [X0: term] :
~ ( '#sk10492' @ X0 ),
inference('sup-',[status(thm)],[zip_derived_cl236,zip_derived_cl4819]) ).
thf(zip_derived_cl3022,plain,
( ( '#sk10492' @ '#sk10494' )
| pushprop_lem1v2 ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl3021]) ).
thf(zip_derived_cl4703_008,plain,
~ pushprop_lem1v2,
inference(clc,[status(thm)],[zip_derived_cl4618,zip_derived_cl647]) ).
thf(zip_derived_cl4706,plain,
'#sk10492' @ '#sk10494',
inference(demod,[status(thm)],[zip_derived_cl3022,zip_derived_cl4703]) ).
thf(zip_derived_cl4942,plain,
$false,
inference('sup+',[status(thm)],[zip_derived_cl4826,zip_derived_cl4706]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.oCcQSEFHhv true
% 0.17/0.34 % Computer : n013.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:58:56 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 % Running portfolio for 300 s
% 0.17/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.35 % Number of cores: 8
% 0.17/0.35 % Python version: Python 3.6.8
% 0.17/0.35 % Running in HO mode
% 0.55/0.63 % Total configuration time : 828
% 0.55/0.63 % Estimated wc time : 1656
% 0.55/0.63 % Estimated cpu time (8 cpus) : 207.0
% 0.56/0.71 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.56/0.71 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.56/0.72 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.56/0.72 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.56/0.75 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.56/0.75 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 0.56/0.75 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 8.05/1.69 % /export/starexec/sandbox/solver/bin/lams/30_b.l.sh running for 90s
% 50.14/7.36 % Solved by lams/30_b.l.sh.
% 50.14/7.36 % done 325 iterations in 5.510s
% 50.14/7.36 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 50.14/7.36 % SZS output start Refutation
% See solution above
% 50.14/7.37
% 50.14/7.37
% 50.14/7.37 % Terminating...
% 8.07/7.51 % Runner terminated.
% 8.07/7.51 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------