fof(t40_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & F != G & r1_analort(A,B,C,D,E,F,G) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d3_analort,t22_rlvect_1,l4_analort,t15_analort,t15_analort,t25_analoaf,t16_analort,t21_analoaf,t21_analoaf,d3_analort,t18_analort,d6_rlvect_1,t22_rlvect_1,t35_rlvect_1]), [file(analort,t40_analort),interesting(1.00)]). fof(t51_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r1_analort(A,B,C,D,E,D,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( r1_analort(A,B,C,G,H,D,E) & ~ ( ~ r1_analort(A,B,C,G,H,D,F) & ~ r1_analort(A,B,C,G,H,F,D) ) & G != H ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l4_analort,t40_analort,t13_analort,d3_analort,d3_analort,t13_analort,d3_analort,t20_analoaf,t16_analort,t20_analoaf,t18_analmetr,t11_analort,l5_analort,l2_analort,l2_analort,l3_analort,t6_xcmplx_1,l5_analort,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t35_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,l2_analort,l3_analort,d7_xcmplx_0,d7_xcmplx_0,t65_xreal_1,l2_analort,l2_analort,l3_analort,t6_xcmplx_1,l5_analort,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t35_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,l2_analort,l3_analort,d7_xcmplx_0,d7_xcmplx_0,t65_xreal_1]), [file(analort,t51_analort),interesting(1.00)]). fof(t41_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & F != G & r2_analort(A,B,C,D,E,F,G) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d4_analort,t19_analort,t22_rlvect_1,l4_analort,t8_analort,t8_analort,t25_analoaf,t21_analoaf,t17_analort,d4_analort,t19_analort,d6_rlvect_1,t22_rlvect_1,t35_rlvect_1]), [file(analort,t41_analort),interesting(0.90)]). fof(t38_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & F != G & r1_analort(A,B,C,F,G,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d3_analort,t22_rlvect_1,l4_analort,t15_analort,t15_analort,t25_analoaf,t21_analoaf,t16_analort,d3_analort,d6_rlvect_1,t22_rlvect_1,t35_rlvect_1]), [file(analort,t38_analort),interesting(0.84)]). fof(t50_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( ~ r1_analort(A,B,C,D,G,E,F) & ~ r1_analort(A,B,C,D,G,F,E) & r1_analort(A,B,C,F,H,F,E) & ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ~ ( ( r1_analort(A,B,C,D,G,D,I) | r1_analort(A,B,C,D,G,I,D) ) & ( r1_analort(A,B,C,F,H,F,I) | r1_analort(A,B,C,F,H,I,F) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t40_analort,d3_analort,t21_analoaf,t18_analoaf,t20_analoaf,d1_analmetr,t31_analoaf,t20_analoaf,d3_analort,t20_analoaf,d3_analort]), [file(analort,t50_analort),interesting(0.83)]). fof(t39_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & F != G & r2_analort(A,B,C,F,G,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d4_analort,t22_rlvect_1,l4_analort,t8_analort,t8_analort,t25_analoaf,t21_analoaf,t17_analort,d4_analort,d6_rlvect_1,t22_rlvect_1,t35_rlvect_1]), [file(analort,t39_analort),interesting(0.82)]). fof(t18_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & r1_analort(A,B,C,D,E,F,G) ) => r1_analort(A,B,C,F,G,E,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analort,t21_analoaf,t16_analort,t14_analort,t14_analort,t21_analoaf,t30_rlvect_1,t24_analoaf,t20_analoaf,d3_analort,t30_rlvect_1,t30_rlvect_1,t18_analoaf,d3_analort]), [file(analort,t18_analort),interesting(0.82)]). fof(t24_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => r3_analmetr(A,D,E,k3_analort(A,B,C,D),k3_analort(A,B,C,E),B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_analort,d6_geomtrap,l6_analort,l6_analort,t34_geomtrap,d3_analmetr]), [file(analort,t24_analort),interesting(0.81)]). fof(t15_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k3_analort(A,B,C,E) != D ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_analort,t14_analort,t30_rlvect_1]), [file(analort,t15_analort),interesting(0.79)]). fof(t29_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ( r3_analmetr(A,D,E,F,G,B,C) <=> ( r1_analort(A,B,C,D,E,F,G) | r1_analort(A,B,C,D,E,G,F) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t9_analmetr,d3_analmetr,t35_rlvect_1,t24_analort,d3_analmetr,d3_analmetr,t13_analmetr,t18_analmetr,d3_analort,d3_analort,t18_analmetr,t23_rlvect_1,t24_rlvect_1,t35_rlvect_1,t13_analort,t28_rlvect_1,t9_analmetr,d3_analmetr,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,t11_analmetr,d3_analmetr,t20_analort]), [file(analort,t29_analort),interesting(0.79)]). fof(t3_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k2_analort(A,B,C,k1_rlvect_1(A)) = k1_rlvect_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_rlvect_1,t2_analort,t23_rlvect_1]), [file(analort,t3_analort),interesting(0.75)]). fof(t9_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k3_analort(A,B,C,k5_rlvect_1(A,D)) = k5_rlvect_1(A,k3_analort(A,B,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l5_analort,t45_rlvect_1,t39_rlvect_1,t38_rlvect_1,t39_rlvect_1,t38_rlvect_1,l6_analort,l6_analort,t38_rlvect_1,t39_rlvect_1,t38_rlvect_1,t39_rlvect_1,t45_rlvect_1]), [file(analort,t9_analort),interesting(0.72)]). fof(t4_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k2_analort(A,B,C,k5_rlvect_1(A,D)) = k5_rlvect_1(A,k2_analort(A,B,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l5_analort,t45_rlvect_1,t39_rlvect_1,t38_rlvect_1,t39_rlvect_1,t38_rlvect_1,l6_analort,l6_analort,t38_rlvect_1,t39_rlvect_1,t38_rlvect_1,t39_rlvect_1,t45_rlvect_1]), [file(analort,t4_analort),interesting(0.72)]). fof(t10_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k3_analort(A,B,C,k1_analort(A,D,E)) = k1_analort(A,k3_analort(A,B,C,D),k3_analort(A,B,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_analort,l7_analort,d9_rlvect_1,t38_rlvect_1,t39_rlvect_1,d9_rlvect_1,t45_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,t39_rlvect_1,t39_rlvect_1,t38_rlvect_1,t38_rlvect_1]), [file(analort,t10_analort),interesting(0.69)]). fof(t1_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k2_analort(A,B,C,k1_analort(A,D,E)) = k1_analort(A,k2_analort(A,B,C,D),k2_analort(A,B,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_analort,l7_analort,d9_rlvect_1,t38_rlvect_1,t39_rlvect_1,d9_rlvect_1,t45_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,t39_rlvect_1,t39_rlvect_1,t38_rlvect_1,t38_rlvect_1]), [file(analort,t1_analort),interesting(0.68)]). fof(t14_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k3_analort(A,B,C,k3_analort(A,B,C,D)) = k5_rlvect_1(A,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_geomtrap,d4_geomtrap,t38_rlvect_1,t39_rlvect_1,t38_rlvect_1,t39_rlvect_1,t45_rlvect_1,l5_analort]), [file(analort,t14_analort),interesting(0.66)]). fof(t11_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k3_analort(A,B,C,k6_rlvect_1(A,D,E)) = k6_rlvect_1(A,k3_analort(A,B,C,D),k3_analort(A,B,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_analort,t9_analort]), [file(analort,t11_analort),interesting(0.65)]). fof(t53_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r2_analort(A,B,C,D,E,D,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( r2_analort(A,B,C,G,H,D,E) & ~ ( ~ r2_analort(A,B,C,G,H,D,F) & ~ r2_analort(A,B,C,G,H,F,D) ) & G != H ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l6_analort,t17_analoaf,d4_analort,t6_analort,d4_analort,t20_analoaf,t18_analmetr,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t26_rlvect_1,t26_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,l2_analort,l2_analort,l3_analort,d7_xcmplx_0,d7_xcmplx_0,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,l2_analort,l2_analort,l3_analort,d7_xcmplx_0,d7_xcmplx_0,d4_analort]), [file(analort,t53_analort),interesting(0.64)]). fof(t27_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ( r1_analoaf(A,D,E,F,G) <=> ? [H] : ( m1_subset_1(H,u1_struct_0(A)) & ? [I] : ( m1_subset_1(I,u1_struct_0(A)) & H != I & r1_analort(A,B,C,H,I,D,E) & r1_analort(A,B,C,H,I,F,G) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d3_analort,l4_analort,t15_analort,t15_analort,t17_analoaf,d3_analort,d3_analort,t15_analort,t15_analort,t17_analoaf,d3_analort,t21_analoaf,d3_analort,t13_analort,d3_analort,t20_analoaf]), [file(analort,t27_analort),interesting(0.61)]). fof(t2_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( r1_analmetr(A,B,C) => k2_analort(A,B,C,k3_rlvect_1(A,D,E)) = k3_rlvect_1(A,k2_analort(A,B,C,D),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_analort,l7_analort,t38_rlvect_1,t39_rlvect_1,d9_rlvect_1,t39_rlvect_1,d9_rlvect_1,d9_rlvect_1,t39_rlvect_1,t38_rlvect_1]), [file(analort,t2_analort),interesting(0.61)]). fof(t5_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k2_analort(A,B,C,k6_rlvect_1(A,D,E)) = k6_rlvect_1(A,k2_analort(A,B,C,D),k2_analort(A,B,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_analort,t4_analort]), [file(analort,t5_analort),interesting(0.57)]). fof(t28_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ( r1_analoaf(A,D,E,F,G) <=> ? [H] : ( m1_subset_1(H,u1_struct_0(A)) & ? [I] : ( m1_subset_1(I,u1_struct_0(A)) & H != I & r2_analort(A,B,C,H,I,D,E) & r2_analort(A,B,C,H,I,F,G) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d4_analort,l4_analort,t8_analort,t8_analort,t17_analoaf,d4_analort,d4_analort,t8_analort,t8_analort,t17_analoaf,d4_analort,t21_analoaf,d4_analort,t6_analort,d4_analort,t20_analoaf]), [file(analort,t28_analort),interesting(0.56)]). fof(t12_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( r1_analmetr(A,B,C) => k3_analort(A,B,C,k3_rlvect_1(A,D,E)) = k3_rlvect_1(A,k3_analort(A,B,C,D),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l7_analort,l7_analort,t38_rlvect_1,t39_rlvect_1,d9_rlvect_1,t39_rlvect_1,d9_rlvect_1,d9_rlvect_1,t39_rlvect_1,t38_rlvect_1]), [file(analort,t12_analort),interesting(0.55)]). fof(l3_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( ( r1_analmetr(A,B,C) & k1_analort(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_analort(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)) ) => ( D = F & E = G ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,l1_analort,d1_analmetr]), [file(analort,l3_analort),interesting(0.53)]). fof(l6_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ( ( r1_analmetr(A,B,C) & D = k1_analort(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) ) => ( E = k2_geomtrap(A,B,C,D) & F = k3_geomtrap(A,B,C,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l5_analort,l3_analort]), [file(analort,l6_analort),interesting(0.50)]). fof(l2_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( B = k1_analort(A,k3_rlvect_1(A,C,E),k3_rlvect_1(A,D,F)) => k3_rlvect_1(A,B,G) = k1_analort(A,k3_rlvect_1(A,C,k4_real_1(G,E)),k3_rlvect_1(A,D,k4_real_1(G,F))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(analort,l2_analort),interesting(0.47)]). fof(l5_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => D = k1_analort(A,k3_rlvect_1(A,B,k2_geomtrap(A,B,C,D)),k3_rlvect_1(A,C,k3_geomtrap(A,B,C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_geomtrap,d5_geomtrap]), [file(analort,l5_analort),interesting(0.46)]). fof(t56_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(k6_analort(A,F,G))) => ! [I] : ( m1_subset_1(I,u1_struct_0(k6_analort(A,F,G))) => ! [J] : ( m1_subset_1(J,u1_struct_0(k6_analort(A,F,G))) => ! [K] : ( m1_subset_1(K,u1_struct_0(k6_analort(A,F,G))) => ( ( B = H & C = I & D = J & E = K ) => ( r2_analoaf(k6_analort(A,F,G),H,I,J,K) <=> r1_analort(A,F,G,B,C,D,E) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_analoaf,d5_analort,t33_zfmisc_1,d5_analort,d2_analoaf]), [file(analort,t56_analort),interesting(0.27)]). fof(t57_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(k7_analort(A,F,G))) => ! [I] : ( m1_subset_1(I,u1_struct_0(k7_analort(A,F,G))) => ! [J] : ( m1_subset_1(J,u1_struct_0(k7_analort(A,F,G))) => ! [K] : ( m1_subset_1(K,u1_struct_0(k7_analort(A,F,G))) => ( ( B = H & C = I & D = J & E = K ) => ( r2_analoaf(k7_analort(A,F,G),H,I,J,K) <=> r2_analort(A,F,G,B,C,D,E) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_analoaf,d6_analort,t33_zfmisc_1,d6_analort,d2_analoaf]), [file(analort,t57_analort),interesting(0.27)]). fof(l1_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( ( B = k1_analort(A,k3_rlvect_1(A,C,F),k3_rlvect_1(A,D,G)) & E = k1_analort(A,k3_rlvect_1(A,C,H),k3_rlvect_1(A,D,I)) ) => ( k1_analort(A,B,E) = k1_analort(A,k3_rlvect_1(A,C,k3_real_1(F,H)),k3_rlvect_1(A,D,k3_real_1(G,I))) & k6_rlvect_1(A,B,E) = k1_analort(A,k3_rlvect_1(A,C,k5_real_1(F,H)),k3_rlvect_1(A,D,k5_real_1(G,I))) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d6_rlvect_1,d9_rlvect_1,t45_rlvect_1,t39_rlvect_1,t39_rlvect_1,t38_rlvect_1,t38_rlvect_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d6_rlvect_1,d9_rlvect_1]), [file(analort,l1_analort),interesting(0.26)]). fof(t18_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analoaf(A,B,C,D,D) & r1_analoaf(A,B,B,C,D) ) ) ) ) ) ), file(analoaf,t18_analoaf), [interesting(0.00)]). fof(d4_analort,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r2_analort(A,B,C,D,E,F,G) <=> r1_analoaf(A,k2_analort(A,B,C,D),k2_analort(A,B,C,E),F,G) ) ) ) ) ) ) ) ) ), file(analort,d4_analort), [interesting(0.00)]). fof(t21_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => r2_analort(A,E,F,B,B,C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d4_analort]), [file(analort,t21_analort),interesting(0.00)]). fof(d3_analort,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r1_analort(A,B,C,D,E,F,G) <=> r1_analoaf(A,k3_analort(A,B,C,D),k3_analort(A,B,C,E),F,G) ) ) ) ) ) ) ) ) ), file(analort,d3_analort), [interesting(0.00)]). fof(t22_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => r1_analort(A,E,F,B,C,D,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d3_analort]), [file(analort,t22_analort),interesting(0.00)]). fof(t23_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => r2_analort(A,E,F,B,C,D,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d4_analort]), [file(analort,t23_analort),interesting(0.00)]). fof(t17_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_analoaf(A,B,C,B,C) ) ) ) ), file(analoaf,t17_analoaf), [interesting(0.00)]). fof(t25_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => r1_analort(A,D,E,B,C,k3_analort(A,D,E,B),k3_analort(A,D,E,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_analoaf,d3_analort]), [file(analort,t25_analort),interesting(0.00)]). fof(t26_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => r2_analort(A,D,E,B,C,k2_analort(A,D,E,B),k2_analort(A,D,E,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_analoaf,d4_analort]), [file(analort,t26_analort),interesting(0.00)]). fof(t23_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ( ( A = 0 | C = k1_rlvect_1(B) ) => k3_rlvect_1(B,C,A) = k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t23_rlvect_1), [interesting(0.00)]). fof(t10_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k1_rlvect_1(A)) = B & k2_rlvect_1(A,k1_rlvect_1(A),B) = B ) ) ) ), file(rlvect_1,t10_rlvect_1), [interesting(0.00)]). fof(d1_analmetr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) <=> ( ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) ) ) ) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) ) ) ) ) ) ), file(analmetr,d1_analmetr), [interesting(0.00)]). fof(l4_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ( B != k1_rlvect_1(A) & C != k1_rlvect_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d1_analmetr,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d1_analmetr]), [file(analort,l4_analort),interesting(0.00)]). fof(d4_geomtrap,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( E = k2_geomtrap(A,B,C,D) <=> ? [F] : ( m1_subset_1(F,k1_numbers) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) ) ) ) ) ) ) ) ) ), file(geomtrap,d4_geomtrap), [interesting(0.00)]). fof(d5_geomtrap,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( E = k3_geomtrap(A,B,C,D) <=> ? [F] : ( m1_subset_1(F,k1_numbers) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,E)) ) ) ) ) ) ) ) ) ), file(geomtrap,d5_geomtrap), [interesting(0.00)]). fof(t45_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k2_rlvect_1(A,k5_rlvect_1(A,C),k5_rlvect_1(A,B)) ) ) ) ), file(rlvect_1,t45_rlvect_1), [interesting(0.00)]). fof(t39_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k5_rlvect_1(B,k3_rlvect_1(B,C,A)) ) ) ) ), file(rlvect_1,t39_rlvect_1), [interesting(0.00)]). fof(t38_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k3_rlvect_1(B,C,k1_real_1(A)) ) ) ) ), file(rlvect_1,t38_rlvect_1), [interesting(0.00)]). fof(t28_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,B,B) = k1_rlvect_1(A) ) ) ), file(rlvect_1,t28_rlvect_1), [interesting(0.00)]). fof(d6_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v4_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D)) ) ) ) ) ) ), file(rlvect_1,d6_rlvect_1), [interesting(0.00)]). fof(d9_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ( v7_rlvect_1(A) <=> ( ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k3_real_1(B,C)) = k2_rlvect_1(A,k3_rlvect_1(A,D,B),k3_rlvect_1(A,D,C)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k4_real_1(B,C)) = k3_rlvect_1(A,k3_rlvect_1(A,D,C),B) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_rlvect_1(A,B,1) = B ) ) ) ) ), file(rlvect_1,d9_rlvect_1), [interesting(0.00)]). fof(t30_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,k5_rlvect_1(A,B)) = B ) ) ), file(rlvect_1,t30_rlvect_1), [interesting(0.00)]). fof(t21_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analoaf(A,B,C,D,E) => ( r1_analoaf(A,C,B,E,D) & r1_analoaf(A,D,E,B,C) ) ) ) ) ) ) ) ), file(analoaf,t21_analoaf), [interesting(0.00)]). fof(t41_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,B,k2_rlvect_1(A,C,D)) = k6_rlvect_1(A,k6_rlvect_1(A,B,D),C) ) ) ) ) ), file(rlvect_1,t41_rlvect_1), [interesting(0.00)]). fof(t49_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & l2_rlvect_1(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => k3_rlvect_1(C,D,k5_real_1(A,B)) = k6_rlvect_1(C,k3_rlvect_1(C,D,A),k3_rlvect_1(C,D,B)) ) ) ) ) ), file(rlvect_1,t49_rlvect_1), [interesting(0.00)]). fof(t13_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & k3_analort(A,B,C,D) = k3_analort(A,B,C,E) ) => D = E ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t41_rlvect_1,d6_rlvect_1,d6_rlvect_1,t49_rlvect_1,t49_rlvect_1,d1_analmetr,l5_analort,l5_analort]), [file(analort,t13_analort),interesting(0.00)]). fof(t20_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( r1_analoaf(A,B,C,D,E) & r1_analoaf(A,B,C,F,G) ) => ( B = C | r1_analoaf(A,D,E,F,G) ) ) ) ) ) ) ) ) ) ), file(analoaf,t20_analoaf), [interesting(0.00)]). fof(t7_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => k2_analort(A,B,C,k2_analort(A,B,C,D)) = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_geomtrap,d5_geomtrap,l5_analort]), [file(analort,t7_analort),interesting(0.00)]). fof(t8_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => D != k2_analort(A,B,C,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_analort]), [file(analort,t8_analort),interesting(0.00)]). fof(t6_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & k2_analort(A,B,C,D) = k2_analort(A,B,C,E) ) => D = E ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t41_rlvect_1,d6_rlvect_1,d6_rlvect_1,t49_rlvect_1,t49_rlvect_1,d1_analmetr,l5_analort,l5_analort]), [file(analort,t6_analort),interesting(0.00)]). fof(t9_analmetr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_analmetr(A,D,k1_rlvect_1(A),B,C) & r2_analmetr(A,k1_rlvect_1(A),E,B,C) ) ) ) ) ) ) ) ), file(analmetr,t9_analmetr), [interesting(0.00)]). fof(d3_analmetr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r3_analmetr(A,B,C,D,E,F,G) <=> r2_analmetr(A,k6_rlvect_1(A,C,B),k6_rlvect_1(A,E,D),F,G) ) ) ) ) ) ) ) ) ), file(analmetr,d3_analmetr), [interesting(0.00)]). fof(t35_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A) => B = C ) ) ) ) ), file(rlvect_1,t35_rlvect_1), [interesting(0.00)]). fof(l7_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ( r1_analmetr(A,B,C) => ( k2_geomtrap(A,B,C,k1_analort(A,D,E)) = k3_real_1(k2_geomtrap(A,B,C,D),k2_geomtrap(A,B,C,E)) & k3_geomtrap(A,B,C,k1_analort(A,D,E)) = k3_real_1(k3_geomtrap(A,B,C,D),k3_geomtrap(A,B,C,E)) & k2_geomtrap(A,B,C,k6_rlvect_1(A,D,E)) = k5_real_1(k2_geomtrap(A,B,C,D),k2_geomtrap(A,B,C,E)) & k3_geomtrap(A,B,C,k6_rlvect_1(A,D,E)) = k5_real_1(k3_geomtrap(A,B,C,D),k3_geomtrap(A,B,C,E)) & k2_geomtrap(A,B,C,k3_rlvect_1(A,D,F)) = k4_real_1(F,k2_geomtrap(A,B,C,D)) & k3_geomtrap(A,B,C,k3_rlvect_1(A,D,F)) = k4_real_1(F,k3_geomtrap(A,B,C,D)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l5_analort,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d9_rlvect_1,l6_analort,l1_analort,l6_analort,l2_analort,l6_analort]), [file(analort,l7_analort),interesting(0.00)]). fof(d6_geomtrap,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k4_geomtrap(A,B,C,D,E) = k3_real_1(k4_real_1(k2_geomtrap(A,B,C,D),k2_geomtrap(A,B,C,E)),k4_real_1(k3_geomtrap(A,B,C,D),k3_geomtrap(A,B,C,E))) ) ) ) ) ) ), file(geomtrap,d6_geomtrap), [interesting(0.00)]). fof(t34_geomtrap,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_analmetr(A,D,E,B,C) <=> k4_geomtrap(A,B,C,D,E) = 0 ) ) ) ) ) ) ) ), file(geomtrap,t34_geomtrap), [interesting(0.00)]). fof(t13_analmetr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r2_analmetr(A,D,E,B,C) & r2_analmetr(A,D,F,B,C) & D != k1_rlvect_1(A) & ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ~ ( k3_rlvect_1(A,E,G) = k3_rlvect_1(A,F,H) & ~ ( G = 0 & H = 0 ) ) ) ) ) ) ) ) ) ) ) ), file(analmetr,t13_analmetr), [interesting(0.00)]). fof(t18_analmetr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ~ ( ( r1_analoaf(A,B,C,D,E) | r1_analoaf(A,B,C,E,D) ) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ~ ( k3_rlvect_1(A,k6_rlvect_1(A,C,B),F) = k3_rlvect_1(A,k6_rlvect_1(A,E,D),G) & ~ ( F = 0 & G = 0 ) ) ) ) ) & ~ ( ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & k3_rlvect_1(A,k6_rlvect_1(A,C,B),F) = k3_rlvect_1(A,k6_rlvect_1(A,E,D),G) & ~ ( F = 0 & G = 0 ) ) ) & ~ r1_analoaf(A,B,C,D,E) & ~ r1_analoaf(A,B,C,E,D) ) ) ) ) ) ) ) ), file(analmetr,t18_analmetr), [interesting(0.00)]). fof(t24_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ~ ( k3_rlvect_1(B,C,A) = k1_rlvect_1(B) & A != 0 & C != k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t24_rlvect_1), [interesting(0.00)]). fof(d7_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( ( A != 0 => ( B = k5_xcmplx_0(A) <=> k3_xcmplx_0(A,B) = 1 ) ) & ( A = 0 => ( B = k5_xcmplx_0(A) <=> B = 0 ) ) ) ) ) ), file(xcmplx_0,d7_xcmplx_0), [interesting(0.00)]). fof(t11_analmetr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( r2_analmetr(A,B,C,D,E) => ( r2_analmetr(A,k3_rlvect_1(A,B,F),C,D,E) & r2_analmetr(A,B,k3_rlvect_1(A,C,G),D,E) ) ) ) ) ) ) ) ) ) ), file(analmetr,t11_analmetr), [interesting(0.00)]). fof(t20_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => r1_analort(A,E,F,B,B,C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analoaf,d3_analort]), [file(analort,t20_analort),interesting(0.00)]). fof(t19_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analoaf(A,B,C,C,B) => B = C ) ) ) ) ), file(analoaf,t19_analoaf), [interesting(0.00)]). fof(t30_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r1_analort(A,B,C,D,E,F,G) & r1_analort(A,B,C,D,E,G,F) & D != E & F != G ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analort,t13_analort,t20_analoaf,t19_analoaf]), [file(analort,t30_analort),interesting(0.00)]). fof(t31_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r2_analort(A,B,C,D,E,F,G) & r2_analort(A,B,C,D,E,G,F) & D != E & F != G ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,t6_analort,t20_analoaf,t19_analoaf]), [file(analort,t31_analort),interesting(0.00)]). fof(t23_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( r1_analoaf(A,B,C,B,D) & ~ r1_analoaf(A,B,C,C,D) & ~ r1_analoaf(A,B,D,D,C) ) ) ) ) ) ), file(analoaf,t23_analoaf), [interesting(0.00)]). fof(t32_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r1_analort(A,B,C,D,E,F,G) & r1_analort(A,B,C,D,E,F,H) & ~ r1_analort(A,B,C,D,E,G,H) & ~ r1_analort(A,B,C,D,E,H,G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analort,t13_analort,t20_analoaf,t21_analoaf,t20_analoaf,d3_analort,t21_analoaf,t20_analoaf,d3_analort,t23_analoaf,t20_analort]), [file(analort,t32_analort),interesting(0.00)]). fof(t33_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r2_analort(A,B,C,D,E,F,G) & r2_analort(A,B,C,D,E,F,H) & ~ r2_analort(A,B,C,D,E,G,H) & ~ r2_analort(A,B,C,D,E,H,G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,t6_analort,t20_analoaf,t23_analoaf,t21_analoaf,t20_analoaf,d4_analort,t18_analoaf,d4_analort]), [file(analort,t33_analort),interesting(0.00)]). fof(t34_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r1_analort(A,F,G,B,C,D,E) => r1_analort(A,F,G,C,B,E,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analort,t21_analoaf,d3_analort]), [file(analort,t34_analort),interesting(0.00)]). fof(t35_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r2_analort(A,F,G,B,C,D,E) => r2_analort(A,F,G,C,B,E,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,t21_analoaf,d4_analort]), [file(analort,t35_analort),interesting(0.00)]). fof(t22_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analoaf(A,B,C,C,D) => r1_analoaf(A,B,C,B,D) ) ) ) ) ) ), file(analoaf,t22_analoaf), [interesting(0.00)]). fof(t36_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & r1_analort(A,B,C,D,E,F,G) & r1_analort(A,B,C,D,E,G,H) ) => r1_analort(A,B,C,D,E,F,H) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analort,t21_analoaf,t13_analort,t20_analoaf,t22_analoaf,t20_analoaf,d3_analort,t18_analoaf,d3_analort]), [file(analort,t36_analort),interesting(0.00)]). fof(t37_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & r2_analort(A,B,C,D,E,F,G) & r2_analort(A,B,C,D,E,G,H) ) => r2_analort(A,B,C,D,E,F,H) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,t21_analoaf,t6_analort,t20_analoaf,t22_analoaf,t20_analoaf,d4_analort,t18_analoaf,d4_analort]), [file(analort,t37_analort),interesting(0.00)]). fof(t22_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( k2_rlvect_1(A,B,C) = B | k2_rlvect_1(A,C,B) = B ) => C = k1_rlvect_1(A) ) ) ) ) ), file(rlvect_1,t22_rlvect_1), [interesting(0.00)]). fof(t25_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( B = k6_rlvect_1(A,k4_rlvect_1(A,C,D),E) => ( r1_analoaf(A,E,C,D,B) & r1_analoaf(A,E,D,C,B) ) ) ) ) ) ) ) ), file(analoaf,t25_analoaf), [interesting(0.00)]). fof(d1_analoaf,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analoaf(A,B,C,D,E) <=> ~ ( B != C & D != E & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ~ ( ~ r1_xreal_0(F,0) & ~ r1_xreal_0(G,0) & k3_rlvect_1(A,k6_rlvect_1(A,C,B),F) = k3_rlvect_1(A,k6_rlvect_1(A,E,D),G) ) ) ) ) ) ) ) ) ) ) ), file(analoaf,d1_analoaf), [interesting(0.00)]). fof(t16_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & r1_analoaf(A,D,E,F,G) ) => r1_analoaf(A,k3_analort(A,B,C,D),k3_analort(A,B,C,E),k3_analort(A,B,C,F),k3_analort(A,B,C,G)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf,t11_analort,t12_analort,t12_analort,t11_analort,d1_analoaf,t18_analoaf]), [file(analort,t16_analort),interesting(0.00)]). fof(t17_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & r1_analoaf(A,D,E,F,G) ) => r1_analoaf(A,k2_analort(A,B,C,D),k2_analort(A,B,C,E),k2_analort(A,B,C,F),k2_analort(A,B,C,G)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf,t5_analort,t2_analort,t2_analort,t5_analort,d1_analoaf,t18_analoaf,t18_analoaf]), [file(analort,t17_analort),interesting(0.00)]). fof(t42_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r1_analort(A,B,C,D,E,F,G) & r1_analort(A,B,C,H,I,F,G) & r1_analort(A,B,C,H,I,J,K) & H != I & F != G & ~ r1_analort(A,B,C,D,E,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analort,t21_analoaf,d3_analort,t21_analoaf,d3_analort,t13_analort,t20_analoaf,t20_analoaf,d3_analort]), [file(analort,t42_analort),interesting(0.00)]). fof(t43_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r2_analort(A,B,C,D,E,F,G) & r2_analort(A,B,C,H,I,F,G) & r2_analort(A,B,C,H,I,J,K) & H != I & F != G & ~ r2_analort(A,B,C,D,E,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,t21_analoaf,d4_analort,t21_analoaf,d4_analort,t6_analort,t20_analoaf,t20_analoaf,d4_analort]), [file(analort,t43_analort),interesting(0.00)]). fof(t44_analort,theorem,( $true ), file(analort,t44_analort), [interesting(0.00)]). fof(t45_analort,theorem,( $true ), file(analort,t45_analort), [interesting(0.00)]). fof(t24_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k6_rlvect_1(A,D,E) => r1_analoaf(A,C,B,E,D) ) ) ) ) ) ) ), file(analoaf,t24_analoaf), [interesting(0.00)]). fof(t46_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r1_analort(A,B,C,D,E,F,G) & r1_analort(A,B,C,F,G,H,I) & r1_analort(A,B,C,J,K,H,I) & ~ r1_analort(A,B,C,D,E,J,K) & F != G & H != I ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_analort,d3_analort,d3_analort,t21_analoaf,d3_analort,t21_analoaf,t20_analoaf,t13_analort,t20_analoaf,t21_analoaf,d3_analort,t18_analort]), [file(analort,t46_analort),interesting(0.00)]). fof(t19_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( r1_analmetr(A,B,C) & r2_analort(A,B,C,D,E,F,G) ) => r2_analort(A,B,C,F,G,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,t21_analoaf,t17_analort,t7_analort,t7_analort,d4_analort]), [file(analort,t19_analort),interesting(0.00)]). fof(t47_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r2_analort(A,B,C,D,E,F,G) & r2_analort(A,B,C,F,G,H,I) & r2_analort(A,B,C,J,K,H,I) & ~ r2_analort(A,B,C,D,E,J,K) & F != G & H != I ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,t21_analoaf,t19_analort,d4_analort,t21_analoaf,t19_analort,d4_analort,t20_analoaf,t6_analort,t20_analoaf,d4_analort]), [file(analort,t47_analort),interesting(0.00)]). fof(t48_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r1_analort(A,B,C,D,E,F,G) & r1_analort(A,B,C,F,G,H,I) & r1_analort(A,B,C,D,E,J,K) & ~ r1_analort(A,B,C,J,K,H,I) & F != G & D != E ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analort,d3_analort,d3_analort,t13_analort,t20_analoaf,t16_analort,t20_analoaf,d3_analort]), [file(analort,t48_analort),interesting(0.00)]). fof(t49_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ~ ( r1_analmetr(A,B,C) & r2_analort(A,B,C,D,E,F,G) & r2_analort(A,B,C,F,G,H,I) & r2_analort(A,B,C,D,E,J,K) & ~ r2_analort(A,B,C,J,K,H,I) & F != G & D != E ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_analort,d4_analort,d4_analort,t6_analort,t20_analoaf,t17_analort,t20_analoaf,d4_analort]), [file(analort,t49_analort),interesting(0.00)]). fof(t31_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) = D ) ) ) ) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r1_analoaf(A,B,C,D,E) & ~ r1_analoaf(A,B,C,E,D) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( ( r1_analoaf(A,B,C,B,F) | r1_analoaf(A,B,C,F,B) ) & ( r1_analoaf(A,D,E,D,F) | r1_analoaf(A,D,E,F,D) ) ) ) ) ) ) ) ) ) ) ), file(analoaf,t31_analoaf), [interesting(0.00)]). fof(t6_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( k3_xcmplx_0(A,B) = 0 & A != 0 & B != 0 ) ) ) ), file(xcmplx_1,t6_xcmplx_1), [interesting(0.00)]). fof(t65_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => r1_xreal_0(0,k3_xcmplx_0(A,A)) ) ), file(xreal_1,t65_xreal_1), [interesting(0.00)]). fof(t52_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( ~ r2_analort(A,B,C,D,G,E,F) & ~ r2_analort(A,B,C,D,G,F,E) & r2_analort(A,B,C,F,H,F,E) & ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ~ ( ( r2_analort(A,B,C,D,G,D,I) | r2_analort(A,B,C,D,G,I,D) ) & ( r2_analort(A,B,C,F,H,F,I) | r2_analort(A,B,C,F,H,I,F) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_analort,d4_analort,t21_analoaf,t18_analoaf,t20_analoaf,d1_analmetr,t31_analoaf,t20_analoaf,d4_analort,t20_analoaf,d4_analort]), [file(analort,t52_analort),interesting(0.00)]). fof(t26_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ), file(rlvect_1,t26_rlvect_1), [interesting(0.00)]). fof(t54_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_analort(A,B,C))) <=> m1_subset_1(D,u1_struct_0(A)) ) ) ) ) ), file(analort,t54_analort), [interesting(0.00)]). fof(t55_analort,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k7_analort(A,B,C))) <=> m1_subset_1(D,u1_struct_0(A)) ) ) ) ) ), file(analort,t55_analort), [interesting(0.00)]). fof(d2_analoaf,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,E) <=> r2_hidden(k1_domain_1(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k1_domain_1(u1_struct_0(A),u1_struct_0(A),B,C),k1_domain_1(u1_struct_0(A),u1_struct_0(A),D,E)),u1_analoaf(A)) ) ) ) ) ) ) ), file(analoaf,d2_analoaf), [interesting(0.00)]). fof(d5_analort,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m2_relset_1(D,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) => ( D = k4_analort(A,B,C) <=> ! [E,F] : ( r2_hidden(k4_tarski(E,F),D) <=> ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & ? [H] : ( m1_subset_1(H,u1_struct_0(A)) & ? [I] : ( m1_subset_1(I,u1_struct_0(A)) & ? [J] : ( m1_subset_1(J,u1_struct_0(A)) & E = k4_tarski(G,H) & F = k4_tarski(I,J) & r1_analort(A,B,C,G,H,I,J) ) ) ) ) ) ) ) ) ) ) ), file(analort,d5_analort), [interesting(0.00)]). fof(t33_zfmisc_1,theorem,( ! [A,B,C,D] : ( k4_tarski(A,B) = k4_tarski(C,D) => ( A = C & B = D ) ) ), file(zfmisc_1,t33_zfmisc_1), [interesting(0.00)]). fof(d6_analort,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m2_relset_1(D,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) => ( D = k5_analort(A,B,C) <=> ! [E,F] : ( r2_hidden(k4_tarski(E,F),D) <=> ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & ? [H] : ( m1_subset_1(H,u1_struct_0(A)) & ? [I] : ( m1_subset_1(I,u1_struct_0(A)) & ? [J] : ( m1_subset_1(J,u1_struct_0(A)) & E = k4_tarski(G,H) & F = k4_tarski(I,J) & r2_analort(A,B,C,G,H,I,J) ) ) ) ) ) ) ) ) ) ) ), file(analort,d6_analort), [interesting(0.00)]).