TPTP Problem File: SWX167^1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX167^1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Benchmark: ALG444^1, Active target: hoasinduction_lem3aa
% Version : Especial.
% English :
% Refs : [Kon26] Kondylidou (2026), Email to Geoff Sutcliffe
% Source : [Kon26]
% Names : ALG444^1__005__axclos.verify [Kon26]
% Status : Theorem
% Rating : 0.50 v9.3.0
% Syntax : Number of formulae : 132 ( 1 unt; 130 typ; 0 def)
% Number of atoms : 255 ( 129 equ; 0 cnn)
% Maximal formula atoms : 248 ( 127 avg)
% Number of connectives : 2618 ( 333 ~; 306 |; 129 &;1750 @)
% ( 56 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 151 ( 76 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 227 ( 227 >; 0 *; 0 +; 0 <<)
% Number of symbols : 127 ( 126 usr; 113 con; 0-4 aty)
% Number of variables : 560 ( 10 ^; 548 !; 2 ?; 560 :)
% SPC : TH0_THM_EQU_NAR
% 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(pushprop_lem1v2_decl,type,
pushprop_lem1v2: $o ).
thf(pushprop_lem1_gthm_decl,type,
pushprop_lem1_gthm: $o ).
thf(axmap_decl,type,
axmap: $o ).
thf(pushprop_lem0_gthm_decl,type,
pushprop_lem0_gthm: $o ).
thf(shinj_decl,type,
shinj: $o ).
thf(hoasinduction_lem1v2_decl,type,
hoasinduction_lem1v2: $o ).
thf(hoasinduction_lem1v2_gthm_decl,type,
hoasinduction_lem1v2_gthm: $o ).
thf(hoasap_decl,type,
hoasap: subst > term > subst > term > term ).
thf(induction2lem_decl,type,
induction2lem: $o ).
thf(hoasinduction_lem3v2_f_decl,type,
hoasinduction_lem3v2_f: $o ).
thf(axvarshift_decl,type,
axvarshift: $o ).
thf(hoasapinj2_decl,type,
hoasapinj2: $o ).
thf(hoasapnotvar_gthm_decl,type,
hoasapnotvar_gthm: $o ).
thf(hoasapinj1_decl,type,
hoasapinj1: $o ).
thf(ulamvar1_decl,type,
ulamvar1: $o ).
thf(induction2lem_lthm_decl,type,
induction2lem_lthm: $o ).
thf(hoasinduction_lem3v2_gthm_decl,type,
hoasinduction_lem3v2_gthm: $o ).
thf(apnotvar_decl,type,
apnotvar: $o ).
thf(pushprop_lthm_orig_decl,type,
pushprop_lthm_orig: $o ).
thf(hoasinduction_lem3v2_f_lthm_decl,type,
hoasinduction_lem3v2_f_lthm: $o ).
thf(hoasinduction_lthm_decl,type,
hoasinduction_lthm: $o ).
thf(hoasinduction_no_psi_cond_lthm_decl,type,
hoasinduction_no_psi_cond_lthm: $o ).
thf(hoaslaminj_decl,type,
hoaslaminj: $o ).
thf(hoasinduction_lem3aaa_decl,type,
hoasinduction_lem3aaa: $o ).
thf(induction2lem_gthm_decl,type,
induction2lem_gthm: $o ).
thf(hoasinduction_lem3aa_lthm_decl,type,
hoasinduction_lem3aa_lthm: $o ).
thf(hoasinduction_lem3_decl,type,
hoasinduction_lem3: $o ).
thf(hoasinduction_lem2_decl,type,
hoasinduction_lem2: $o ).
thf(termmset_lthm_decl,type,
termmset_lthm: $o ).
thf(hoasinduction_lem1_decl,type,
hoasinduction_lem1: $o ).
thf(hoaslamnotap_lthm_decl,type,
hoaslamnotap_lthm: $o ).
thf(pushprop_lem1v2_lthm_decl,type,
pushprop_lem1v2_lthm: $o ).
thf(hoasapnotvar_decl,type,
hoasapnotvar: $o ).
thf(hoasinduction_lem0_decl,type,
hoasinduction_lem0: $o ).
thf(hoasinduction_decl,type,
hoasinduction: $o ).
thf(hoasinduction_gthm_decl,type,
hoasinduction_gthm: $o ).
thf(axapp_decl,type,
axapp: $o ).
thf(hoaslamnotvar_lthm_decl,type,
hoaslamnotvar_lthm: $o ).
thf(pushprop_lem3v2_lthm_decl,type,
pushprop_lem3v2_lthm: $o ).
thf(hoasinduction_lem3b_lthm_decl,type,
hoasinduction_lem3b_lthm: $o ).
thf(ulamvarind_decl,type,
ulamvarind: $o ).
thf(induction_decl,type,
induction: $o ).
thf(hoasinduction_lem3a_lthm_decl,type,
hoasinduction_lem3a_lthm: $o ).
thf(termmset_gthm_decl,type,
termmset_gthm: $o ).
thf(hoasinduction_lem3aa_decl,type,
hoasinduction_lem3aa: $o ).
thf(pushprop_lem1v2_gthm_decl,type,
pushprop_lem1v2_gthm: $o ).
thf(hoaslamnotap_gthm_decl,type,
hoaslamnotap_gthm: $o ).
thf(hoaslamnotvar_gthm_decl,type,
hoaslamnotvar_gthm: $o ).
thf(hoasinduction_lem3b_gthm_decl,type,
hoasinduction_lem3b_gthm: $o ).
thf(pushprop_lem2v2_decl,type,
pushprop_lem2v2: $o ).
thf(hoasinduction_lem3a_gthm_decl,type,
hoasinduction_lem3a_gthm: $o ).
thf(axclos_decl,type,
axclos: $o ).
thf(axassoc_decl,type,
axassoc: $o ).
thf(hoasinduction_lem2v2_decl,type,
hoasinduction_lem2v2: $o ).
thf(pushprop_lthm_decl,type,
pushprop_lthm: $o ).
thf(apinj2_decl,type,
apinj2: $o ).
thf(apinj1_decl,type,
apinj1: $o ).
thf(hoasapinj2_lthm_decl,type,
hoasapinj2_lthm: $o ).
thf(hoasinduction_lem3v2a_decl,type,
hoasinduction_lem3v2a: $o ).
thf(hoasapinj1_lthm_decl,type,
hoasapinj1_lthm: $o ).
thf(hoaslaminj_lthm_decl,type,
hoaslaminj_lthm: $o ).
thf(axvarcons_decl,type,
axvarcons: $o ).
thf(hoaslam_decl,type,
hoaslam: subst > ( subst > term > term ) > term ).
thf(axscons_decl,type,
axscons: $o ).
thf(hoasinduction_lem2v2_gthm_decl,type,
hoasinduction_lem2v2_gthm: $o ).
thf(axidr_decl,type,
axidr: $o ).
thf(pushprop_lem1_decl,type,
pushprop_lem1: $o ).
thf(laminj_decl,type,
laminj: $o ).
thf(hoasinduction_lem3_lthm_decl,type,
hoasinduction_lem3_lthm: $o ).
thf(pushprop_lem0_decl,type,
pushprop_lem0: $o ).
thf(pushprop_gthm_decl,type,
pushprop_gthm: $o ).
thf(axabs_decl,type,
axabs: $o ).
thf(hoasinduction_lem3v2a_lthm_decl,type,
hoasinduction_lem3v2a_lthm: $o ).
thf(hoasinduction_lem2_lthm_decl,type,
hoasinduction_lem2_lthm: $o ).
thf(hoasapinj2_gthm_decl,type,
hoasapinj2_gthm: $o ).
thf(hoasinduction_p_and_p_prime_decl,type,
hoasinduction_p_and_p_prime: ( subst > term > subst > $o ) > ( term > $o ) > $o ).
thf(hoasinduction_lem1_lthm_decl,type,
hoasinduction_lem1_lthm: $o ).
thf(lamnotap_decl,type,
lamnotap: $o ).
thf(hoasapinj1_gthm_decl,type,
hoasapinj1_gthm: $o ).
thf(hoaslamnotvar_decl,type,
hoaslamnotvar: $o ).
thf(axidl_decl,type,
axidl: $o ).
thf(hoaslaminj_gthm_decl,type,
hoaslaminj_gthm: $o ).
thf(induction2_lthm_decl,type,
induction2_lthm: $o ).
thf(hoasinduction_lem0_lthm_decl,type,
hoasinduction_lem0_lthm: $o ).
thf(substmonoid_lthm_decl,type,
substmonoid_lthm: $o ).
thf(pushprop_decl,type,
pushprop: $o ).
thf(hoasinduction_lem3_gthm_decl,type,
hoasinduction_lem3_gthm: $o ).
thf(hoasinduction_lem2_gthm_decl,type,
hoasinduction_lem2_gthm: $o ).
thf(hoasinduction_lem3b_decl,type,
hoasinduction_lem3b: $o ).
thf(substmonoid_decl,type,
substmonoid: $o ).
thf(lamnotvar_decl,type,
lamnotvar: $o ).
thf(hoasinduction_lem3a_decl,type,
hoasinduction_lem3a: $o ).
thf(hoasinduction_lem1_gthm_decl,type,
hoasinduction_lem1_gthm: $o ).
thf(hoasinduction_no_psi_cond_decl,type,
hoasinduction_no_psi_cond: $o ).
thf(induction2_gthm_decl,type,
induction2_gthm: $o ).
thf(pushprop_lem2v2_lthm_decl,type,
pushprop_lem2v2_lthm: $o ).
thf(hoasvar_decl,type,
hoasvar: subst > term > subst > $o ).
thf(hoaslamnotap_decl,type,
hoaslamnotap: $o ).
thf(substmonoid_gthm_decl,type,
substmonoid_gthm: $o ).
thf(ulamvarsh_decl,type,
ulamvarsh: $o ).
thf(induction2_decl,type,
induction2: $o ).
thf(pushprop_lem3v2_decl,type,
pushprop_lem3v2: $o ).
thf(pushprop_lem2v2_gthm_decl,type,
pushprop_lem2v2_gthm: $o ).
thf(pushprop_lem1_lthm_decl,type,
pushprop_lem1_lthm: $o ).
thf(hoasinduction_lem3v2_decl,type,
hoasinduction_lem3v2: $o ).
thf(axshiftcons_decl,type,
axshiftcons: $o ).
thf(termmset_decl,type,
termmset: $o ).
thf(pushprop_lem0_lthm_decl,type,
pushprop_lem0_lthm: $o ).
thf(hoasapnotvar_lthm_decl,type,
hoasapnotvar_lthm: $o ).
thf(hoasinduction_lem3v2_lthm_decl,type,
hoasinduction_lem3v2_lthm: $o ).
thf(pushprop_p_and_p_prime_decl,type,
pushprop_p_and_p_prime: term > subst > ( term > $o ) > ( term > $o ) > $o ).
thf(axvarid_decl,type,
axvarid: $o ).
thf(hoasinduction_lthm_3_decl,type,
hoasinduction_lthm_3: $o ).
%----Types of the domains
thf(d_term_type,type,
d_term: $tType ).
thf(d_subst_type,type,
d_subst: $tType ).
%----Types of the promotion functions
thf(d2term_decl,type,
d2term: d_term > term ).
thf(d2subst_decl,type,
d2subst: d_subst > subst ).
%----Types of the domain elements
thf(d_one_decl,type,
d_one: d_term ).
thf(d_id_decl,type,
d_id: d_subst ).
thf(alg444_1,axiom,
( ! [T: term] :
? [DT: d_term] :
( T
= ( d2term @ DT ) )
& ! [DT: d_term] : ( DT = d_one )
& ! [DT1: d_term,DT2: d_term] :
( ( ( d2term @ DT1 )
= ( d2term @ DT2 ) )
=> ( DT1 = DT2 ) )
& ! [S: subst] :
? [DS: d_subst] :
( S
= ( d2subst @ DS ) )
& ! [DS: d_subst] : ( DS = d_id )
& ! [DS1: d_subst,DS2: d_subst] :
( ( ( d2subst @ DS1 )
= ( d2subst @ DS2 ) )
=> ( DS1 = DS2 ) )
& ( one
= ( d2term @ d_one ) )
& ( ( ap @ ( d2term @ d_one ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( lam @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( ( sub @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2term @ d_one ) )
& ( id
= ( d2subst @ d_id ) )
& ( sh
= ( d2subst @ d_id ) )
& ( ( push @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( comp @ ( d2subst @ d_id ) @ ( d2subst @ d_id ) )
= ( d2subst @ d_id ) )
& ( ( hoasap @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) @ ( d2term @ d_one ) )
= ( d2term @ d_one ) )
& ( hoaslam
= ( ^ [Bound_variable_4913: subst,Bound_variable_4915: subst > term > term] : ( d2term @ d_one ) ) )
& ( hoasinduction_p_and_p_prime
= ( ^ [P: subst > term > subst > $o,Q: term > $o] :
! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) ) ) )
& ( pushprop_p_and_p_prime
= ( ^ [A: term,M: subst,P: term > $o,Q: term > $o] :
! [X: term] :
( ( Q @ X )
= ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) ) )
& ~ ( var @ ( d2term @ d_one ) )
& ( pushprop_lem1v2
<=> ! [P: term > $o,Q: term > $o,A: term,M: subst] :
( ~ ( P @ A )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ ( sub @ X @ ( push @ A @ M ) ) ) )
| ( Q @ one ) ) )
& pushprop_lem1_gthm
& axmap
& pushprop_lem0_gthm
& ( shinj
<=> ! [A: term,B: term] :
( ( ( sub @ A @ sh )
!= ( sub @ B @ sh ) )
| ( A = B ) ) )
& hoasinduction_lem1v2
& hoasinduction_lem1v2_gthm
& ( induction2lem
<=> ! [P: term > $o,Bound_variable_2340: term,Bound_variable_2342: subst] :
( ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ~ ! [B: term] :
( ~ ( var @ B )
| ( P @ ( sub @ B @ Bound_variable_2342 ) ) )
| ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) ) )
& ( hoasinduction_lem3v2_f
<=> ! [B: term] :
~ ! [F: subst > term > term] :
~ ! [A: term,M: subst] :
( ( sub @ B @ ( push @ A @ M ) )
= ( F @ M @ A ) ) )
& axvarshift
& ( hoasapinj2
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( C = D ) ) )
& hoasapnotvar_gthm
& ( hoasapinj1
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( A = B ) ) )
& ~ ulamvar1
& ( induction2lem_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ( ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) )
=> ( ! [M: subst] :
( M
= ( comp @ M @ id ) )
=> ( ! [P: term > $o,Bound_variable_2140: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ( P @ A )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2140 ) )
=> ! [P: term > $o,Bound_variable_2340: term,Bound_variable_2342: subst] :
( ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ~ ! [B: term] :
( ~ ( var @ B )
| ( P @ ( sub @ B @ Bound_variable_2342 ) ) )
| ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) ) ) ) ) ) )
& hoasinduction_lem3v2_gthm
& apnotvar
& pushprop_lthm_orig
& ( hoasinduction_lem3v2_f_lthm
<=> ! [B: term] :
~ ! [F: subst > term > term] :
~ ! [A: term,M: subst] :
( ( sub @ B @ ( push @ A @ M ) )
= ( F @ M @ A ) ) )
& ( hoasinduction_lthm
<=> ( ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_2999: term,Bound_variable_3001: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ( P @ id @ Bound_variable_2999 @ id )
| ~ ( P @ id @ Bound_variable_3001 @ id )
| ( P @ id @ ( ap @ Bound_variable_2999 @ Bound_variable_3001 ) @ id ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_3211: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3283: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term] :
( ~ ( var @ ( sub @ A @ id ) )
| ( P @ id @ A @ id ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3283 @ id ) ) ) ) ) )
& ( hoasinduction_no_psi_cond_lthm
<=> ( ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
=> ( ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3295: term] :
( ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3295 @ id ) ) ) ) ) ) )
& ( hoaslaminj
<=> ! [F: subst > term > term,Bound_variable_2547: subst > term > term,Bound_variable_2549: subst,Bound_variable_2551: term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( Bound_variable_2547 @ M @ A ) @ N )
= ( Bound_variable_2547 @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ( ( lam @ ( F @ sh @ one ) )
!= ( lam @ ( Bound_variable_2547 @ sh @ one ) ) )
| ( ( F @ Bound_variable_2549 @ Bound_variable_2551 )
= ( Bound_variable_2547 @ Bound_variable_2549 @ Bound_variable_2551 ) ) ) )
& ( hoasinduction_lem3aaa
<=> ! [P: subst > term > subst > $o,Bound_variable_3171: term] :
( ~ ! [F: subst > term > term,Bound_variable_3149: term] :
( ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id )
| ~ ! [Bound_variable_3072: subst,Bound_variable_3074: term,Bound_variable_3076: subst] :
( ( sub @ ( F @ Bound_variable_3072 @ Bound_variable_3074 ) @ Bound_variable_3076 )
= ( sub @ ( sub @ Bound_variable_3149 @ ( push @ Bound_variable_3074 @ Bound_variable_3072 ) ) @ Bound_variable_3076 ) )
| ~ ! [Bound_variable_3090: subst,Bound_variable_3092: term,Bound_variable_3094: subst] :
( ( F @ ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) @ ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) )
= ( sub @ Bound_variable_3149 @ ( push @ ( sub @ Bound_variable_3092 @ Bound_variable_3094 ) @ ( comp @ Bound_variable_3090 @ Bound_variable_3094 ) ) ) ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3171 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3171 @ ( push @ one @ sh ) ) ) @ id ) ) )
& induction2lem_gthm
& ( hoasinduction_lem3aa_lthm
<=> ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) ) )
& ( hoasinduction_lem3
<=> ! [P: subst > term > subst > $o,Bound_variable_3211: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) ) )
& ( hoasinduction_lem2
<=> ! [P: subst > term > subst > $o,Bound_variable_2999: term,Bound_variable_3001: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ( P @ id @ Bound_variable_2999 @ id )
| ~ ( P @ id @ Bound_variable_3001 @ id )
| ( P @ id @ ( ap @ Bound_variable_2999 @ Bound_variable_3001 ) @ id ) ) )
& ( termmset_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [A: term] :
( A
= ( sub @ A @ id ) ) ) )
& hoasinduction_lem1
& hoaslamnotap_lthm
& ( pushprop_lem1v2_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ! [P: term > $o,Q: term > $o,A: term,M: subst] :
( ~ ( P @ A )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ ( sub @ X @ ( push @ A @ M ) ) ) )
| ( Q @ one ) ) ) )
& hoasapnotvar
& ( hoasinduction_lem0
<=> ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) ) )
& ( hoasinduction
<=> ! [P: subst > term > subst > $o,Bound_variable_3283: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term] :
( ~ ( var @ ( sub @ A @ id ) )
| ( P @ id @ A @ id ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3283 @ id ) ) )
& hoasinduction_gthm
& axapp
& hoaslamnotvar_lthm
& pushprop_lem3v2_lthm
& ( hoasinduction_lem3b_lthm
<=> ! [B: term] :
~ ! [F: subst > term > term] :
( ( F @ sh @ one )
!= ( sub @ B @ ( push @ one @ sh ) ) ) )
& ulamvarind
& ( induction
<=> ! [P: term > $o,Bound_variable_2140: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ( P @ A )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2140 ) ) )
& ( hoasinduction_lem3a_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3232: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3232 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3232 ) @ id ) ) ) ) )
& termmset_gthm
& ( hoasinduction_lem3aa
<=> ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) ) )
& pushprop_lem1v2_gthm
& hoaslamnotap_gthm
& hoaslamnotvar_gthm
& hoasinduction_lem3b_gthm
& pushprop_lem2v2
& hoasinduction_lem3a_gthm
& axclos
& axassoc
& ( hoasinduction_lem2v2
<=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2820: term,Bound_variable_2822: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
| ~ ( Q @ Bound_variable_2820 )
| ~ ( Q @ Bound_variable_2822 )
| ( Q @ ( ap @ Bound_variable_2820 @ Bound_variable_2822 ) ) ) )
& pushprop_lthm
& ( apinj2
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( C = D ) ) )
& ( apinj1
<=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( A = B ) ) )
& ( hoasapinj2_lthm
<=> ( ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( C = D ) )
=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( C = D ) ) ) )
& ( hoasinduction_lem3v2a
<=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) ) )
& ( hoasapinj1_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ A @ C )
!= ( ap @ B @ D ) )
| ( A = B ) )
=> ! [A: term,B: term,C: term,D: term] :
( ( ( ap @ ( sub @ A @ id ) @ C )
!= ( ap @ ( sub @ B @ id ) @ D ) )
| ( A = B ) ) ) ) )
& ( hoaslaminj_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ( ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) )
=> ( ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) )
=> ! [F: subst > term > term,Bound_variable_2547: subst > term > term,Bound_variable_2549: subst,Bound_variable_2551: term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( Bound_variable_2547 @ M @ A ) @ N )
= ( Bound_variable_2547 @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ( ( lam @ ( F @ sh @ one ) )
!= ( lam @ ( Bound_variable_2547 @ sh @ one ) ) )
| ( ( F @ Bound_variable_2549 @ Bound_variable_2551 )
= ( Bound_variable_2547 @ Bound_variable_2549 @ Bound_variable_2551 ) ) ) ) ) ) )
& ( axvarcons
<=> ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) ) )
& ( axscons
<=> ! [M: subst] :
( M
= ( push @ ( sub @ one @ M ) @ ( comp @ sh @ M ) ) ) )
& hoasinduction_lem2v2_gthm
& ( axidr
<=> ! [M: subst] :
( M
= ( comp @ M @ id ) ) )
& ( pushprop_lem1
<=> ! [P: term > $o,K: term > $o,A: term,M: subst,B: term] :
( ~ ( P @ A )
| ( K @ ( sub @ A @ ( push @ B @ M ) ) ) ) )
& ( laminj
<=> ! [A: term,B: term] :
( ( ( lam @ A )
!= ( lam @ B ) )
| ( A = B ) ) )
& ( hoasinduction_lem3_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Bound_variable_3046: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3046 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ ( sub @ Bound_variable_3046 @ ( push @ one @ sh ) ) ) @ id ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3211: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3211 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3211 ) @ id ) ) ) ) )
& ( pushprop_lem0
<=> ! [P: term > $o,A: term,M: subst] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
= ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) )
& pushprop_gthm
& axabs
& ( hoasinduction_lem3v2a_lthm
<=> ( ! [B: term] :
~ ! [F: subst > term > term] :
~ ! [A: term,M: subst] :
( ( sub @ B @ ( push @ A @ M ) )
= ( F @ M @ A ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) ) ) ) )
& hoasinduction_lem2_lthm
& hoasapinj2_gthm
& hoasinduction_lem1_lthm
& ~ lamnotap
& hoasapinj1_gthm
& hoaslamnotvar
& ( axidl
<=> ! [M: subst] :
( M
= ( comp @ id @ M ) ) )
& hoaslaminj_gthm
& ( induction2_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: term > $o,Bound_variable_2340: term,Bound_variable_2342: subst] :
( ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ~ ! [B: term] :
( ~ ( var @ B )
| ( P @ ( sub @ B @ Bound_variable_2342 ) ) )
| ( P @ ( sub @ Bound_variable_2340 @ Bound_variable_2342 ) ) )
=> ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) ) ) ) )
& ( hoasinduction_lem0_lthm
<=> ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) ) )
& ( substmonoid_lthm
<=> ( ! [M: subst] :
( M
= ( comp @ id @ M ) )
=> ( ! [M: subst] :
( M
= ( comp @ M @ id ) )
=> ( ! [M: subst] :
( M
= ( comp @ id @ M ) )
& ! [M: subst] :
( M
= ( comp @ M @ id ) ) ) ) ) )
& pushprop
& hoasinduction_lem3_gthm
& hoasinduction_lem2_gthm
& ( hoasinduction_lem3b
<=> ! [B: term] :
~ ! [F: subst > term > term] :
( ( F @ sh @ one )
!= ( sub @ B @ ( push @ one @ sh ) ) ) )
& ( substmonoid
<=> ( ! [M: subst] :
( M
= ( comp @ id @ M ) )
& ! [M: subst] :
( M
= ( comp @ M @ id ) ) ) )
& lamnotvar
& ( hoasinduction_lem3a
<=> ! [P: subst > term > subst > $o,Bound_variable_3232: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [B: term] :
( ~ ( P @ id @ B @ id )
| ( P @ id @ ( sub @ Bound_variable_3232 @ ( push @ B @ id ) ) @ id ) )
| ( P @ id @ ( lam @ Bound_variable_3232 ) @ id ) ) )
& hoasinduction_lem1_gthm
& ( hoasinduction_no_psi_cond
<=> ! [P: subst > term > subst > $o,Bound_variable_3295: term] :
( ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3295 @ id ) ) )
& induction2_gthm
& pushprop_lem2v2_lthm
& ~ ( hoasvar @ ( d2subst @ d_id ) @ ( d2term @ d_one ) @ ( d2subst @ d_id ) )
& ( hoaslamnotap
<=> ! [F: subst > term > term,Bound_variable_2603: term,Bound_variable_2605: term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ( ( lam @ ( F @ sh @ one ) )
!= ( ap @ ( sub @ Bound_variable_2603 @ id ) @ Bound_variable_2605 ) ) ) )
& substmonoid_gthm
& ulamvarsh
& ( induction2
<=> ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) ) )
& pushprop_lem3v2
& pushprop_lem2v2_gthm
& ( pushprop_lem1_lthm
<=> ( ! [A: term,M: subst] :
( A
= ( sub @ one @ ( push @ A @ M ) ) )
=> ( ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) )
=> ! [P: term > $o,K: term > $o,A: term,M: subst,B: term] :
( ~ ( P @ A )
| ( K @ ( sub @ A @ ( push @ B @ M ) ) ) ) ) ) )
& ( hoasinduction_lem3v2
<=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2910: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2910 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2910 ) ) ) )
& ( axshiftcons
<=> ! [A: term,M: subst] :
( M
= ( comp @ sh @ ( push @ A @ M ) ) ) )
& ( termmset
<=> ! [A: term] :
( A
= ( sub @ A @ id ) ) )
& ( pushprop_lem0_lthm
<=> ! [P: term > $o,A: term,M: subst] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
= ( P @ ( sub @ X @ ( push @ A @ M ) ) ) ) )
& hoasapnotvar_lthm
& ( hoasinduction_lem3v2_lthm
<=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2910: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2910 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2910 ) ) ) ) )
& ( axvarid
<=> ! [A: term] :
( A
= ( sub @ A @ id ) ) )
& ( hoasinduction_lthm_3
<=> ( ! [P: subst > term > subst > $o] :
~ ! [Q: term > $o] :
~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
=> ( ! [P: term > $o,Bound_variable_2367: term] :
( ~ ! [A: term] :
( ~ ( var @ A )
| ( P @ A ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ A )
| ~ ( P @ B )
| ( P @ ( ap @ A @ B ) ) )
| ~ ! [A: term] :
( ~ ! [B: term] :
( ~ ( P @ B )
| ( P @ ( sub @ A @ ( push @ B @ id ) ) ) )
| ( P @ ( lam @ A ) ) )
| ( P @ Bound_variable_2367 ) )
=> ( ! [A: term] :
( A
= ( sub @ A @ id ) )
=> ( ! [P: subst > term > subst > $o,Q: term > $o,Bound_variable_2931: term] :
( ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ~ ! [X: term] :
( ( Q @ X )
= ( P @ id @ X @ id ) )
| ~ ! [B: term] :
( ~ ( Q @ B )
| ( Q @ ( sub @ Bound_variable_2931 @ ( push @ B @ id ) ) ) )
| ( Q @ ( lam @ Bound_variable_2931 ) ) )
=> ! [P: subst > term > subst > $o,Bound_variable_3283: term] :
( ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ M @ A @ ( comp @ K @ N ) )
| ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N ) )
| ~ ! [M: subst,A: term,N: subst,K: subst] :
( ~ ( P @ ( comp @ M @ K ) @ ( sub @ A @ K ) @ N )
| ( P @ M @ A @ ( comp @ K @ N ) ) )
| ~ ! [A: term] :
( ~ ( var @ ( sub @ A @ id ) )
| ( P @ id @ A @ id ) )
| ~ ! [A: term,B: term] :
( ~ ( P @ id @ A @ id )
| ~ ( P @ id @ B @ id )
| ( P @ id @ ( ap @ ( sub @ A @ id ) @ B ) @ id ) )
| ~ ! [F: subst > term > term] :
( ~ ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
| ~ ! [A: term] :
( ~ ( P @ id @ A @ id )
| ( P @ id @ ( F @ id @ A ) @ id ) )
| ( P @ id @ ( lam @ ( F @ sh @ one ) ) @ id ) )
| ( P @ id @ Bound_variable_3283 @ id ) ) ) ) ) ) ) ) ).
thf(hoasinduction_lem3aa,conjecture,
( hoasinduction_lem3aa
= ( ! [P: subst > term > subst > $o] :
( ! [F: subst > term > term] :
( ! [M: subst,A: term,N: subst] :
( ( sub @ ( F @ M @ A ) @ N )
= ( F @ ( comp @ M @ N ) @ ( sub @ A @ N ) ) )
=> ( ! [A: term] :
( ( P @ id @ A @ id )
=> ( P @ id @ ( F @ id @ A ) @ id ) )
=> ( P @ id
@ ( hoaslam @ id
@ ^ [M: subst,A: term] : ( F @ M @ A ) )
@ id ) ) )
=> ! [A: term] :
( ! [B: term] :
( ( P @ id @ B @ id )
=> ( P @ id @ ( sub @ A @ ( push @ B @ id ) ) @ id ) )
=> ( P @ id @ ( lam @ ( sub @ A @ ( push @ one @ sh ) ) ) @ id ) ) ) ) ) ).
%------------------------------------------------------------------------------