%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWX154^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:40:32 AM UTC 2026
% Result : Theorem 29.51s 10.14s
% Output : Refutation 30.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 7
% Syntax : Number of formulae : 29 ( 24 unt; 0 typ; 5 def)
% Number of atoms : 959 ( 578 equ; 0 cnn)
% Maximal formula atoms : 130 ( 33 avg)
% Number of connectives : 7650 (1014 ~; 922 |; 387 &;5217 @)
% ( 0 <=>; 110 =>; 0 <=; 0 <~>)
% Maximal formula depth : 137 ( 15 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 561 ( 561 >; 0 *; 0 +; 0 <<)
% Number of symbols : 133 ( 131 usr; 117 con; 0-4 aty)
% Number of variables : 1678 ( 26 ^;1643 !; 4 ?;1678 :)
% ( 0 !>; 0 ?*; 0 @-; 5 @+)
% Comments :
%------------------------------------------------------------------------------
thf(term_type,type,
term: $tType ).
thf(subst_type,type,
subst: $tType ).
thf(d_term_type,type,
d_term: $tType ).
thf(d_subst_type,type,
d_subst: $tType ).
thf(one_decl,type,
one: term ).
thf(ap_decl,type,
ap: term > term > term ).
thf(lam_decl,type,
lam: term > term ).
thf(sub_decl,type,
sub: term > subst > term ).
thf(id_decl,type,
id: subst ).
thf(sh_decl,type,
sh: subst ).
thf(push_decl,type,
push: term > subst > subst ).
thf(comp_decl,type,
comp: subst > subst > subst ).
thf(var_decl,type,
var: term > $o ).
thf(pushprop_lem1v2_decl,type,
pushprop_lem1v2: $o ).
thf(pushprop_lem1_gthm_decl,type,
pushprop_lem1_gthm: $o ).
thf(axmap_decl,type,
axmap: $o ).
thf(pushprop_lem0_gthm_decl,type,
pushprop_lem0_gthm: $o ).
thf(shinj_decl,type,
shinj: $o ).
thf(hoasinduction_lem1v2_decl,type,
hoasinduction_lem1v2: $o ).
thf(hoasinduction_lem1v2_gthm_decl,type,
hoasinduction_lem1v2_gthm: $o ).
thf(hoasap_decl,type,
hoasap: subst > term > subst > term > term ).
thf(induction2lem_decl,type,
induction2lem: $o ).
thf(hoasinduction_lem3v2_f_decl,type,
hoasinduction_lem3v2_f: $o ).
thf(axvarshift_decl,type,
axvarshift: $o ).
thf(hoasapinj2_decl,type,
hoasapinj2: $o ).
thf(hoasapnotvar_gthm_decl,type,
hoasapnotvar_gthm: $o ).
thf(hoasapinj1_decl,type,
hoasapinj1: $o ).
thf(ulamvar1_decl,type,
ulamvar1: $o ).
thf(induction2lem_lthm_decl,type,
induction2lem_lthm: $o ).
thf(hoasinduction_lem3v2_gthm_decl,type,
hoasinduction_lem3v2_gthm: $o ).
thf(apnotvar_decl,type,
apnotvar: $o ).
thf(pushprop_lthm_orig_decl,type,
pushprop_lthm_orig: $o ).
thf(hoasinduction_lem3v2_f_lthm_decl,type,
hoasinduction_lem3v2_f_lthm: $o ).
thf(hoasinduction_lthm_decl,type,
hoasinduction_lthm: $o ).
thf(hoasinduction_no_psi_cond_lthm_decl,type,
hoasinduction_no_psi_cond_lthm: $o ).
thf(hoaslaminj_decl,type,
hoaslaminj: $o ).
thf(hoasinduction_lem3aaa_decl,type,
hoasinduction_lem3aaa: $o ).
thf(induction2lem_gthm_decl,type,
induction2lem_gthm: $o ).
thf(hoasinduction_lem3aa_lthm_decl,type,
hoasinduction_lem3aa_lthm: $o ).
thf(hoasinduction_lem3_decl,type,
hoasinduction_lem3: $o ).
thf(hoasinduction_lem2_decl,type,
hoasinduction_lem2: $o ).
thf(termmset_lthm_decl,type,
termmset_lthm: $o ).
thf(hoasinduction_lem1_decl,type,
hoasinduction_lem1: $o ).
thf(hoaslamnotap_lthm_decl,type,
hoaslamnotap_lthm: $o ).
thf(pushprop_lem1v2_lthm_decl,type,
pushprop_lem1v2_lthm: $o ).
thf(hoasapnotvar_decl,type,
hoasapnotvar: $o ).
thf(hoasinduction_lem0_decl,type,
hoasinduction_lem0: $o ).
thf(hoasinduction_decl,type,
hoasinduction: $o ).
thf(hoasinduction_gthm_decl,type,
hoasinduction_gthm: $o ).
thf(axapp_decl,type,
axapp: $o ).
thf(hoaslamnotvar_lthm_decl,type,
hoaslamnotvar_lthm: $o ).
thf(pushprop_lem3v2_lthm_decl,type,
pushprop_lem3v2_lthm: $o ).
thf(hoasinduction_lem3b_lthm_decl,type,
hoasinduction_lem3b_lthm: $o ).
thf(ulamvarind_decl,type,
ulamvarind: $o ).
thf(induction_decl,type,
induction: $o ).
thf(hoasinduction_lem3a_lthm_decl,type,
hoasinduction_lem3a_lthm: $o ).
thf(termmset_gthm_decl,type,
termmset_gthm: $o ).
thf(hoasinduction_lem3aa_decl,type,
hoasinduction_lem3aa: $o ).
thf(pushprop_lem1v2_gthm_decl,type,
pushprop_lem1v2_gthm: $o ).
thf(hoaslamnotap_gthm_decl,type,
hoaslamnotap_gthm: $o ).
thf(hoaslamnotvar_gthm_decl,type,
hoaslamnotvar_gthm: $o ).
thf(hoasinduction_lem3b_gthm_decl,type,
hoasinduction_lem3b_gthm: $o ).
thf(pushprop_lem2v2_decl,type,
pushprop_lem2v2: $o ).
thf(hoasinduction_lem3a_gthm_decl,type,
hoasinduction_lem3a_gthm: $o ).
thf(axclos_decl,type,
axclos: $o ).
thf(axassoc_decl,type,
axassoc: $o ).
thf(hoasinduction_lem2v2_decl,type,
hoasinduction_lem2v2: $o ).
thf(pushprop_lthm_decl,type,
pushprop_lthm: $o ).
thf(apinj2_decl,type,
apinj2: $o ).
thf(apinj1_decl,type,
apinj1: $o ).
thf(hoasapinj2_lthm_decl,type,
hoasapinj2_lthm: $o ).
thf(hoasinduction_lem3v2a_decl,type,
hoasinduction_lem3v2a: $o ).
thf(hoasapinj1_lthm_decl,type,
hoasapinj1_lthm: $o ).
thf(hoaslaminj_lthm_decl,type,
hoaslaminj_lthm: $o ).
thf(axvarcons_decl,type,
axvarcons: $o ).
thf(hoaslam_decl,type,
hoaslam: subst > ( subst > term > term ) > term ).
thf(axscons_decl,type,
axscons: $o ).
thf(hoasinduction_lem2v2_gthm_decl,type,
hoasinduction_lem2v2_gthm: $o ).
thf(axidr_decl,type,
axidr: $o ).
thf(pushprop_lem1_decl,type,
pushprop_lem1: $o ).
thf(laminj_decl,type,
laminj: $o ).
thf(hoasinduction_lem3_lthm_decl,type,
hoasinduction_lem3_lthm: $o ).
thf(pushprop_lem0_decl,type,
pushprop_lem0: $o ).
thf(pushprop_gthm_decl,type,
pushprop_gthm: $o ).
thf(axabs_decl,type,
axabs: $o ).
thf(hoasinduction_lem3v2a_lthm_decl,type,
hoasinduction_lem3v2a_lthm: $o ).
thf(hoasinduction_lem2_lthm_decl,type,
hoasinduction_lem2_lthm: $o ).
thf(hoasapinj2_gthm_decl,type,
hoasapinj2_gthm: $o ).
thf(hoasinduction_p_and_p_prime_decl,type,
hoasinduction_p_and_p_prime: ( subst > term > subst > $o ) > ( term > $o ) > $o ).
thf(hoasinduction_lem1_lthm_decl,type,
hoasinduction_lem1_lthm: $o ).
thf(lamnotap_decl,type,
lamnotap: $o ).
thf(hoasapinj1_gthm_decl,type,
hoasapinj1_gthm: $o ).
thf(hoaslamnotvar_decl,type,
hoaslamnotvar: $o ).
thf(axidl_decl,type,
axidl: $o ).
thf(hoaslaminj_gthm_decl,type,
hoaslaminj_gthm: $o ).
thf(induction2_lthm_decl,type,
induction2_lthm: $o ).
thf(hoasinduction_lem0_lthm_decl,type,
hoasinduction_lem0_lthm: $o ).
thf(substmonoid_lthm_decl,type,
substmonoid_lthm: $o ).
thf(pushprop_decl,type,
pushprop: $o ).
thf(hoasinduction_lem3_gthm_decl,type,
hoasinduction_lem3_gthm: $o ).
thf(hoasinduction_lem2_gthm_decl,type,
hoasinduction_lem2_gthm: $o ).
thf(hoasinduction_lem3b_decl,type,
hoasinduction_lem3b: $o ).
thf(substmonoid_decl,type,
substmonoid: $o ).
thf(lamnotvar_decl,type,
lamnotvar: $o ).
thf(hoasinduction_lem3a_decl,type,
hoasinduction_lem3a: $o ).
thf(hoasinduction_lem1_gthm_decl,type,
hoasinduction_lem1_gthm: $o ).
thf(hoasinduction_no_psi_cond_decl,type,
hoasinduction_no_psi_cond: $o ).
thf(induction2_gthm_decl,type,
induction2_gthm: $o ).
thf(pushprop_lem2v2_lthm_decl,type,
pushprop_lem2v2_lthm: $o ).
thf(hoasvar_decl,type,
hoasvar: subst > term > subst > $o ).
thf(hoaslamnotap_decl,type,
hoaslamnotap: $o ).
thf(substmonoid_gthm_decl,type,
substmonoid_gthm: $o ).
thf(ulamvarsh_decl,type,
ulamvarsh: $o ).
thf(induction2_decl,type,
induction2: $o ).
thf(pushprop_lem3v2_decl,type,
pushprop_lem3v2: $o ).
thf(pushprop_lem2v2_gthm_decl,type,
pushprop_lem2v2_gthm: $o ).
thf(pushprop_lem1_lthm_decl,type,
pushprop_lem1_lthm: $o ).
thf(hoasinduction_lem3v2_decl,type,
hoasinduction_lem3v2: $o ).
thf(axshiftcons_decl,type,
axshiftcons: $o ).
thf(termmset_decl,type,
termmset: $o ).
thf(pushprop_lem0_lthm_decl,type,
pushprop_lem0_lthm: $o ).
thf(hoasapnotvar_lthm_decl,type,
hoasapnotvar_lthm: $o ).
thf(hoasinduction_lem3v2_lthm_decl,type,
hoasinduction_lem3v2_lthm: $o ).
thf(pushprop_p_and_p_prime_decl,type,
pushprop_p_and_p_prime: term > subst > ( term > $o ) > ( term > $o ) > $o ).
thf(axvarid_decl,type,
axvarid: $o ).
thf(hoasinduction_lthm_3_decl,type,
hoasinduction_lthm_3: $o ).
thf(d2term_decl,type,
d2term: d_term > term ).
thf(d2subst_decl,type,
d2subst: d_subst > subst ).
thf(d_one_decl,type,
d_one: d_term ).
thf(d_id_decl,type,
d_id: d_subst ).
thf(sk1_decl,type,
sk1: term > d_term ).
thf(sk2_decl,type,
sk2: subst > d_subst ).
thf(sk5_decl,type,
sk5: term ).
thf(sk6_decl,type,
sk6: subst ).
thf(sk7_decl,type,
sk7: subst ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: term] :
@+[B: d_term] :
( A
= ( d2term @ B ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: subst] :
@+[B: d_subst] :
( A
= ( d2subst @ B ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: term] :
~ ! [B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: subst] :
~ ! [B: subst] :
( ( sub @ ( sub @ sk5 @ A ) @ B )
= ( sub @ sk5 @ ( comp @ A @ B ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: subst] :
( ( sub @ ( sub @ sk5 @ sk6 ) @ A )
!= ( sub @ sk5 @ ( comp @ sk6 @ A ) ) ) ) ) ).
thf(3,axiom,
( ! [A: term] :
? [B: d_term] :
( A
= ( d2term @ B ) )
& ! [A: d_term] : ( A = d_one )
& ! [A: d_term,B: d_term] :
( ( ( d2term @ A )
= ( d2term @ B ) )
=> ( A = B ) )
& ! [A: subst] :
? [B: d_subst] :
( A
= ( d2subst @ B ) )
& ! [A: d_subst] : ( A = d_id )
& ! [A: d_subst,B: d_subst] :
( ( ( d2subst @ A )
= ( d2subst @ B ) )
=> ( A = B ) )
& ( 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
= ( ^ [A: subst,B: subst > term > term] : ( d2term @ d_one ) ) )
& ( hoasinduction_p_and_p_prime
= ( ^ [A: subst > term > subst > $o,B: term > $o] :
! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) ) ) )
& ( pushprop_p_and_p_prime
= ( ^ [A: term,B: subst,C: term > $o,D: term > $o] :
! [E: term] :
( ( D @ E )
= ( C @ ( sub @ E @ ( push @ A @ B ) ) ) ) ) )
& ~ ( var @ ( d2term @ d_one ) )
& ( pushprop_lem1v2
= ( ! [A: term > $o,B: term > $o,C: term,D: subst] :
( ~ ( A @ C )
| ~ ! [E: term] :
( ( B @ E )
= ( A @ ( sub @ E @ ( push @ C @ D ) ) ) )
| ( B @ 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
= ( ! [A: term > $o,B: term,C: subst] :
( ~ ! [D: term,E: term] :
( ~ ( A @ D )
| ~ ( A @ E )
| ( A @ ( ap @ D @ E ) ) )
| ~ ! [D: term] :
( ~ ! [E: term] :
( ~ ( A @ E )
| ( A @ ( sub @ D @ ( push @ E @ id ) ) ) )
| ( A @ ( lam @ D ) ) )
| ~ ! [D: term] :
( ~ ( var @ D )
| ( A @ ( sub @ D @ C ) ) )
| ( A @ ( sub @ B @ C ) ) ) ) )
& ( hoasinduction_lem3v2_f
= ( ! [A: term] :
~ ! [B: subst > term > term] :
~ ! [C: term,D: subst] :
( ( sub @ A @ ( push @ C @ D ) )
= ( B @ D @ C ) ) ) )
& 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,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) )
=> ( ! [A: subst] :
( A
= ( comp @ A @ id ) )
=> ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ( A @ C )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ! [A: term > $o,B: term,C: subst] :
( ~ ! [D: term,E: term] :
( ~ ( A @ D )
| ~ ( A @ E )
| ( A @ ( ap @ D @ E ) ) )
| ~ ! [D: term] :
( ~ ! [E: term] :
( ~ ( A @ E )
| ( A @ ( sub @ D @ ( push @ E @ id ) ) ) )
| ( A @ ( lam @ D ) ) )
| ~ ! [D: term] :
( ~ ( var @ D )
| ( A @ ( sub @ D @ C ) ) )
| ( A @ ( sub @ B @ C ) ) ) ) ) ) ) )
& hoasinduction_lem3v2_gthm
& apnotvar
& pushprop_lthm_orig
& ( hoasinduction_lem3v2_f_lthm
= ( ! [A: term] :
~ ! [B: subst > term > term] :
~ ! [C: term,D: subst] :
( ( sub @ A @ ( push @ C @ D ) )
= ( B @ D @ C ) ) ) )
& ( hoasinduction_lthm
= ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ( ! [A: subst > term > subst > $o,B: term,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: term,E: term] :
( ~ ( A @ id @ D @ id )
| ~ ( A @ id @ E @ id )
| ( A @ id @ ( ap @ ( sub @ D @ id ) @ E ) @ id ) )
| ~ ( A @ id @ B @ id )
| ~ ( A @ id @ C @ id )
| ( A @ id @ ( ap @ B @ C ) @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: term] :
( ~ ( var @ ( sub @ C @ id ) )
| ( A @ id @ C @ id ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) ) ) )
& ( hoasinduction_no_psi_cond_lthm
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) )
=> ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) ) ) ) )
& ( hoaslaminj
= ( ! [A: subst > term > term,B: subst > term > term,C: subst,D: term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( A @ E @ F ) @ G )
= ( A @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( B @ E @ F ) @ G )
= ( B @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ( ( lam @ ( A @ sh @ one ) )
!= ( lam @ ( B @ sh @ one ) ) )
| ( ( A @ C @ D )
= ( B @ C @ D ) ) ) ) )
& ( hoasinduction_lem3aaa
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term,D: term] :
( ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( C @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id )
| ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( C @ E @ F ) @ G )
= ( sub @ ( sub @ D @ ( push @ F @ E ) ) @ G ) )
| ~ ! [E: subst,F: term,G: subst] :
( ( C @ ( comp @ E @ G ) @ ( sub @ F @ G ) )
= ( sub @ D @ ( push @ ( sub @ F @ G ) @ ( comp @ E @ G ) ) ) ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& induction2lem_gthm
& ( hoasinduction_lem3aa_lthm
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& ( hoasinduction_lem3
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) )
& ( hoasinduction_lem2
= ( ! [A: subst > term > subst > $o,B: term,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: term,E: term] :
( ~ ( A @ id @ D @ id )
| ~ ( A @ id @ E @ id )
| ( A @ id @ ( ap @ ( sub @ D @ id ) @ E ) @ id ) )
| ~ ( A @ id @ B @ id )
| ~ ( A @ id @ C @ id )
| ( A @ id @ ( ap @ B @ C ) @ id ) ) ) )
& ( termmset_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [A: term] :
( A
= ( sub @ A @ id ) ) ) )
& hoasinduction_lem1
& hoaslamnotap_lthm
& ( pushprop_lem1v2_lthm
= ( ! [A: term,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ! [A: term > $o,B: term > $o,C: term,D: subst] :
( ~ ( A @ C )
| ~ ! [E: term] :
( ( B @ E )
= ( A @ ( sub @ E @ ( push @ C @ D ) ) ) )
| ( B @ one ) ) ) )
& hoasapnotvar
& ( hoasinduction_lem0
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) ) ) )
& ( hoasinduction
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: term] :
( ~ ( var @ ( sub @ C @ id ) )
| ( A @ id @ C @ id ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) )
& hoasinduction_gthm
& axapp
& hoaslamnotvar_lthm
& pushprop_lem3v2_lthm
& ( hoasinduction_lem3b_lthm
= ( ! [A: term] :
~ ! [B: subst > term > term] :
( ( B @ sh @ one )
!= ( sub @ A @ ( push @ one @ sh ) ) ) ) )
& ulamvarind
& ( induction
= ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ( A @ C )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) ) ) )
& ( hoasinduction_lem3a_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) ) )
& termmset_gthm
& ( hoasinduction_lem3aa
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& pushprop_lem1v2_gthm
& hoaslamnotap_gthm
& hoaslamnotvar_gthm
& hoasinduction_lem3b_gthm
& pushprop_lem2v2
& hoasinduction_lem3a_gthm
& axclos
& axassoc
& ( hoasinduction_lem2v2
= ( ! [A: subst > term > subst > $o,B: term > $o,C: term,D: term] :
( ~ ! [E: subst,F: term,G: subst,H: subst] :
( ~ ( A @ E @ F @ ( comp @ H @ G ) )
| ( A @ ( comp @ E @ H ) @ ( sub @ F @ H ) @ G ) )
| ~ ! [E: subst,F: term,G: subst,H: subst] :
( ~ ( A @ ( comp @ E @ H ) @ ( sub @ F @ H ) @ G )
| ( A @ E @ F @ ( comp @ H @ G ) ) )
| ~ ! [E: term,F: term] :
( ~ ( A @ id @ E @ id )
| ~ ( A @ id @ F @ id )
| ( A @ id @ ( ap @ ( sub @ E @ id ) @ F ) @ id ) )
| ~ ! [E: term] :
( ( B @ E )
= ( A @ id @ E @ id ) )
| ~ ( B @ C )
| ~ ( B @ D )
| ( B @ ( ap @ C @ D ) ) ) ) )
& 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
= ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) )
& ( 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,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) )
=> ! [A: subst > term > term,B: subst > term > term,C: subst,D: term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( A @ E @ F ) @ G )
= ( A @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( B @ E @ F ) @ G )
= ( B @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ( ( lam @ ( A @ sh @ one ) )
!= ( lam @ ( B @ sh @ one ) ) )
| ( ( A @ C @ D )
= ( B @ C @ D ) ) ) ) ) ) )
& ( axvarcons
= ( ! [A: term,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) ) ) )
& ( axscons
= ( ! [A: subst] :
( A
= ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) ) ) ) )
& hoasinduction_lem2v2_gthm
& ( axidr
= ( ! [A: subst] :
( A
= ( comp @ A @ id ) ) ) )
& ( pushprop_lem1
= ( ! [A: term > $o,B: term > $o,C: term,D: subst,E: term] :
( ~ ( A @ C )
| ( B @ ( sub @ C @ ( push @ E @ D ) ) ) ) ) )
& ( laminj
= ( ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) ) ) )
& ( hoasinduction_lem3_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) ) )
& ( pushprop_lem0
= ( ! [A: term > $o,B: term,C: subst] :
~ ! [D: term > $o] :
~ ! [E: term] :
( ( D @ E )
= ( A @ ( sub @ E @ ( push @ B @ C ) ) ) ) ) )
& pushprop_gthm
& axabs
& ( hoasinduction_lem3v2a_lthm
= ( ! [A: term] :
~ ! [B: subst > term > term] :
~ ! [C: term,D: subst] :
( ( sub @ A @ ( push @ C @ D ) )
= ( B @ D @ C ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) ) )
& hoasinduction_lem2_lthm
& hoasapinj2_gthm
& hoasinduction_lem1_lthm
& ~ lamnotap
& hoasapinj1_gthm
& hoaslamnotvar
& ( axidl
= ( ! [A: subst] :
( A
= ( comp @ id @ A ) ) ) )
& hoaslaminj_gthm
& ( induction2_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: term > $o,B: term,C: subst] :
( ~ ! [D: term,E: term] :
( ~ ( A @ D )
| ~ ( A @ E )
| ( A @ ( ap @ D @ E ) ) )
| ~ ! [D: term] :
( ~ ! [E: term] :
( ~ ( A @ E )
| ( A @ ( sub @ D @ ( push @ E @ id ) ) ) )
| ( A @ ( lam @ D ) ) )
| ~ ! [D: term] :
( ~ ( var @ D )
| ( A @ ( sub @ D @ C ) ) )
| ( A @ ( sub @ B @ C ) ) )
=> ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) ) ) ) )
& ( hoasinduction_lem0_lthm
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) ) ) )
& ( substmonoid_lthm
= ( ! [A: subst] :
( A
= ( comp @ id @ A ) )
=> ( ! [A: subst] :
( A
= ( comp @ A @ id ) )
=> ( ! [A: subst] :
( A
= ( comp @ id @ A ) )
& ! [A: subst] :
( A
= ( comp @ A @ id ) ) ) ) ) )
& pushprop
& hoasinduction_lem3_gthm
& hoasinduction_lem2_gthm
& ( hoasinduction_lem3b
= ( ! [A: term] :
~ ! [B: subst > term > term] :
( ( B @ sh @ one )
!= ( sub @ A @ ( push @ one @ sh ) ) ) ) )
& ( substmonoid
= ( ! [A: subst] :
( A
= ( comp @ id @ A ) )
& ! [A: subst] :
( A
= ( comp @ A @ id ) ) ) )
& lamnotvar
& ( hoasinduction_lem3a
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) )
& hoasinduction_lem1_gthm
& ( hoasinduction_no_psi_cond
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) )
& induction2_gthm
& pushprop_lem2v2_lthm
& ~ ( hoasvar @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
& ( hoaslamnotap
= ( ! [A: subst > term > term,B: term,C: term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( A @ D @ E ) @ F )
= ( A @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ( ( lam @ ( A @ sh @ one ) )
!= ( ap @ ( sub @ B @ id ) @ C ) ) ) ) )
& substmonoid_gthm
& ulamvarsh
& ( induction2
= ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) ) ) )
& pushprop_lem3v2
& pushprop_lem2v2_gthm
& ( pushprop_lem1_lthm
= ( ! [A: term,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) )
=> ! [A: term > $o,B: term > $o,C: term,D: subst,E: term] :
( ~ ( A @ C )
| ( B @ ( sub @ C @ ( push @ E @ D ) ) ) ) ) ) )
& ( hoasinduction_lem3v2
= ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) )
& ( axshiftcons
= ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) ) ) )
& ( termmset
= ( ! [A: term] :
( A
= ( sub @ A @ id ) ) ) )
& ( pushprop_lem0_lthm
= ( ! [A: term > $o,B: term,C: subst] :
~ ! [D: term > $o] :
~ ! [E: term] :
( ( D @ E )
= ( A @ ( sub @ E @ ( push @ B @ C ) ) ) ) ) )
& hoasapnotvar_lthm
& ( hoasinduction_lem3v2_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) )
& ( axvarid
= ( ! [A: term] :
( A
= ( sub @ A @ id ) ) ) )
& ( hoasinduction_lthm_3
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) )
=> ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: term] :
( ~ ( var @ ( sub @ C @ id ) )
| ( A @ id @ C @ id ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alg444_1) ).
thf(6,plain,
( ! [A: term] :
? [B: d_term] :
( A
= ( d2term @ B ) )
& ! [A: d_term] : ( A = d_one )
& ! [A: d_term,B: d_term] :
( ( ( d2term @ A )
= ( d2term @ B ) )
=> ( A = B ) )
& ! [A: subst] :
? [B: d_subst] :
( A
= ( d2subst @ B ) )
& ! [A: d_subst] : ( A = d_id )
& ! [A: d_subst,B: d_subst] :
( ( ( d2subst @ A )
= ( d2subst @ B ) )
=> ( A = B ) )
& ( 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
= ( ^ [A: subst,B: subst > term > term] : ( d2term @ d_one ) ) )
& ( hoasinduction_p_and_p_prime
= ( ^ [A: subst > term > subst > $o,B: term > $o] :
! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) ) ) )
& ( pushprop_p_and_p_prime
= ( ^ [A: term,B: subst,C: term > $o,D: term > $o] :
! [E: term] :
( ( D @ E )
= ( C @ ( sub @ E @ ( push @ A @ B ) ) ) ) ) )
& ~ ( var @ ( d2term @ d_one ) )
& ( pushprop_lem1v2
= ( ! [A: term > $o,B: term > $o,C: term,D: subst] :
( ~ ( A @ C )
| ~ ! [E: term] :
( ( B @ E )
= ( A @ ( sub @ E @ ( push @ C @ D ) ) ) )
| ( B @ 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
= ( ! [A: term > $o,B: term,C: subst] :
( ~ ! [D: term,E: term] :
( ~ ( A @ D )
| ~ ( A @ E )
| ( A @ ( ap @ D @ E ) ) )
| ~ ! [D: term] :
( ~ ! [E: term] :
( ~ ( A @ E )
| ( A @ ( sub @ D @ ( push @ E @ id ) ) ) )
| ( A @ ( lam @ D ) ) )
| ~ ! [D: term] :
( ~ ( var @ D )
| ( A @ ( sub @ D @ C ) ) )
| ( A @ ( sub @ B @ C ) ) ) ) )
& ( hoasinduction_lem3v2_f
= ( ! [A: term] :
~ ! [B: subst > term > term] :
~ ! [C: term,D: subst] :
( ( sub @ A @ ( push @ C @ D ) )
= ( B @ D @ C ) ) ) )
& 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,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) )
=> ( ! [A: subst] :
( A
= ( comp @ A @ id ) )
=> ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ( A @ C )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ! [A: term > $o,B: term,C: subst] :
( ~ ! [D: term,E: term] :
( ~ ( A @ D )
| ~ ( A @ E )
| ( A @ ( ap @ D @ E ) ) )
| ~ ! [D: term] :
( ~ ! [E: term] :
( ~ ( A @ E )
| ( A @ ( sub @ D @ ( push @ E @ id ) ) ) )
| ( A @ ( lam @ D ) ) )
| ~ ! [D: term] :
( ~ ( var @ D )
| ( A @ ( sub @ D @ C ) ) )
| ( A @ ( sub @ B @ C ) ) ) ) ) ) ) )
& hoasinduction_lem3v2_gthm
& apnotvar
& pushprop_lthm_orig
& ( hoasinduction_lem3v2_f_lthm
= ( ! [A: term] :
~ ! [B: subst > term > term] :
~ ! [C: term,D: subst] :
( ( sub @ A @ ( push @ C @ D ) )
= ( B @ D @ C ) ) ) )
& ( hoasinduction_lthm
= ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ( ! [A: subst > term > subst > $o,B: term,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: term,E: term] :
( ~ ( A @ id @ D @ id )
| ~ ( A @ id @ E @ id )
| ( A @ id @ ( ap @ ( sub @ D @ id ) @ E ) @ id ) )
| ~ ( A @ id @ B @ id )
| ~ ( A @ id @ C @ id )
| ( A @ id @ ( ap @ B @ C ) @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: term] :
( ~ ( var @ ( sub @ C @ id ) )
| ( A @ id @ C @ id ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) ) ) )
& ( hoasinduction_no_psi_cond_lthm
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) )
=> ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) ) ) ) )
& ( hoaslaminj
= ( ! [A: subst > term > term,B: subst > term > term,C: subst,D: term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( A @ E @ F ) @ G )
= ( A @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( B @ E @ F ) @ G )
= ( B @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ( ( lam @ ( A @ sh @ one ) )
!= ( lam @ ( B @ sh @ one ) ) )
| ( ( A @ C @ D )
= ( B @ C @ D ) ) ) ) )
& ( hoasinduction_lem3aaa
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term,D: term] :
( ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( C @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id )
| ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( C @ E @ F ) @ G )
= ( sub @ ( sub @ D @ ( push @ F @ E ) ) @ G ) )
| ~ ! [E: subst,F: term,G: subst] :
( ( C @ ( comp @ E @ G ) @ ( sub @ F @ G ) )
= ( sub @ D @ ( push @ ( sub @ F @ G ) @ ( comp @ E @ G ) ) ) ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& induction2lem_gthm
& ( hoasinduction_lem3aa_lthm
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& ( hoasinduction_lem3
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) )
& ( hoasinduction_lem2
= ( ! [A: subst > term > subst > $o,B: term,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: term,E: term] :
( ~ ( A @ id @ D @ id )
| ~ ( A @ id @ E @ id )
| ( A @ id @ ( ap @ ( sub @ D @ id ) @ E ) @ id ) )
| ~ ( A @ id @ B @ id )
| ~ ( A @ id @ C @ id )
| ( A @ id @ ( ap @ B @ C ) @ id ) ) ) )
& termmset_lthm
& hoasinduction_lem1
& hoaslamnotap_lthm
& ( pushprop_lem1v2_lthm
= ( ! [A: term,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ! [A: term > $o,B: term > $o,C: term,D: subst] :
( ~ ( A @ C )
| ~ ! [E: term] :
( ( B @ E )
= ( A @ ( sub @ E @ ( push @ C @ D ) ) ) )
| ( B @ one ) ) ) )
& hoasapnotvar
& ( hoasinduction_lem0
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) ) ) )
& ( hoasinduction
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: term] :
( ~ ( var @ ( sub @ C @ id ) )
| ( A @ id @ C @ id ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) )
& hoasinduction_gthm
& axapp
& hoaslamnotvar_lthm
& pushprop_lem3v2_lthm
& ( hoasinduction_lem3b_lthm
= ( ! [A: term] :
~ ! [B: subst > term > term] :
( ( B @ sh @ one )
!= ( sub @ A @ ( push @ one @ sh ) ) ) ) )
& ulamvarind
& ( induction
= ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ( A @ C )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) ) ) )
& ( hoasinduction_lem3a_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) ) )
& termmset_gthm
& ( hoasinduction_lem3aa
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& pushprop_lem1v2_gthm
& hoaslamnotap_gthm
& hoaslamnotvar_gthm
& hoasinduction_lem3b_gthm
& pushprop_lem2v2
& hoasinduction_lem3a_gthm
& axclos
& axassoc
& ( hoasinduction_lem2v2
= ( ! [A: subst > term > subst > $o,B: term > $o,C: term,D: term] :
( ~ ! [E: subst,F: term,G: subst,H: subst] :
( ~ ( A @ E @ F @ ( comp @ H @ G ) )
| ( A @ ( comp @ E @ H ) @ ( sub @ F @ H ) @ G ) )
| ~ ! [E: subst,F: term,G: subst,H: subst] :
( ~ ( A @ ( comp @ E @ H ) @ ( sub @ F @ H ) @ G )
| ( A @ E @ F @ ( comp @ H @ G ) ) )
| ~ ! [E: term,F: term] :
( ~ ( A @ id @ E @ id )
| ~ ( A @ id @ F @ id )
| ( A @ id @ ( ap @ ( sub @ E @ id ) @ F ) @ id ) )
| ~ ! [E: term] :
( ( B @ E )
= ( A @ id @ E @ id ) )
| ~ ( B @ C )
| ~ ( B @ D )
| ( B @ ( ap @ C @ D ) ) ) ) )
& 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
= ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) )
& ( 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,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) )
=> ! [A: subst > term > term,B: subst > term > term,C: subst,D: term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( A @ E @ F ) @ G )
= ( A @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( B @ E @ F ) @ G )
= ( B @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ( ( lam @ ( A @ sh @ one ) )
!= ( lam @ ( B @ sh @ one ) ) )
| ( ( A @ C @ D )
= ( B @ C @ D ) ) ) ) ) ) )
& ( axvarcons
= ( ! [A: term,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) ) ) )
& ( axscons
= ( ! [A: subst] :
( A
= ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) ) ) ) )
& hoasinduction_lem2v2_gthm
& ( axidr
= ( ! [A: subst] :
( A
= ( comp @ A @ id ) ) ) )
& ( pushprop_lem1
= ( ! [A: term > $o,B: term > $o,C: term,D: subst,E: term] :
( ~ ( A @ C )
| ( B @ ( sub @ C @ ( push @ E @ D ) ) ) ) ) )
& ( laminj
= ( ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) ) ) )
& ( hoasinduction_lem3_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ ( sub @ B @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) ) )
& ( pushprop_lem0
= ( ! [A: term > $o,B: term,C: subst] :
~ ! [D: term > $o] :
~ ! [E: term] :
( ( D @ E )
= ( A @ ( sub @ E @ ( push @ B @ C ) ) ) ) ) )
& pushprop_gthm
& axabs
& ( hoasinduction_lem3v2a_lthm
= ( ! [A: term] :
~ ! [B: subst > term > term] :
~ ! [C: term,D: subst] :
( ( sub @ A @ ( push @ C @ D ) )
= ( B @ D @ C ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) ) )
& hoasinduction_lem2_lthm
& hoasapinj2_gthm
& hoasinduction_lem1_lthm
& ~ lamnotap
& hoasapinj1_gthm
& hoaslamnotvar
& ( axidl
= ( ! [A: subst] :
( A
= ( comp @ id @ A ) ) ) )
& hoaslaminj_gthm
& ( induction2_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: term > $o,B: term,C: subst] :
( ~ ! [D: term,E: term] :
( ~ ( A @ D )
| ~ ( A @ E )
| ( A @ ( ap @ D @ E ) ) )
| ~ ! [D: term] :
( ~ ! [E: term] :
( ~ ( A @ E )
| ( A @ ( sub @ D @ ( push @ E @ id ) ) ) )
| ( A @ ( lam @ D ) ) )
| ~ ! [D: term] :
( ~ ( var @ D )
| ( A @ ( sub @ D @ C ) ) )
| ( A @ ( sub @ B @ C ) ) )
=> ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) ) ) ) )
& ( hoasinduction_lem0_lthm
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) ) ) )
& ( substmonoid_lthm
= ( ! [A: subst] :
( A
= ( comp @ id @ A ) )
=> ( ! [A: subst] :
( A
= ( comp @ A @ id ) )
=> ( ! [A: subst] :
( A
= ( comp @ id @ A ) )
& ! [A: subst] :
( A
= ( comp @ A @ id ) ) ) ) ) )
& pushprop
& hoasinduction_lem3_gthm
& hoasinduction_lem2_gthm
& ( hoasinduction_lem3b
= ( ! [A: term] :
~ ! [B: subst > term > term] :
( ( B @ sh @ one )
!= ( sub @ A @ ( push @ one @ sh ) ) ) ) )
& ( substmonoid
= ( ! [A: subst] :
( A
= ( comp @ id @ A ) )
& ! [A: subst] :
( A
= ( comp @ A @ id ) ) ) )
& lamnotvar
& ( hoasinduction_lem3a
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ~ ! [C: term] :
( ~ ( A @ id @ C @ id )
| ( A @ id @ ( sub @ B @ ( push @ C @ id ) ) @ id ) )
| ( A @ id @ ( lam @ B ) @ id ) ) ) )
& hoasinduction_lem1_gthm
& ( hoasinduction_no_psi_cond
= ( ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) )
& induction2_gthm
& pushprop_lem2v2_lthm
& ~ ( hoasvar @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
& ( hoaslamnotap
= ( ! [A: subst > term > term,B: term,C: term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( A @ D @ E ) @ F )
= ( A @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ( ( lam @ ( A @ sh @ one ) )
!= ( ap @ ( sub @ B @ id ) @ C ) ) ) ) )
& substmonoid_gthm
& ulamvarsh
& ( induction2
= ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) ) ) )
& pushprop_lem3v2
& pushprop_lem2v2_gthm
& ( pushprop_lem1_lthm
= ( ! [A: term,B: subst] :
( A
= ( sub @ one @ ( push @ A @ B ) ) )
=> ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) )
=> ! [A: term > $o,B: term > $o,C: term,D: subst,E: term] :
( ~ ( A @ C )
| ( B @ ( sub @ C @ ( push @ E @ D ) ) ) ) ) ) )
& ( hoasinduction_lem3v2
= ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) )
& ( axshiftcons
= ( ! [A: term,B: subst] :
( B
= ( comp @ sh @ ( push @ A @ B ) ) ) ) )
& ( termmset
= ( ! [A: term] :
( A
= ( sub @ A @ id ) ) ) )
& ( pushprop_lem0_lthm
= ( ! [A: term > $o,B: term,C: subst] :
~ ! [D: term > $o] :
~ ! [E: term] :
( ( D @ E )
= ( A @ ( sub @ E @ ( push @ B @ C ) ) ) ) ) )
& hoasapnotvar_lthm
& ( hoasinduction_lem3v2_lthm
= ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ D @ E @ ( comp @ G @ F ) )
| ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F ) )
| ~ ! [D: subst,E: term,F: subst,G: subst] :
( ~ ( A @ ( comp @ D @ G ) @ ( sub @ E @ G ) @ F )
| ( A @ D @ E @ ( comp @ G @ F ) ) )
| ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) ) ) )
& ( axvarid
= ( ! [A: term] :
( A
= ( sub @ A @ id ) ) ) )
& ( hoasinduction_lthm_3
= ( ! [A: subst > term > subst > $o] :
~ ! [B: term > $o] :
~ ! [C: term] :
( ( B @ C )
= ( A @ id @ C @ id ) )
=> ( ! [A: term > $o,B: term] :
( ~ ! [C: term] :
( ~ ( var @ C )
| ( A @ C ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ C )
| ~ ( A @ D )
| ( A @ ( ap @ C @ D ) ) )
| ~ ! [C: term] :
( ~ ! [D: term] :
( ~ ( A @ D )
| ( A @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( A @ ( lam @ C ) ) )
| ( A @ B ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: subst > term > subst > $o,B: term > $o,C: term] :
( ~ ! [D: subst > term > term] :
( ~ ! [E: subst,F: term,G: subst] :
( ( sub @ ( D @ E @ F ) @ G )
= ( D @ ( comp @ E @ G ) @ ( sub @ F @ G ) ) )
| ~ ! [E: term] :
( ~ ( A @ id @ E @ id )
| ( A @ id @ ( D @ id @ E ) @ id ) )
| ( A @ id @ ( lam @ ( D @ sh @ one ) ) @ id ) )
| ~ ! [D: term] :
( ( B @ D )
= ( A @ id @ D @ id ) )
| ~ ! [D: term] :
( ~ ( B @ D )
| ( B @ ( sub @ C @ ( push @ D @ id ) ) ) )
| ( B @ ( lam @ C ) ) )
=> ! [A: subst > term > subst > $o,B: term] :
( ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ C @ D @ ( comp @ F @ E ) )
| ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E ) )
| ~ ! [C: subst,D: term,E: subst,F: subst] :
( ~ ( A @ ( comp @ C @ F ) @ ( sub @ D @ F ) @ E )
| ( A @ C @ D @ ( comp @ F @ E ) ) )
| ~ ! [C: term] :
( ~ ( var @ ( sub @ C @ id ) )
| ( A @ id @ C @ id ) )
| ~ ! [C: term,D: term] :
( ~ ( A @ id @ C @ id )
| ~ ( A @ id @ D @ id )
| ( A @ id @ ( ap @ ( sub @ C @ id ) @ D ) @ id ) )
| ~ ! [C: subst > term > term] :
( ~ ! [D: subst,E: term,F: subst] :
( ( sub @ ( C @ D @ E ) @ F )
= ( C @ ( comp @ D @ F ) @ ( sub @ E @ F ) ) )
| ~ ! [D: term] :
( ~ ( A @ id @ D @ id )
| ( A @ id @ ( C @ id @ D ) @ id ) )
| ( A @ id @ ( lam @ ( C @ sh @ one ) ) @ id ) )
| ( A @ id @ B @ id ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(7,plain,
! [H: d_subst,G: d_subst,F: d_subst,E: subst,D: d_term,C: d_term,B: d_term,A: term] :
( ( A
= ( d2term @ ( sk1 @ A ) ) )
& ( B = d_one )
& ( ( ( d2term @ C )
!= ( d2term @ D ) )
| ( C = D ) )
& ( E
= ( d2subst @ ( sk2 @ E ) ) )
& ( F = d_id )
& ( ( ( d2subst @ G )
!= ( d2subst @ H ) )
| ( G = H ) )
& ( 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
= ( ^ [I: subst,J: subst > term > term] : ( d2term @ d_one ) ) )
& ( hoasinduction_p_and_p_prime
= ( ^ [I: subst > term > subst > $o,J: term > $o] :
! [K: term] :
( ( J @ K )
= ( I @ id @ K @ id ) ) ) )
& ( pushprop_p_and_p_prime
= ( ^ [I: term,J: subst,K: term > $o,L: term > $o] :
! [M: term] :
( ( L @ M )
= ( K @ ( sub @ M @ ( push @ I @ J ) ) ) ) ) )
& ~ ( var @ ( d2term @ d_one ) )
& ( pushprop_lem1v2
= ( ! [I: term > $o,J: term > $o,K: term,L: subst] :
( ~ ( I @ K )
| ~ ! [M: term] :
( ( J @ M )
= ( I @ ( sub @ M @ ( push @ K @ L ) ) ) )
| ( J @ one ) ) ) )
& pushprop_lem1_gthm
& axmap
& pushprop_lem0_gthm
& ( shinj
= ( ! [I: term,J: term] :
( ( ( sub @ I @ sh )
!= ( sub @ J @ sh ) )
| ( I = J ) ) ) )
& hoasinduction_lem1v2
& hoasinduction_lem1v2_gthm
& ( induction2lem
= ( ! [I: term > $o,J: term,K: subst] :
( ~ ! [L: term,M: term] :
( ~ ( I @ L )
| ~ ( I @ M )
| ( I @ ( ap @ L @ M ) ) )
| ~ ! [L: term] :
( ~ ! [M: term] :
( ~ ( I @ M )
| ( I @ ( sub @ L @ ( push @ M @ id ) ) ) )
| ( I @ ( lam @ L ) ) )
| ~ ! [L: term] :
( ~ ( var @ L )
| ( I @ ( sub @ L @ K ) ) )
| ( I @ ( sub @ J @ K ) ) ) ) )
& ( hoasinduction_lem3v2_f
= ( ! [I: term] :
~ ! [J: subst > term > term] :
~ ! [K: term,L: subst] :
( ( sub @ I @ ( push @ K @ L ) )
= ( J @ L @ K ) ) ) )
& axvarshift
& ( hoasapinj2
= ( ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ ( sub @ I @ id ) @ K )
!= ( ap @ ( sub @ J @ id ) @ L ) )
| ( K = L ) ) ) )
& hoasapnotvar_gthm
& ( hoasapinj1
= ( ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ ( sub @ I @ id ) @ K )
!= ( ap @ ( sub @ J @ id ) @ L ) )
| ( I = J ) ) ) )
& ~ ulamvar1
& ( induction2lem_lthm
= ( ! [I: term,J: subst] :
( I
= ( sub @ one @ ( push @ I @ J ) ) )
=> ( ! [I: term,J: subst] :
( J
= ( comp @ sh @ ( push @ I @ J ) ) )
=> ( ! [I: subst] :
( I
= ( comp @ I @ id ) )
=> ( ! [I: term > $o,J: term] :
( ~ ! [K: term] :
( ~ ( var @ K )
| ( I @ K ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ K )
| ~ ( I @ L )
| ( I @ ( ap @ K @ L ) ) )
| ~ ! [K: term] :
( ~ ( I @ K )
| ( I @ ( lam @ K ) ) )
| ( I @ J ) )
=> ! [I: term > $o,J: term,K: subst] :
( ~ ! [L: term,M: term] :
( ~ ( I @ L )
| ~ ( I @ M )
| ( I @ ( ap @ L @ M ) ) )
| ~ ! [L: term] :
( ~ ! [M: term] :
( ~ ( I @ M )
| ( I @ ( sub @ L @ ( push @ M @ id ) ) ) )
| ( I @ ( lam @ L ) ) )
| ~ ! [L: term] :
( ~ ( var @ L )
| ( I @ ( sub @ L @ K ) ) )
| ( I @ ( sub @ J @ K ) ) ) ) ) ) ) )
& hoasinduction_lem3v2_gthm
& apnotvar
& pushprop_lthm_orig
& ( hoasinduction_lem3v2_f_lthm
= ( ! [I: term] :
~ ! [J: subst > term > term] :
~ ! [K: term,L: subst] :
( ( sub @ I @ ( push @ K @ L ) )
= ( J @ L @ K ) ) ) )
& ( hoasinduction_lthm
= ( ! [I: term > $o,J: term] :
( ~ ! [K: term] :
( ~ ( var @ K )
| ( I @ K ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ K )
| ~ ( I @ L )
| ( I @ ( ap @ K @ L ) ) )
| ~ ! [K: term] :
( ~ ! [L: term] :
( ~ ( I @ L )
| ( I @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( I @ ( lam @ K ) ) )
| ( I @ J ) )
=> ( ! [I: subst > term > subst > $o,J: term,K: term] :
( ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ L @ M @ ( comp @ O @ N ) )
| ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N ) )
| ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N )
| ( I @ L @ M @ ( comp @ O @ N ) ) )
| ~ ! [L: term,M: term] :
( ~ ( I @ id @ L @ id )
| ~ ( I @ id @ M @ id )
| ( I @ id @ ( ap @ ( sub @ L @ id ) @ M ) @ id ) )
| ~ ( I @ id @ J @ id )
| ~ ( I @ id @ K @ id )
| ( I @ id @ ( ap @ J @ K ) @ id ) )
=> ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ K @ L @ ( comp @ N @ M ) )
| ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M ) )
| ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M )
| ( I @ K @ L @ ( comp @ N @ M ) ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ J ) @ id ) )
=> ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ K @ L @ ( comp @ N @ M ) )
| ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M ) )
| ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M )
| ( I @ K @ L @ ( comp @ N @ M ) ) )
| ~ ! [K: term] :
( ~ ( var @ ( sub @ K @ id ) )
| ( I @ id @ K @ id ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ id @ K @ id )
| ~ ( I @ id @ L @ id )
| ( I @ id @ ( ap @ ( sub @ K @ id ) @ L ) @ id ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ( I @ id @ J @ id ) ) ) ) ) )
& ( hoasinduction_no_psi_cond_lthm
= ( ! [I: subst > term > subst > $o] :
~ ! [J: term > $o] :
~ ! [K: term] :
( ( J @ K )
= ( I @ id @ K @ id ) )
=> ( ! [I: term > $o,J: term] :
( ~ ! [K: term] :
( ~ ( var @ K )
| ( I @ K ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ K )
| ~ ( I @ L )
| ( I @ ( ap @ K @ L ) ) )
| ~ ! [K: term] :
( ~ ! [L: term] :
( ~ ( I @ L )
| ( I @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( I @ ( lam @ K ) ) )
| ( I @ J ) )
=> ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ( ! [I: subst > term > subst > $o,J: term > $o,K: term] :
( ~ ! [L: subst > term > term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( L @ M @ N ) @ O )
= ( L @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: term] :
( ~ ( I @ id @ M @ id )
| ( I @ id @ ( L @ id @ M ) @ id ) )
| ( I @ id @ ( lam @ ( L @ sh @ one ) ) @ id ) )
| ~ ! [L: term] :
( ( J @ L )
= ( I @ id @ L @ id ) )
| ~ ! [L: term] :
( ~ ( J @ L )
| ( J @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( J @ ( lam @ K ) ) )
=> ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: term,L: term] :
( ~ ( I @ id @ K @ id )
| ~ ( I @ id @ L @ id )
| ( I @ id @ ( ap @ ( sub @ K @ id ) @ L ) @ id ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ( I @ id @ J @ id ) ) ) ) ) ) )
& ( hoaslaminj
= ( ! [I: subst > term > term,J: subst > term > term,K: subst,L: term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( I @ M @ N ) @ O )
= ( I @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( J @ M @ N ) @ O )
= ( J @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ( ( lam @ ( I @ sh @ one ) )
!= ( lam @ ( J @ sh @ one ) ) )
| ( ( I @ K @ L )
= ( J @ K @ L ) ) ) ) )
& ( hoasinduction_lem3aaa
= ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst > term > term,L: term] :
( ~ ! [M: term] :
( ~ ( I @ id @ M @ id )
| ( I @ id @ ( K @ id @ M ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id )
| ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( K @ M @ N ) @ O )
= ( sub @ ( sub @ L @ ( push @ N @ M ) ) @ O ) )
| ~ ! [M: subst,N: term,O: subst] :
( ( K @ ( comp @ M @ O ) @ ( sub @ N @ O ) )
= ( sub @ L @ ( push @ ( sub @ N @ O ) @ ( comp @ M @ O ) ) ) ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ ( sub @ J @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& induction2lem_gthm
& ( hoasinduction_lem3aa_lthm
= ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ ( sub @ J @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& ( hoasinduction_lem3
= ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ K @ L @ ( comp @ N @ M ) )
| ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M ) )
| ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M )
| ( I @ K @ L @ ( comp @ N @ M ) ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ J ) @ id ) ) ) )
& ( hoasinduction_lem2
= ( ! [I: subst > term > subst > $o,J: term,K: term] :
( ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ L @ M @ ( comp @ O @ N ) )
| ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N ) )
| ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N )
| ( I @ L @ M @ ( comp @ O @ N ) ) )
| ~ ! [L: term,M: term] :
( ~ ( I @ id @ L @ id )
| ~ ( I @ id @ M @ id )
| ( I @ id @ ( ap @ ( sub @ L @ id ) @ M ) @ id ) )
| ~ ( I @ id @ J @ id )
| ~ ( I @ id @ K @ id )
| ( I @ id @ ( ap @ J @ K ) @ id ) ) ) )
& termmset_lthm
& hoasinduction_lem1
& hoaslamnotap_lthm
& ( pushprop_lem1v2_lthm
= ( ! [I: term,J: subst] :
( I
= ( sub @ one @ ( push @ I @ J ) ) )
=> ! [I: term > $o,J: term > $o,K: term,L: subst] :
( ~ ( I @ K )
| ~ ! [M: term] :
( ( J @ M )
= ( I @ ( sub @ M @ ( push @ K @ L ) ) ) )
| ( J @ one ) ) ) )
& hoasapnotvar
& ( hoasinduction_lem0
= ( ! [I: subst > term > subst > $o] :
~ ! [J: term > $o] :
~ ! [K: term] :
( ( J @ K )
= ( I @ id @ K @ id ) ) ) )
& ( hoasinduction
= ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ K @ L @ ( comp @ N @ M ) )
| ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M ) )
| ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M )
| ( I @ K @ L @ ( comp @ N @ M ) ) )
| ~ ! [K: term] :
( ~ ( var @ ( sub @ K @ id ) )
| ( I @ id @ K @ id ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ id @ K @ id )
| ~ ( I @ id @ L @ id )
| ( I @ id @ ( ap @ ( sub @ K @ id ) @ L ) @ id ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ( I @ id @ J @ id ) ) ) )
& hoasinduction_gthm
& axapp
& hoaslamnotvar_lthm
& pushprop_lem3v2_lthm
& ( hoasinduction_lem3b_lthm
= ( ! [I: term] :
~ ! [J: subst > term > term] :
( ( J @ sh @ one )
!= ( sub @ I @ ( push @ one @ sh ) ) ) ) )
& ulamvarind
& ( induction
= ( ! [I: term > $o,J: term] :
( ~ ! [K: term] :
( ~ ( var @ K )
| ( I @ K ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ K )
| ~ ( I @ L )
| ( I @ ( ap @ K @ L ) ) )
| ~ ! [K: term] :
( ~ ( I @ K )
| ( I @ ( lam @ K ) ) )
| ( I @ J ) ) ) )
& ( hoasinduction_lem3a_lthm
= ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ ( sub @ J @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ J ) @ id ) ) ) ) )
& termmset_gthm
& ( hoasinduction_lem3aa
= ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ ( sub @ J @ ( push @ one @ sh ) ) ) @ id ) ) ) )
& pushprop_lem1v2_gthm
& hoaslamnotap_gthm
& hoaslamnotvar_gthm
& hoasinduction_lem3b_gthm
& pushprop_lem2v2
& hoasinduction_lem3a_gthm
& axclos
& axassoc
& ( hoasinduction_lem2v2
= ( ! [I: subst > term > subst > $o,J: term > $o,K: term,L: term] :
( ~ ! [M: subst,N: term,O: subst,P: subst] :
( ~ ( I @ M @ N @ ( comp @ P @ O ) )
| ( I @ ( comp @ M @ P ) @ ( sub @ N @ P ) @ O ) )
| ~ ! [M: subst,N: term,O: subst,P: subst] :
( ~ ( I @ ( comp @ M @ P ) @ ( sub @ N @ P ) @ O )
| ( I @ M @ N @ ( comp @ P @ O ) ) )
| ~ ! [M: term,N: term] :
( ~ ( I @ id @ M @ id )
| ~ ( I @ id @ N @ id )
| ( I @ id @ ( ap @ ( sub @ M @ id ) @ N ) @ id ) )
| ~ ! [M: term] :
( ( J @ M )
= ( I @ id @ M @ id ) )
| ~ ( J @ K )
| ~ ( J @ L )
| ( J @ ( ap @ K @ L ) ) ) ) )
& pushprop_lthm
& ( apinj2
= ( ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ I @ K )
!= ( ap @ J @ L ) )
| ( K = L ) ) ) )
& ( apinj1
= ( ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ I @ K )
!= ( ap @ J @ L ) )
| ( I = J ) ) ) )
& ( hoasapinj2_lthm
= ( ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ I @ K )
!= ( ap @ J @ L ) )
| ( K = L ) )
=> ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ ( sub @ I @ id ) @ K )
!= ( ap @ ( sub @ J @ id ) @ L ) )
| ( K = L ) ) ) )
& ( hoasinduction_lem3v2a
= ( ! [I: subst > term > subst > $o,J: term > $o,K: term] :
( ~ ! [L: subst > term > term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( L @ M @ N ) @ O )
= ( L @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: term] :
( ~ ( I @ id @ M @ id )
| ( I @ id @ ( L @ id @ M ) @ id ) )
| ( I @ id @ ( lam @ ( L @ sh @ one ) ) @ id ) )
| ~ ! [L: term] :
( ( J @ L )
= ( I @ id @ L @ id ) )
| ~ ! [L: term] :
( ~ ( J @ L )
| ( J @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( J @ ( lam @ K ) ) ) ) )
& ( hoasapinj1_lthm
= ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ( ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ I @ K )
!= ( ap @ J @ L ) )
| ( I = J ) )
=> ! [I: term,J: term,K: term,L: term] :
( ( ( ap @ ( sub @ I @ id ) @ K )
!= ( ap @ ( sub @ J @ id ) @ L ) )
| ( I = J ) ) ) ) )
& ( hoaslaminj_lthm
= ( ! [I: term,J: subst] :
( I
= ( sub @ one @ ( push @ I @ J ) ) )
=> ( ! [I: term,J: subst] :
( J
= ( comp @ sh @ ( push @ I @ J ) ) )
=> ( ! [I: term,J: term] :
( ( ( lam @ I )
!= ( lam @ J ) )
| ( I = J ) )
=> ! [I: subst > term > term,J: subst > term > term,K: subst,L: term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( I @ M @ N ) @ O )
= ( I @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( J @ M @ N ) @ O )
= ( J @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ( ( lam @ ( I @ sh @ one ) )
!= ( lam @ ( J @ sh @ one ) ) )
| ( ( I @ K @ L )
= ( J @ K @ L ) ) ) ) ) ) )
& ( axvarcons
= ( ! [I: term,J: subst] :
( I
= ( sub @ one @ ( push @ I @ J ) ) ) ) )
& ( axscons
= ( ! [I: subst] :
( I
= ( push @ ( sub @ one @ I ) @ ( comp @ sh @ I ) ) ) ) )
& hoasinduction_lem2v2_gthm
& ( axidr
= ( ! [I: subst] :
( I
= ( comp @ I @ id ) ) ) )
& ( pushprop_lem1
= ( ! [I: term > $o,J: term > $o,K: term,L: subst,M: term] :
( ~ ( I @ K )
| ( J @ ( sub @ K @ ( push @ M @ L ) ) ) ) ) )
& ( laminj
= ( ! [I: term,J: term] :
( ( ( lam @ I )
!= ( lam @ J ) )
| ( I = J ) ) ) )
& ( hoasinduction_lem3_lthm
= ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ ( sub @ J @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ K @ L @ ( comp @ N @ M ) )
| ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M ) )
| ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M )
| ( I @ K @ L @ ( comp @ N @ M ) ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ J ) @ id ) ) ) ) )
& ( pushprop_lem0
= ( ! [I: term > $o,J: term,K: subst] :
~ ! [L: term > $o] :
~ ! [M: term] :
( ( L @ M )
= ( I @ ( sub @ M @ ( push @ J @ K ) ) ) ) ) )
& pushprop_gthm
& axabs
& ( hoasinduction_lem3v2a_lthm
= ( ! [I: term] :
~ ! [J: subst > term > term] :
~ ! [K: term,L: subst] :
( ( sub @ I @ ( push @ K @ L ) )
= ( J @ L @ K ) )
=> ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ! [I: subst > term > subst > $o,J: term > $o,K: term] :
( ~ ! [L: subst > term > term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( L @ M @ N ) @ O )
= ( L @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: term] :
( ~ ( I @ id @ M @ id )
| ( I @ id @ ( L @ id @ M ) @ id ) )
| ( I @ id @ ( lam @ ( L @ sh @ one ) ) @ id ) )
| ~ ! [L: term] :
( ( J @ L )
= ( I @ id @ L @ id ) )
| ~ ! [L: term] :
( ~ ( J @ L )
| ( J @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( J @ ( lam @ K ) ) ) ) ) )
& hoasinduction_lem2_lthm
& hoasapinj2_gthm
& hoasinduction_lem1_lthm
& ~ lamnotap
& hoasapinj1_gthm
& hoaslamnotvar
& ( axidl
= ( ! [I: subst] :
( I
= ( comp @ id @ I ) ) ) )
& hoaslaminj_gthm
& ( induction2_lthm
= ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ( ! [I: term > $o,J: term,K: subst] :
( ~ ! [L: term,M: term] :
( ~ ( I @ L )
| ~ ( I @ M )
| ( I @ ( ap @ L @ M ) ) )
| ~ ! [L: term] :
( ~ ! [M: term] :
( ~ ( I @ M )
| ( I @ ( sub @ L @ ( push @ M @ id ) ) ) )
| ( I @ ( lam @ L ) ) )
| ~ ! [L: term] :
( ~ ( var @ L )
| ( I @ ( sub @ L @ K ) ) )
| ( I @ ( sub @ J @ K ) ) )
=> ! [I: term > $o,J: term] :
( ~ ! [K: term] :
( ~ ( var @ K )
| ( I @ K ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ K )
| ~ ( I @ L )
| ( I @ ( ap @ K @ L ) ) )
| ~ ! [K: term] :
( ~ ! [L: term] :
( ~ ( I @ L )
| ( I @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( I @ ( lam @ K ) ) )
| ( I @ J ) ) ) ) )
& ( hoasinduction_lem0_lthm
= ( ! [I: subst > term > subst > $o] :
~ ! [J: term > $o] :
~ ! [K: term] :
( ( J @ K )
= ( I @ id @ K @ id ) ) ) )
& ( substmonoid_lthm
= ( ! [I: subst] :
( I
= ( comp @ id @ I ) )
=> ( ! [I: subst] :
( I
= ( comp @ I @ id ) )
=> ( ! [I: subst] :
( I
= ( comp @ id @ I ) )
& ! [I: subst] :
( I
= ( comp @ I @ id ) ) ) ) ) )
& pushprop
& hoasinduction_lem3_gthm
& hoasinduction_lem2_gthm
& ( hoasinduction_lem3b
= ( ! [I: term] :
~ ! [J: subst > term > term] :
( ( J @ sh @ one )
!= ( sub @ I @ ( push @ one @ sh ) ) ) ) )
& ( substmonoid
= ( ! [I: subst] :
( I
= ( comp @ id @ I ) )
& ! [I: subst] :
( I
= ( comp @ I @ id ) ) ) )
& lamnotvar
& ( hoasinduction_lem3a
= ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ~ ! [K: term] :
( ~ ( I @ id @ K @ id )
| ( I @ id @ ( sub @ J @ ( push @ K @ id ) ) @ id ) )
| ( I @ id @ ( lam @ J ) @ id ) ) ) )
& hoasinduction_lem1_gthm
& ( hoasinduction_no_psi_cond
= ( ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: term,L: term] :
( ~ ( I @ id @ K @ id )
| ~ ( I @ id @ L @ id )
| ( I @ id @ ( ap @ ( sub @ K @ id ) @ L ) @ id ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ( I @ id @ J @ id ) ) ) )
& induction2_gthm
& pushprop_lem2v2_lthm
& ~ ( hoasvar @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
& ( hoaslamnotap
= ( ! [I: subst > term > term,J: term,K: term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( I @ L @ M ) @ N )
= ( I @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ( ( lam @ ( I @ sh @ one ) )
!= ( ap @ ( sub @ J @ id ) @ K ) ) ) ) )
& substmonoid_gthm
& ulamvarsh
& ( induction2
= ( ! [I: term > $o,J: term] :
( ~ ! [K: term] :
( ~ ( var @ K )
| ( I @ K ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ K )
| ~ ( I @ L )
| ( I @ ( ap @ K @ L ) ) )
| ~ ! [K: term] :
( ~ ! [L: term] :
( ~ ( I @ L )
| ( I @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( I @ ( lam @ K ) ) )
| ( I @ J ) ) ) )
& pushprop_lem3v2
& pushprop_lem2v2_gthm
& ( pushprop_lem1_lthm
= ( ! [I: term,J: subst] :
( I
= ( sub @ one @ ( push @ I @ J ) ) )
=> ( ! [I: term,J: subst] :
( J
= ( comp @ sh @ ( push @ I @ J ) ) )
=> ! [I: term > $o,J: term > $o,K: term,L: subst,M: term] :
( ~ ( I @ K )
| ( J @ ( sub @ K @ ( push @ M @ L ) ) ) ) ) ) )
& ( hoasinduction_lem3v2
= ( ! [I: subst > term > subst > $o,J: term > $o,K: term] :
( ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ L @ M @ ( comp @ O @ N ) )
| ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N ) )
| ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N )
| ( I @ L @ M @ ( comp @ O @ N ) ) )
| ~ ! [L: subst > term > term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( L @ M @ N ) @ O )
= ( L @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: term] :
( ~ ( I @ id @ M @ id )
| ( I @ id @ ( L @ id @ M ) @ id ) )
| ( I @ id @ ( lam @ ( L @ sh @ one ) ) @ id ) )
| ~ ! [L: term] :
( ( J @ L )
= ( I @ id @ L @ id ) )
| ~ ! [L: term] :
( ~ ( J @ L )
| ( J @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( J @ ( lam @ K ) ) ) ) )
& ( axshiftcons
= ( ! [I: term,J: subst] :
( J
= ( comp @ sh @ ( push @ I @ J ) ) ) ) )
& ( termmset
= ( ! [I: term] :
( I
= ( sub @ I @ id ) ) ) )
& ( pushprop_lem0_lthm
= ( ! [I: term > $o,J: term,K: subst] :
~ ! [L: term > $o] :
~ ! [M: term] :
( ( L @ M )
= ( I @ ( sub @ M @ ( push @ J @ K ) ) ) ) ) )
& hoasapnotvar_lthm
& ( hoasinduction_lem3v2_lthm
= ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ! [I: subst > term > subst > $o,J: term > $o,K: term] :
( ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ L @ M @ ( comp @ O @ N ) )
| ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N ) )
| ~ ! [L: subst,M: term,N: subst,O: subst] :
( ~ ( I @ ( comp @ L @ O ) @ ( sub @ M @ O ) @ N )
| ( I @ L @ M @ ( comp @ O @ N ) ) )
| ~ ! [L: subst > term > term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( L @ M @ N ) @ O )
= ( L @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: term] :
( ~ ( I @ id @ M @ id )
| ( I @ id @ ( L @ id @ M ) @ id ) )
| ( I @ id @ ( lam @ ( L @ sh @ one ) ) @ id ) )
| ~ ! [L: term] :
( ( J @ L )
= ( I @ id @ L @ id ) )
| ~ ! [L: term] :
( ~ ( J @ L )
| ( J @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( J @ ( lam @ K ) ) ) ) )
& ( axvarid
= ( ! [I: term] :
( I
= ( sub @ I @ id ) ) ) )
& ( hoasinduction_lthm_3
= ( ! [I: subst > term > subst > $o] :
~ ! [J: term > $o] :
~ ! [K: term] :
( ( J @ K )
= ( I @ id @ K @ id ) )
=> ( ! [I: term > $o,J: term] :
( ~ ! [K: term] :
( ~ ( var @ K )
| ( I @ K ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ K )
| ~ ( I @ L )
| ( I @ ( ap @ K @ L ) ) )
| ~ ! [K: term] :
( ~ ! [L: term] :
( ~ ( I @ L )
| ( I @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( I @ ( lam @ K ) ) )
| ( I @ J ) )
=> ( ! [I: term] :
( I
= ( sub @ I @ id ) )
=> ( ! [I: subst > term > subst > $o,J: term > $o,K: term] :
( ~ ! [L: subst > term > term] :
( ~ ! [M: subst,N: term,O: subst] :
( ( sub @ ( L @ M @ N ) @ O )
= ( L @ ( comp @ M @ O ) @ ( sub @ N @ O ) ) )
| ~ ! [M: term] :
( ~ ( I @ id @ M @ id )
| ( I @ id @ ( L @ id @ M ) @ id ) )
| ( I @ id @ ( lam @ ( L @ sh @ one ) ) @ id ) )
| ~ ! [L: term] :
( ( J @ L )
= ( I @ id @ L @ id ) )
| ~ ! [L: term] :
( ~ ( J @ L )
| ( J @ ( sub @ K @ ( push @ L @ id ) ) ) )
| ( J @ ( lam @ K ) ) )
=> ! [I: subst > term > subst > $o,J: term] :
( ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ K @ L @ ( comp @ N @ M ) )
| ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M ) )
| ~ ! [K: subst,L: term,M: subst,N: subst] :
( ~ ( I @ ( comp @ K @ N ) @ ( sub @ L @ N ) @ M )
| ( I @ K @ L @ ( comp @ N @ M ) ) )
| ~ ! [K: term] :
( ~ ( var @ ( sub @ K @ id ) )
| ( I @ id @ K @ id ) )
| ~ ! [K: term,L: term] :
( ~ ( I @ id @ K @ id )
| ~ ( I @ id @ L @ id )
| ( I @ id @ ( ap @ ( sub @ K @ id ) @ L ) @ id ) )
| ~ ! [K: subst > term > term] :
( ~ ! [L: subst,M: term,N: subst] :
( ( sub @ ( K @ L @ M ) @ N )
= ( K @ ( comp @ L @ N ) @ ( sub @ M @ N ) ) )
| ~ ! [L: term] :
( ~ ( I @ id @ L @ id )
| ( I @ id @ ( K @ id @ L ) @ id ) )
| ( I @ id @ ( lam @ ( K @ sh @ one ) ) @ id ) )
| ( I @ id @ J @ id ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[6]) ).
thf(66,plain,
! [A: term] :
( A
= ( d2term @ ( sk1 @ A ) ) ),
inference(cnfConj,[status(thm)],[7]) ).
thf(182,plain,
! [A: term] :
( ( d2term @ ( sk1 @ A ) )
= A ),
inference(lifteq,[status(thm)],[66]) ).
thf(20,plain,
! [A: d_term] : ( A = d_one ),
inference(cnfConj,[status(thm)],[7]) ).
thf(145,plain,
! [A: d_term] : ( A = d_one ),
inference(lifteq,[status(thm)],[20]) ).
thf(146,plain,
! [A: d_term] : ( A = d_one ),
inference(simp,[status(thm)],[145]) ).
thf(31,plain,
( one
= ( d2term @ d_one ) ),
inference(cnfConj,[status(thm)],[7]) ).
thf(192,plain,
( ( d2term @ d_one )
= one ),
inference(lifteq,[status(thm)],[31]) ).
thf(397,plain,
! [A: d_term] :
( ( ( d2term @ A )
= one )
| ( d_one != d_one ) ),
inference(paramod_ordered,[status(thm)],[146,192]) ).
thf(398,plain,
! [A: d_term] :
( ( d2term @ A )
= one ),
inference(pattern_uni,[status(thm)],[397:[]]) ).
thf(828,plain,
! [A: term] : ( one = A ),
inference(rewrite,[status(thm)],[182,398]) ).
thf(1,conjecture,
( axclos
= ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axclos) ).
thf(2,negated_conjecture,
( axclos
!= ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(4,plain,
( axclos
!= ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(5,plain,
( axclos
!= ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ) ) ),
inference(lifteq,[status(thm)],[4]) ).
thf(10,plain,
axclos,
inference(cnfConj,[status(thm)],[7]) ).
thf(218,plain,
~ ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ),
inference(rewrite,[status(thm)],[5,10]) ).
thf(219,plain,
( ( sub @ ( sub @ sk5 @ sk6 ) @ sk7 )
!= ( sub @ sk5 @ ( comp @ sk6 @ sk7 ) ) ),
inference(cnf,[status(esa)],[218]) ).
thf(220,plain,
( ( sub @ ( sub @ sk5 @ sk6 ) @ sk7 )
!= ( sub @ sk5 @ ( comp @ sk6 @ sk7 ) ) ),
inference(lifteq,[status(thm)],[219]) ).
thf(861,plain,
! [A: term] :
( ( ( sub @ sk5 @ ( comp @ sk6 @ sk7 ) )
!= one )
| ( A
!= ( sub @ ( sub @ sk5 @ sk6 ) @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[828,220]) ).
thf(862,plain,
( ( sub @ sk5 @ ( comp @ sk6 @ sk7 ) )
!= one ),
inference(pattern_uni,[status(thm)],[861:[bind(A,$thf( sub @ ( sub @ sk5 @ sk6 ) @ sk7 ))]]) ).
thf(967,plain,
$false,
inference(simplifyReflect,[status(thm)],[862,828]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX154^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 16:10:44 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.90/0.78 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.08/1.16 % [INFO] Parsing done (378ms).
% 2.08/1.18 % [INFO] Running in sequential loop mode.
% 2.87/1.56 % [INFO] eprover registered as external prover.
% 2.87/1.57 % [INFO] Scanning for conjecture ...
% 3.33/1.75 % [INFO] Found a conjecture (or negated_conjecture) and 1 axioms. Running axiom selection ...
% 3.33/1.79 % [INFO] Axiom selection finished. Selected 1 axioms (removed 0 axioms).
% 4.69/2.45 % [INFO] Problem is higher-order (TPTP THF).
% 4.69/2.49 % [INFO] Type checking passed.
% 4.69/2.49 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 9.76/5.53 % [INFO] [Domain constraints] Detected constraint on d_term
% 9.76/5.53 % [INFO] [Domain constraints] dom(d_term) ⊆ {d_one}
% 10.06/5.69 % [INFO] [Domain constraints] Detected constraint on d_subst
% 10.06/5.69 % [INFO] [Domain constraints] dom(d_subst) ⊆ {d_id}
% 29.51/10.13 % [INFO] Killing All external provers ...
% 29.51/10.13 % Time passed: 9797ms (effective reasoning time: 8947ms)
% 29.51/10.13 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 29.51/10.14 % Axioms used in derivation (1): alg444_1
% 29.51/10.14 % No. of inferences in proof: 24
% 29.51/10.14 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 9797 ms resp. 8947 ms w/o parsing
% 30.76/10.41 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 30.76/10.41 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------