%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ALG253^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n006.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 07:45:02 AM UTC 2026
% Result : Theorem 190.02s 49.94s
% Output : Refutation 190.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 44
% Syntax : Number of formulae : 654 ( 292 unt; 0 typ; 43 def)
% Number of atoms : 2024 ( 869 equ; 100 cnn)
% Maximal formula atoms : 64 ( 3 avg)
% Number of connectives : 6527 ( 788 ~; 696 |; 45 &;4789 @)
% ( 0 <=>; 209 =>; 0 <=; 0 <~>)
% Maximal formula depth : 103 ( 5 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 123 ( 123 >; 0 *; 0 +; 0 <<)
% Number of symbols : 62 ( 57 usr; 37 con; 0-3 aty)
% Number of variables : 1170 ( 113 ^;1030 !; 11 ?;1170 :)
% ( 0 !>; 0 ?*; 0 @-; 16 @+)
% Comments :
%------------------------------------------------------------------------------
thf(term_type,type,
term: $tType ).
thf(subst_type,type,
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(axmap_decl,type,
axmap: $o ).
thf(shinj_decl,type,
shinj: $o ).
thf(induction2lem_decl,type,
induction2lem: $o ).
thf(axvarshift_decl,type,
axvarshift: $o ).
thf(ulamvar1_decl,type,
ulamvar1: $o ).
thf(apnotvar_decl,type,
apnotvar: $o ).
thf(axapp_decl,type,
axapp: $o ).
thf(ulamvarind_decl,type,
ulamvarind: $o ).
thf(induction_decl,type,
induction: $o ).
thf(axclos_decl,type,
axclos: $o ).
thf(axassoc_decl,type,
axassoc: $o ).
thf(apinj2_decl,type,
apinj2: $o ).
thf(apinj1_decl,type,
apinj1: $o ).
thf(axvarcons_decl,type,
axvarcons: $o ).
thf(axscons_decl,type,
axscons: $o ).
thf(axidr_decl,type,
axidr: $o ).
thf(laminj_decl,type,
laminj: $o ).
thf(axabs_decl,type,
axabs: $o ).
thf(lamnotap_decl,type,
lamnotap: $o ).
thf(axidl_decl,type,
axidl: $o ).
thf(pushprop_decl,type,
pushprop: $o ).
thf(lamnotvar_decl,type,
lamnotvar: $o ).
thf(induction2_gthm_decl,type,
induction2_gthm: $o ).
thf(ulamvarsh_decl,type,
ulamvarsh: $o ).
thf(induction2_decl,type,
induction2: $o ).
thf(axshiftcons_decl,type,
axshiftcons: $o ).
thf(axvarid_decl,type,
axvarid: $o ).
thf(sk1_decl,type,
sk1: ( term > $o ) > term ).
thf(sk2_decl,type,
sk2: ( term > $o ) > $o ).
thf(sk3_decl,type,
sk3: ( term > $o ) > term ).
thf(sk4_decl,type,
sk4: ( term > $o ) > term ).
thf(sk5_decl,type,
sk5: ( term > $o ) > term ).
thf(sk6_decl,type,
sk6: ( term > $o ) > term ).
thf(sk7_decl,type,
sk7: subst > term > ( term > $o ) > term ).
thf(sk8_decl,type,
sk8: ( term > $o ) > $o ).
thf(sk9_decl,type,
sk9: ( term > $o ) > term ).
thf(sk10_decl,type,
sk10: ( term > $o ) > term ).
thf(sk11_decl,type,
sk11: ( term > $o ) > $o ).
thf(sk12_decl,type,
sk12: ( term > $o ) > term ).
thf(sk13_decl,type,
sk13: subst > term > ( term > $o ) > term ).
thf(sk14_decl,type,
sk14: term > $o ).
thf(sk15_decl,type,
sk15: term > term ).
thf(sk16_decl,type,
sk16: term ).
thf(sk17_decl,type,
sk17: term > term > term ).
thf(sk18_decl,type,
sk18: term > term ).
thf(sk19_decl,type,
sk19: term > term > term ).
thf(sk20_decl,type,
sk20: term ).
thf(sk21_decl,type,
sk21: term ).
thf(axmap_def,definition,
( axmap
= ( ! [A: term,B: subst,C: subst] :
( ( comp @ ( push @ A @ B ) @ C )
= ( push @ ( sub @ A @ C ) @ ( comp @ B @ C ) ) ) ) ) ).
thf(shinj_def,definition,
( shinj
= ( ! [A: term,B: term] :
( ( ( sub @ A @ sh )
= ( sub @ B @ sh ) )
=> ( A = B ) ) ) ) ).
thf(induction2lem_def,definition,
( induction2lem
= ( ! [A: term > $o] :
( ! [B: term,C: term] :
( ( A @ B )
=> ( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( A @ ( sub @ B @ C ) ) ) ) ) ) ) ).
thf(axvarshift_def,definition,
( axvarshift
= ( ( push @ one @ sh )
= id ) ) ).
thf(ulamvar1_def,definition,
( ulamvar1
= ( var @ one ) ) ).
thf(apnotvar_def,definition,
( apnotvar
= ( ! [A: term,B: term] :
~ ( var @ ( ap @ A @ B ) ) ) ) ).
thf(axapp_def,definition,
( axapp
= ( ! [A: term,B: term,C: subst] :
( ( sub @ ( ap @ A @ B ) @ C )
= ( ap @ ( sub @ A @ C ) @ ( sub @ B @ C ) ) ) ) ) ).
thf(ulamvarind_def,definition,
( ulamvarind
= ( ! [A: term > $o] :
( ( A @ one )
=> ( ! [B: term] :
( ( var @ B )
=> ( ( A @ B )
=> ( A @ ( sub @ B @ sh ) ) ) )
=> ! [B: term] :
( ( var @ B )
=> ( A @ B ) ) ) ) ) ) ).
thf(induction_def,definition,
( induction
= ( ! [A: term > $o] :
( ! [B: term] :
( ( var @ B )
=> ( A @ B ) )
=> ( ! [B: term,C: term] :
( ( A @ B )
=> ( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ( A @ B )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term] : ( A @ B ) ) ) ) ) ) ).
thf(axclos_def,definition,
( axclos
= ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ) ) ) ).
thf(axassoc_def,definition,
( axassoc
= ( ! [A: subst,B: subst,C: subst] :
( ( comp @ ( comp @ A @ B ) @ C )
= ( comp @ A @ ( comp @ B @ C ) ) ) ) ) ).
thf(apinj2_def,definition,
( apinj2
= ( ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
= ( ap @ B @ D ) )
=> ( C = D ) ) ) ) ).
thf(apinj1_def,definition,
( apinj1
= ( ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
= ( ap @ B @ D ) )
=> ( A = B ) ) ) ) ).
thf(axvarcons_def,definition,
( axvarcons
= ( ! [A: term,B: subst] :
( ( sub @ one @ ( push @ A @ B ) )
= A ) ) ) ).
thf(axscons_def,definition,
( axscons
= ( ! [A: subst] :
( ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) )
= A ) ) ) ).
thf(axidr_def,definition,
( axidr
= ( ! [A: subst] :
( ( comp @ A @ id )
= A ) ) ) ).
thf(laminj_def,definition,
( laminj
= ( ! [A: term,B: term] :
( ( ( lam @ A )
= ( lam @ B ) )
=> ( A = B ) ) ) ) ).
thf(axabs_def,definition,
( axabs
= ( ! [A: term,B: subst] :
( ( sub @ ( lam @ A ) @ B )
= ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) ) ) ) ) ).
thf(lamnotap_def,definition,
( lamnotap
= ( ! [A: term,B: term,C: term] :
( ( lam @ A )
!= ( ap @ B @ C ) ) ) ) ).
thf(axidl_def,definition,
( axidl
= ( ! [A: subst] :
( ( comp @ id @ A )
= A ) ) ) ).
thf(pushprop_def,definition,
( pushprop
= ( ! [A: term > $o,B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( ( A @ B )
=> ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ) ) ) ) ) ).
thf(lamnotvar_def,definition,
( lamnotvar
= ( ! [A: term] :
~ ( var @ ( lam @ A ) ) ) ) ).
thf(induction2_gthm_def,definition,
( induction2_gthm
= ( axapp
=> ( axvarcons
=> ( axvarid
=> ( axabs
=> ( axclos
=> ( axidl
=> ( axshiftcons
=> ( axassoc
=> ( axmap
=> ( axidr
=> ( axvarshift
=> ( axscons
=> ( ulamvar1
=> ( ulamvarsh
=> ( ulamvarind
=> ( apinj1
=> ( apinj2
=> ( laminj
=> ( shinj
=> ( lamnotap
=> ( apnotvar
=> ( lamnotvar
=> ( induction
=> ( pushprop
=> ( induction2lem
=> induction2 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(ulamvarsh_def,definition,
( ulamvarsh
= ( ! [A: term] :
( ( var @ A )
=> ( var @ ( sub @ A @ sh ) ) ) ) ) ).
thf(induction2_def,definition,
( induction2
= ( ! [A: term > $o] :
( ! [B: term] :
( ( var @ B )
=> ( A @ B ) )
=> ( ! [B: term,C: term] :
( ( A @ B )
=> ( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term] : ( A @ B ) ) ) ) ) ) ).
thf(axshiftcons_def,definition,
( axshiftcons
= ( ! [A: term,B: subst] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ) ) ) ).
thf(axvarid_def,definition,
( axvarid
= ( ! [A: term] :
( ( sub @ A @ id )
= A ) ) ) ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( var @ B )
=> ( ( A @ B )
=> ( A @ ( sub @ B @ sh ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( var @ B )
=> ( A @ B ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( A @ B )
=> ! [C: term] :
( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( A @ B )
=> ( A @ ( ap @ ( sk4 @ A ) @ B ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( A @ B )
=> ( A @ ( lam @ B ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: subst,B: term,C: term > $o] :
@+[D: term] :
~ ( ( var @ D )
=> ( C @ ( sub @ D @ A ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( A @ B )
=> ! [C: term] :
( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( A @ B )
=> ( A @ ( ap @ ( sk9 @ A ) @ B ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: subst,B: term,C: term > $o] :
@+[D: term] :
~ ( ( var @ D )
=> ( C @ ( sub @ D @ A ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( @+[A: term > $o] :
~ ( ! [B: term] :
( ( var @ B )
=> ( A @ B ) )
=> ( ! [B: term] :
( ( A @ B )
=> ! [C: term] :
( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term] : ( A @ B ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: term] :
@+[B: term] :
~ ( ( sk14 @ B )
=> ( sk14 @ ( sub @ A @ ( push @ B @ id ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( @+[A: term] :
~ ( sk14 @ A ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( @+[A: term > term > term] :
! [B: term,C: term] :
( ( A @ C @ ( ap @ B @ C ) )
= B ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( @+[A: term > term] :
! [B: term] :
( ( A @ ( lam @ B ) )
= B ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( @+[A: term > term > term] :
! [B: term,C: term] :
( ( A @ B @ ( ap @ B @ C ) )
= C ) ) ) ).
thf(1,conjecture,
induction2_gthm,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm) ).
thf(2,negated_conjecture,
~ induction2_gthm,
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ! [A: term,B: term,C: subst] :
( ( sub @ ( ap @ A @ B ) @ C )
= ( ap @ ( sub @ A @ C ) @ ( sub @ B @ C ) ) )
=> ( ! [A: term,B: subst] :
( ( sub @ one @ ( push @ A @ B ) )
= A )
=> ( ! [A: term] :
( ( sub @ A @ id )
= A )
=> ( ! [A: term,B: subst] :
( ( sub @ ( lam @ A ) @ B )
= ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) ) )
=> ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) )
=> ( ! [A: subst] :
( ( comp @ id @ A )
= A )
=> ( ! [A: term,B: subst] :
( ( comp @ sh @ ( push @ A @ B ) )
= B )
=> ( ! [A: subst,B: subst,C: subst] :
( ( comp @ ( comp @ A @ B ) @ C )
= ( comp @ A @ ( comp @ B @ C ) ) )
=> ( ! [A: term,B: subst,C: subst] :
( ( comp @ ( push @ A @ B ) @ C )
= ( push @ ( sub @ A @ C ) @ ( comp @ B @ C ) ) )
=> ( ! [A: subst] :
( ( comp @ A @ id )
= A )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [A: subst] :
( ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) )
= A )
=> ( ( var @ one )
=> ( ! [A: term] :
( ( var @ A )
=> ( var @ ( sub @ A @ sh ) ) )
=> ( ! [A: term > $o] :
( ( A @ one )
=> ( ! [B: term] :
( ( var @ B )
=> ( ( A @ B )
=> ( A @ ( sub @ B @ sh ) ) ) )
=> ! [B: term] :
( ( var @ B )
=> ( A @ B ) ) ) )
=> ( ! [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 @ A @ C )
= ( ap @ B @ D ) )
=> ( C = D ) )
=> ( ! [A: term,B: term] :
( ( ( lam @ A )
= ( lam @ B ) )
=> ( A = B ) )
=> ( ! [A: term,B: term] :
( ( ( sub @ A @ sh )
= ( sub @ B @ sh ) )
=> ( A = B ) )
=> ( ! [A: term,B: term,C: term] :
( ( lam @ A )
!= ( ap @ B @ C ) )
=> ( ! [A: term,B: term] :
~ ( var @ ( ap @ A @ B ) )
=> ( ! [A: term] :
~ ( var @ ( lam @ A ) )
=> ( ! [A: term > $o] :
( ! [B: term] :
( ( var @ B )
=> ( A @ B ) )
=> ( ! [B: term,C: term] :
( ( A @ B )
=> ( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ( A @ B )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term] : ( A @ B ) ) ) )
=> ( ! [A: term > $o,B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( ( A @ B )
=> ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ) ) )
=> ( ! [A: term > $o] :
( ! [B: term,C: term] :
( ( A @ B )
=> ( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( A @ ( sub @ B @ C ) ) ) ) )
=> ! [A: term > $o] :
( ! [B: term] :
( ( var @ B )
=> ( A @ B ) )
=> ( ! [B: term,C: term] :
( ( A @ B )
=> ( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term] : ( A @ B ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
~ ( ! [A: term,B: term,C: subst] :
( ( sub @ ( ap @ A @ B ) @ C )
= ( ap @ ( sub @ A @ C ) @ ( sub @ B @ C ) ) )
=> ( ! [A: term,B: subst] :
( ( sub @ one @ ( push @ A @ B ) )
= A )
=> ( ! [A: term] :
( ( sub @ A @ id )
= A )
=> ( ! [A: term,B: subst] :
( ( sub @ ( lam @ A ) @ B )
= ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) ) )
=> ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) )
=> ( ! [A: subst] :
( ( comp @ id @ A )
= A )
=> ( ! [A: term,B: subst] :
( ( comp @ sh @ ( push @ A @ B ) )
= B )
=> ( ! [A: subst,B: subst,C: subst] :
( ( comp @ ( comp @ A @ B ) @ C )
= ( comp @ A @ ( comp @ B @ C ) ) )
=> ( ! [A: term,B: subst,C: subst] :
( ( comp @ ( push @ A @ B ) @ C )
= ( push @ ( sub @ A @ C ) @ ( comp @ B @ C ) ) )
=> ( ! [A: subst] :
( ( comp @ A @ id )
= A )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [A: subst] :
( ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) )
= A )
=> ( ( var @ one )
=> ( ! [A: term] :
( ( var @ A )
=> ( var @ ( sub @ A @ sh ) ) )
=> ( ! [A: term > $o] :
( ( A @ one )
=> ( ! [B: term] :
( ( var @ B )
=> ( ( A @ B )
=> ( A @ ( sub @ B @ sh ) ) ) )
=> ! [B: term] :
( ( var @ B )
=> ( A @ B ) ) ) )
=> ( ! [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 @ A @ C )
= ( ap @ B @ D ) )
=> ( C = D ) )
=> ( ! [A: term,B: term] :
( ( ( lam @ A )
= ( lam @ B ) )
=> ( A = B ) )
=> ( ! [A: term,B: term] :
( ( ( sub @ A @ sh )
= ( sub @ B @ sh ) )
=> ( A = B ) )
=> ( ~ ? [A: term,B: term,C: term] :
( ( lam @ A )
= ( ap @ B @ C ) )
=> ( ~ ? [A: term,B: term] : ( var @ ( ap @ A @ B ) )
=> ( ~ ? [A: term] : ( var @ ( lam @ A ) )
=> ( ! [A: term > $o] :
( ! [B: term] :
( ( var @ B )
=> ( A @ B ) )
=> ( ! [B: term] :
( ( A @ B )
=> ! [C: term] :
( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ( A @ B )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term] : ( A @ B ) ) ) )
=> ( ! [A: term > $o,B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( ( A @ B )
=> ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ) ) )
=> ( ! [A: term > $o] :
( ! [B: term] :
( ( A @ B )
=> ! [C: term] :
( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( A @ ( sub @ B @ C ) ) ) ) )
=> ! [A: term > $o] :
( ! [B: term] :
( ( var @ B )
=> ( A @ B ) )
=> ( ! [B: term] :
( ( A @ B )
=> ! [C: term] :
( ( A @ C )
=> ( A @ ( ap @ B @ C ) ) ) )
=> ( ! [B: term] :
( ! [C: term] :
( ( A @ C )
=> ( A @ ( sub @ B @ ( push @ C @ id ) ) ) )
=> ( A @ ( lam @ B ) ) )
=> ! [B: term] : ( A @ B ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[3]) ).
thf(5,plain,
! [ZZE: term,ZZD: term,ZZC: term,ZZB: term,ZZA: subst,ZZ: term,ZY: term,ZX: term > $o,ZW: term,ZV: subst,ZU: term,ZT: term > $o,ZS: term,ZR: term > $o,ZQ: term,ZP: term,ZO: term,ZN: term,ZM: term,ZL: term,ZK: term,ZJ: term,ZI: term,ZH: term,ZG: term,ZF: term,ZE: term,ZD: term,ZC: term,ZB: term,ZA: term,Z: term,Y: term,X: term > $o,W: term,V: subst,U: subst,T: subst,S: subst,R: term,Q: subst,P: subst,O: subst,N: subst,M: term,L: subst,K: subst,J: subst,I: term,H: subst,G: term,F: term,E: subst,D: term,C: subst,B: term,A: term] :
( ( ( sub @ ( ap @ A @ B ) @ C )
= ( ap @ ( sub @ A @ C ) @ ( sub @ B @ C ) ) )
& ( ( sub @ one @ ( push @ D @ E ) )
= D )
& ( ( sub @ F @ id )
= F )
& ( ( sub @ ( lam @ G ) @ H )
= ( lam @ ( sub @ G @ ( push @ one @ ( comp @ H @ sh ) ) ) ) )
& ( ( sub @ ( sub @ I @ J ) @ K )
= ( sub @ I @ ( comp @ J @ K ) ) )
& ( ( comp @ id @ L )
= L )
& ( ( comp @ sh @ ( push @ M @ N ) )
= N )
& ( ( comp @ ( comp @ O @ P ) @ Q )
= ( comp @ O @ ( comp @ P @ Q ) ) )
& ( ( comp @ ( push @ R @ S ) @ T )
= ( push @ ( sub @ R @ T ) @ ( comp @ S @ T ) ) )
& ( ( comp @ U @ id )
= U )
& ( ( push @ one @ sh )
= id )
& ( ( push @ ( sub @ one @ V ) @ ( comp @ sh @ V ) )
= V )
& ( var @ one )
& ( ~ ( var @ W )
| ( var @ ( sub @ W @ sh ) ) )
& ( ~ ( X @ one )
| ( var @ ( sk1 @ X ) )
| ~ ( var @ Y )
| ( X @ Y ) )
& ( ~ ( X @ one )
| ( X @ ( sk1 @ X ) )
| ~ ( var @ Y )
| ( X @ Y ) )
& ( ~ ( X @ one )
| ~ ( X @ ( sub @ ( sk1 @ X ) @ sh ) )
| ~ ( var @ Y )
| ( X @ Y ) )
& ( ( ( ap @ Z @ ZB )
!= ( ap @ ZA @ ZC ) )
| ( Z = ZA ) )
& ( ( ( ap @ ZD @ ZF )
!= ( ap @ ZE @ ZG ) )
| ( ZF = ZG ) )
& ( ( ( lam @ ZH )
!= ( lam @ ZI ) )
| ( ZH = ZI ) )
& ( ( ( sub @ ZJ @ sh )
!= ( sub @ ZK @ sh ) )
| ( ZJ = ZK ) )
& ( ( lam @ ZL )
!= ( ap @ ZM @ ZN ) )
& ~ ( var @ ( ap @ ZO @ ZP ) )
& ~ ( var @ ( lam @ ZQ ) )
& ( ( var @ ( sk3 @ ZR ) )
| ( sk2 @ ZR ) )
& ( ~ ( ZR @ ( sk3 @ ZR ) )
| ( sk2 @ ZR ) )
& ( ~ ( sk2 @ ZR )
| ( ZR @ ( sk4 @ ZR ) )
| ( ZR @ ( sk6 @ ZR ) )
| ( ZR @ ZS ) )
& ( ~ ( sk2 @ ZR )
| ( ZR @ ( sk4 @ ZR ) )
| ~ ( ZR @ ( lam @ ( sk6 @ ZR ) ) )
| ( ZR @ ZS ) )
& ( ~ ( sk2 @ ZR )
| ( ZR @ ( sk5 @ ZR ) )
| ( ZR @ ( sk6 @ ZR ) )
| ( ZR @ ZS ) )
& ( ~ ( sk2 @ ZR )
| ( ZR @ ( sk5 @ ZR ) )
| ~ ( ZR @ ( lam @ ( sk6 @ ZR ) ) )
| ( ZR @ ZS ) )
& ( ~ ( sk2 @ ZR )
| ~ ( ZR @ ( ap @ ( sk4 @ ZR ) @ ( sk5 @ ZR ) ) )
| ( ZR @ ( sk6 @ ZR ) )
| ( ZR @ ZS ) )
& ( ~ ( sk2 @ ZR )
| ~ ( ZR @ ( ap @ ( sk4 @ ZR ) @ ( sk5 @ ZR ) ) )
| ~ ( ZR @ ( lam @ ( sk6 @ ZR ) ) )
| ( ZR @ ZS ) )
& ( ( var @ ( sk7 @ ZV @ ZU @ ZT ) )
| ~ ( ZT @ ZU )
| ~ ( var @ ZW )
| ( ZT @ ( sub @ ZW @ ( push @ ZU @ ZV ) ) ) )
& ( ~ ( ZT @ ( sub @ ( sk7 @ ZV @ ZU @ ZT ) @ ZV ) )
| ~ ( ZT @ ZU )
| ~ ( var @ ZW )
| ( ZT @ ( sub @ ZW @ ( push @ ZU @ ZV ) ) ) )
& ( ( ZX @ ( sk9 @ ZX ) )
| ( sk8 @ ZX ) )
& ( ( ZX @ ( sk10 @ ZX ) )
| ( sk8 @ ZX ) )
& ( ~ ( ZX @ ( ap @ ( sk9 @ ZX ) @ ( sk10 @ ZX ) ) )
| ( sk8 @ ZX ) )
& ( ~ ( sk8 @ ZX )
| ~ ( ZX @ ZY )
| ( ZX @ ( sub @ ( sk12 @ ZX ) @ ( push @ ZY @ id ) ) )
| ( sk11 @ ZX ) )
& ( ~ ( sk8 @ ZX )
| ~ ( ZX @ ( lam @ ( sk12 @ ZX ) ) )
| ( sk11 @ ZX ) )
& ( ~ ( sk8 @ ZX )
| ~ ( sk11 @ ZX )
| ( var @ ( sk13 @ ZZA @ ZZ @ ZX ) )
| ( ZX @ ( sub @ ZZ @ ZZA ) ) )
& ( ~ ( sk8 @ ZX )
| ~ ( sk11 @ ZX )
| ~ ( ZX @ ( sub @ ( sk13 @ ZZA @ ZZ @ ZX ) @ ZZA ) )
| ( ZX @ ( sub @ ZZ @ ZZA ) ) )
& ( ~ ( var @ ZZB )
| ( sk14 @ ZZB ) )
& ( ~ ( sk14 @ ZZC )
| ~ ( sk14 @ ZZD )
| ( sk14 @ ( ap @ ZZC @ ZZD ) ) )
& ( ( sk14 @ ( sk15 @ ZZE ) )
| ( sk14 @ ( lam @ ZZE ) ) )
& ( ~ ( sk14 @ ( sub @ ZZE @ ( push @ ( sk15 @ ZZE ) @ id ) ) )
| ( sk14 @ ( lam @ ZZE ) ) )
& ~ ( sk14 @ sk16 ) ),
inference(cnf,[status(esa)],[4]) ).
thf(49,plain,
! [C: subst,B: subst,A: term] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(111,plain,
! [C: subst,B: subst,A: term] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ),
inference(lifteq,[status(thm)],[49]) ).
thf(112,plain,
! [C: subst,B: subst,A: term] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ),
inference(simp,[status(thm)],[111]) ).
thf(6,plain,
var @ one,
inference(cnfConj,[status(thm)],[5]) ).
thf(45,plain,
! [A: term] :
( ~ ( var @ A )
| ( var @ ( sub @ A @ sh ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(99,plain,
! [A: term] :
( ~ ( var @ A )
| ( var @ ( sub @ A @ sh ) ) ),
inference(simp,[status(thm)],[45]) ).
thf(6514,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ one )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6,99]) ).
thf(6515,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ one )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[6514]) ).
thf(6516,plain,
var @ ( sub @ one @ sh ),
inference(pattern_uni,[status(thm)],[6515:[bind(A,$thf( one ))]]) ).
thf(6750,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6516,99]) ).
thf(6751,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[6750]) ).
thf(6752,plain,
var @ ( sub @ ( sub @ one @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[6751:[bind(A,$thf( sub @ one @ sh ))]]) ).
thf(26,plain,
! [A: term] :
( ~ ( var @ A )
| ( sk14 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(128,plain,
! [A: term] :
( ~ ( var @ A )
| ( sk14 @ A ) ),
inference(simp,[status(thm)],[26]) ).
thf(7001,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6752,128]) ).
thf(7002,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[7001]) ).
thf(7003,plain,
sk14 @ ( sub @ ( sub @ one @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[7002:[bind(A,$thf( sub @ ( sub @ one @ sh ) @ sh ))]]) ).
thf(14753,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,7003]) ).
thf(14754,plain,
sk14 @ ( sub @ one @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[14753:[bind(A,$thf( one )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(22,plain,
! [A: term > $o] :
( ( var @ ( sk3 @ A ) )
| ( sk2 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(103,plain,
! [A: term > $o] :
( ( var @ ( sk3 @ A ) )
| ( sk2 @ A ) ),
inference(simp,[status(thm)],[22]) ).
thf(43,plain,
! [A: term > $o] :
( ~ ( A @ ( sk3 @ A ) )
| ( sk2 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(126,plain,
! [A: term > $o] :
( ~ ( A @ ( sk3 @ A ) )
| ( sk2 @ A ) ),
inference(simp,[status(thm)],[43]) ).
thf(25655,plain,
! [B: term > $o,A: term > $o] :
( ( sk2 @ A )
| ~ $true
| ( sk2 @ B )
| ( ( var @ ( sk3 @ A ) )
!= ( B @ ( sk3 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[103,126]) ).
thf(25656,plain,
! [B: term > $o,A: term > $o] :
( ( sk2 @ A )
| ( sk2 @ B )
| ( ( var @ ( sk3 @ A ) )
!= ( B @ ( sk3 @ B ) ) ) ),
inference(simp,[status(thm)],[25655]) ).
thf(25826,plain,
( ( sk2 @ var )
| ( sk2 @ var ) ),
inference(pre_uni,[status(thm)],[25656:[bind(A,$thf( var )),bind(B,$thf( var ))]]) ).
thf(25941,plain,
sk2 @ var,
inference(simp,[status(thm)],[25826]) ).
thf(39,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk5 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(114,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk5 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[39]) ).
thf(17614,plain,
( ~ ( sk2
@ ^ [A: term] : $false )
| $false
| $false
| $false ),
inference(prim_subst,[status(thm)],[114:[bind(A,$thf( ^ [C: term] : $false ))]]) ).
thf(17995,plain,
~ ( sk2
@ ^ [A: term] : $false ),
inference(simp,[status(thm)],[17614]) ).
thf(26263,plain,
( ~ $true
| ( ( sk2 @ var )
!= ( sk2
@ ^ [A: term] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[25941,17995]) ).
thf(26264,plain,
( ( sk2 @ var )
!= ( sk2
@ ^ [A: term] : $false ) ),
inference(simp,[status(thm)],[26263]) ).
thf(26323,plain,
( var
!= ( ^ [A: term] : $false ) ),
inference(simp,[status(thm)],[26264]) ).
thf(26357,plain,
var @ sk21,
inference(func_ext,[status(esa)],[26323]) ).
thf(26506,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[26357,99]) ).
thf(26507,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[26506]) ).
thf(26508,plain,
var @ ( sub @ sk21 @ sh ),
inference(pattern_uni,[status(thm)],[26507:[bind(A,$thf( sk21 ))]]) ).
thf(28401,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[26508,99]) ).
thf(28402,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[28401]) ).
thf(28403,plain,
var @ ( sub @ ( sub @ sk21 @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[28402:[bind(A,$thf( sub @ sk21 @ sh ))]]) ).
thf(31360,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[28403,99]) ).
thf(31361,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[31360]) ).
thf(31362,plain,
var @ ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[31361:[bind(A,$thf( sub @ ( sub @ sk21 @ sh ) @ sh ))]]) ).
thf(42465,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,31362]) ).
thf(42466,plain,
var @ ( sub @ ( sub @ sk21 @ sh ) @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[42465:[bind(A,$thf( sub @ sk21 @ sh )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(28,plain,
~ ( sk14 @ sk16 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(239,plain,
! [A: term] :
( ~ ( var @ A )
| ~ $true
| ( ( sk14 @ A )
!= ( sk14 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[128,28]) ).
thf(240,plain,
! [A: term] :
( ~ ( var @ A )
| ( ( sk14 @ A )
!= ( sk14 @ sk16 ) ) ),
inference(simp,[status(thm)],[239]) ).
thf(241,plain,
~ ( var @ sk16 ),
inference(pattern_uni,[status(thm)],[240:[bind(A,$thf( sk16 ))]]) ).
thf(43376,plain,
( ~ $true
| ( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ ( comp @ sh @ sh ) ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[42466,241]) ).
thf(43377,plain,
( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ ( comp @ sh @ sh ) ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[43376]) ).
thf(43500,plain,
( ( sub @ ( sub @ sk21 @ sh ) @ ( comp @ sh @ sh ) )
!= sk16 ),
inference(simp,[status(thm)],[43377]) ).
thf(32,plain,
! [D: term,C: subst,B: term,A: term > $o] :
( ( var @ ( sk7 @ C @ B @ A ) )
| ~ ( A @ B )
| ~ ( var @ D )
| ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(101,plain,
! [D: term,C: subst,B: term,A: term > $o] :
( ( var @ ( sk7 @ C @ B @ A ) )
| ~ ( A @ B )
| ~ ( var @ D )
| ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ),
inference(simp,[status(thm)],[32]) ).
thf(14605,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,6752]) ).
thf(14606,plain,
var @ ( sub @ one @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[14605:[bind(A,$thf( one )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(18,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( A @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(60,plain,
! [A: term] :
( ( one != one )
| ( one
= ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A )
| ( one = A ) ),
inference(replace_leibeq,[status(thm)],[18:[bind(A,$thf( (=) @ term @ one ))]]) ).
thf(87,plain,
! [A: term] :
( ( one != one )
| ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ ( var @ A ) ),
inference(lifteq,[status(thm)],[60]) ).
thf(88,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ ( var @ A ) ),
inference(simp,[status(thm)],[87]) ).
thf(396,plain,
! [B: term,A: term > $o] :
( ( sk2 @ A )
| ~ $true
| ( sk14 @ B )
| ( ( var @ ( sk3 @ A ) )
!= ( var @ B ) ) ),
inference(paramod_ordered,[status(thm)],[103,128]) ).
thf(397,plain,
! [B: term,A: term > $o] :
( ( sk2 @ A )
| ( sk14 @ B )
| ( ( var @ ( sk3 @ A ) )
!= ( var @ B ) ) ),
inference(simp,[status(thm)],[396]) ).
thf(398,plain,
! [A: term > $o] :
( ( sk2 @ A )
| ( sk14 @ ( sk3 @ A ) ) ),
inference(pattern_uni,[status(thm)],[397:[bind(A,$thf( C )),bind(B,$thf( sk3 @ C ))]]) ).
thf(408,plain,
! [A: term > $o] :
( ( sk2 @ A )
| ( sk14 @ ( sk3 @ A ) ) ),
inference(simp,[status(thm)],[398]) ).
thf(48,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk4 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(115,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk4 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[48]) ).
thf(10,plain,
! [B: subst,A: term] :
( ( sub @ one @ ( push @ A @ B ) )
= A ),
inference(cnfConj,[status(thm)],[5]) ).
thf(67,plain,
! [B: subst,A: term] :
( ( sub @ one @ ( push @ A @ B ) )
= A ),
inference(lifteq,[status(thm)],[10]) ).
thf(68,plain,
! [B: subst,A: term] :
( ( sub @ one @ ( push @ A @ B ) )
= A ),
inference(simp,[status(thm)],[67]) ).
thf(23,plain,
! [B: subst,A: term] :
( ( sub @ ( lam @ A ) @ B )
= ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(131,plain,
! [B: subst,A: term] :
( ( sub @ ( lam @ A ) @ B )
= ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) ) ),
inference(lifteq,[status(thm)],[23]) ).
thf(132,plain,
! [B: subst,A: term] :
( ( sub @ ( lam @ A ) @ B )
= ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) ) ),
inference(simp,[status(thm)],[131]) ).
thf(932,plain,
! [D: subst,C: term,B: subst,A: term] :
( ( ( lam @ A )
= ( sub @ ( lam @ C ) @ D ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ C @ ( push @ one @ ( comp @ D @ sh ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[68,132]) ).
thf(933,plain,
! [A: subst] :
( ( sub @ ( lam @ one ) @ A )
= ( lam @ one ) ),
inference(pattern_uni,[status(thm)],[932:[bind(A,$thf( one )),bind(B,$thf( comp @ E @ sh )),bind(C,$thf( one )),bind(D,$thf( E ))]]) ).
thf(997,plain,
! [A: subst] :
( ( sub @ ( lam @ one ) @ A )
= ( lam @ one ) ),
inference(simp,[status(thm)],[933]) ).
thf(1009,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ ( lam @ B ) @ C )
= ( lam @ ( lam @ one ) ) )
| ( ( sub @ ( lam @ one ) @ A )
!= ( sub @ B @ ( push @ one @ ( comp @ C @ sh ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[997,132]) ).
thf(1010,plain,
! [A: subst] :
( ( sub @ ( lam @ ( lam @ one ) ) @ A )
= ( lam @ ( lam @ one ) ) ),
inference(pattern_uni,[status(thm)],[1009:[bind(A,$thf( push @ one @ ( comp @ G @ sh ) )),bind(B,$thf( lam @ one )),bind(C,$thf( G ))]]) ).
thf(1055,plain,
! [A: subst] :
( ( sub @ ( lam @ ( lam @ one ) ) @ A )
= ( lam @ ( lam @ one ) ) ),
inference(simp,[status(thm)],[1010]) ).
thf(1145,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ ( lam @ B ) @ C )
= ( lam @ ( lam @ ( lam @ one ) ) ) )
| ( ( sub @ ( lam @ ( lam @ one ) ) @ A )
!= ( sub @ B @ ( push @ one @ ( comp @ C @ sh ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1055,132]) ).
thf(1146,plain,
! [A: subst] :
( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
= ( lam @ ( lam @ ( lam @ one ) ) ) ),
inference(pattern_uni,[status(thm)],[1145:[bind(A,$thf( push @ one @ ( comp @ H @ sh ) )),bind(B,$thf( lam @ ( lam @ one ) )),bind(C,$thf( H ))]]) ).
thf(1213,plain,
! [A: subst] :
( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
= ( lam @ ( lam @ ( lam @ one ) ) ) ),
inference(simp,[status(thm)],[1146]) ).
thf(41,plain,
! [A: term] :
~ ( var @ ( lam @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(98,plain,
! [A: term] :
~ ( var @ ( lam @ A ) ),
inference(simp,[status(thm)],[41]) ).
thf(7008,plain,
! [A: term] :
( ~ $true
| ( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ ( lam @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[6752,98]) ).
thf(7009,plain,
! [A: term] :
( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ ( lam @ A ) ) ),
inference(simp,[status(thm)],[7008]) ).
thf(7078,plain,
! [A: term] :
( ( sub @ ( sub @ one @ sh ) @ sh )
!= ( lam @ A ) ),
inference(simp,[status(thm)],[7009]) ).
thf(9992,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ one ) ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1213,7078]) ).
thf(10029,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ one ) )
!= B )
| ( ( sub @ one @ sh )
!= ( lam @ ( lam @ ( lam @ one ) ) ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[9992]) ).
thf(10061,plain,
( ( sub @ one @ sh )
!= ( lam @ ( lam @ ( lam @ one ) ) ) ),
inference(simp,[status(thm)],[10029]) ).
thf(236,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ one )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6,128]) ).
thf(237,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ one )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[236]) ).
thf(238,plain,
sk14 @ one,
inference(pattern_uni,[status(thm)],[237:[bind(A,$thf( one ))]]) ).
thf(242,plain,
( ~ $true
| ( ( sk14 @ sk16 )
!= ( sk14 @ one ) ) ),
inference(paramod_ordered,[status(thm)],[238,28]) ).
thf(243,plain,
( ( sk14 @ sk16 )
!= ( sk14 @ one ) ),
inference(simp,[status(thm)],[242]) ).
thf(247,plain,
sk16 != one,
inference(simp,[status(thm)],[243]) ).
thf(31313,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[28403,128]) ).
thf(31314,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[31313]) ).
thf(31315,plain,
sk14 @ ( sub @ ( sub @ sk21 @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[31314:[bind(A,$thf( sub @ ( sub @ sk21 @ sh ) @ sh ))]]) ).
thf(50,plain,
! [A: term] :
( ( sub @ A @ id )
= A ),
inference(cnfConj,[status(thm)],[5]) ).
thf(117,plain,
! [A: term] :
( ( sub @ A @ id )
= A ),
inference(lifteq,[status(thm)],[50]) ).
thf(118,plain,
! [A: term] :
( ( sub @ A @ id )
= A ),
inference(simp,[status(thm)],[117]) ).
thf(920,plain,
! [C: term,B: subst,A: term] :
( ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
= C )
| ( ( sub @ ( lam @ A ) @ B )
!= ( sub @ C @ id ) ) ),
inference(paramod_ordered,[status(thm)],[132,118]) ).
thf(921,plain,
! [A: term] :
( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ id @ sh ) ) ) )
= ( lam @ A ) ),
inference(pattern_uni,[status(thm)],[920:[bind(A,$thf( D )),bind(B,$thf( id )),bind(C,$thf( lam @ D ))]]) ).
thf(993,plain,
! [A: term] :
( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ id @ sh ) ) ) )
= ( lam @ A ) ),
inference(simp,[status(thm)],[921]) ).
thf(35,plain,
! [A: subst] :
( ( comp @ id @ A )
= A ),
inference(cnfConj,[status(thm)],[5]) ).
thf(65,plain,
! [A: subst] :
( ( comp @ id @ A )
= A ),
inference(lifteq,[status(thm)],[35]) ).
thf(66,plain,
! [A: subst] :
( ( comp @ id @ A )
= A ),
inference(simp,[status(thm)],[65]) ).
thf(5396,plain,
! [A: term] :
( ( lam @ ( sub @ A @ ( push @ one @ sh ) ) )
= ( lam @ A ) ),
inference(rewrite,[status(thm)],[993,66]) ).
thf(37,plain,
( ( push @ one @ sh )
= id ),
inference(cnfConj,[status(thm)],[5]) ).
thf(73,plain,
( ( push @ one @ sh )
= id ),
inference(lifteq,[status(thm)],[37]) ).
thf(150,plain,
! [A: term] :
( ~ $true
| ( ( var @ ( lam @ A ) )
!= ( var @ one ) ) ),
inference(paramod_ordered,[status(thm)],[6,98]) ).
thf(151,plain,
! [A: term] :
( ( var @ ( lam @ A ) )
!= ( var @ one ) ),
inference(simp,[status(thm)],[150]) ).
thf(152,plain,
! [A: term] :
( ( lam @ A )
!= one ),
inference(simp,[status(thm)],[151]) ).
thf(902,plain,
! [C: term,B: subst,A: term] :
( ( ( sub @ ( lam @ A ) @ B )
!= one )
| ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= ( lam @ C ) ) ),
inference(paramod_ordered,[status(thm)],[132,152]) ).
thf(903,plain,
! [B: subst,A: term] :
( ( sub @ ( lam @ A ) @ B )
!= one ),
inference(pattern_uni,[status(thm)],[902:[bind(A,$thf( D )),bind(B,$thf( H )),bind(C,$thf( sub @ D @ ( push @ one @ ( comp @ H @ sh ) ) ))]]) ).
thf(979,plain,
! [B: subst,A: term] :
( ( sub @ ( lam @ A ) @ B )
!= one ),
inference(simp,[status(thm)],[903]) ).
thf(1065,plain,
! [D: subst,C: term,B: subst,A: term] :
( ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= one )
| ( ( sub @ ( lam @ A ) @ B )
!= ( sub @ ( lam @ C ) @ D ) ) ),
inference(paramod_ordered,[status(thm)],[132,979]) ).
thf(1066,plain,
! [B: subst,A: term] :
( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[1065:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(1775,plain,
! [C: subst,B: term,A: subst] :
( ( ( lam @ ( sub @ B @ ( push @ one @ A ) ) )
!= one )
| ( ( comp @ id @ A )
!= ( comp @ C @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[66,1066]) ).
thf(1776,plain,
! [A: term] :
( ( lam @ ( sub @ A @ ( push @ one @ sh ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[1775:[bind(A,$thf( sh )),bind(B,$thf( B )),bind(C,$thf( id ))]]) ).
thf(1791,plain,
! [A: term] :
( ( lam @ ( sub @ A @ ( push @ one @ sh ) ) )
!= one ),
inference(simp,[status(thm)],[1776]) ).
thf(1829,plain,
! [A: term] :
( ( lam @ ( sub @ A @ id ) )
!= one ),
inference(rewrite,[status(thm)],[1791,73]) ).
thf(1832,plain,
! [C: term,B: subst,A: term] :
( ( ( lam @ ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) ) )
!= one )
| ( ( sub @ ( lam @ A ) @ B )
!= ( sub @ C @ id ) ) ),
inference(paramod_ordered,[status(thm)],[132,1829]) ).
thf(1833,plain,
! [A: term] :
( ( lam @ ( lam @ ( sub @ A @ ( push @ one @ ( comp @ id @ sh ) ) ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[1832:[bind(A,$thf( D )),bind(B,$thf( id )),bind(C,$thf( lam @ D ))]]) ).
thf(1856,plain,
! [A: term] :
( ( lam @ ( lam @ ( sub @ A @ ( push @ one @ ( comp @ id @ sh ) ) ) ) )
!= one ),
inference(simp,[status(thm)],[1833]) ).
thf(1863,plain,
! [A: term] :
( ( lam @ ( lam @ ( sub @ A @ ( push @ one @ sh ) ) ) )
!= one ),
inference(rewrite,[status(thm)],[1856,66]) ).
thf(1895,plain,
! [A: term] :
( ( ( lam @ ( lam @ ( sub @ A @ id ) ) )
!= one )
| ( ( push @ one @ sh )
!= ( push @ one @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[73,1863]) ).
thf(1896,plain,
! [A: term] :
( ( lam @ ( lam @ ( sub @ A @ id ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[1895:[]]) ).
thf(1951,plain,
! [A: term] :
( ( lam @ ( lam @ A ) )
!= one ),
inference(rewrite,[status(thm)],[1896,118]) ).
thf(1953,plain,
! [C: term,B: subst,A: term] :
( ( ( lam @ ( sub @ ( lam @ A ) @ B ) )
!= one )
| ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= ( lam @ C ) ) ),
inference(paramod_ordered,[status(thm)],[132,1951]) ).
thf(1954,plain,
! [B: subst,A: term] :
( ( lam @ ( sub @ ( lam @ A ) @ B ) )
!= one ),
inference(pattern_uni,[status(thm)],[1953:[bind(A,$thf( D )),bind(B,$thf( H )),bind(C,$thf( sub @ D @ ( push @ one @ ( comp @ H @ sh ) ) ))]]) ).
thf(1966,plain,
! [B: subst,A: term] :
( ( lam @ ( sub @ ( lam @ A ) @ B ) )
!= one ),
inference(simp,[status(thm)],[1954]) ).
thf(2716,plain,
! [D: subst,C: term,B: subst,A: term] :
( ( ( sub @ ( lam @ A ) @ B )
!= one )
| ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= ( lam @ ( sub @ ( lam @ C ) @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[132,1966]) ).
thf(2717,plain,
! [B: subst,A: term] :
( ( sub @ ( lam @ ( lam @ A ) ) @ B )
!= one ),
inference(pattern_uni,[status(thm)],[2716:[bind(A,$thf( lam @ E )),bind(B,$thf( H )),bind(C,$thf( E )),bind(D,$thf( push @ one @ ( comp @ H @ sh ) ))]]) ).
thf(2769,plain,
! [B: subst,A: term] :
( ( sub @ ( lam @ ( lam @ A ) ) @ B )
!= one ),
inference(simp,[status(thm)],[2717]) ).
thf(5479,plain,
! [C: subst,B: term,A: term] :
( ( ( sub @ ( lam @ ( lam @ A ) ) @ C )
!= one )
| ( ( lam @ ( sub @ A @ ( push @ one @ sh ) ) )
!= ( lam @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5396,2769]) ).
thf(5480,plain,
! [B: term,A: subst] :
( ( sub @ ( lam @ ( lam @ B ) ) @ A )
!= one ),
inference(pattern_uni,[status(thm)],[5479:[bind(A,$thf( D )),bind(B,$thf( sub @ D @ ( push @ one @ sh ) )),bind(C,$thf( C ))]]) ).
thf(5614,plain,
! [B: term,A: subst] :
( ( sub @ ( lam @ ( lam @ B ) ) @ A )
!= one ),
inference(simp,[status(thm)],[5480]) ).
thf(6730,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6516,128]) ).
thf(6731,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[6730]) ).
thf(6732,plain,
sk14 @ ( sub @ one @ sh ),
inference(pattern_uni,[status(thm)],[6731:[bind(A,$thf( sub @ one @ sh ))]]) ).
thf(40,plain,
! [A: term > $o] :
( ( A @ ( sk9 @ A ) )
| ( sk8 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(127,plain,
! [A: term > $o] :
( ( A @ ( sk9 @ A ) )
| ( sk8 @ A ) ),
inference(simp,[status(thm)],[40]) ).
thf(26785,plain,
( ( var @ ( sk9 @ var ) )
| ( sk8 @ var ) ),
inference(prim_subst,[status(thm)],[127:[bind(A,$thf( var ))]]) ).
thf(30267,plain,
! [A: term] :
( ( sk8 @ var )
| ~ $true
| ( sk14 @ A )
| ( ( var @ ( sk9 @ var ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[26785,128]) ).
thf(30268,plain,
! [A: term] :
( ( sk8 @ var )
| ( sk14 @ A )
| ( ( var @ ( sk9 @ var ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[30267]) ).
thf(30269,plain,
( ( sk8 @ var )
| ( sk14 @ ( sk9 @ var ) ) ),
inference(pattern_uni,[status(thm)],[30268:[bind(A,$thf( sk9 @ var ))]]) ).
thf(18025,plain,
! [A: term > $o] :
( ( var @ ( sk3 @ A ) )
| ~ $true
| ( ( sk2 @ A )
!= ( sk2
@ ^ [B: term] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[103,17995]) ).
thf(18026,plain,
! [A: term > $o] :
( ( var @ ( sk3 @ A ) )
| ( ( sk2 @ A )
!= ( sk2
@ ^ [B: term] : $false ) ) ),
inference(simp,[status(thm)],[18025]) ).
thf(18027,plain,
( var
@ ( sk3
@ ^ [A: term] : $false ) ),
inference(pattern_uni,[status(thm)],[18026:[bind(A,$thf( ^ [B: term] : $false ))]]) ).
thf(18192,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18027,99]) ).
thf(18193,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[18192]) ).
thf(18194,plain,
( var
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh ) ),
inference(pattern_uni,[status(thm)],[18193:[bind(A,$thf( sk3 @ ^ [B: term] : $false ))]]) ).
thf(18611,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18194,99]) ).
thf(18612,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[18611]) ).
thf(18613,plain,
( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ sh ) ),
inference(pattern_uni,[status(thm)],[18612:[bind(A,$thf( sub @ ( sk3 @ ^ [B: term] : $false ) @ sh ))]]) ).
thf(21532,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh )
@ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18613,128]) ).
thf(21533,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh )
@ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[21532]) ).
thf(21534,plain,
( sk14
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ sh ) ),
inference(pattern_uni,[status(thm)],[21533:[bind(A,$thf( sub @ ( sub @ ( sk3 @ ^ [B: term] : $false ) @ sh ) @ sh ))]]) ).
thf(7012,plain,
( ~ $true
| ( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[6752,241]) ).
thf(7013,plain,
( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[7012]) ).
thf(7075,plain,
( ( sub @ ( sub @ one @ sh ) @ sh )
!= sk16 ),
inference(simp,[status(thm)],[7013]) ).
thf(14518,plain,
! [C: subst,B: subst,A: term] :
( ( ( sub @ A @ ( comp @ B @ C ) )
!= sk16 )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,7075]) ).
thf(14519,plain,
( ( sub @ one @ ( comp @ sh @ sh ) )
!= sk16 ),
inference(pattern_uni,[status(thm)],[14518:[bind(A,$thf( one )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(28378,plain,
! [A: term] :
( ~ $true
| ( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ ( lam @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[26508,98]) ).
thf(28379,plain,
! [A: term] :
( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ ( lam @ A ) ) ),
inference(simp,[status(thm)],[28378]) ).
thf(28454,plain,
! [A: term] :
( ( sub @ sk21 @ sh )
!= ( lam @ A ) ),
inference(simp,[status(thm)],[28379]) ).
thf(36498,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ one ) ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= ( sub @ sk21 @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1213,28454]) ).
thf(36533,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ one ) )
!= B )
| ( ( lam @ ( lam @ ( lam @ one ) ) )
!= sk21 )
| ( A != sh ) ),
inference(simp,[status(thm)],[36498]) ).
thf(36569,plain,
( ( lam @ ( lam @ ( lam @ one ) ) )
!= sk21 ),
inference(simp,[status(thm)],[36533]) ).
thf(16,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(61,plain,
! [A: term] :
( ( one != one )
| ( one
!= ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh ) )
| ~ ( var @ A )
| ( one = A ) ),
inference(replace_leibeq,[status(thm)],[16:[bind(A,$thf( (=) @ term @ one ))]]) ).
thf(63,plain,
! [A: term] :
( ( one != one )
| ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ( one = A )
| ~ ( var @ A ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(64,plain,
! [A: term] :
( ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ( one = A )
| ~ ( var @ A ) ),
inference(simp,[status(thm)],[63]) ).
thf(214,plain,
! [C: term,B: subst,A: term] :
( ( A != one )
| ( one = C )
| ~ ( var @ C )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[68,64]) ).
thf(224,plain,
! [B: term,A: subst] :
( ( one = B )
| ~ ( var @ B )
| ( ( sub @ one @ ( push @ one @ A ) )
!= ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh ) ) ),
inference(simp,[status(thm)],[214]) ).
thf(226,plain,
! [B: term,A: subst] :
( ( one = B )
| ~ ( var @ B )
| ( ( sub @ one @ ( push @ one @ A ) )
!= ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh ) ) ),
inference(simp,[status(thm)],[224]) ).
thf(38702,plain,
! [A: term] :
( ( one = A )
| ~ ( var @ A )
| ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one ) ),
inference(rewrite,[status(thm)],[226,68]) ).
thf(1529,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ ( lam @ B ) @ C )
= ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) )
| ( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= ( sub @ B @ ( push @ one @ ( comp @ C @ sh ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1213,132]) ).
thf(1530,plain,
! [A: subst] :
( ( sub @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) @ A )
= ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1529:[bind(A,$thf( push @ one @ ( comp @ I @ sh ) )),bind(B,$thf( lam @ ( lam @ ( lam @ one ) ) )),bind(C,$thf( I ))]]) ).
thf(1616,plain,
! [A: subst] :
( ( sub @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) @ A )
= ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) ),
inference(simp,[status(thm)],[1530]) ).
thf(36485,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) @ A )
!= ( sub @ sk21 @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1616,28454]) ).
thf(36528,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ one ) ) )
!= B )
| ( ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) )
!= sk21 )
| ( A != sh ) ),
inference(simp,[status(thm)],[36485]) ).
thf(36564,plain,
( ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) )
!= sk21 ),
inference(simp,[status(thm)],[36528]) ).
thf(21,plain,
! [A: term > $o] :
( ( A @ ( sk10 @ A ) )
| ( sk8 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(89,plain,
! [A: term > $o] :
( ( A @ ( sk10 @ A ) )
| ( sk8 @ A ) ),
inference(simp,[status(thm)],[21]) ).
thf(3622,plain,
( ( var @ ( sk10 @ var ) )
| ( sk8 @ var ) ),
inference(prim_subst,[status(thm)],[89:[bind(A,$thf( var ))]]) ).
thf(4236,plain,
! [A: term] :
( ( sk8 @ var )
| ~ $true
| ( sk14 @ A )
| ( ( var @ ( sk10 @ var ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3622,128]) ).
thf(4237,plain,
! [A: term] :
( ( sk8 @ var )
| ( sk14 @ A )
| ( ( var @ ( sk10 @ var ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[4236]) ).
thf(4238,plain,
( ( sk8 @ var )
| ( sk14 @ ( sk10 @ var ) ) ),
inference(pattern_uni,[status(thm)],[4237:[bind(A,$thf( sk10 @ var ))]]) ).
thf(42,plain,
! [A: term] :
( ~ ( sk14 @ ( sub @ A @ ( push @ ( sk15 @ A ) @ id ) ) )
| ( sk14 @ ( lam @ A ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(71,plain,
! [A: term] :
( ~ ( sk14 @ ( sub @ A @ ( push @ ( sk15 @ A ) @ id ) ) )
| ( sk14 @ ( lam @ A ) ) ),
inference(simp,[status(thm)],[42]) ).
thf(1025,plain,
! [B: term,A: subst] :
( ~ ( sk14 @ ( lam @ one ) )
| ( sk14 @ ( lam @ B ) )
| ( ( sub @ ( lam @ one ) @ A )
!= ( sub @ B @ ( push @ ( sk15 @ B ) @ id ) ) ) ),
inference(paramod_ordered,[status(thm)],[997,71]) ).
thf(1026,plain,
( ~ ( sk14 @ ( lam @ one ) )
| ( sk14 @ ( lam @ ( lam @ one ) ) ) ),
inference(pattern_uni,[status(thm)],[1025:[bind(A,$thf( push @ ( sk15 @ ( lam @ one ) ) @ id )),bind(B,$thf( lam @ one ))]]) ).
thf(27,plain,
! [A: term] :
( ( sk14 @ ( sk15 @ A ) )
| ( sk14 @ ( lam @ A ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(107,plain,
! [A: term] :
( ( sk14 @ ( sk15 @ A ) )
| ( sk14 @ ( lam @ A ) ) ),
inference(simp,[status(thm)],[27]) ).
thf(416,plain,
! [C: term,B: subst,A: term] :
( ~ ( sk14 @ A )
| ( sk14 @ ( lam @ C ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ C @ ( push @ ( sk15 @ C ) @ id ) ) ) ),
inference(paramod_ordered,[status(thm)],[68,71]) ).
thf(417,plain,
( ~ ( sk14 @ ( sk15 @ one ) )
| ( sk14 @ ( lam @ one ) ) ),
inference(pattern_uni,[status(thm)],[416:[bind(A,$thf( sk15 @ one )),bind(B,$thf( id )),bind(C,$thf( one ))]]) ).
thf(1320,plain,
! [A: term] :
( ( sk14 @ ( lam @ A ) )
| ~ $true
| ( sk14 @ ( lam @ one ) )
| ( ( sk14 @ ( sk15 @ A ) )
!= ( sk14 @ ( sk15 @ one ) ) ) ),
inference(paramod_ordered,[status(thm)],[107,417]) ).
thf(1321,plain,
! [A: term] :
( ( sk14 @ ( lam @ A ) )
| ( sk14 @ ( lam @ one ) )
| ( ( sk14 @ ( sk15 @ A ) )
!= ( sk14 @ ( sk15 @ one ) ) ) ),
inference(simp,[status(thm)],[1320]) ).
thf(1322,plain,
( ( sk14 @ ( lam @ one ) )
| ( sk14 @ ( lam @ one ) ) ),
inference(pattern_uni,[status(thm)],[1321:[bind(A,$thf( one ))]]) ).
thf(1347,plain,
sk14 @ ( lam @ one ),
inference(simp,[status(thm)],[1322]) ).
thf(6395,plain,
( ~ $true
| ( sk14 @ ( lam @ ( lam @ one ) ) ) ),
inference(rewrite,[status(thm)],[1026,1347]) ).
thf(6396,plain,
sk14 @ ( lam @ ( lam @ one ) ),
inference(simp,[status(thm)],[6395]) ).
thf(7023,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6752,99]) ).
thf(7024,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ ( sub @ one @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[7023]) ).
thf(7025,plain,
var @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[7024:[bind(A,$thf( sub @ ( sub @ one @ sh ) @ sh ))]]) ).
thf(8630,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7025,128]) ).
thf(8631,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[8630]) ).
thf(8632,plain,
sk14 @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[8631:[bind(A,$thf( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ))]]) ).
thf(1777,plain,
! [C: subst,B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) )
!= one )
| ( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= ( sub @ B @ ( push @ one @ ( comp @ C @ sh ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1213,1066]) ).
thf(1778,plain,
( ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[1777:[bind(A,$thf( push @ one @ ( comp @ I @ sh ) )),bind(B,$thf( lam @ ( lam @ ( lam @ one ) ) )),bind(C,$thf( I ))]]) ).
thf(215,plain,
! [C: subst,B: term,A: term] :
( ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ~ ( var @ A )
| ( ( sub @ A @ ( push @ B @ C ) )
= B )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[64,68]) ).
thf(216,plain,
! [C: subst,B: term,A: term] :
( ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ~ ( var @ A )
| ( ( sub @ A @ ( push @ B @ C ) )
= B ) ),
inference(pattern_uni,[status(thm)],[215:[]]) ).
thf(21555,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub
@ ( sub
@ ( sk3
@ ^ [D: term] : $false )
@ sh )
@ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,18613]) ).
thf(21556,plain,
( var
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ ( comp @ sh @ sh ) ) ),
inference(pattern_uni,[status(thm)],[21555:[bind(A,$thf( sk3 @ ^ [D: term] : $false )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(6532,plain,
! [A: term] :
( ( sk8 @ var )
| ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sk10 @ var ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3622,99]) ).
thf(6533,plain,
! [A: term] :
( ( sk8 @ var )
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sk10 @ var ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[6532]) ).
thf(6534,plain,
( ( sk8 @ var )
| ( var @ ( sub @ ( sk10 @ var ) @ sh ) ) ),
inference(pattern_uni,[status(thm)],[6533:[bind(A,$thf( sk10 @ var ))]]) ).
thf(7,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk4 @ A ) )
| ~ ( A @ ( lam @ ( sk6 @ A ) ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(59,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= ( sk4 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
!= ( lam @ ( sk6 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= B ) ),
inference(replace_leibeq,[status(thm)],[7:[bind(A,$thf( (=) @ term @ ( lam @ ( sk6 @ A ) ) ))]]) ).
thf(105,plain,
! [B: term,A: term > $o] :
( ( ( lam @ ( sk6 @ A ) )
= ( sk4 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
!= ( lam @ ( sk6 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= B )
| ~ ( sk2 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ),
inference(lifteq,[status(thm)],[59]) ).
thf(106,plain,
! [B: term,A: term > $o] :
( ( ( lam @ ( sk6 @ A ) )
= ( sk4 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
!= ( lam @ ( sk6 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= B )
| ~ ( sk2 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[105]) ).
thf(1067,plain,
! [D: subst,C: term,B: subst,A: term] :
( ( ( sub @ ( sub @ ( lam @ A ) @ B ) @ D )
!= one )
| ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= ( lam @ C ) ) ),
inference(paramod_ordered,[status(thm)],[132,979]) ).
thf(1068,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ ( sub @ ( lam @ B ) @ C ) @ A )
!= one ),
inference(pattern_uni,[status(thm)],[1067:[bind(A,$thf( E )),bind(B,$thf( I )),bind(C,$thf( sub @ E @ ( push @ one @ ( comp @ I @ sh ) ) )),bind(D,$thf( D ))]]) ).
thf(1091,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ ( sub @ ( lam @ B ) @ C ) @ A )
!= one ),
inference(simp,[status(thm)],[1068]) ).
thf(2868,plain,
! [D: subst,C: term,B: subst,A: term] :
( ( A != one )
| ( ( sub @ A @ id )
!= ( sub @ ( sub @ ( lam @ C ) @ D ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[118,1091]) ).
thf(2869,plain,
! [B: term,A: subst] :
( ( sub @ ( lam @ B ) @ A )
!= one ),
inference(pattern_uni,[status(thm)],[2868:[bind(A,$thf( sub @ ( lam @ G ) @ F )),bind(B,$thf( id )),bind(C,$thf( G )),bind(D,$thf( F ))]]) ).
thf(2925,plain,
! [B: term,A: subst] :
( ( sub @ ( lam @ B ) @ A )
!= one ),
inference(simp,[status(thm)],[2869]) ).
thf(951,plain,
! [C: term,B: subst,A: term] :
( ~ ( var @ ( sub @ ( lam @ A ) @ B ) )
| ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= ( lam @ C ) ) ),
inference(paramod_ordered,[status(thm)],[132,98]) ).
thf(952,plain,
! [B: subst,A: term] :
~ ( var @ ( sub @ ( lam @ A ) @ B ) ),
inference(pattern_uni,[status(thm)],[951:[bind(A,$thf( D )),bind(B,$thf( H )),bind(C,$thf( sub @ D @ ( push @ one @ ( comp @ H @ sh ) ) ))]]) ).
thf(1003,plain,
! [B: subst,A: term] :
~ ( var @ ( sub @ ( lam @ A ) @ B ) ),
inference(simp,[status(thm)],[952]) ).
thf(1253,plain,
! [D: subst,C: term,B: subst,A: term] :
( ~ ( var @ ( sub @ ( sub @ ( lam @ A ) @ B ) @ D ) )
| ( ( lam @ ( sub @ A @ ( push @ one @ ( comp @ B @ sh ) ) ) )
!= ( lam @ C ) ) ),
inference(paramod_ordered,[status(thm)],[132,1003]) ).
thf(1254,plain,
! [C: subst,B: term,A: subst] :
~ ( var @ ( sub @ ( sub @ ( lam @ B ) @ C ) @ A ) ),
inference(pattern_uni,[status(thm)],[1253:[bind(A,$thf( E )),bind(B,$thf( I )),bind(C,$thf( sub @ E @ ( push @ one @ ( comp @ I @ sh ) ) )),bind(D,$thf( D ))]]) ).
thf(1283,plain,
! [C: subst,B: term,A: subst] :
~ ( var @ ( sub @ ( sub @ ( lam @ B ) @ C ) @ A ) ),
inference(simp,[status(thm)],[1254]) ).
thf(21570,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh )
@ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18613,99]) ).
thf(21571,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh )
@ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[21570]) ).
thf(21572,plain,
( var
@ ( sub
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ sh )
@ sh ) ),
inference(pattern_uni,[status(thm)],[21571:[bind(A,$thf( sub @ ( sub @ ( sk3 @ ^ [B: term] : $false ) @ sh ) @ sh ))]]) ).
thf(50676,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub
@ ( sub
@ ( sub
@ ( sk3
@ ^ [D: term] : $false )
@ sh )
@ sh )
@ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,21572]) ).
thf(50677,plain,
( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ ( comp @ sh @ sh ) ) ),
inference(pattern_uni,[status(thm)],[50676:[bind(A,$thf( sub @ ( sk3 @ ^ [D: term] : $false ) @ sh )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(31,plain,
! [C: subst,B: subst,A: term] :
( ( comp @ ( push @ A @ B ) @ C )
= ( push @ ( sub @ A @ C ) @ ( comp @ B @ C ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(120,plain,
! [C: subst,B: subst,A: term] :
( ( comp @ ( push @ A @ B ) @ C )
= ( push @ ( sub @ A @ C ) @ ( comp @ B @ C ) ) ),
inference(lifteq,[status(thm)],[31]) ).
thf(121,plain,
! [C: subst,B: subst,A: term] :
( ( comp @ ( push @ A @ B ) @ C )
= ( push @ ( sub @ A @ C ) @ ( comp @ B @ C ) ) ),
inference(simp,[status(thm)],[120]) ).
thf(15,plain,
! [C: subst,B: subst,A: subst] :
( ( comp @ ( comp @ A @ B ) @ C )
= ( comp @ A @ ( comp @ B @ C ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(146,plain,
! [C: subst,B: subst,A: subst] :
( ( comp @ ( comp @ A @ B ) @ C )
= ( comp @ A @ ( comp @ B @ C ) ) ),
inference(lifteq,[status(thm)],[15]) ).
thf(147,plain,
! [C: subst,B: subst,A: subst] :
( ( comp @ ( comp @ A @ B ) @ C )
= ( comp @ A @ ( comp @ B @ C ) ) ),
inference(simp,[status(thm)],[146]) ).
thf(14526,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,8632]) ).
thf(14527,plain,
sk14 @ ( sub @ ( sub @ one @ sh ) @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[14526:[bind(A,$thf( sub @ one @ sh )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(116,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( A @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(simp,[status(thm)],[18]) ).
thf(2964,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) ) )
!= one )
| ( ( sub @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) @ A )
!= ( sub @ B @ ( push @ one @ sh ) ) ) ),
inference(paramod_ordered,[status(thm)],[1616,1863]) ).
thf(2965,plain,
( ( lam @ ( lam @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[2964:[bind(A,$thf( push @ one @ sh )),bind(B,$thf( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ))]]) ).
thf(14739,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ ( sub @ A @ ( comp @ B @ C ) ) @ sh ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,7025]) ).
thf(14740,plain,
var @ ( sub @ ( sub @ one @ ( comp @ sh @ sh ) ) @ sh ),
inference(pattern_uni,[status(thm)],[14739:[bind(A,$thf( one )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(24788,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ ( comp @ sh @ sh ) ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,14740]) ).
thf(24789,plain,
var @ ( sub @ one @ ( comp @ ( comp @ sh @ sh ) @ sh ) ),
inference(pattern_uni,[status(thm)],[24788:[bind(A,$thf( one )),bind(B,$thf( comp @ sh @ sh )),bind(C,$thf( sh ))]]) ).
thf(40261,plain,
var @ ( sub @ one @ ( comp @ sh @ ( comp @ sh @ sh ) ) ),
inference(rewrite,[status(thm)],[24789,147]) ).
thf(8,plain,
! [C: subst,B: term,A: term] :
( ( sub @ ( ap @ A @ B ) @ C )
= ( ap @ ( sub @ A @ C ) @ ( sub @ B @ C ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(133,plain,
! [C: subst,B: term,A: term] :
( ( sub @ ( ap @ A @ B ) @ C )
= ( ap @ ( sub @ A @ C ) @ ( sub @ B @ C ) ) ),
inference(lifteq,[status(thm)],[8]) ).
thf(34,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( var @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(56,plain,
! [A: term] :
( ( one != one )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A )
| ( one = A ) ),
inference(replace_leibeq,[status(thm)],[34:[bind(A,$thf( (=) @ term @ one ))]]) ).
thf(69,plain,
! [A: term] :
( ( one != one )
| ( one = A )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A ) ),
inference(lifteq,[status(thm)],[56]) ).
thf(70,plain,
! [A: term] :
( ( one = A )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A ) ),
inference(simp,[status(thm)],[69]) ).
thf(264,plain,
! [B: term,A: term] :
( ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A )
| ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ( A = B )
| ~ ( var @ B )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[70,64]) ).
thf(265,plain,
! [B: term,A: term] :
( ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A )
| ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ( A = B )
| ~ ( var @ B ) ),
inference(pattern_uni,[status(thm)],[264:[]]) ).
thf(4248,plain,
( ( sk8 @ var )
| ~ $true
| ( ( var @ ( sk10 @ var ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[3622,241]) ).
thf(4249,plain,
( ( sk8 @ var )
| ( ( var @ ( sk10 @ var ) )
!= ( var @ sk16 ) ) ),
inference(simp,[status(thm)],[4248]) ).
thf(4285,plain,
( ( sk8 @ var )
| ( ( sk10 @ var )
!= sk16 ) ),
inference(simp,[status(thm)],[4249]) ).
thf(26491,plain,
! [A: term] :
( ~ $true
| ( ( var @ ( lam @ A ) )
!= ( var @ sk21 ) ) ),
inference(paramod_ordered,[status(thm)],[26357,98]) ).
thf(26492,plain,
! [A: term] :
( ( var @ ( lam @ A ) )
!= ( var @ sk21 ) ),
inference(simp,[status(thm)],[26491]) ).
thf(26567,plain,
! [A: term] :
( ( lam @ A )
!= sk21 ),
inference(simp,[status(thm)],[26492]) ).
thf(18590,plain,
! [A: term] :
( ~ $true
| ( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh ) )
!= ( var @ ( lam @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[18194,98]) ).
thf(18591,plain,
! [A: term] :
( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh ) )
!= ( var @ ( lam @ A ) ) ),
inference(simp,[status(thm)],[18590]) ).
thf(18712,plain,
! [A: term] :
( ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh )
!= ( lam @ A ) ),
inference(simp,[status(thm)],[18591]) ).
thf(49834,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ one ) ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= ( sub
@ ( sk3
@ ^ [C: term] : $false )
@ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1213,18712]) ).
thf(49900,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ one ) )
!= B )
| ( ( sk3
@ ^ [C: term] : $false )
!= ( lam @ ( lam @ ( lam @ one ) ) ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[49834]) ).
thf(50004,plain,
( ( sk3
@ ^ [A: term] : $false )
!= ( lam @ ( lam @ ( lam @ one ) ) ) ),
inference(simp,[status(thm)],[49900]) ).
thf(18143,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ $true
| ( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18027,88]) ).
thf(18144,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[18143]) ).
thf(18145,plain,
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( ( sk3
@ ^ [A: term] : $false )
= one ) ),
inference(pattern_uni,[status(thm)],[18144:[bind(A,$thf( sk3 @ ^ [B: term] : $false ))]]) ).
thf(44,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk5 @ A ) )
| ~ ( A @ ( lam @ ( sk6 @ A ) ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(57,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= ( sk5 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
!= ( lam @ ( sk6 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= B ) ),
inference(replace_leibeq,[status(thm)],[44:[bind(A,$thf( (=) @ term @ ( lam @ ( sk6 @ A ) ) ))]]) ).
thf(84,plain,
! [B: term,A: term > $o] :
( ( ( lam @ ( sk6 @ A ) )
= ( sk5 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
!= ( lam @ ( sk6 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= B )
| ~ ( sk2 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ),
inference(lifteq,[status(thm)],[57]) ).
thf(85,plain,
! [B: term,A: term > $o] :
( ( ( lam @ ( sk6 @ A ) )
= ( sk5 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
!= ( lam @ ( sk6 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ) )
| ( ( lam @ ( sk6 @ A ) )
= B )
| ~ ( sk2 @ ( (=) @ term @ ( lam @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[84]) ).
thf(102,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( var @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(simp,[status(thm)],[34]) ).
thf(9988,plain,
! [B: term,A: subst] :
( ( ( lam @ one )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ one ) @ A )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[997,7078]) ).
thf(10015,plain,
! [B: term,A: subst] :
( ( one != B )
| ( ( sub @ one @ sh )
!= ( lam @ one ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[9988]) ).
thf(10048,plain,
( ( sub @ one @ sh )
!= ( lam @ one ) ),
inference(simp,[status(thm)],[10015]) ).
thf(10103,plain,
! [B: subst,A: term] :
( ( A
!= ( lam @ one ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[68,10048]) ).
thf(10105,plain,
! [A: subst] :
( ( one != one )
| ( ( push @ ( lam @ one ) @ A )
!= sh ) ),
inference(simp,[status(thm)],[10103]) ).
thf(10133,plain,
! [A: subst] :
( ( push @ ( lam @ one ) @ A )
!= sh ),
inference(simp,[status(thm)],[10105]) ).
thf(14523,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ ( sub @ A @ ( comp @ B @ C ) ) @ sh ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,8632]) ).
thf(14524,plain,
sk14 @ ( sub @ ( sub @ one @ ( comp @ sh @ sh ) ) @ sh ),
inference(pattern_uni,[status(thm)],[14523:[bind(A,$thf( one )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(36,plain,
! [A: subst] :
( ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) )
= A ),
inference(cnfConj,[status(thm)],[5]) ).
thf(136,plain,
! [A: subst] :
( ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) )
= A ),
inference(lifteq,[status(thm)],[36]) ).
thf(137,plain,
! [A: subst] :
( ( push @ ( sub @ one @ A ) @ ( comp @ sh @ A ) )
= A ),
inference(simp,[status(thm)],[136]) ).
thf(38,plain,
! [B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ),
inference(cnfConj,[status(thm)],[5]) ).
thf(91,plain,
! [B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ),
inference(lifteq,[status(thm)],[38]) ).
thf(92,plain,
! [B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ),
inference(simp,[status(thm)],[91]) ).
thf(221,plain,
! [C: subst,B: term,A: term] :
( ( A = B )
| ( ( sub @ A @ id )
!= ( sub @ one @ ( push @ B @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[118,68]) ).
thf(222,plain,
! [C: subst,B: term,A: term] :
( ( A = B )
| ( A != one )
| ( ( push @ B @ C )
!= id ) ),
inference(simp,[status(thm)],[221]) ).
thf(229,plain,
! [B: subst,A: term] :
( ( one = A )
| ( ( push @ A @ B )
!= id ) ),
inference(simp,[status(thm)],[222]) ).
thf(13,plain,
! [C: subst,B: term,A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( sk11 @ A )
| ( var @ ( sk13 @ C @ B @ A ) )
| ( A @ ( sub @ B @ C ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(97,plain,
! [C: subst,B: term,A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( sk11 @ A )
| ( var @ ( sk13 @ C @ B @ A ) )
| ( A @ ( sub @ B @ C ) ) ),
inference(simp,[status(thm)],[13]) ).
thf(49815,plain,
! [B: term,A: subst] :
( ( ( lam @ one )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ one ) @ A )
!= ( sub
@ ( sk3
@ ^ [C: term] : $false )
@ sh ) ) ),
inference(paramod_ordered,[status(thm)],[997,18712]) ).
thf(49909,plain,
! [B: term,A: subst] :
( ( one != B )
| ( ( sk3
@ ^ [C: term] : $false )
!= ( lam @ one ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[49815]) ).
thf(50013,plain,
( ( sk3
@ ^ [A: term] : $false )
!= ( lam @ one ) ),
inference(simp,[status(thm)],[49909]) ).
thf(18596,plain,
( ~ $true
| ( ( var
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[18194,241]) ).
thf(18597,plain,
( ( var
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[18596]) ).
thf(18673,plain,
( ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
!= sk16 ),
inference(simp,[status(thm)],[18597]) ).
thf(30,plain,
! [D: term,C: term,B: term,A: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( C = D ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(138,plain,
! [D: term,C: term,B: term,A: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( C = D ) ),
inference(lifteq,[status(thm)],[30]) ).
thf(139,plain,
! [D: term,C: term,B: term,A: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( C = D ) ),
inference(simp,[status(thm)],[138]) ).
thf(140,plain,
? [A: term > term > term] :
! [B: term,C: term] :
( ( A @ B @ ( ap @ B @ C ) )
= C ),
inference(detectInverse,[status(thm)],[139]) ).
thf(141,plain,
! [B: term,A: term] :
( ( sk19 @ A @ ( ap @ A @ B ) )
= B ),
inference(cnf,[status(esa)],[140]) ).
thf(889,plain,
! [B: term,A: term] :
( ( sk19 @ A @ ( ap @ A @ B ) )
= B ),
inference(lifteq,[status(thm)],[141]) ).
thf(31342,plain,
( ~ $true
| ( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[28403,241]) ).
thf(31343,plain,
( ( var @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[31342]) ).
thf(31465,plain,
( ( sub @ ( sub @ sk21 @ sh ) @ sh )
!= sk16 ),
inference(simp,[status(thm)],[31343]) ).
thf(42457,plain,
( ~ $true
| ( ( var @ ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[31362,241]) ).
thf(42458,plain,
( ( var @ ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[42457]) ).
thf(42568,plain,
( ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh )
!= sk16 ),
inference(simp,[status(thm)],[42458]) ).
thf(25611,plain,
! [A: term > $o] :
( ( sk8 @ var )
| ~ $true
| ( sk2 @ A )
| ( ( var @ ( sk10 @ var ) )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[3622,126]) ).
thf(25612,plain,
! [A: term > $o] :
( ( sk8 @ var )
| ( sk2 @ A )
| ( ( var @ ( sk10 @ var ) )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(simp,[status(thm)],[25611]) ).
thf(25806,plain,
( ( sk8 @ var )
| ( sk2
@ ^ [A: term] : ( var @ ( sk10 @ var ) ) ) ),
inference(pre_uni,[status(thm)],[25612:[bind(A,$thf( ^ [B: term] : ( var @ ( sk10 @ var ) ) ))]]) ).
thf(1566,plain,
! [C: subst,B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ one ) ) )
!= one )
| ( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= ( sub @ ( lam @ B ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1213,979]) ).
thf(1567,plain,
( ( lam @ ( lam @ ( lam @ one ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[1566:[bind(A,$thf( A )),bind(B,$thf( lam @ ( lam @ one ) )),bind(C,$thf( A ))]]) ).
thf(6736,plain,
! [A: term] :
( ~ $true
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ ( lam @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[6516,98]) ).
thf(6737,plain,
! [A: term] :
( ( var @ ( sub @ one @ sh ) )
!= ( var @ ( lam @ A ) ) ),
inference(simp,[status(thm)],[6736]) ).
thf(6786,plain,
! [A: term] :
( ( sub @ one @ sh )
!= ( lam @ A ) ),
inference(simp,[status(thm)],[6737]) ).
thf(8507,plain,
! [C: term,B: subst,A: term] :
( ( A
!= ( lam @ C ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[68,6786]) ).
thf(8525,plain,
! [B: term,A: subst] :
( ( one != one )
| ( ( push @ ( lam @ B ) @ A )
!= sh ) ),
inference(simp,[status(thm)],[8507]) ).
thf(8544,plain,
! [B: term,A: subst] :
( ( push @ ( lam @ B ) @ A )
!= sh ),
inference(simp,[status(thm)],[8525]) ).
thf(21850,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub
@ ( sub
@ ( sk3
@ ^ [D: term] : $false )
@ sh )
@ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,21534]) ).
thf(21851,plain,
( sk14
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ ( comp @ sh @ sh ) ) ),
inference(pattern_uni,[status(thm)],[21850:[bind(A,$thf( sk3 @ ^ [D: term] : $false )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(6739,plain,
( ~ $true
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[6516,241]) ).
thf(6740,plain,
( ( var @ ( sub @ one @ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[6739]) ).
thf(6783,plain,
( ( sub @ one @ sh )
!= sk16 ),
inference(simp,[status(thm)],[6740]) ).
thf(6931,plain,
! [B: subst,A: term] :
( ( A != sk16 )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[68,6783]) ).
thf(6935,plain,
! [A: subst] :
( ( one != one )
| ( ( push @ sk16 @ A )
!= sh ) ),
inference(simp,[status(thm)],[6931]) ).
thf(6946,plain,
! [A: subst] :
( ( push @ sk16 @ A )
!= sh ),
inference(simp,[status(thm)],[6935]) ).
thf(29,plain,
! [B: term,A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( A @ B )
| ( A @ ( sub @ ( sk12 @ A ) @ ( push @ B @ id ) ) )
| ( sk11 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(53,plain,
! [A: term] :
( ~ ( sk8 @ ( (=) @ term @ A ) )
| ( A != A )
| ( A
= ( sub @ ( sk12 @ ( (=) @ term @ A ) ) @ ( push @ A @ id ) ) )
| ( sk11 @ ( (=) @ term @ A ) ) ),
inference(replace_leibeq,[status(thm)],[29:[bind(A,$thf( (=) @ term @ B ))]]) ).
thf(95,plain,
! [A: term] :
( ( A != A )
| ( ( sub @ ( sk12 @ ( (=) @ term @ A ) ) @ ( push @ A @ id ) )
= A )
| ~ ( sk8 @ ( (=) @ term @ A ) )
| ( sk11 @ ( (=) @ term @ A ) ) ),
inference(lifteq,[status(thm)],[53]) ).
thf(96,plain,
! [A: term] :
( ( ( sub @ ( sk12 @ ( (=) @ term @ A ) ) @ ( push @ A @ id ) )
= A )
| ~ ( sk8 @ ( (=) @ term @ A ) )
| ( sk11 @ ( (=) @ term @ A ) ) ),
inference(simp,[status(thm)],[95]) ).
thf(25551,plain,
! [A: term > $o] :
( ( sk8 @ var )
| ~ $true
| ( sk2 @ A )
| ( ( sk14 @ ( sk10 @ var ) )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4238,126]) ).
thf(25552,plain,
! [A: term > $o] :
( ( sk8 @ var )
| ( sk2 @ A )
| ( ( sk14 @ ( sk10 @ var ) )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(simp,[status(thm)],[25551]) ).
thf(25794,plain,
( ( sk8 @ var )
| ( sk2
@ ^ [A: term] : ( sk14 @ ( sk10 @ var ) ) ) ),
inference(pre_uni,[status(thm)],[25552:[bind(A,$thf( ^ [B: term] : ( sk14 @ ( sk10 @ var ) ) ))]]) ).
thf(18579,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18194,128]) ).
thf(18580,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[18579]) ).
thf(18581,plain,
( sk14
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh ) ),
inference(pattern_uni,[status(thm)],[18580:[bind(A,$thf( sub @ ( sk3 @ ^ [B: term] : $false ) @ sh ))]]) ).
thf(49763,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ one ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ one ) ) @ A )
!= ( sub
@ ( sk3
@ ^ [C: term] : $false )
@ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1055,18712]) ).
thf(49912,plain,
! [B: term,A: subst] :
( ( ( lam @ one )
!= B )
| ( ( sk3
@ ^ [C: term] : $false )
!= ( lam @ ( lam @ one ) ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[49763]) ).
thf(50016,plain,
( ( sk3
@ ^ [A: term] : $false )
!= ( lam @ ( lam @ one ) ) ),
inference(simp,[status(thm)],[49912]) ).
thf(30333,plain,
! [A: term > $o] :
( ( var @ ( sk9 @ var ) )
| ~ $true
| ( sk2 @ A )
| ( ( sk8 @ var )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[26785,126]) ).
thf(30334,plain,
! [A: term > $o] :
( ( var @ ( sk9 @ var ) )
| ( sk2 @ A )
| ( ( sk8 @ var )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(simp,[status(thm)],[30333]) ).
thf(30401,plain,
( ( var @ ( sk9 @ var ) )
| ( sk2
@ ^ [A: term] : ( sk8 @ var ) ) ),
inference(pre_uni,[status(thm)],[30334:[bind(A,$thf( ^ [B: term] : ( sk8 @ var ) ))]]) ).
thf(49463,plain,
! [B: term,A: term > $o] :
( ( var @ ( sk9 @ var ) )
| ~ $true
| ( A @ ( sk5 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B )
| ( ( sk2
@ ^ [C: term] : ( sk8 @ var ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[30401,114]) ).
thf(49464,plain,
! [B: term,A: term > $o] :
( ( var @ ( sk9 @ var ) )
| ( A @ ( sk5 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B )
| ( ( sk2
@ ^ [C: term] : ( sk8 @ var ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[49463]) ).
thf(49465,plain,
( ( var @ ( sk9 @ var ) )
| ( sk8 @ var )
| ( sk8 @ var )
| ( sk8 @ var ) ),
inference(pattern_uni,[status(thm)],[49464:[bind(A,$thf( ^ [C: term] : ( sk8 @ var ) )),bind(B,$thf( B ))]]) ).
thf(49645,plain,
( ( var @ ( sk9 @ var ) )
| ( sk8 @ var ) ),
inference(simp,[status(thm)],[49465]) ).
thf(50619,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var
@ ( sub
@ ( sub
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh )
@ sh )
@ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[21572,128]) ).
thf(50620,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var
@ ( sub
@ ( sub
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ sh )
@ sh )
@ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[50619]) ).
thf(50621,plain,
( sk14
@ ( sub
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ sh )
@ sh ) ),
inference(pattern_uni,[status(thm)],[50620:[bind(A,$thf( sub @ ( sub @ ( sub @ ( sk3 @ ^ [B: term] : $false ) @ sh ) @ sh ) @ sh ))]]) ).
thf(295,plain,
! [C: subst,B: term,A: term] :
( ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A )
| ( ( sub @ A @ ( push @ B @ C ) )
= B )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[70,68]) ).
thf(296,plain,
! [C: subst,B: term,A: term] :
( ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A )
| ( ( sub @ A @ ( push @ B @ C ) )
= B ) ),
inference(pattern_uni,[status(thm)],[295:[]]) ).
thf(19,plain,
! [C: subst,B: term,A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( sk11 @ A )
| ~ ( A @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) )
| ( A @ ( sub @ B @ C ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(62,plain,
! [C: subst,B: term,A: term > $o] :
( ~ ( sk8 @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) )
| ~ ( sk11 @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) )
| ( ( sub @ ( sk13 @ C @ B @ A ) @ C )
!= ( sub @ ( sk13 @ C @ B @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) ) @ C ) )
| ( ( sub @ ( sk13 @ C @ B @ A ) @ C )
= ( sub @ B @ C ) ) ),
inference(replace_leibeq,[status(thm)],[19:[bind(A,$thf( (=) @ term @ ( sub @ ( sk13 @ C @ B @ (@) ) @ C ) ))]]) ).
thf(148,plain,
! [C: subst,B: term,A: term > $o] :
( ( ( sub @ ( sk13 @ C @ B @ A ) @ C )
!= ( sub @ ( sk13 @ C @ B @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) ) @ C ) )
| ( ( sub @ ( sk13 @ C @ B @ A ) @ C )
= ( sub @ B @ C ) )
| ~ ( sk8 @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) )
| ~ ( sk11 @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) ) ),
inference(lifteq,[status(thm)],[62]) ).
thf(149,plain,
! [C: subst,B: term,A: term > $o] :
( ( ( sub @ ( sk13 @ C @ B @ A ) @ C )
!= ( sub @ ( sk13 @ C @ B @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) ) @ C ) )
| ( ( sub @ ( sk13 @ C @ B @ A ) @ C )
= ( sub @ B @ C ) )
| ~ ( sk8 @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) )
| ~ ( sk11 @ ( (=) @ term @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) ) ) ),
inference(simp,[status(thm)],[148]) ).
thf(26484,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[26357,128]) ).
thf(26485,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[26484]) ).
thf(26486,plain,
sk14 @ sk21,
inference(pattern_uni,[status(thm)],[26485:[bind(A,$thf( sk21 ))]]) ).
thf(28387,plain,
( ~ $true
| ( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[26508,241]) ).
thf(28388,plain,
( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[28387]) ).
thf(28489,plain,
( ( sub @ sk21 @ sh )
!= sk16 ),
inference(simp,[status(thm)],[28388]) ).
thf(14742,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,7025]) ).
thf(14743,plain,
var @ ( sub @ ( sub @ one @ sh ) @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[14742:[bind(A,$thf( sub @ one @ sh )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(8643,plain,
( ~ $true
| ( ( var @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[7025,241]) ).
thf(8644,plain,
( ( var @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[8643]) ).
thf(8722,plain,
( ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh )
!= sk16 ),
inference(simp,[status(thm)],[8644]) ).
thf(14703,plain,
! [C: subst,B: subst,A: term] :
( ( ( sub @ ( sub @ A @ ( comp @ B @ C ) ) @ sh )
!= sk16 )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,8722]) ).
thf(14704,plain,
( ( sub @ ( sub @ one @ ( comp @ sh @ sh ) ) @ sh )
!= sk16 ),
inference(pattern_uni,[status(thm)],[14703:[bind(A,$thf( one )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(17191,plain,
! [C: subst,B: subst,A: term] :
( ( ( sub @ A @ ( comp @ B @ C ) )
!= sk16 )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ ( comp @ sh @ sh ) ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,14704]) ).
thf(17192,plain,
( ( sub @ one @ ( comp @ ( comp @ sh @ sh ) @ sh ) )
!= sk16 ),
inference(pattern_uni,[status(thm)],[17191:[bind(A,$thf( one )),bind(B,$thf( comp @ sh @ sh )),bind(C,$thf( sh ))]]) ).
thf(38309,plain,
( ( sub @ one @ ( comp @ sh @ ( comp @ sh @ sh ) ) )
!= sk16 ),
inference(rewrite,[status(thm)],[17192,147]) ).
thf(17040,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ one @ sh ) @ ( comp @ sh @ sh ) ) ) ),
inference(paramod_ordered,[status(thm)],[112,14527]) ).
thf(17041,plain,
sk14 @ ( sub @ one @ ( comp @ sh @ ( comp @ sh @ sh ) ) ),
inference(pattern_uni,[status(thm)],[17040:[bind(A,$thf( one )),bind(B,$thf( sh )),bind(C,$thf( comp @ sh @ sh ))]]) ).
thf(144,plain,
! [C: subst,B: term,A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( sk11 @ A )
| ~ ( A @ ( sub @ ( sk13 @ C @ B @ A ) @ C ) )
| ( A @ ( sub @ B @ C ) ) ),
inference(simp,[status(thm)],[19]) ).
thf(4216,plain,
! [A: term] :
( ( sk8 @ var )
| ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ $true
| ( ( var @ ( sk10 @ var ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3622,88]) ).
thf(4217,plain,
! [A: term] :
( ( sk8 @ var )
| ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ( ( var @ ( sk10 @ var ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[4216]) ).
thf(4218,plain,
( ( sk8 @ var )
| ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( ( sk10 @ var )
= one ) ),
inference(pattern_uni,[status(thm)],[4217:[bind(A,$thf( sk10 @ var ))]]) ).
thf(7534,plain,
! [A: term] :
( ( sk8 @ var )
| ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sk10 @ var ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6534,128]) ).
thf(7535,plain,
! [A: term] :
( ( sk8 @ var )
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sk10 @ var ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[7534]) ).
thf(7536,plain,
( ( sk8 @ var )
| ( sk14 @ ( sub @ ( sk10 @ var ) @ sh ) ) ),
inference(pattern_uni,[status(thm)],[7535:[bind(A,$thf( sub @ ( sk10 @ var ) @ sh ))]]) ).
thf(8654,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7025,99]) ).
thf(8655,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[8654]) ).
thf(8656,plain,
var @ ( sub @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[8655:[bind(A,$thf( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ))]]) ).
thf(18165,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18027,128]) ).
thf(18166,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[18165]) ).
thf(18167,plain,
( sk14
@ ( sk3
@ ^ [A: term] : $false ) ),
inference(pattern_uni,[status(thm)],[18166:[bind(A,$thf( sk3 @ ^ [B: term] : $false ))]]) ).
thf(86,plain,
! [B: term,A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( A @ B )
| ( A @ ( sub @ ( sk12 @ A ) @ ( push @ B @ id ) ) )
| ( sk11 @ A ) ),
inference(simp,[status(thm)],[29]) ).
thf(113,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk4 @ A ) )
| ~ ( A @ ( lam @ ( sk6 @ A ) ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[7]) ).
thf(14,plain,
! [A: subst] :
( ( comp @ A @ id )
= A ),
inference(cnfConj,[status(thm)],[5]) ).
thf(80,plain,
! [A: subst] :
( ( comp @ A @ id )
= A ),
inference(lifteq,[status(thm)],[14]) ).
thf(81,plain,
! [A: subst] :
( ( comp @ A @ id )
= A ),
inference(simp,[status(thm)],[80]) ).
thf(26495,plain,
( ~ $true
| ( ( var @ sk21 )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[26357,241]) ).
thf(26496,plain,
( ( var @ sk21 )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[26495]) ).
thf(26568,plain,
sk21 != sk16,
inference(simp,[status(thm)],[26496]) ).
thf(25538,plain,
! [B: term > $o,A: term > $o] :
( ( sk2 @ A )
| ~ $true
| ( sk2 @ B )
| ( ( sk14 @ ( sk3 @ A ) )
!= ( B @ ( sk3 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[408,126]) ).
thf(25539,plain,
! [B: term > $o,A: term > $o] :
( ( sk2 @ A )
| ( sk2 @ B )
| ( ( sk14 @ ( sk3 @ A ) )
!= ( B @ ( sk3 @ B ) ) ) ),
inference(simp,[status(thm)],[25538]) ).
thf(25876,plain,
( ( sk2 @ sk14 )
| ( sk2 @ sk14 ) ),
inference(pre_uni,[status(thm)],[25539:[bind(A,$thf( sk14 )),bind(B,$thf( sk14 ))]]) ).
thf(25894,plain,
sk2 @ sk14,
inference(simp,[status(thm)],[25876]) ).
thf(25970,plain,
( ~ $true
| ( ( sk2 @ sk14 )
!= ( sk2
@ ^ [A: term] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[25894,17995]) ).
thf(25971,plain,
( ( sk2 @ sk14 )
!= ( sk2
@ ^ [A: term] : $false ) ),
inference(simp,[status(thm)],[25970]) ).
thf(26042,plain,
( sk14
!= ( ^ [A: term] : $false ) ),
inference(simp,[status(thm)],[25971]) ).
thf(26461,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ $true
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[26357,88]) ).
thf(26462,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[26461]) ).
thf(26463,plain,
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( sk21 = one ) ),
inference(pattern_uni,[status(thm)],[26462:[bind(A,$thf( sk21 ))]]) ).
thf(46,plain,
! [B: term,A: term] :
~ ( var @ ( ap @ A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(83,plain,
! [B: term,A: term] :
~ ( var @ ( ap @ A @ B ) ),
inference(simp,[status(thm)],[46]) ).
thf(153,plain,
! [B: term,A: term] :
( ~ $true
| ( ( var @ ( ap @ A @ B ) )
!= ( var @ one ) ) ),
inference(paramod_ordered,[status(thm)],[6,83]) ).
thf(154,plain,
! [B: term,A: term] :
( ( var @ ( ap @ A @ B ) )
!= ( var @ one ) ),
inference(simp,[status(thm)],[153]) ).
thf(155,plain,
! [B: term,A: term] :
( ( ap @ A @ B )
!= one ),
inference(simp,[status(thm)],[154]) ).
thf(26356,plain,
sk14 @ sk20,
inference(func_ext,[status(esa)],[26042]) ).
thf(15108,plain,
! [B: subst,A: term] :
( ( A != sk16 )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ ( comp @ sh @ sh ) ) ) ),
inference(paramod_ordered,[status(thm)],[68,14519]) ).
thf(15126,plain,
! [A: subst] :
( ( one != one )
| ( ( push @ sk16 @ A )
!= ( comp @ sh @ sh ) ) ),
inference(simp,[status(thm)],[15108]) ).
thf(15140,plain,
! [A: subst] :
( ( push @ sk16 @ A )
!= ( comp @ sh @ sh ) ),
inference(simp,[status(thm)],[15126]) ).
thf(26479,plain,
! [A: term] :
( ( one = A )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ $true
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[26357,70]) ).
thf(26480,plain,
! [A: term] :
( ( one = A )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ( ( var @ sk21 )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[26479]) ).
thf(26481,plain,
( ( sk21 = one )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) ) ),
inference(pattern_uni,[status(thm)],[26480:[bind(A,$thf( sk21 ))]]) ).
thf(12,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ~ ( A @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(108,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ~ ( A @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[12]) ).
thf(55,plain,
! [C: term,B: subst,A: term] :
( ( var @ ( sk7 @ B @ A @ ( (=) @ term @ A ) ) )
| ( A != A )
| ~ ( var @ C )
| ( A
= ( sub @ C @ ( push @ A @ B ) ) ) ),
inference(replace_leibeq,[status(thm)],[32:[bind(A,$thf( (=) @ term @ B ))]]) ).
thf(129,plain,
! [C: term,B: subst,A: term] :
( ( A != A )
| ( ( sub @ C @ ( push @ A @ B ) )
= A )
| ( var @ ( sk7 @ B @ A @ ( (=) @ term @ A ) ) )
| ~ ( var @ C ) ),
inference(lifteq,[status(thm)],[55]) ).
thf(130,plain,
! [C: term,B: subst,A: term] :
( ( ( sub @ C @ ( push @ A @ B ) )
= A )
| ( var @ ( sk7 @ B @ A @ ( (=) @ term @ A ) ) )
| ~ ( var @ C ) ),
inference(simp,[status(thm)],[129]) ).
thf(58,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) )
| ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
!= ( ap @ ( sk4 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) @ ( sk5 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) ) )
| ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
= ( sk6 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) )
| ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
= B ) ),
inference(replace_leibeq,[status(thm)],[12:[bind(A,$thf( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ))]]) ).
thf(134,plain,
! [B: term,A: term > $o] :
( ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
!= ( ap @ ( sk4 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) @ ( sk5 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) ) )
| ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
= ( sk6 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) )
| ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
= B )
| ~ ( sk2 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(135,plain,
! [B: term,A: term > $o] :
( ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
!= ( ap @ ( sk4 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) @ ( sk5 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) ) )
| ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
= ( sk6 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) )
| ( ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) )
= B )
| ~ ( sk2 @ ( (=) @ term @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(3627,plain,
( $false
| ( sk8
@ ^ [A: term] : $false ) ),
inference(prim_subst,[status(thm)],[89:[bind(A,$thf( ^ [B: term] : $false ))]]) ).
thf(3706,plain,
( sk8
@ ^ [A: term] : $false ),
inference(simp,[status(thm)],[3627]) ).
thf(49816,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) @ A )
!= ( sub
@ ( sk3
@ ^ [C: term] : $false )
@ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1616,18712]) ).
thf(49889,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ one ) ) )
!= B )
| ( ( sk3
@ ^ [C: term] : $false )
!= ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[49816]) ).
thf(49993,plain,
( ( sk3
@ ^ [A: term] : $false )
!= ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) ),
inference(simp,[status(thm)],[49889]) ).
thf(6696,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ $true
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6516,88]) ).
thf(6697,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[6696]) ).
thf(6698,plain,
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( ( sub @ one @ sh )
= one ) ),
inference(pattern_uni,[status(thm)],[6697:[bind(A,$thf( sub @ one @ sh ))]]) ).
thf(31786,plain,
! [C: subst,B: subst,A: term] :
( ( ( sub @ A @ ( comp @ B @ C ) )
!= sk16 )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ sk21 @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,31465]) ).
thf(31787,plain,
( ( sub @ sk21 @ ( comp @ sh @ sh ) )
!= sk16 ),
inference(pattern_uni,[status(thm)],[31786:[bind(A,$thf( sk21 )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(18180,plain,
( ~ $true
| ( ( var
@ ( sk3
@ ^ [A: term] : $false ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[18027,241]) ).
thf(18181,plain,
( ( var
@ ( sk3
@ ^ [A: term] : $false ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[18180]) ).
thf(18254,plain,
( ( sk3
@ ^ [A: term] : $false )
!= sk16 ),
inference(simp,[status(thm)],[18181]) ).
thf(31347,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ sk21 @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,28403]) ).
thf(31348,plain,
var @ ( sub @ sk21 @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[31347:[bind(A,$thf( sk21 )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(34259,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[31348,99]) ).
thf(34260,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[34259]) ).
thf(34261,plain,
var @ ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ),
inference(pattern_uni,[status(thm)],[34260:[bind(A,$thf( sub @ sk21 @ ( comp @ sh @ sh ) ))]]) ).
thf(42810,plain,
( ~ $true
| ( ( var @ ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[34261,241]) ).
thf(42811,plain,
( ( var @ ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[42810]) ).
thf(42938,plain,
( ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh )
!= sk16 ),
inference(simp,[status(thm)],[42811]) ).
thf(11,plain,
! [B: term,A: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(122,plain,
! [B: term,A: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[11]) ).
thf(123,plain,
! [B: term,A: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) ),
inference(simp,[status(thm)],[122]) ).
thf(1180,plain,
! [C: subst,B: term,A: subst] :
( ( ( lam @ ( lam @ one ) )
!= one )
| ( ( sub @ ( lam @ ( lam @ one ) ) @ A )
!= ( sub @ ( lam @ B ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1055,979]) ).
thf(1181,plain,
( ( lam @ ( lam @ one ) )
!= one ),
inference(pattern_uni,[status(thm)],[1180:[bind(A,$thf( A )),bind(B,$thf( lam @ one )),bind(C,$thf( A ))]]) ).
thf(182,plain,
! [B: term,A: term] :
( ( A != one )
| ( one = B )
| ~ ( var @ B )
| ( ( sub @ A @ id )
!= ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[118,64]) ).
thf(188,plain,
! [A: term] :
( ( one = A )
| ~ ( var @ A )
| ( ( sk1 @ ( (=) @ term @ one ) )
!= one )
| ( sh != id ) ),
inference(simp,[status(thm)],[182]) ).
thf(194,plain,
! [A: term] :
( ( one = A )
| ~ ( var @ A )
| ( ( sk1 @ ( (=) @ term @ one ) )
!= one )
| ( sh != id ) ),
inference(simp,[status(thm)],[188]) ).
thf(47,plain,
! [A: term > $o] :
( ~ ( A @ ( ap @ ( sk9 @ A ) @ ( sk10 @ A ) ) )
| ( sk8 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(145,plain,
! [A: term > $o] :
( ~ ( A @ ( ap @ ( sk9 @ A ) @ ( sk10 @ A ) ) )
| ( sk8 @ A ) ),
inference(simp,[status(thm)],[47]) ).
thf(20,plain,
! [A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( A @ ( lam @ ( sk12 @ A ) ) )
| ( sk11 @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(82,plain,
! [A: term > $o] :
( ~ ( sk8 @ A )
| ~ ( A @ ( lam @ ( sk12 @ A ) ) )
| ( sk11 @ A ) ),
inference(simp,[status(thm)],[20]) ).
thf(1693,plain,
( ~ ( sk8
@ ^ [A: term] : $true )
| ~ $true
| ( sk11
@ ^ [A: term] : $true ) ),
inference(prim_subst,[status(thm)],[82:[bind(A,$thf( ^ [B: term] : $true ))]]) ).
thf(1723,plain,
( ~ ( sk8
@ ^ [A: term] : $true )
| ( sk11
@ ^ [A: term] : $true ) ),
inference(simp,[status(thm)],[1693]) ).
thf(31951,plain,
! [A: term > $o] :
( ~ ( A @ ( ap @ ( sk9 @ A ) @ ( sk10 @ A ) ) )
| ~ $true
| ( sk11
@ ^ [B: term] : $true )
| ( ( sk8 @ A )
!= ( sk8
@ ^ [B: term] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[145,1723]) ).
thf(31952,plain,
! [A: term > $o] :
( ~ ( A @ ( ap @ ( sk9 @ A ) @ ( sk10 @ A ) ) )
| ( sk11
@ ^ [B: term] : $true )
| ( ( sk8 @ A )
!= ( sk8
@ ^ [B: term] : $true ) ) ),
inference(simp,[status(thm)],[31951]) ).
thf(31953,plain,
( ~ $true
| ( sk11
@ ^ [A: term] : $true ) ),
inference(pattern_uni,[status(thm)],[31952:[bind(A,$thf( ^ [B: term] : $true ))]]) ).
thf(32358,plain,
( sk11
@ ^ [A: term] : $true ),
inference(simp,[status(thm)],[31953]) ).
thf(25613,plain,
! [A: term > $o] :
( ( var @ ( sk10 @ var ) )
| ~ $true
| ( sk2 @ A )
| ( ( sk8 @ var )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[3622,126]) ).
thf(25614,plain,
! [A: term > $o] :
( ( var @ ( sk10 @ var ) )
| ( sk2 @ A )
| ( ( sk8 @ var )
!= ( A @ ( sk3 @ A ) ) ) ),
inference(simp,[status(thm)],[25613]) ).
thf(25815,plain,
( ( var @ ( sk10 @ var ) )
| ( sk2
@ ^ [A: term] : ( sk8 @ var ) ) ),
inference(pre_uni,[status(thm)],[25614:[bind(A,$thf( ^ [B: term] : ( sk8 @ var ) ))]]) ).
thf(1069,plain,
! [C: subst,B: term,A: subst] :
( ( ( lam @ one )
!= one )
| ( ( sub @ ( lam @ one ) @ A )
!= ( sub @ ( lam @ B ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[997,979]) ).
thf(1070,plain,
( ( lam @ one )
!= one ),
inference(pattern_uni,[status(thm)],[1069:[bind(A,$thf( A )),bind(B,$thf( one )),bind(C,$thf( A ))]]) ).
thf(21551,plain,
( ~ $true
| ( ( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ sh ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[18613,241]) ).
thf(21552,plain,
( ( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ sh ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[21551]) ).
thf(21696,plain,
( ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ sh )
@ sh )
!= sk16 ),
inference(simp,[status(thm)],[21552]) ).
thf(14079,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[8656,128]) ).
thf(14080,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[14079]) ).
thf(14081,plain,
sk14 @ ( sub @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[14080:[bind(A,$thf( sub @ ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) @ sh ))]]) ).
thf(124,plain,
? [A: term > term] :
! [B: term] :
( ( A @ ( lam @ B ) )
= B ),
inference(detectInverse,[status(thm)],[123]) ).
thf(125,plain,
! [A: term] :
( ( sk18 @ ( lam @ A ) )
= A ),
inference(cnf,[status(esa)],[124]) ).
thf(199,plain,
! [A: term] :
( ( sk18 @ ( lam @ A ) )
= A ),
inference(lifteq,[status(thm)],[125]) ).
thf(28369,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[26508,128]) ).
thf(28370,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ sk21 @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[28369]) ).
thf(28371,plain,
sk14 @ ( sub @ sk21 @ sh ),
inference(pattern_uni,[status(thm)],[28370:[bind(A,$thf( sub @ sk21 @ sh ))]]) ).
thf(42773,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[34261,128]) ).
thf(42774,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[42773]) ).
thf(42775,plain,
sk14 @ ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ),
inference(pattern_uni,[status(thm)],[42774:[bind(A,$thf( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ))]]) ).
thf(43847,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,42775]) ).
thf(43848,plain,
sk14 @ ( sub @ sk21 @ ( comp @ ( comp @ sh @ sh ) @ sh ) ),
inference(pattern_uni,[status(thm)],[43847:[bind(A,$thf( sk21 )),bind(B,$thf( comp @ sh @ sh )),bind(C,$thf( sh ))]]) ).
thf(45467,plain,
sk14 @ ( sub @ sk21 @ ( comp @ sh @ ( comp @ sh @ sh ) ) ),
inference(rewrite,[status(thm)],[43848,147]) ).
thf(42817,plain,
! [C: subst,B: subst,A: term] :
( ( var @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ sk21 @ ( comp @ sh @ sh ) ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,34261]) ).
thf(42818,plain,
var @ ( sub @ sk21 @ ( comp @ ( comp @ sh @ sh ) @ sh ) ),
inference(pattern_uni,[status(thm)],[42817:[bind(A,$thf( sk21 )),bind(B,$thf( comp @ sh @ sh )),bind(C,$thf( sh ))]]) ).
thf(44065,plain,
var @ ( sub @ sk21 @ ( comp @ sh @ ( comp @ sh @ sh ) ) ),
inference(rewrite,[status(thm)],[42818,147]) ).
thf(14706,plain,
! [C: subst,B: subst,A: term] :
( ( ( sub @ A @ ( comp @ B @ C ) )
!= sk16 )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ ( sub @ one @ sh ) @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,8722]) ).
thf(14707,plain,
( ( sub @ ( sub @ one @ sh ) @ ( comp @ sh @ sh ) )
!= sk16 ),
inference(pattern_uni,[status(thm)],[14706:[bind(A,$thf( sub @ one @ sh )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(1897,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) )
!= one )
| ( ( sub @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= ( sub @ B @ ( push @ one @ sh ) ) ) ),
inference(paramod_ordered,[status(thm)],[1213,1863]) ).
thf(1898,plain,
( ( lam @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) )
!= one ),
inference(pattern_uni,[status(thm)],[1897:[bind(A,$thf( push @ one @ sh )),bind(B,$thf( lam @ ( lam @ ( lam @ one ) ) ))]]) ).
thf(51,plain,
! [C: term,B: term,A: term] :
( ( lam @ A )
!= ( ap @ B @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(142,plain,
! [C: term,B: term,A: term] :
( ( lam @ A )
!= ( ap @ B @ C ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(143,plain,
! [C: term,B: term,A: term] :
( ( lam @ A )
!= ( ap @ B @ C ) ),
inference(simp,[status(thm)],[142]) ).
thf(36452,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ one ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ one ) ) @ A )
!= ( sub @ sk21 @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1055,28454]) ).
thf(36520,plain,
! [B: term,A: subst] :
( ( ( lam @ one )
!= B )
| ( ( lam @ ( lam @ one ) )
!= sk21 )
| ( A != sh ) ),
inference(simp,[status(thm)],[36452]) ).
thf(36556,plain,
( ( lam @ ( lam @ one ) )
!= sk21 ),
inference(simp,[status(thm)],[36520]) ).
thf(42416,plain,
! [A: term] :
( ~ $true
| ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[31362,128]) ).
thf(42417,plain,
! [A: term] :
( ( sk14 @ A )
| ( ( var @ ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[42416]) ).
thf(42418,plain,
sk14 @ ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ),
inference(pattern_uni,[status(thm)],[42417:[bind(A,$thf( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ))]]) ).
thf(25733,plain,
( ~ $true
| ( sk2
@ ^ [A: term] : $true ) ),
inference(prim_subst,[status(thm)],[126:[bind(A,$thf( ^ [B: term] : $true ))]]) ).
thf(25903,plain,
( sk2
@ ^ [A: term] : $true ),
inference(simp,[status(thm)],[25733]) ).
thf(24,plain,
! [D: term,C: subst,B: term,A: term > $o] :
( ~ ( A @ ( sub @ ( sk7 @ C @ B @ A ) @ C ) )
| ~ ( A @ B )
| ~ ( var @ D )
| ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(72,plain,
! [D: term,C: subst,B: term,A: term > $o] :
( ~ ( A @ ( sub @ ( sk7 @ C @ B @ A ) @ C ) )
| ~ ( A @ B )
| ~ ( var @ D )
| ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ),
inference(simp,[status(thm)],[24]) ).
thf(9957,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ one ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ one ) ) @ A )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1055,7078]) ).
thf(10000,plain,
! [B: term,A: subst] :
( ( ( lam @ one )
!= B )
| ( ( sub @ one @ sh )
!= ( lam @ ( lam @ one ) ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[9957]) ).
thf(10033,plain,
( ( sub @ one @ sh )
!= ( lam @ ( lam @ one ) ) ),
inference(simp,[status(thm)],[10000]) ).
thf(31590,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ sk21 @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,31315]) ).
thf(31591,plain,
sk14 @ ( sub @ sk21 @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[31590:[bind(A,$thf( sk21 )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(104,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ( A @ ( sk5 @ A ) )
| ~ ( A @ ( lam @ ( sk6 @ A ) ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[44]) ).
thf(43094,plain,
! [C: subst,B: subst,A: term] :
( ( sk14 @ ( sub @ A @ ( comp @ B @ C ) ) )
| ( ( sub @ ( sub @ A @ B ) @ C )
!= ( sub @ ( sub @ ( sub @ sk21 @ sh ) @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[112,42418]) ).
thf(43095,plain,
sk14 @ ( sub @ ( sub @ sk21 @ sh ) @ ( comp @ sh @ sh ) ),
inference(pattern_uni,[status(thm)],[43094:[bind(A,$thf( sub @ sk21 @ sh )),bind(B,$thf( sh )),bind(C,$thf( sh ))]]) ).
thf(18175,plain,
! [A: term] :
( ~ $true
| ( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ ( lam @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[18027,98]) ).
thf(18176,plain,
! [A: term] :
( ( var
@ ( sk3
@ ^ [B: term] : $false ) )
!= ( var @ ( lam @ A ) ) ),
inference(simp,[status(thm)],[18175]) ).
thf(18249,plain,
! [A: term] :
( ( sk3
@ ^ [B: term] : $false )
!= ( lam @ A ) ),
inference(simp,[status(thm)],[18176]) ).
thf(170,plain,
! [A: term] :
( ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ~ ( var @ A )
| ( ( push @ A @ sh )
= id )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[64,73]) ).
thf(171,plain,
! [A: term] :
( ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ~ ( var @ A )
| ( ( push @ A @ sh )
= id ) ),
inference(pattern_uni,[status(thm)],[170:[]]) ).
thf(387,plain,
! [A: term > $o] :
( ( sk2 @ A )
| ~ $true
| ( ( var @ ( sk3 @ A ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[103,241]) ).
thf(388,plain,
! [A: term > $o] :
( ( sk2 @ A )
| ( ( var @ ( sk3 @ A ) )
!= ( var @ sk16 ) ) ),
inference(simp,[status(thm)],[387]) ).
thf(401,plain,
! [A: term > $o] :
( ( sk2 @ A )
| ( ( sk3 @ A )
!= sk16 ) ),
inference(simp,[status(thm)],[388]) ).
thf(119,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(simp,[status(thm)],[16]) ).
thf(44156,plain,
( ~ $true
| ( ( var @ ( sub @ sk21 @ ( comp @ sh @ ( comp @ sh @ sh ) ) ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[44065,241]) ).
thf(44157,plain,
( ( var @ ( sub @ sk21 @ ( comp @ sh @ ( comp @ sh @ sh ) ) ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[44156]) ).
thf(44271,plain,
( ( sub @ sk21 @ ( comp @ sh @ ( comp @ sh @ sh ) ) )
!= sk16 ),
inference(simp,[status(thm)],[44157]) ).
thf(6416,plain,
( ~ $true
| ( ( sk14 @ ( lam @ ( lam @ one ) ) )
!= ( sk14 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[6396,28]) ).
thf(6417,plain,
( ( sk14 @ ( lam @ ( lam @ one ) ) )
!= ( sk14 @ sk16 ) ),
inference(simp,[status(thm)],[6416]) ).
thf(6462,plain,
( ( lam @ ( lam @ one ) )
!= sk16 ),
inference(simp,[status(thm)],[6417]) ).
thf(25,plain,
! [D: term,C: term,B: term,A: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(74,plain,
! [D: term,C: term,B: term,A: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[25]) ).
thf(75,plain,
! [D: term,C: term,B: term,A: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( A = B ) ),
inference(simp,[status(thm)],[74]) ).
thf(11136,plain,
! [B: subst,A: term] :
( ( A
!= ( lam @ ( lam @ ( lam @ one ) ) ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[68,10061]) ).
thf(11149,plain,
! [A: subst] :
( ( one != one )
| ( ( push @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= sh ) ),
inference(simp,[status(thm)],[11136]) ).
thf(11167,plain,
! [A: subst] :
( ( push @ ( lam @ ( lam @ ( lam @ one ) ) ) @ A )
!= sh ),
inference(simp,[status(thm)],[11149]) ).
thf(5422,plain,
! [C: subst,B: term,A: term] :
( ( ( lam @ ( sub @ ( lam @ A ) @ C ) )
!= one )
| ( ( lam @ ( sub @ A @ ( push @ one @ sh ) ) )
!= ( lam @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5396,1966]) ).
thf(5423,plain,
! [B: term,A: subst] :
( ( lam @ ( sub @ ( lam @ B ) @ A ) )
!= one ),
inference(pattern_uni,[status(thm)],[5422:[bind(A,$thf( D )),bind(B,$thf( sub @ D @ ( push @ one @ sh ) )),bind(C,$thf( C ))]]) ).
thf(5601,plain,
! [B: term,A: subst] :
( ( lam @ ( sub @ ( lam @ B ) @ A ) )
!= one ),
inference(simp,[status(thm)],[5423]) ).
thf(9990,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) @ A )
!= ( sub @ ( sub @ one @ sh ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1616,7078]) ).
thf(10003,plain,
! [B: term,A: subst] :
( ( ( lam @ ( lam @ ( lam @ one ) ) )
!= B )
| ( ( sub @ one @ sh )
!= ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) )
| ( A != sh ) ),
inference(simp,[status(thm)],[9990]) ).
thf(10036,plain,
( ( sub @ one @ sh )
!= ( lam @ ( lam @ ( lam @ ( lam @ one ) ) ) ) ),
inference(simp,[status(thm)],[10003]) ).
thf(52,plain,
! [C: term,B: subst,A: term] :
( ( A
!= ( sub @ ( sk7 @ B @ A @ ( (=) @ term @ A ) ) @ B ) )
| ( A != A )
| ~ ( var @ C )
| ( A
= ( sub @ C @ ( push @ A @ B ) ) ) ),
inference(replace_leibeq,[status(thm)],[24:[bind(A,$thf( (=) @ term @ B ))]]) ).
thf(78,plain,
! [C: term,B: subst,A: term] :
( ( ( sub @ ( sk7 @ B @ A @ ( (=) @ term @ A ) ) @ B )
!= A )
| ( A != A )
| ( ( sub @ C @ ( push @ A @ B ) )
= A )
| ~ ( var @ C ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(79,plain,
! [C: term,B: subst,A: term] :
( ( ( sub @ ( sk7 @ B @ A @ ( (=) @ term @ A ) ) @ B )
!= A )
| ( ( sub @ C @ ( push @ A @ B ) )
= A )
| ~ ( var @ C ) ),
inference(simp,[status(thm)],[78]) ).
thf(76,plain,
? [A: term > term > term] :
! [B: term,C: term] :
( ( A @ C @ ( ap @ B @ C ) )
= B ),
inference(detectInverse,[status(thm)],[75]) ).
thf(77,plain,
! [B: term,A: term] :
( ( sk17 @ B @ ( ap @ A @ B ) )
= A ),
inference(cnf,[status(esa)],[76]) ).
thf(474,plain,
! [B: term,A: term] :
( ( sk17 @ B @ ( ap @ A @ B ) )
= A ),
inference(lifteq,[status(thm)],[77]) ).
thf(22125,plain,
( ~ $true
| ( ( var
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ ( comp @ sh @ sh ) ) )
!= ( var @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[21556,241]) ).
thf(22126,plain,
( ( var
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ ( comp @ sh @ sh ) ) )
!= ( var @ sk16 ) ),
inference(simp,[status(thm)],[22125]) ).
thf(22267,plain,
( ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ ( comp @ sh @ sh ) )
!= sk16 ),
inference(simp,[status(thm)],[22126]) ).
thf(26529,plain,
! [B: term,A: term] :
( ~ $true
| ( ( var @ ( ap @ A @ B ) )
!= ( var @ sk21 ) ) ),
inference(paramod_ordered,[status(thm)],[26357,83]) ).
thf(26530,plain,
! [B: term,A: term] :
( ( var @ ( ap @ A @ B ) )
!= ( var @ sk21 ) ),
inference(simp,[status(thm)],[26529]) ).
thf(26558,plain,
! [B: term,A: term] :
( ( ap @ A @ B )
!= sk21 ),
inference(simp,[status(thm)],[26530]) ).
thf(22141,plain,
! [A: term] :
( ~ $true
| ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ ( comp @ sh @ sh ) ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[21556,99]) ).
thf(22142,plain,
! [A: term] :
( ( var @ ( sub @ A @ sh ) )
| ( ( var
@ ( sub
@ ( sk3
@ ^ [B: term] : $false )
@ ( comp @ sh @ sh ) ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[22141]) ).
thf(22143,plain,
( var
@ ( sub
@ ( sub
@ ( sk3
@ ^ [A: term] : $false )
@ ( comp @ sh @ sh ) )
@ sh ) ),
inference(pattern_uni,[status(thm)],[22142:[bind(A,$thf( sub @ ( sk3 @ ^ [B: term] : $false ) @ ( comp @ sh @ sh ) ))]]) ).
thf(26369,plain,
( ~ $true
| ( ( sk14 @ sk20 )
!= ( sk14 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[26356,28]) ).
thf(26370,plain,
( ( sk14 @ sk20 )
!= ( sk14 @ sk16 ) ),
inference(simp,[status(thm)],[26369]) ).
thf(26426,plain,
sk20 != sk16,
inference(simp,[status(thm)],[26370]) ).
thf(9,plain,
! [B: term,A: term] :
( ( ( sub @ A @ sh )
!= ( sub @ B @ sh ) )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(93,plain,
! [B: term,A: term] :
( ( ( sub @ A @ sh )
!= ( sub @ B @ sh ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[9]) ).
thf(94,plain,
! [B: term,A: term] :
( ( ( sub @ A @ sh )
!= ( sub @ B @ sh ) )
| ( A = B ) ),
inference(simp,[status(thm)],[93]) ).
thf(25731,plain,
( ~ ( var @ ( sk3 @ var ) )
| ( sk2 @ var ) ),
inference(prim_subst,[status(thm)],[126:[bind(A,$thf( var ))]]) ).
thf(36484,plain,
! [B: term,A: subst] :
( ( ( lam @ one )
!= ( lam @ B ) )
| ( ( sub @ ( lam @ one ) @ A )
!= ( sub @ sk21 @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[997,28454]) ).
thf(36524,plain,
! [B: term,A: subst] :
( ( one != B )
| ( ( lam @ one )
!= sk21 )
| ( A != sh ) ),
inference(simp,[status(thm)],[36484]) ).
thf(36560,plain,
( ( lam @ one )
!= sk21 ),
inference(simp,[status(thm)],[36524]) ).
thf(32127,plain,
( ~ $true
| ( sk8
@ ^ [A: term] : $true ) ),
inference(prim_subst,[status(thm)],[145:[bind(A,$thf( ^ [B: term] : $true ))]]) ).
thf(32321,plain,
( sk8
@ ^ [A: term] : $true ),
inference(simp,[status(thm)],[32127]) ).
thf(1361,plain,
( ~ $true
| ( ( sk14 @ ( lam @ one ) )
!= ( sk14 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[1347,28]) ).
thf(1362,plain,
( ( sk14 @ ( lam @ one ) )
!= ( sk14 @ sk16 ) ),
inference(simp,[status(thm)],[1361]) ).
thf(1378,plain,
( ( lam @ one )
!= sk16 ),
inference(simp,[status(thm)],[1362]) ).
thf(33,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ~ ( A @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) )
| ~ ( A @ ( lam @ ( sk6 @ A ) ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(90,plain,
! [B: term,A: term > $o] :
( ~ ( sk2 @ A )
| ~ ( A @ ( ap @ ( sk4 @ A ) @ ( sk5 @ A ) ) )
| ~ ( A @ ( lam @ ( sk6 @ A ) ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[33]) ).
thf(225,plain,
! [B: term,A: subst] :
( ( one = B )
| ~ ( var @ B )
| ( ( sk1 @ ( (=) @ term @ one ) )
!= one )
| ( ( push @ one @ A )
!= sh ) ),
inference(simp,[status(thm)],[214]) ).
thf(227,plain,
! [B: term,A: subst] :
( ( one = B )
| ~ ( var @ B )
| ( ( sk1 @ ( (=) @ term @ one ) )
!= one )
| ( ( push @ one @ A )
!= sh ) ),
inference(simp,[status(thm)],[225]) ).
thf(10165,plain,
! [B: subst,A: term] :
( ( A
!= ( lam @ ( lam @ one ) ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[68,10033]) ).
thf(10176,plain,
! [A: subst] :
( ( one != one )
| ( ( push @ ( lam @ ( lam @ one ) ) @ A )
!= sh ) ),
inference(simp,[status(thm)],[10165]) ).
thf(10187,plain,
! [A: subst] :
( ( push @ ( lam @ ( lam @ one ) ) @ A )
!= sh ),
inference(simp,[status(thm)],[10176]) ).
thf(5507,plain,
! [D: term,C: term,B: term,A: term] :
( ( ( lam @ A )
!= ( ap @ C @ D ) )
| ( ( lam @ ( sub @ A @ ( push @ one @ sh ) ) )
!= ( lam @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5396,143]) ).
thf(5508,plain,
! [C: term,B: term,A: term] :
( ( lam @ C )
!= ( ap @ A @ B ) ),
inference(pattern_uni,[status(thm)],[5507:[bind(A,$thf( E )),bind(B,$thf( sub @ E @ ( push @ one @ sh ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(5618,plain,
! [C: term,B: term,A: term] :
( ( lam @ C )
!= ( ap @ A @ B ) ),
inference(simp,[status(thm)],[5508]) ).
thf(36715,plain,
! [B: term,A: term > $o] :
( ( sk8 @ var )
| ~ $true
| ( A @ ( sk4 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B )
| ( ( sk2
@ ^ [C: term] : ( var @ ( sk10 @ var ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[25806,115]) ).
thf(36716,plain,
! [B: term,A: term > $o] :
( ( sk8 @ var )
| ( A @ ( sk4 @ A ) )
| ( A @ ( sk6 @ A ) )
| ( A @ B )
| ( ( sk2
@ ^ [C: term] : ( var @ ( sk10 @ var ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[36715]) ).
thf(36717,plain,
( ( sk8 @ var )
| ( var @ ( sk10 @ var ) )
| ( var @ ( sk10 @ var ) )
| ( var @ ( sk10 @ var ) ) ),
inference(pattern_uni,[status(thm)],[36716:[bind(A,$thf( ^ [C: term] : ( var @ ( sk10 @ var ) ) )),bind(B,$thf( B ))]]) ).
thf(37052,plain,
( ( sk8 @ var )
| ( var @ ( sk10 @ var ) ) ),
inference(simp,[status(thm)],[36717]) ).
thf(6720,plain,
! [A: term] :
( ( one = A )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ~ $true
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6516,70]) ).
thf(6721,plain,
! [A: term] :
( ( one = A )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ( ( var @ ( sub @ one @ sh ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[6720]) ).
thf(6722,plain,
( ( ( sub @ one @ sh )
= one )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) ) ),
inference(pattern_uni,[status(thm)],[6721:[bind(A,$thf( sub @ one @ sh ))]]) ).
thf(17,plain,
! [B: term,A: term] :
( ~ ( sk14 @ A )
| ~ ( sk14 @ B )
| ( sk14 @ ( ap @ A @ B ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(100,plain,
! [B: term,A: term] :
( ~ ( sk14 @ A )
| ~ ( sk14 @ B )
| ( sk14 @ ( ap @ A @ B ) ) ),
inference(simp,[status(thm)],[17]) ).
thf(64909,plain,
$false,
inference(e,[status(thm)],[14754,43500,101,14606,88,408,42466,115,31362,10061,247,31315,5614,6732,30269,21534,26785,14519,36569,38702,36564,1055,4238,6396,1347,7075,152,8632,1778,216,21556,6534,106,238,2925,1283,50677,121,147,14527,132,116,2965,40261,89,133,265,4285,26567,50004,6,18145,85,102,7078,10133,1091,28,70,14524,137,5396,92,229,97,1951,50013,18673,889,31465,42568,2769,18613,28454,25806,1567,8544,3622,21851,26357,21572,6946,96,25794,6752,997,17995,25941,14740,18027,18581,50016,73,128,1616,49645,50621,64,296,149,26486,118,28489,71,14743,38309,17041,144,4218,7536,8656,18167,86,979,113,81,26568,98,103,26042,66,26463,155,26356,15140,26481,108,130,18712,1066,6783,135,3706,49993,26508,241,6698,31787,1213,3,18254,112,42938,123,1181,194,145,32358,25815,1070,1003,26323,21696,28403,14081,10048,199,28371,45467,44065,127,14707,1898,143,31348,36556,42418,25903,72,99,1966,10033,31591,104,43095,18249,114,171,139,18194,401,8722,119,44271,6462,82,75,6516,11167,25894,6786,5601,107,126,10036,79,474,22267,26558,14704,22143,26426,94,25731,1829,36560,32321,1378,7025,68,90,227,10187,5618,34261,37052,7003,6722,42775,100,30401,83]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG253^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.22 % Computer : n006.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 17:32:24 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.85/0.62 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.88/1.01 % [INFO] Parsing done (387ms).
% 1.88/1.02 % [INFO] Running in sequential loop mode.
% 3.38/1.36 % [INFO] eprover registered as external prover.
% 3.38/1.36 % [INFO] Scanning for conjecture ...
% 5.14/2.03 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 5.48/2.07 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 5.48/2.07 % [INFO] Problem is higher-order (TPTP THF).
% 5.48/2.08 % [INFO] Type checking passed.
% 5.48/2.08 % [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 ...
% 190.02/49.93 % External prover 'e' found a proof!
% 190.02/49.93 % [INFO] Killing All external provers ...
% 190.02/49.94 % Time passed: 49617ms (effective reasoning time: 48911ms)
% 190.02/49.94 % 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)>
% 190.02/49.94 % Axioms used in derivation (0):
% 190.02/49.94 % No. of inferences in proof: 611
% 190.02/49.94 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 49617 ms resp. 48911 ms w/o parsing
% 190.79/50.11 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 190.79/50.11 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------