include('Axioms/SET010^0.ax').
thf(k1_funct_1_type, type, k1_funct_1: $i > $i > $i).
thf(k1_pboole_type, type, k1_pboole: $i > $i).
thf(k1_xboole_0_type, type, k1_xboole_0: $i).
thf(k2_funcop_1_type, type, k2_funcop_1: $i > $i > $i).
thf(k9_xtuple_0_type, type, k9_xtuple_0: $i > $i).
thf(r1_tarski_type, type, r1_tarski: $i > $i > $o).
thf(k10_xtuple_0_type, type, k10_xtuple_0: $i > $i).
thf(k1_tarski_type, type, k1_tarski: $i > $i).
thf(k7_funcop_1_type, type, k7_funcop_1: $i > $i > $i).
thf(v1_relat_1_type, type, v1_relat_1: $i > $o).
thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(k4_tarski_type, type, k4_tarski: $i > $i > $i).
thf(t7_funcop_1, axiom,   (! [A: $i] :  (! [B: $i] :  (! [C: $i] :  ( ( (r2_hidden @ B)  @ A)  =>  ( (= @  ( (k1_funct_1 @  ( (k2_funcop_1 @ A)  @ C) )  @ B) )  @ C) ) ) ) ) , file(funcop_1, t7_funcop_1)).
thf(t13_funcop_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (= @  (k9_xtuple_0 @  ( (k2_funcop_1 @ A)  @ B) ) )  @ A)  &  ( (r1_tarski @  (k10_xtuple_0 @  ( (k2_funcop_1 @ A)  @ B) ) )  @  (k1_tarski @ B) ) ) ) ) , file(funcop_1, t13_funcop_1)).
thf(redefinition_k7_funcop_1, axiom,   (! [A: $i, B: $i] :  ( (= @  ( (k7_funcop_1 @ A)  @ B) )  @  ( (k2_funcop_1 @ A)  @ B) ) ) , file(funcop_1, k7_funcop_1)).
thf(fc1_funcop_1, axiom,   (! [A: $i, B: $i] :  ( (v1_relat_1 @  ( (k2_funcop_1 @ A)  @ B) )  &  (v1_funct_1 @  ( (k2_funcop_1 @ A)  @ B) ) ) ) , file(funcop_1, fc1_funcop_1)).
thf(d3_pboole, axiom,   (! [A: $i] :  ( (= @  (k1_pboole @ A) )  @  ( (k7_funcop_1 @ A)  @ k1_xboole_0) ) ) , file(pboole, d3_pboole)).
thf(d2_funct_1, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  (v1_funct_1 @ A) )  =>  (! [B: $i] :  (! [C: $i] :  ( ( ( (r2_hidden @ B)  @  (k9_xtuple_0 @ A) )  =>  ( ( (= @ C)  @  ( (k1_funct_1 @ A)  @ B) )  <=>  ( (r2_hidden @  ( (k4_tarski @ B)  @ C) )  @ A) ) )  &  ( ~ ( ( (r2_hidden @ B)  @  (k9_xtuple_0 @ A) ) )  =>  ( ( (= @ C)  @  ( (k1_funct_1 @ A)  @ B) )  <=>  ( (= @ C)  @ k1_xboole_0) ) ) ) ) ) ) ) , file(funct_1, d2_funct_1)).
thf(t5_pboole, conjecture,   (! [A: $i] :  (! [B: $i] :  ( (= @  ( (k1_funct_1 @  (k1_pboole @ B) )  @ A) )  @ k1_xboole_0) ) ) , file(pboole, t5_pboole)).