fof(t20_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( A = k7_arytm_2(B,C) => r1_arytm_2(C,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_arytm_2,t1_arytm_2,t7_arytm_2,d8_arytm_2,t12_arytm_2,t6_arytm_2,d8_arytm_2]), [file(arytm_2,t20_arytm_2),interesting(1.00)]). fof(l35_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => k4_arytm_2(k3_arytm_2(A)) = A ) ), inference(mizar_proof,[status(thm)],[l23_arytm_2,l34_arytm_2]), [file(arytm_2,l35_arytm_2),interesting(0.96)]). fof(l5_arytm_2,theorem,( r1_xboole_0(k6_arytm_3,a_0_1_arytm_2) ), inference(mizar_proof,[status(thm)],[t3_xboole_0,t71_arytm_3,t75_arytm_3,d3_tarski,t99_arytm_3,t101_arytm_3]), [file(arytm_2,l5_arytm_2),interesting(0.95)]). fof(t12_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( k7_arytm_2(A,B) = k7_arytm_2(A,C) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_arytm_2,t7_arytm_2,l57_arytm_2,d8_arytm_2,t7_arytm_2,l57_arytm_2,d8_arytm_2]), [file(arytm_2,t12_arytm_2),interesting(0.95)]). fof(l3_arytm_2,theorem,( ! [A,B] : ~ r2_hidden(k4_tarski(A,B),a_0_0_arytm_2) ), inference(mizar_proof,[status(thm)],[d2_tarski,t82_arytm_3,d2_tarski]), [file(arytm_2,l3_arytm_2),interesting(0.94)]). fof(t1_arytm_2,theorem,( r1_tarski(k6_arytm_3,k2_arytm_2) ), inference(mizar_proof,[status(thm)],[l4_arytm_2,l5_arytm_2,t86_xboole_1]), [file(arytm_2,t1_arytm_2),interesting(0.90)]). fof(t10_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ~ ( r1_arytm_2(A,B) & ! [C] : ( m1_subset_1(C,k2_arytm_2) => k7_arytm_2(A,C) != B ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_arytm_2,t1_arytm_2,d8_arytm_2,l21_arytm_2,l34_arytm_2,l59_arytm_2,l58_arytm_2,d1_xboole_0,d6_arytm_2,t3_xboole_1,l22_arytm_2,d8_arytm_2,l23_arytm_2,l35_arytm_2]), [file(arytm_2,t10_arytm_2),interesting(0.86)]). fof(t8_arytm_2,theorem,( v6_ordinal1(a_0_0_arytm_2) ), inference(mizar_proof,[status(thm)],[d9_ordinal1,d9_xboole_0,d3_tarski,d3_tarski]), [file(arytm_2,t8_arytm_2),interesting(0.86)]). fof(l19_arytm_2,theorem,( r2_hidden(k12_arytm_3,k1_arytm_2) ), inference(mizar_proof,[status(thm)],[t2_xboole_1,t64_zfmisc_1]), [file(arytm_2,l19_arytm_2),interesting(0.85)]). fof(t11_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ~ ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( k7_arytm_2(A,C) != B & k7_arytm_2(B,C) != A ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_arytm_2]), [file(arytm_2,t11_arytm_2),interesting(0.85)]). fof(l70_arytm_2,theorem,( m1_subset_1(k13_arytm_3,k2_arytm_2) ), inference(mizar_proof,[status(thm)],[l69_arytm_2,t1_arytm_2]), [file(arytm_2,l70_arytm_2),interesting(0.84)]). fof(t2_arytm_2,theorem,( r1_tarski(k5_ordinal2,k2_arytm_2) ), inference(mizar_proof,[status(thm)],[t1_arytm_2,t34_arytm_3,t1_xboole_1]), [file(arytm_2,t2_arytm_2),interesting(0.84)]). fof(l8_arytm_2,theorem,( r1_tarski(k1_arytm_2,a_0_0_arytm_2) ), inference(mizar_proof,[status(thm)],[t36_xboole_1]), [file(arytm_2,l8_arytm_2),interesting(0.84)]). fof(l33_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( ( r1_arytm_2(A,B) & r1_arytm_2(B,A) ) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[l26_arytm_2,t73_arytm_3,d5_arytm_2,d5_arytm_2,d5_arytm_2,d10_xboole_0]), [file(arytm_2,l33_arytm_2),interesting(0.81)]). fof(l34_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( k3_arytm_2(A) = k3_arytm_2(B) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[l32_arytm_2,l33_arytm_2]), [file(arytm_2,l34_arytm_2),interesting(0.80)]). fof(l57_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( k7_arytm_2(A,B) = A => B = k12_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[t6_arytm_2,l21_arytm_2,d8_arytm_2,l23_arytm_2,l56_arytm_2,l21_arytm_2]), [file(arytm_2,l57_arytm_2),interesting(0.79)]). fof(l24_arytm_2,theorem,( ! [A,B] : ~ ( r2_hidden(A,a_0_0_arytm_2) & r2_hidden(B,a_0_0_arytm_2) & ~ r1_tarski(A,B) & ~ r1_tarski(B,A) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_tarski]), [file(arytm_2,l24_arytm_2),interesting(0.78)]). fof(t15_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ~ ( A != k12_arytm_3 & ! [B] : ( m1_subset_1(B,k2_arytm_2) => k8_arytm_2(A,B) != k13_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[l21_arytm_2,l72_arytm_2,l23_arytm_2,l35_arytm_2]), [file(arytm_2,t15_arytm_2),interesting(0.76)]). fof(l59_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( r1_arytm_2(A,B) => r1_tarski(k3_arytm_2(A),k3_arytm_2(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_xboole_0,l24_arytm_2,l32_arytm_2,l33_arytm_2]), [file(arytm_2,l59_arytm_2),interesting(0.76)]). fof(t3_arytm_2,theorem,( ! [A] : ~ r2_hidden(k4_tarski(k12_arytm_3,A),k2_arytm_2) ), inference(mizar_proof,[status(thm)],[t68_arytm_3,l3_arytm_2,l10_arytm_2,d2_xboole_0]), [file(arytm_2,t3_arytm_2),interesting(0.76)]). fof(l4_arytm_2,theorem,( r1_tarski(k6_arytm_3,k2_xboole_0(k6_arytm_3,k1_arytm_2)) ), inference(mizar_proof,[status(thm)],[t7_xboole_1]), [file(arytm_2,l4_arytm_2),interesting(0.75)]). fof(l29_arytm_2,theorem,( ! [A] : ( r2_hidden(A,k1_arytm_2) => ( A = k12_arytm_3 | r2_hidden(k12_arytm_3,A) ) ) ), inference(mizar_proof,[status(thm)],[t10_subset_1,t71_arytm_3,l28_arytm_2]), [file(arytm_2,l29_arytm_2),interesting(0.75)]). fof(l32_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( r1_tarski(k3_arytm_2(A),k3_arytm_2(B)) => r1_arytm_2(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_arytm_2,l29_arytm_2,d5_arytm_2,l21_arytm_2,t3_xboole_1,l21_arytm_2,d3_arytm_2,d3_arytm_2,l26_arytm_2,d3_arytm_2,d3_arytm_2,l31_arytm_2,d10_xboole_0,t7_subset_1,l28_arytm_2,d5_arytm_2,d3_arytm_2,d3_arytm_2,l31_arytm_2,d10_xboole_0,t7_subset_1,l28_arytm_2,d5_arytm_2,d3_arytm_2,d5_arytm_2]), [file(arytm_2,l32_arytm_2),interesting(0.75)]). fof(l77_arytm_2,theorem,( m1_subset_1(k13_arytm_3,k5_ordinal2) ), inference(mizar_proof,[status(thm)],[d21_ordinal2]), [file(arytm_2,l77_arytm_2),interesting(0.72)]). fof(t7_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => k7_arytm_2(A,k7_arytm_2(B,C)) = k7_arytm_2(k7_arytm_2(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_arytm_2,d8_arytm_2,d8_arytm_2,d8_arytm_2,d8_arytm_2,d8_arytm_2,l22_arytm_2,l46_arytm_2,l21_arytm_2,l22_arytm_2,l46_arytm_2,l21_arytm_2,d8_arytm_2,d8_arytm_2,l23_arytm_2,l45_arytm_2,l23_arytm_2,d8_arytm_2,d8_arytm_2]), [file(arytm_2,t7_arytm_2),interesting(0.72)]). fof(l21_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ( k3_arytm_2(A) = k12_arytm_3 <=> A = k12_arytm_3 ) ) ), inference(mizar_proof,[status(thm)],[d3_arytm_2,t71_arytm_3,t75_arytm_3,d3_arytm_2,t71_arytm_3,d3_arytm_2,d1_xboole_0]), [file(arytm_2,l21_arytm_2),interesting(0.70)]). fof(t16_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( A = k13_arytm_3 => k8_arytm_2(A,B) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_arytm_2,l74_arytm_2,l35_arytm_2]), [file(arytm_2,t16_arytm_2),interesting(0.70)]). fof(t6_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( k7_arytm_2(A,B) = k12_arytm_3 => A = k12_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[d8_arytm_2,d8_arytm_2,l22_arytm_2,l21_arytm_2,t10_subset_1,l21_arytm_2,t10_subset_1]), [file(arytm_2,t6_arytm_2),interesting(0.70)]). fof(l7_arytm_2,theorem,( r1_tarski(k2_arytm_2,k2_xboole_0(k6_arytm_3,k1_arytm_2)) ), inference(mizar_proof,[status(thm)],[t36_xboole_1]), [file(arytm_2,l7_arytm_2),interesting(0.70)]). fof(l23_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => k3_arytm_2(k4_arytm_2(A)) = A ) ), inference(mizar_proof,[status(thm)],[d4_arytm_2,d3_arytm_2,d3_tarski,d10_xboole_0,d3_tarski,l22_arytm_2,l21_arytm_2,d4_arytm_2,d3_xboole_0,l20_arytm_2,d1_tarski,l22_arytm_2,d3_arytm_2]), [file(arytm_2,l23_arytm_2),interesting(0.69)]). fof(t4_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( A = k12_arytm_3 => k8_arytm_2(A,B) = k12_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[l21_arytm_2,d1_xboole_0,l22_arytm_2]), [file(arytm_2,t4_arytm_2),interesting(0.69)]). fof(l10_arytm_2,theorem,( r1_tarski(k2_arytm_2,k2_xboole_0(k6_arytm_3,a_0_0_arytm_2)) ), inference(mizar_proof,[status(thm)],[l9_arytm_2,l7_arytm_2,t1_xboole_1]), [file(arytm_2,l10_arytm_2),interesting(0.69)]). fof(l9_arytm_2,theorem,( r1_tarski(k2_xboole_0(k6_arytm_3,k1_arytm_2),k2_xboole_0(k6_arytm_3,a_0_0_arytm_2)) ), inference(mizar_proof,[status(thm)],[l8_arytm_2,t9_xboole_1]), [file(arytm_2,l9_arytm_2),interesting(0.67)]). fof(l16_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ( ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( ~ ( ~ r3_arytm_3(A,C) & r3_arytm_3(B,C) ) & ~ ( ~ r3_arytm_3(B,C) & r3_arytm_3(A,C) ) ) ) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[t73_arytm_3]), [file(arytm_2,l16_arytm_2),interesting(0.66)]). fof(t21_arytm_2,theorem, ( r2_hidden(k12_arytm_3,k2_arytm_2) & r2_hidden(k13_arytm_3,k2_arytm_2) ), inference(mizar_proof,[status(thm)],[t1_arytm_2]), [file(arytm_2,t21_arytm_2),interesting(0.66)]). fof(l31_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ( r2_hidden(k3_arytm_2(A),a_0_1_arytm_2) => r2_hidden(A,k6_arytm_3) ) ) ), inference(mizar_proof,[status(thm)],[d3_arytm_2,d4_xboole_0]), [file(arytm_2,l31_arytm_2),interesting(0.65)]). fof(l37_arytm_2,theorem,( ! [A] : ~ ( r2_hidden(A,k1_arytm_2) & ! [B] : ( m1_subset_1(B,k6_arytm_3) => r2_hidden(B,A) ) ) ), inference(mizar_proof,[status(thm)],[t64_zfmisc_1,t49_subset_1]), [file(arytm_2,l37_arytm_2),interesting(0.64)]). fof(l18_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ~ ( r2_hidden(B,k1_arytm_2) & r2_hidden(A,B) & ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( r2_hidden(C,B) & ~ r3_arytm_3(C,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_xboole_0]), [file(arytm_2,l18_arytm_2),interesting(0.64)]). fof(l66_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ~ ( k8_arytm_2(A,B) = k12_arytm_3 & A != k12_arytm_3 & B != k12_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[l22_arytm_2,t10_subset_1,t10_subset_1,l21_arytm_2]), [file(arytm_2,l66_arytm_2),interesting(0.64)]). fof(l28_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( ( r2_hidden(C,k1_arytm_2) & r2_hidden(A,C) & r3_arytm_3(B,A) ) => r2_hidden(B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_xboole_0]), [file(arytm_2,l28_arytm_2),interesting(0.64)]). fof(l71_arytm_2,theorem,( ! [A] : ~ ( r2_hidden(A,a_0_0_arytm_2) & A != k12_arytm_3 & ! [B] : ( m1_subset_1(B,k6_arytm_3) => ~ ( r2_hidden(B,A) & B != k12_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[t10_subset_1,t82_arytm_3]), [file(arytm_2,l71_arytm_2),interesting(0.63)]). fof(l27_arytm_2,theorem,( ! [A] : ~ ( r2_hidden(A,k1_arytm_2) & A != k12_arytm_3 & ! [B] : ( m1_subset_1(B,k6_arytm_3) => ~ ( r2_hidden(B,A) & B != k12_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[d4_xboole_0,t10_subset_1,t82_arytm_3]), [file(arytm_2,l27_arytm_2),interesting(0.63)]). fof(l22_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ( k4_arytm_2(A) = k12_arytm_3 <=> A = k12_arytm_3 ) ) ), inference(mizar_proof,[status(thm)],[d4_arytm_2,t10_subset_1,t71_arytm_3,d4_arytm_2,t71_arytm_3,d4_arytm_2,t71_arytm_3,t75_arytm_3]), [file(arytm_2,l22_arytm_2),interesting(0.57)]). fof(t13_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => k8_arytm_2(A,k8_arytm_2(B,C)) = k8_arytm_2(k8_arytm_2(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[l23_arytm_2,l64_arytm_2,l23_arytm_2]), [file(arytm_2,t13_arytm_2),interesting(0.56)]). fof(l52_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( ( r1_arytm_2(A,B) & r1_arytm_2(B,C) ) => r1_arytm_2(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l26_arytm_2,l26_arytm_2,t74_arytm_3,l26_arytm_2,l10_arytm_2,d2_xboole_0,l26_arytm_2,d5_arytm_2,d5_arytm_2,l10_arytm_2,d2_xboole_0,d5_arytm_2,d5_arytm_2,l26_arytm_2,l10_arytm_2,d2_xboole_0,l10_arytm_2,d2_xboole_0,d5_arytm_2,d5_arytm_2,d5_arytm_2,l10_arytm_2,d2_xboole_0,d5_arytm_2,l26_arytm_2,d5_arytm_2,l10_arytm_2,d2_xboole_0,l10_arytm_2,d2_xboole_0,d5_arytm_2,d5_arytm_2,d3_tarski,d5_arytm_2,l10_arytm_2,d2_xboole_0,l10_arytm_2,d2_xboole_0,d5_arytm_2,d5_arytm_2,d5_arytm_2,l10_arytm_2,d2_xboole_0,l10_arytm_2,d2_xboole_0,l10_arytm_2,d2_xboole_0,d5_arytm_2,d5_arytm_2,t1_xboole_1,d5_arytm_2]), [file(arytm_2,l52_arytm_2),interesting(0.56)]). fof(l49_arytm_2,theorem,( ! [A] : ~ ( r2_hidden(A,k2_arytm_2) & A = k6_arytm_3 ) ), inference(mizar_proof,[status(thm)],[d4_xboole_0,d2_xboole_0,t64_zfmisc_1]), [file(arytm_2,l49_arytm_2),interesting(0.56)]). fof(l76_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k5_ordinal2) => ! [B] : ( m1_subset_1(B,k5_ordinal2) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ! [D] : ( m1_subset_1(D,k6_arytm_3) => ( ( A = C & B = D ) => k1_arytm_3(A,B) = k10_arytm_3(C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_arytm_3,d8_arytm_3,t56_ordinal2,t56_ordinal2,t56_ordinal2,d7_arytm_3,d7_arytm_3,t29_arytm_3,t29_arytm_3,d9_arytm_3,d10_arytm_3]), [file(arytm_2,l76_arytm_2),interesting(0.55)]). fof(t14_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => k8_arytm_2(A,k7_arytm_2(B,C)) = k7_arytm_2(k8_arytm_2(A,B),k8_arytm_2(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_arytm_2,d8_arytm_2,t4_arytm_2,t4_arytm_2,d8_arytm_2,d8_arytm_2,t4_arytm_2,d8_arytm_2,d8_arytm_2,t4_arytm_2,l66_arytm_2,l66_arytm_2,d8_arytm_2,l23_arytm_2,l67_arytm_2,l23_arytm_2,l23_arytm_2,d8_arytm_2]), [file(arytm_2,t14_arytm_2),interesting(0.54)]). fof(l74_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ( A = a_0_2_arytm_2 => k6_arytm_2(A,B) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t90_arytm_3,t59_arytm_3,l28_arytm_2,d10_xboole_0,d3_tarski,l18_arytm_2,t71_arytm_3,t61_arytm_3,t59_arytm_3,t91_arytm_3,t59_arytm_3,t75_arytm_3]), [file(arytm_2,l74_arytm_2),interesting(0.54)]). fof(l20_arytm_2,theorem,( k3_xboole_0(k1_arytm_2,k6_arytm_3) = k1_tarski(k12_arytm_3) ), inference(mizar_proof,[status(thm)],[d3_xboole_0,d3_xboole_0,t99_arytm_3,l18_arytm_2,l19_arytm_2,d3_xboole_0,d1_tarski]), [file(arytm_2,l20_arytm_2),interesting(0.53)]). fof(l26_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ! [D] : ( m1_subset_1(D,k2_arytm_2) => ( ( C = A & D = B ) => ( r1_arytm_2(C,D) <=> r3_arytm_3(A,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_arytm_2,d5_arytm_2]), [file(arytm_2,l26_arytm_2),interesting(0.53)]). fof(t17_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( ( r2_hidden(A,k5_ordinal2) & r2_hidden(B,k5_ordinal2) ) => r2_hidden(k7_arytm_2(B,A),k5_ordinal2) ) ) ) ), inference(mizar_proof,[status(thm)],[l79_arytm_2,t34_arytm_3,l76_arytm_2,d21_ordinal2]), [file(arytm_2,t17_arytm_2),interesting(0.53)]). fof(l12_arytm_2,theorem,( r1_tarski(k4_xboole_0(k1_arytm_2,a_0_1_arytm_2),k2_arytm_2) ), inference(mizar_proof,[status(thm)],[l11_arytm_2,t7_xboole_1]), [file(arytm_2,l12_arytm_2),interesting(0.53)]). fof(l72_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ~ ( A != k12_arytm_3 & ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => k6_arytm_2(A,B) != k3_arytm_2(c3) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_arytm_3,d3_tarski,t76_arytm_3,t101_arytm_3,t64_zfmisc_1,d3_tarski,t62_arytm_3,t90_arytm_3,t75_arytm_3,t90_arytm_3,t76_arytm_3,d10_xboole_0,d3_tarski,t87_arytm_3,t75_arytm_3,l18_arytm_2,t90_arytm_3,t87_arytm_3,t62_arytm_3,t75_arytm_3,d3_arytm_2,t64_zfmisc_1,t49_subset_1,t54_arytm_3,t71_arytm_3,d3_tarski,t64_zfmisc_1,t10_subset_1,t71_arytm_3,l50_arytm_2,t90_arytm_3,t74_arytm_3,d4_xboole_0,l30_arytm_2,t61_arytm_3,t90_arytm_3,t74_arytm_3,t88_arytm_3,t90_arytm_3,t54_arytm_3,t73_arytm_3,t62_arytm_3,t75_arytm_3,l71_arytm_2,t61_arytm_3,t54_arytm_3,t88_arytm_3,l50_arytm_2,d1_tarski,d4_xboole_0,l50_arytm_2,t90_arytm_3,t74_arytm_3,t54_arytm_3,t73_arytm_3,t62_arytm_3,t75_arytm_3,t54_arytm_3,t61_arytm_3,d12_arytm_3,t49_subset_1,t56_arytm_3,t86_arytm_3,t103_arytm_3,t54_arytm_3,l50_arytm_2,s2_arytm_3,l54_arytm_2,l55_arytm_2,d3_tarski,t63_arytm_3,t59_arytm_3,t90_arytm_3,t83_arytm_3,t90_arytm_3,t83_arytm_3,t63_arytm_3,t59_arytm_3,l50_arytm_2,t54_arytm_3,t61_arytm_3,t58_arytm_3,t59_arytm_3,t58_arytm_3,t58_arytm_3,t59_arytm_3,t58_arytm_3,t59_arytm_3,d4_arytm_2,l23_arytm_2]), [file(arytm_2,l72_arytm_2),interesting(0.51)]). fof(l56_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ( k5_arytm_2(A,B) = A => ( A = k12_arytm_3 | B = k12_arytm_3 ) ) ) ) ), inference(mizar_proof,[status(thm)],[l27_arytm_2,t64_zfmisc_1,t49_subset_1,t103_arytm_3,l28_arytm_2,t10_subset_1,t71_arytm_3,t54_arytm_3,l28_arytm_2,s2_arytm_3,l54_arytm_2,l55_arytm_2,t63_arytm_3,t59_arytm_3]), [file(arytm_2,l56_arytm_2),interesting(0.49)]). fof(l11_arytm_2,theorem,( k2_arytm_2 = k2_xboole_0(k6_arytm_3,k4_xboole_0(k4_xboole_0(a_0_0_arytm_2,k1_tarski(k6_arytm_3)),a_0_1_arytm_2)) ), inference(mizar_proof,[status(thm)],[l5_arytm_2,t87_xboole_1]), [file(arytm_2,l11_arytm_2),interesting(0.48)]). fof(t19_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ( r2_hidden(A,k5_ordinal2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( r2_hidden(B,A) <=> ( r2_hidden(B,k5_ordinal2) & B != A & r1_arytm_2(B,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_ordinal1,t34_arytm_3,t34_arytm_3,d2_ordinal1,t30_ordinal3,t27_ordinal3,t22_ordinal1,t34_arytm_3,l76_arytm_2,d12_arytm_3,l26_arytm_2,t34_arytm_3,l26_arytm_2,d12_arytm_3,t78_arytm_3,l76_arytm_2,t27_ordinal3,d8_xboole_0,t21_ordinal1]), [file(arytm_2,t19_arytm_2),interesting(0.46)]). fof(l79_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ~ ( r2_hidden(A,k6_arytm_3) & r2_hidden(B,k6_arytm_3) & ! [C] : ( m1_subset_1(C,k6_arytm_3) => ! [D] : ( m1_subset_1(D,k6_arytm_3) => ~ ( A = C & B = D & k7_arytm_2(A,B) = k10_arytm_3(C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_arytm_2,t56_arytm_3,d8_arytm_2,t56_arytm_3,d3_arytm_2,d3_arytm_2,t83_arytm_3,t83_arytm_3,t76_arytm_3,l78_arytm_2,d4_arytm_2,d8_arytm_2,l16_arytm_2]), [file(arytm_2,l79_arytm_2),interesting(0.45)]). fof(l51_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ~ ( ~ r1_arytm_2(B,A) & ! [C] : ( m1_subset_1(C,k2_arytm_2) => ~ ( r2_hidden(C,k6_arytm_3) & ~ r1_arytm_2(B,C) & ~ r1_arytm_2(C,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l26_arytm_2,t101_arytm_3,t1_arytm_2,l26_arytm_2,l10_arytm_2,d2_xboole_0,d5_arytm_2,t1_arytm_2,d5_arytm_2,l26_arytm_2,l10_arytm_2,d2_xboole_0,d5_arytm_2,t10_subset_1,t71_arytm_3,d3_tarski,d10_xboole_0,d3_tarski,d4_xboole_0,t1_arytm_2,l26_arytm_2,d5_arytm_2,d5_arytm_2,l10_arytm_2,d2_xboole_0,l10_arytm_2,d2_xboole_0,t7_subset_1,t1_arytm_2,d5_arytm_2,d5_arytm_2]), [file(arytm_2,l51_arytm_2),interesting(0.44)]). fof(l46_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ~ ( k5_arytm_2(A,B) = k12_arytm_3 & A != k12_arytm_3 & B != k12_arytm_3 ) ) ) ), inference(mizar_proof,[status(thm)],[t10_subset_1,t10_subset_1]), [file(arytm_2,l46_arytm_2),interesting(0.39)]). fof(l67_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [C] : ( m2_subset_1(C,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => k6_arytm_2(A,k5_arytm_2(B,C)) = k5_arytm_2(k6_arytm_2(A,B),k6_arytm_2(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t63_arytm_3,d10_xboole_0,d3_tarski,t90_arytm_3,t87_arytm_3,l28_arytm_2,t63_arytm_3,t90_arytm_3,t87_arytm_3,l28_arytm_2,t63_arytm_3]), [file(arytm_2,l67_arytm_2),interesting(0.37)]). fof(l58_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ~ ( A != k12_arytm_3 & r1_tarski(A,B) & A != B & ! [C] : ( m2_subset_1(C,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => k5_arytm_2(A,C) != B ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,t7_subset_1,t92_arytm_3,d3_tarski,d12_arytm_3,t85_arytm_3,t85_arytm_3,t74_arytm_3,d12_arytm_3,t57_arytm_3,t69_arytm_3,t85_arytm_3,l28_arytm_2,l18_arytm_2,d12_arytm_3,t57_arytm_3,t85_arytm_3,t75_arytm_3,t64_zfmisc_1,t49_subset_1,t85_arytm_3,l28_arytm_2,t64_zfmisc_1,d3_tarski,t92_arytm_3,l18_arytm_2,l28_arytm_2,t92_arytm_3,t92_arytm_3,d12_arytm_3,t92_arytm_3,t103_arytm_3,l28_arytm_2,t10_subset_1,t54_arytm_3,l29_arytm_2,s2_arytm_3,l54_arytm_2,l55_arytm_2,t63_arytm_3,t59_arytm_3,l28_arytm_2,t83_arytm_3,d12_arytm_3,t57_arytm_3,t69_arytm_3,d10_xboole_0,d3_tarski,l28_arytm_2,t83_arytm_3,l28_arytm_2]), [file(arytm_2,l58_arytm_2),interesting(0.37)]). fof(l30_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ~ ( r2_hidden(B,k4_xboole_0(k1_arytm_2,a_0_1_arytm_2)) & ~ r2_hidden(A,B) & B != k12_arytm_3 & ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( ~ r2_hidden(C,B) & ~ r3_arytm_3(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_xboole_0,l29_arytm_2,d3_tarski,d4_xboole_0,l28_arytm_2,d10_xboole_0,d3_tarski,d4_xboole_0]), [file(arytm_2,l30_arytm_2),interesting(0.30)]). fof(t22_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ~ ( r2_hidden(A,k6_arytm_3) & r2_hidden(B,k6_arytm_3) & ! [C] : ( m1_subset_1(C,k6_arytm_3) => ! [D] : ( m1_subset_1(D,k6_arytm_3) => ~ ( A = C & B = D & k8_arytm_2(A,B) = k11_arytm_3(C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_arytm_2,t54_arytm_3,t4_arytm_2,t54_arytm_3,d3_arytm_2,d3_arytm_2,t62_arytm_3,t90_arytm_3,t75_arytm_3,t90_arytm_3,t76_arytm_3,t87_arytm_3,t75_arytm_3,t101_arytm_3,t90_arytm_3,t87_arytm_3,t62_arytm_3,t75_arytm_3,d4_arytm_2,l16_arytm_2]), [file(arytm_2,t22_arytm_2),interesting(0.26)]). fof(l63_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [C] : ( m2_subset_1(C,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => r1_tarski(k6_arytm_2(A,k6_arytm_2(B,C)),k6_arytm_2(k6_arytm_2(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t58_arytm_3]), [file(arytm_2,l63_arytm_2),interesting(0.14)]). fof(t64_zfmisc_1,theorem,( ! [A,B,C] : ( r2_hidden(A,k4_xboole_0(B,k1_tarski(C))) <=> ( r2_hidden(A,B) & A != C ) ) ), file(zfmisc_1,t64_zfmisc_1), [interesting(0.00)]). fof(t49_subset_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ( ! [C] : ( m1_subset_1(C,A) => r2_hidden(C,B) ) => A = B ) ) ), file(subset_1,t49_subset_1), [interesting(0.00)]). fof(l69_arytm_2,theorem,( r2_hidden(k13_arytm_3,k6_arytm_3) ), file(arytm_2,l69_arytm_2), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(t71_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => r3_arytm_3(k12_arytm_3,A) ) ), file(arytm_3,t71_arytm_3), [interesting(0.00)]). fof(t75_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ( ~ r3_arytm_3(B,A) <=> ( r3_arytm_3(A,B) & A != B ) ) ) ) ), file(arytm_3,t75_arytm_3), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(t99_arytm_3,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m1_subset_1(A,k1_zfmisc_1(k6_arytm_3)) ) => ~ ( r2_hidden(A,k6_arytm_3) & ! [B] : ( m1_subset_1(B,k6_arytm_3) => ~ ( r2_hidden(B,A) & ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( r2_hidden(C,A) => r3_arytm_3(C,B) ) ) ) ) ) ) ), file(arytm_3,t99_arytm_3), [interesting(0.00)]). fof(t101_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ~ ( ~ r3_arytm_3(B,A) & ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( ~ r3_arytm_3(C,A) & ~ r3_arytm_3(B,C) ) ) ) ) ) ), file(arytm_3,t101_arytm_3), [interesting(0.00)]). fof(t86_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_xboole_0(A,C) ) => r1_tarski(A,k4_xboole_0(B,C)) ) ), file(xboole_1,t86_xboole_1), [interesting(0.00)]). fof(d21_ordinal2,definition,( ! [A] : ( v4_ordinal2(A) <=> r2_hidden(A,k5_ordinal2) ) ), file(ordinal2,d21_ordinal2), [interesting(0.00)]). fof(d4_arytm_2,definition,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( ( ? [C] : ( m1_subset_1(C,k6_arytm_3) & ! [D] : ( m1_subset_1(D,k6_arytm_3) => ( r2_hidden(D,A) <=> ~ r3_arytm_3(C,D) ) ) ) => ( B = k4_arytm_2(A) <=> ? [C] : ( m1_subset_1(C,k6_arytm_3) & B = C & ! [D] : ( m1_subset_1(D,k6_arytm_3) => ( r2_hidden(D,A) <=> ~ r3_arytm_3(C,D) ) ) ) ) ) & ( ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ! [D] : ( m1_subset_1(D,k6_arytm_3) => ( r2_hidden(D,A) <=> ~ r3_arytm_3(C,D) ) ) ) => ( B = k4_arytm_2(A) <=> B = A ) ) ) ) ) ), file(arytm_2,d4_arytm_2), [interesting(0.00)]). fof(d3_arytm_2,definition,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ( ( r2_hidden(A,k6_arytm_3) => ( B = k3_arytm_2(A) <=> ? [C] : ( m1_subset_1(C,k6_arytm_3) & A = C & B = a_1_0_arytm_2(C) ) ) ) & ( ~ r2_hidden(A,k6_arytm_3) => ( B = k3_arytm_2(A) <=> B = A ) ) ) ) ) ), file(arytm_2,d3_arytm_2), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(t10_subset_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ~ ( B != k1_xboole_0 & ! [C] : ( m1_subset_1(C,A) => ~ r2_hidden(C,B) ) ) ) ), file(subset_1,t10_subset_1), [interesting(0.00)]). fof(d1_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(t2_xboole_1,theorem,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t58_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => k11_arytm_3(k11_arytm_3(A,B),C) = k11_arytm_3(A,k11_arytm_3(B,C)) ) ) ) ), file(arytm_3,t58_arytm_3), [interesting(0.00)]). fof(l64_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [C] : ( m2_subset_1(C,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => k6_arytm_2(A,k6_arytm_2(B,C)) = k6_arytm_2(k6_arytm_2(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[l63_arytm_2,d10_xboole_0]), [file(arytm_2,l64_arytm_2),interesting(0.00)]). fof(d8_arytm_2,definition,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( ( B = k12_arytm_3 => k7_arytm_2(A,B) = A ) & ( A = k12_arytm_3 => k7_arytm_2(A,B) = B ) & ~ ( B != k12_arytm_3 & A != k12_arytm_3 & k7_arytm_2(A,B) != k4_arytm_2(k5_arytm_2(k3_arytm_2(A),k3_arytm_2(B))) ) ) ) ) ), file(arytm_2,d8_arytm_2), [interesting(0.00)]). fof(t63_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => k11_arytm_3(A,k10_arytm_3(B,C)) = k10_arytm_3(k11_arytm_3(A,B),k11_arytm_3(A,C)) ) ) ) ), file(arytm_3,t63_arytm_3), [interesting(0.00)]). fof(t90_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( r3_arytm_3(A,B) => r3_arytm_3(k11_arytm_3(A,C),k11_arytm_3(B,C)) ) ) ) ) ), file(arytm_3,t90_arytm_3), [interesting(0.00)]). fof(t87_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( r3_arytm_3(A,k11_arytm_3(B,C)) & ! [D] : ( m1_subset_1(D,k6_arytm_3) => ~ ( A = k11_arytm_3(B,D) & r3_arytm_3(D,C) ) ) ) ) ) ) ), file(arytm_3,t87_arytm_3), [interesting(0.00)]). fof(t60_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ~ ( A != k12_arytm_3 & ! [B] : ( m1_subset_1(B,k6_arytm_3) => k11_arytm_3(A,B) != k13_arytm_3 ) ) ) ), file(arytm_3,t60_arytm_3), [interesting(0.00)]). fof(t76_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( ( ( ~ r3_arytm_3(B,A) & r3_arytm_3(B,C) ) | ( r3_arytm_3(A,B) & ~ r3_arytm_3(C,B) ) ) & r3_arytm_3(C,A) ) ) ) ) ), file(arytm_3,t76_arytm_3), [interesting(0.00)]). fof(t62_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( k11_arytm_3(A,B) = k11_arytm_3(A,C) => ( A = k12_arytm_3 | B = C ) ) ) ) ) ), file(arytm_3,t62_arytm_3), [interesting(0.00)]). fof(t54_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => k11_arytm_3(A,k12_arytm_3) = k12_arytm_3 ) ), file(arytm_3,t54_arytm_3), [interesting(0.00)]). fof(l50_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( ( r2_hidden(C,a_0_0_arytm_2) & r2_hidden(A,C) & r3_arytm_3(B,A) ) => r2_hidden(B,C) ) ) ) ), file(arytm_2,l50_arytm_2), [interesting(0.00)]). fof(t74_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( ( r3_arytm_3(A,B) & r3_arytm_3(B,C) ) => r3_arytm_3(A,C) ) ) ) ) ), file(arytm_3,t74_arytm_3), [interesting(0.00)]). fof(t61_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ~ ( A != k12_arytm_3 & ! [C] : ( m1_subset_1(C,k6_arytm_3) => B != k11_arytm_3(A,C) ) ) ) ) ), file(arytm_3,t61_arytm_3), [interesting(0.00)]). fof(t88_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( r3_arytm_3(k11_arytm_3(B,A),k11_arytm_3(C,A)) => ( A = k12_arytm_3 | r3_arytm_3(B,C) ) ) ) ) ) ), file(arytm_3,t88_arytm_3), [interesting(0.00)]). fof(t73_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ( ( r3_arytm_3(A,B) & r3_arytm_3(B,A) ) => A = B ) ) ) ), file(arytm_3,t73_arytm_3), [interesting(0.00)]). fof(t82_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(k6_arytm_3)) => ~ ( ? [B] : ( m1_subset_1(B,k6_arytm_3) & r2_hidden(B,A) & B != k12_arytm_3 ) & ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( ( r2_hidden(B,A) & r3_arytm_3(C,B) ) => r2_hidden(C,A) ) ) ) & ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ! [D] : ( m1_subset_1(D,k6_arytm_3) => ~ ( r2_hidden(B,A) & r2_hidden(C,A) & r2_hidden(D,A) & B != C & C != D & D != B ) ) ) ) ) ) ), file(arytm_3,t82_arytm_3), [interesting(0.00)]). fof(d12_arytm_3,definition,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ( r3_arytm_3(A,B) <=> ? [C] : ( m1_subset_1(C,k6_arytm_3) & B = k10_arytm_3(A,C) ) ) ) ) ), file(arytm_3,d12_arytm_3), [interesting(0.00)]). fof(t56_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => k10_arytm_3(A,k12_arytm_3) = A ) ), file(arytm_3,t56_arytm_3), [interesting(0.00)]). fof(t86_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ~ ( k11_arytm_3(A,B) = k12_arytm_3 & A != k12_arytm_3 & B != k12_arytm_3 ) ) ) ), file(arytm_3,t86_arytm_3), [interesting(0.00)]). fof(t103_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ~ ( A != k12_arytm_3 & ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( r2_hidden(C,k5_ordinal2) & r3_arytm_3(B,k11_arytm_3(C,A)) ) ) ) ) ) ), file(arytm_3,t103_arytm_3), [interesting(0.00)]). fof(s2_arytm_3,theorem, ( ( f2_s2_arytm_3 = k13_arytm_3 & f1_s2_arytm_3 = k12_arytm_3 & r2_hidden(f3_s2_arytm_3,k5_ordinal2) & p1_s2_arytm_3(f1_s2_arytm_3) & ~ p1_s2_arytm_3(f3_s2_arytm_3) ) => ? [A] : ( m1_subset_1(A,k6_arytm_3) & r2_hidden(A,k5_ordinal2) & p1_s2_arytm_3(A) & ~ p1_s2_arytm_3(k10_arytm_3(A,f2_s2_arytm_3)) ) ), file(arytm_3,s2_arytm_3), [interesting(0.00)]). fof(l54_arytm_2,theorem,( k13_arytm_3 = k13_arytm_3 ), file(arytm_2,l54_arytm_2), [interesting(0.00)]). fof(l55_arytm_2,theorem,( k12_arytm_3 = k12_arytm_3 ), file(arytm_2,l55_arytm_2), [interesting(0.00)]). fof(t59_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => k11_arytm_3(A,k13_arytm_3) = A ) ), file(arytm_3,t59_arytm_3), [interesting(0.00)]). fof(t83_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( r3_arytm_3(k10_arytm_3(A,B),k10_arytm_3(C,B)) <=> r3_arytm_3(A,C) ) ) ) ) ), file(arytm_3,t83_arytm_3), [interesting(0.00)]). fof(d5_arytm_2,definition,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( ( ( r2_hidden(A,k6_arytm_3) & r2_hidden(B,k6_arytm_3) ) => ( r1_arytm_2(A,B) <=> ? [C] : ( m1_subset_1(C,k6_arytm_3) & ? [D] : ( m1_subset_1(D,k6_arytm_3) & A = C & B = D & r3_arytm_3(C,D) ) ) ) ) & ( r2_hidden(A,k6_arytm_3) => ( r2_hidden(B,k6_arytm_3) | ( r1_arytm_2(A,B) <=> r2_hidden(A,B) ) ) ) & ( r2_hidden(B,k6_arytm_3) => ( r2_hidden(A,k6_arytm_3) | ( r1_arytm_2(A,B) <=> ~ r2_hidden(B,A) ) ) ) & ~ ( ~ ( r2_hidden(A,k6_arytm_3) & r2_hidden(B,k6_arytm_3) ) & ~ ( r2_hidden(A,k6_arytm_3) & ~ r2_hidden(B,k6_arytm_3) ) & ~ ( ~ r2_hidden(A,k6_arytm_3) & r2_hidden(B,k6_arytm_3) ) & ~ ( r1_arytm_2(A,B) <=> r1_tarski(A,B) ) ) ) ) ) ), file(arytm_2,d5_arytm_2), [interesting(0.00)]). fof(t3_xboole_1,theorem,( ! [A] : ( r1_tarski(A,k1_xboole_0) => A = k1_xboole_0 ) ), file(xboole_1,t3_xboole_1), [interesting(0.00)]). fof(t7_subset_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ( ! [D] : ( m1_subset_1(D,A) => ( r2_hidden(D,B) => r2_hidden(D,C) ) ) => r1_tarski(B,C) ) ) ) ), file(subset_1,t7_subset_1), [interesting(0.00)]). fof(t91_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ! [D] : ( m1_subset_1(D,k6_arytm_3) => ~ ( k11_arytm_3(A,B) = k11_arytm_3(C,D) & ~ r3_arytm_3(A,C) & ~ r3_arytm_3(B,D) ) ) ) ) ) ), file(arytm_3,t91_arytm_3), [interesting(0.00)]). fof(t98_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( ~ r3_arytm_3(k10_arytm_3(B,C),A) & C != k12_arytm_3 & ! [D] : ( m1_subset_1(D,k6_arytm_3) => ! [E] : ( m1_subset_1(E,k6_arytm_3) => ~ ( A = k10_arytm_3(D,E) & r3_arytm_3(D,B) & r3_arytm_3(E,C) & E != C ) ) ) ) ) ) ) ), file(arytm_3,t98_arytm_3), [interesting(0.00)]). fof(l78_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ~ ( ~ r3_arytm_3(k10_arytm_3(B,C),A) & B != k12_arytm_3 & C != k12_arytm_3 & ! [D] : ( m1_subset_1(D,k6_arytm_3) => ! [E] : ( m1_subset_1(E,k6_arytm_3) => ~ ( A = k10_arytm_3(D,E) & ~ r3_arytm_3(B,D) & ~ r3_arytm_3(C,E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t98_arytm_3,t71_arytm_3,t75_arytm_3,t75_arytm_3,t75_arytm_3,t101_arytm_3,t83_arytm_3,t98_arytm_3,t75_arytm_3,t76_arytm_3,t76_arytm_3]), [file(arytm_2,l78_arytm_2),interesting(0.00)]). fof(t34_arytm_3,theorem,( r1_tarski(k5_ordinal2,k6_arytm_3) ), file(arytm_3,t34_arytm_3), [interesting(0.00)]). fof(d8_arytm_3,definition,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k5_ordinal2) => ( ( r2_hidden(A,k5_ordinal2) => ( B = k8_arytm_3(A) <=> B = k4_ordinal2 ) ) & ( ~ r2_hidden(A,k5_ordinal2) => ( B = k8_arytm_3(A) <=> ? [C] : ( v3_ordinal1(C) & v4_ordinal2(C) & A = k4_tarski(C,B) ) ) ) ) ) ) ), file(arytm_3,d8_arytm_3), [interesting(0.00)]). fof(t56_ordinal2,theorem,( ! [A] : ( v3_ordinal1(A) => ( k15_ordinal2(k4_ordinal2,A) = A & k15_ordinal2(A,k4_ordinal2) = A ) ) ), file(ordinal2,t56_ordinal2), [interesting(0.00)]). fof(d7_arytm_3,definition,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k5_ordinal2) => ( ( r2_hidden(A,k5_ordinal2) => ( B = k7_arytm_3(A) <=> B = A ) ) & ( ~ r2_hidden(A,k5_ordinal2) => ( B = k7_arytm_3(A) <=> ? [C] : ( v3_ordinal1(C) & v4_ordinal2(C) & A = k4_tarski(B,C) ) ) ) ) ) ) ), file(arytm_3,d7_arytm_3), [interesting(0.00)]). fof(t29_arytm_3,theorem,( ! [A] : ( ( v3_ordinal1(A) & v4_ordinal2(A) ) => ( k5_arytm_3(A,k4_ordinal2) = A & k5_arytm_3(k4_ordinal2,A) = k4_ordinal2 ) ) ), file(arytm_3,t29_arytm_3), [interesting(0.00)]). fof(d9_arytm_3,definition,( ! [A] : ( ( v3_ordinal1(A) & v4_ordinal2(A) ) => ! [B] : ( ( v3_ordinal1(B) & v4_ordinal2(B) ) => ( ( B = k1_xboole_0 => k9_arytm_3(A,B) = k1_xboole_0 ) & ( k5_arytm_3(B,A) = k4_ordinal2 => k9_arytm_3(A,B) = k5_arytm_3(A,B) ) & ~ ( B != k1_xboole_0 & k5_arytm_3(B,A) != k4_ordinal2 & k9_arytm_3(A,B) != k4_tarski(k5_arytm_3(A,B),k5_arytm_3(B,A)) ) ) ) ) ), file(arytm_3,d9_arytm_3), [interesting(0.00)]). fof(d10_arytm_3,definition,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => k10_arytm_3(A,B) = k9_arytm_3(k1_arytm_3(k2_arytm_3(k7_arytm_3(A),k8_arytm_3(B)),k2_arytm_3(k7_arytm_3(B),k8_arytm_3(A))),k2_arytm_3(k8_arytm_3(A),k8_arytm_3(B))) ) ) ), file(arytm_3,d10_arytm_3), [interesting(0.00)]). fof(t48_ordinal2,theorem,( ! [A] : ( v3_ordinal1(A) => k14_ordinal2(A,k4_ordinal2) = k1_ordinal1(A) ) ), file(ordinal2,t48_ordinal2), [interesting(0.00)]). fof(s1_arytm_3,theorem, ( ( p1_s1_arytm_3(k1_xboole_0) & ! [A] : ( ( v3_ordinal1(A) & v4_ordinal2(A) ) => ( p1_s1_arytm_3(A) => p1_s1_arytm_3(k1_ordinal1(A)) ) ) ) => ! [A] : ( ( v3_ordinal1(A) & v4_ordinal2(A) ) => p1_s1_arytm_3(A) ) ), file(arytm_3,s1_arytm_3), [interesting(0.00)]). fof(t23_ordinal1,theorem,( ! [A,B] : ( v3_ordinal1(B) => ( r2_hidden(A,B) => v3_ordinal1(A) ) ) ), file(ordinal1,t23_ordinal1), [interesting(0.00)]). fof(t18_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(k2_arytm_2)) => ( ( r2_hidden(k12_arytm_3,A) & ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( ( r2_hidden(B,A) & C = k13_arytm_3 ) => r2_hidden(k7_arytm_2(B,C),A) ) ) ) ) => r1_tarski(k5_ordinal2,A) ) ) ), inference(mizar_proof,[status(thm)],[t1_arytm_2,d21_ordinal2,t34_arytm_3,t1_arytm_2,l79_arytm_2,t34_arytm_3,d21_ordinal2,l76_arytm_2,t48_ordinal2,s1_arytm_3,d3_tarski,t23_ordinal1,d21_ordinal2]), [file(arytm_2,t18_arytm_2),interesting(0.00)]). fof(d2_ordinal1,definition,( ! [A] : ( v1_ordinal1(A) <=> ! [B] : ( r2_hidden(B,A) => r1_tarski(B,A) ) ) ), file(ordinal1,d2_ordinal1), [interesting(0.00)]). fof(t30_ordinal3,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ~ ( r1_ordinal1(A,B) & ! [C] : ( v3_ordinal1(C) => B != k14_ordinal2(A,C) ) ) ) ) ), file(ordinal3,t30_ordinal3), [interesting(0.00)]). fof(t27_ordinal3,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ( r1_ordinal1(A,k14_ordinal2(A,B)) & r1_ordinal1(B,k14_ordinal2(A,B)) ) ) ) ), file(ordinal3,t27_ordinal3), [interesting(0.00)]). fof(t22_ordinal1,theorem,( ! [A] : ( v1_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ! [C] : ( v3_ordinal1(C) => ( ( r1_tarski(A,B) & r2_hidden(B,C) ) => r2_hidden(A,C) ) ) ) ) ), file(ordinal1,t22_ordinal1), [interesting(0.00)]). fof(t78_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ( ( r2_hidden(A,k5_ordinal2) & r2_hidden(k10_arytm_3(A,B),k5_ordinal2) ) => r2_hidden(B,k5_ordinal2) ) ) ) ), file(arytm_3,t78_arytm_3), [interesting(0.00)]). fof(d8_xboole_0,definition,( ! [A,B] : ( r2_xboole_0(A,B) <=> ( r1_tarski(A,B) & A != B ) ) ), file(xboole_0,d8_xboole_0), [interesting(0.00)]). fof(t21_ordinal1,theorem,( ! [A] : ( v1_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ( r2_xboole_0(A,B) => r2_hidden(A,B) ) ) ) ), file(ordinal1,t21_ordinal1), [interesting(0.00)]). fof(t92_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ( A = k12_arytm_3 <=> k10_arytm_3(A,B) = B ) ) ) ), file(arytm_3,t92_arytm_3), [interesting(0.00)]). fof(t85_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => r3_arytm_3(A,k10_arytm_3(A,B)) ) ) ), file(arytm_3,t85_arytm_3), [interesting(0.00)]). fof(t57_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => k10_arytm_3(k10_arytm_3(A,B),C) = k10_arytm_3(A,k10_arytm_3(B,C)) ) ) ) ), file(arytm_3,t57_arytm_3), [interesting(0.00)]). fof(t69_arytm_3,theorem,( ! [A] : ( m1_subset_1(A,k6_arytm_3) => ! [B] : ( m1_subset_1(B,k6_arytm_3) => ! [C] : ( m1_subset_1(C,k6_arytm_3) => ( k10_arytm_3(A,B) = k10_arytm_3(C,B) => A = C ) ) ) ) ), file(arytm_3,t69_arytm_3), [interesting(0.00)]). fof(d6_arytm_2,definition,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => k5_arytm_2(A,B) = a_2_0_arytm_2(A,B) ) ) ), file(arytm_2,d6_arytm_2), [interesting(0.00)]). fof(l44_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [C] : ( m2_subset_1(C,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => r1_tarski(k5_arytm_2(A,k5_arytm_2(B,C)),k5_arytm_2(k5_arytm_2(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t57_arytm_3]), [file(arytm_2,l44_arytm_2),interesting(0.00)]). fof(l45_arytm_2,theorem,( ! [A] : ( m2_subset_1(A,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [B] : ( m2_subset_1(B,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => ! [C] : ( m2_subset_1(C,k1_zfmisc_1(k6_arytm_3),k1_arytm_2) => k5_arytm_2(A,k5_arytm_2(B,C)) = k5_arytm_2(k5_arytm_2(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[l44_arytm_2,d10_xboole_0]), [file(arytm_2,l45_arytm_2),interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t68_arytm_3,theorem,( ! [A] : ~ r2_hidden(k4_tarski(k12_arytm_3,A),k6_arytm_3) ), file(arytm_3,t68_arytm_3), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(t36_xboole_1,theorem,( ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ), file(xboole_1,t36_xboole_1), [interesting(0.00)]). fof(t9_xboole_1,theorem,( ! [A,B,C] : ( r1_tarski(A,B) => r1_tarski(k2_xboole_0(A,C),k2_xboole_0(B,C)) ) ), file(xboole_1,t9_xboole_1), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(t5_arytm_2,theorem,( $true ), file(arytm_2,t5_arytm_2), [interesting(0.00)]). fof(d9_ordinal1,definition,( ! [A] : ( v6_ordinal1(A) <=> ! [B,C] : ( ( r2_hidden(B,A) & r2_hidden(C,A) ) => r3_xboole_0(B,C) ) ) ), file(ordinal1,d9_ordinal1), [interesting(0.00)]). fof(d9_xboole_0,definition,( ! [A,B] : ( r3_xboole_0(A,B) <=> ( r1_tarski(A,B) | r1_tarski(B,A) ) ) ), file(xboole_0,d9_xboole_0), [interesting(0.00)]). fof(t87_xboole_1,theorem,( ! [A,B,C] : ( r1_xboole_0(A,B) => k2_xboole_0(k4_xboole_0(C,A),B) = k4_xboole_0(k2_xboole_0(C,B),A) ) ), file(xboole_1,t87_xboole_1), [interesting(0.00)]). fof(t9_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(k2_arytm_2)) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k2_arytm_2)) => ~ ( ? [C] : ( m1_subset_1(C,k2_arytm_2) & r2_hidden(C,A) ) & ? [C] : ( m1_subset_1(C,k2_arytm_2) & r2_hidden(C,B) ) & ! [C] : ( m1_subset_1(C,k2_arytm_2) => ! [D] : ( m1_subset_1(D,k2_arytm_2) => ( ( r2_hidden(C,A) & r2_hidden(D,B) ) => r1_arytm_2(C,D) ) ) ) & ! [C] : ( m1_subset_1(C,k2_arytm_2) => ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & r2_hidden(D,A) & r2_hidden(E,B) & ~ ( r1_arytm_2(D,C) & r1_arytm_2(C,E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_arytm_2,l51_arytm_2,l26_arytm_2,l51_arytm_2,l26_arytm_2,l52_arytm_2,t71_arytm_3,d3_tarski,t1_arytm_2,t1_arytm_2,l26_arytm_2,l52_arytm_2,l51_arytm_2,l26_arytm_2,l10_arytm_2,d2_xboole_0,l49_arytm_2,t49_subset_1,t1_arytm_2,d5_arytm_2,l52_arytm_2,t64_zfmisc_1,d4_xboole_0,l12_arytm_2,l20_arytm_2,d3_xboole_0,d1_tarski,l51_arytm_2,d5_arytm_2,l51_arytm_2,d5_arytm_2,l52_arytm_2]), [file(arytm_2,t9_arytm_2),interesting(0.00)]).