fof(t16_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,k6_valuat_1(A,B,C)) = k3_bvfunc26(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_bvfunc26,t6_bvfunc_1]),
    [file(bvfunc26,t16_bvfunc26),interesting(1.00)]).

fof(t46_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => k15_bvfunc_1(A,k18_bvfunc_1(A),k19_bvfunc_1(A)) = k18_bvfunc_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t12_bvfunc25,t5_bvfunc_1,t14_bvfunc25,t5_bvfunc_1]),
    [file(bvfunc26,t46_bvfunc26),interesting(0.92)]).

fof(t45_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => k15_bvfunc_1(A,k18_bvfunc_1(A),k18_bvfunc_1(A)) = k19_bvfunc_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t12_bvfunc25,t13_bvfunc25,t5_bvfunc_1]),
    [file(bvfunc26,t45_bvfunc26),interesting(0.91)]).

fof(t47_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => k15_bvfunc_1(A,k19_bvfunc_1(A),k19_bvfunc_1(A)) = k19_bvfunc_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t12_bvfunc25,t14_bvfunc_8,t4_bvfunc_1]),
    [file(bvfunc26,t47_bvfunc26),interesting(0.87)]).

fof(t61_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,k3_bvfunc26(A,B,C)) = k18_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t55_bvfunc26,t6_bvfunc_4,t13_bvfunc_1,t5_bvfunc_1]),
    [file(bvfunc26,t61_bvfunc26),interesting(0.86)]).

fof(t73_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,k4_bvfunc26(A,B,C)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t67_bvfunc26,t6_bvfunc_4,t13_bvfunc_1]),
    [file(bvfunc26,t73_bvfunc26),interesting(0.84)]).

fof(t43_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,k3_bvfunc26(A,B,C)) = k18_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t37_bvfunc26,t5_bvfunc_4,t8_bvfunc_1]),
    [file(bvfunc26,t43_bvfunc26),interesting(0.83)]).

fof(t22_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,B,C) = k3_bvfunc26(A,k3_bvfunc26(A,B,C),k3_bvfunc26(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t1_bvfunc26,t1_bvfunc26,t17_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t10_bvfunc_1]),
    [file(bvfunc26,t22_bvfunc26),interesting(0.82)]).

fof(t44_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,k4_bvfunc26(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t38_bvfunc26,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1]),
    [file(bvfunc26,t44_bvfunc26),interesting(0.79)]).

fof(t6_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( k3_bvfunc26(A,B,B) = k5_valuat_1(A,B)
            & k5_valuat_1(A,k3_bvfunc26(A,B,B)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t6_bvfunc_1,t4_bvfunc_1]),
    [file(bvfunc26,t6_bvfunc26),interesting(0.75)]).

fof(t20_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,k4_bvfunc26(A,B,C)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t2_bvfunc26,t17_bvfunc_1,t4_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1]),
    [file(bvfunc26,t20_bvfunc26),interesting(0.74)]).

fof(t26_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k4_bvfunc26(A,k19_bvfunc_1(A),B) = k18_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t13_bvfunc_1,t5_bvfunc_1]),
    [file(bvfunc26,t26_bvfunc26),interesting(0.74)]).

fof(t29_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( k4_bvfunc26(A,B,B) = k5_valuat_1(A,B)
            & k5_valuat_1(A,k4_bvfunc26(A,B,B)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t10_bvfunc_1,t4_bvfunc_1]),
    [file(bvfunc26,t29_bvfunc26),interesting(0.74)]).

fof(t4_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k3_bvfunc26(A,k18_bvfunc_1(A),B) = k19_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t8_bvfunc_1,t5_bvfunc_1]),
    [file(bvfunc26,t4_bvfunc26),interesting(0.74)]).

fof(t27_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k4_bvfunc26(A,k18_bvfunc_1(A),B) = k5_valuat_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t12_bvfunc_1]),
    [file(bvfunc26,t27_bvfunc26),interesting(0.73)]).

fof(t3_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k3_bvfunc26(A,k19_bvfunc_1(A),B) = k5_valuat_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t9_bvfunc_1]),
    [file(bvfunc26,t3_bvfunc26),interesting(0.73)]).

fof(t57_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,B,k3_bvfunc26(A,B,C)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t51_bvfunc26,t6_bvfunc_4,t13_bvfunc_1]),
    [file(bvfunc26,t57_bvfunc26),interesting(0.72)]).

fof(t68_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,B,k4_bvfunc26(A,B,C)) = k18_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t62_bvfunc26,t5_bvfunc_4,t8_bvfunc_1]),
    [file(bvfunc26,t68_bvfunc26),interesting(0.72)]).

fof(t42_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,k14_bvfunc_1(A,B,C)) = k18_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t36_bvfunc26,t5_bvfunc_4,t8_bvfunc_1]),
    [file(bvfunc26,t42_bvfunc26),interesting(0.71)]).

fof(t41_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,k15_bvfunc_1(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_bvfunc26,t9_bvfunc_4,t15_bvfunc_1,t7_bvfunc_1,t5_bvfunc_4,t8_bvfunc_1,t12_bvfunc_1,t7_bvfunc_1,t6_bvfunc_1]),
    [file(bvfunc26,t41_bvfunc26),interesting(0.70)]).

fof(t49_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,k8_bvfunc_1(A,B,C)) = k8_bvfunc_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_bvfunc25,t9_bvfunc_4,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t16_bvfunc_1,t7_bvfunc_1,t5_bvfunc_4,t8_bvfunc_1,t12_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1]),
    [file(bvfunc26,t49_bvfunc26),interesting(0.70)]).

fof(t56_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,B,k3_bvfunc26(A,B,C)) = k6_valuat_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t50_bvfunc26,t5_bvfunc_4,t12_bvfunc_1]),
    [file(bvfunc26,t56_bvfunc26),interesting(0.70)]).

fof(t69_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,B,k4_bvfunc26(A,B,C)) = k8_bvfunc_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_bvfunc26,t6_bvfunc_4,t9_bvfunc_1]),
    [file(bvfunc26,t69_bvfunc26),interesting(0.70)]).

fof(t32_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,k5_valuat_1(A,B),k9_bvfunc_1(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t15_bvfunc_1,t7_bvfunc_1,t6_bvfunc_1,t7_bvfunc_1,t5_bvfunc_4,t8_bvfunc_1,t12_bvfunc_1]),
    [file(bvfunc26,t32_bvfunc26),interesting(0.69)]).

fof(t40_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,k8_bvfunc_1(A,B,C)) = k5_valuat_1(A,k8_bvfunc_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t34_bvfunc26,t10_bvfunc_1]),
    [file(bvfunc26,t40_bvfunc26),interesting(0.66)]).

fof(t70_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,k4_bvfunc26(A,B,C)) = k8_bvfunc_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t64_bvfunc26,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t16_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1]),
    [file(bvfunc26,t70_bvfunc26),interesting(0.66)]).

fof(t59_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,k3_bvfunc26(A,B,C)) = k6_valuat_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t53_bvfunc26,t5_bvfunc_4,t8_bvfunc_1,t12_bvfunc_1,t17_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1]),
    [file(bvfunc26,t59_bvfunc26),interesting(0.65)]).

fof(t58_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,k3_bvfunc26(A,B,C)) = k8_bvfunc_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t52_bvfunc26,t6_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1]),
    [file(bvfunc26,t58_bvfunc26),interesting(0.63)]).

fof(t1_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,C) = k5_valuat_1(A,k6_valuat_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_valuat_1,d6_valuat_1,t4_binari_5,t40_margrel1,d3_bvfunc26,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc26,t1_bvfunc26),interesting(0.61)]).

fof(t25_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,k14_bvfunc_1(A,B,C)) = k5_valuat_1(A,k6_valuat_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t24_bvfunc26,t6_bvfunc_4,t9_bvfunc_1]),
    [file(bvfunc26,t25_bvfunc26),interesting(0.61)]).

fof(t71_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,k4_bvfunc26(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t65_bvfunc26,t10_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1]),
    [file(bvfunc26,t71_bvfunc26),interesting(0.61)]).

fof(t2_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,C) = k5_valuat_1(A,k8_bvfunc_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_valuat_1,d7_bvfunc_1,t13_binari_5,t40_margrel1,d4_bvfunc26,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc26,t2_bvfunc26),interesting(0.60)]).

fof(t37_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k4_bvfunc26(A,B,k3_bvfunc26(A,C,D)) = k6_valuat_1(A,k6_valuat_1(A,k5_valuat_1(A,B),C),D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t1_bvfunc26,t16_bvfunc_1,t4_bvfunc_1,t7_bvfunc_1]),
    [file(bvfunc26,t37_bvfunc26),interesting(0.58)]).

fof(t60_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,k3_bvfunc26(A,B,C)) = k5_valuat_1(A,k6_valuat_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t54_bvfunc26,t6_bvfunc_1]),
    [file(bvfunc26,t60_bvfunc26),interesting(0.58)]).

fof(t67_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,B,k4_bvfunc26(A,C,D)) = k8_bvfunc_1(A,k8_bvfunc_1(A,k5_valuat_1(A,B),C),D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t1_bvfunc26,t17_bvfunc_1,t4_bvfunc_1,t11_bvfunc_1]),
    [file(bvfunc26,t67_bvfunc26),interesting(0.58)]).

fof(t21_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,k15_bvfunc_1(A,B,C)) = k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t12_bvfunc25,t17_bvfunc_1,t4_bvfunc_1,t13_bvfunc_8,t14_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t11_bvfunc_1,t10_bvfunc_1]),
    [file(bvfunc26,t21_bvfunc26),interesting(0.53)]).

fof(t30_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k4_bvfunc26(A,B,C)) = k8_bvfunc_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t4_bvfunc_1]),
    [file(bvfunc26,t30_bvfunc26),interesting(0.53)]).

fof(t7_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k3_bvfunc26(A,B,C)) = k6_valuat_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t4_bvfunc_1]),
    [file(bvfunc26,t7_bvfunc26),interesting(0.53)]).

fof(t55_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k4_bvfunc26(A,B,k3_bvfunc26(A,C,D)) = k5_valuat_1(A,k8_bvfunc_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,C)),k5_valuat_1(A,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t2_bvfunc26,t17_bvfunc_1,t11_bvfunc_1]),
    [file(bvfunc26,t55_bvfunc26),interesting(0.52)]).

fof(t54_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,B,k3_bvfunc26(A,C,D)) = k5_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t8_bvfunc_4,t17_bvfunc_1,t7_bvfunc_1]),
    [file(bvfunc26,t54_bvfunc26),interesting(0.48)]).

fof(t36_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k4_bvfunc26(A,B,k14_bvfunc_1(A,C,D)) = k6_valuat_1(A,k6_valuat_1(A,k5_valuat_1(A,B),C),k5_valuat_1(A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t16_bvfunc_1,t1_bvfunc25,t7_bvfunc_1]),
    [file(bvfunc26,t36_bvfunc26),interesting(0.45)]).

fof(t72_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,k4_bvfunc26(A,B,C)) = k5_valuat_1(A,k8_bvfunc_1(A,B,k6_valuat_1(A,B,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t66_bvfunc26,t15_bvfunc_1,t6_bvfunc_1]),
    [file(bvfunc26,t72_bvfunc26),interesting(0.42)]).

fof(t19_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ( k3_bvfunc26(A,B,k3_bvfunc26(A,B,C)) = k8_bvfunc_1(A,k5_valuat_1(A,B),C)
                & k3_bvfunc26(A,B,k3_bvfunc26(A,B,C)) = k14_bvfunc_1(A,B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t1_bvfunc26,t17_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc26,t19_bvfunc26),interesting(0.39)]).

fof(t31_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( k4_bvfunc26(A,B,k5_valuat_1(A,B)) = k18_bvfunc_1(A)
            & k5_valuat_1(A,k4_bvfunc26(A,B,k5_valuat_1(A,B))) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t6_bvfunc_4,t5_bvfunc_1,t5_bvfunc_1]),
    [file(bvfunc26,t31_bvfunc26),interesting(0.37)]).

fof(t8_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( k3_bvfunc26(A,B,k5_valuat_1(A,B)) = k19_bvfunc_1(A)
            & k5_valuat_1(A,k3_bvfunc26(A,B,k5_valuat_1(A,B))) = k18_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t5_bvfunc_4,t5_bvfunc_1,t5_bvfunc_1]),
    [file(bvfunc26,t8_bvfunc26),interesting(0.37)]).

fof(t18_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,k15_bvfunc_1(A,B,C)) = k14_bvfunc_1(A,B,k9_bvfunc_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t17_bvfunc_1,t12_bvfunc25,t4_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc26,t18_bvfunc26),interesting(0.35)]).

fof(t66_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,B,k4_bvfunc26(A,C,D)) = k5_valuat_1(A,k6_valuat_1(A,B,k8_bvfunc_1(A,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t8_bvfunc_4,t17_bvfunc_1]),
    [file(bvfunc26,t66_bvfunc26),interesting(0.34)]).

fof(t24_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,B,k14_bvfunc_1(A,C,D)) = k6_valuat_1(A,k8_bvfunc_1(A,k5_valuat_1(A,B),C),k5_valuat_1(A,k6_valuat_1(A,B,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t8_bvfunc_4,t15_bvfunc_1,t16_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1]),
    [file(bvfunc26,t24_bvfunc26),interesting(0.33)]).

fof(t35_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k4_bvfunc26(A,B,k15_bvfunc_1(A,C,D)) = k6_valuat_1(A,k5_valuat_1(A,B),k9_bvfunc_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t16_bvfunc_1,t12_bvfunc25,t4_bvfunc_1]),
    [file(bvfunc26,t35_bvfunc26),interesting(0.32)]).

fof(t48_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( k15_bvfunc_1(A,B,B) = k19_bvfunc_1(A)
            & k5_valuat_1(A,k15_bvfunc_1(A,B,B)) = k18_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_bvfunc25,t13_bvfunc25,t5_bvfunc_1,t5_bvfunc_1]),
    [file(bvfunc26,t48_bvfunc26),interesting(0.29)]).

fof(t52_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k9_bvfunc_1(A,B,k3_bvfunc26(A,C,D)) = k8_bvfunc_1(A,k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,k6_valuat_1(A,C,D))),k6_valuat_1(A,k6_valuat_1(A,B,C),D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t9_bvfunc_4,t4_bvfunc_1,t7_bvfunc_1]),
    [file(bvfunc26,t52_bvfunc26),interesting(0.24)]).

fof(t53_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k15_bvfunc_1(A,B,k3_bvfunc26(A,C,D)) = k8_bvfunc_1(A,k6_valuat_1(A,B,k5_valuat_1(A,k6_valuat_1(A,C,D))),k6_valuat_1(A,k6_valuat_1(A,k5_valuat_1(A,B),C),D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t19_bvfunc_8,t4_bvfunc_1,t7_bvfunc_1]),
    [file(bvfunc26,t53_bvfunc26),interesting(0.24)]).

fof(t64_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k9_bvfunc_1(A,B,k4_bvfunc26(A,C,D)) = k6_valuat_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,k8_bvfunc_1(A,C,D))),k8_bvfunc_1(A,k8_bvfunc_1(A,k5_valuat_1(A,B),C),D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t13_bvfunc_8,t4_bvfunc_1,t11_bvfunc_1]),
    [file(bvfunc26,t64_bvfunc26),interesting(0.24)]).

fof(t65_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k15_bvfunc_1(A,B,k4_bvfunc26(A,C,D)) = k6_valuat_1(A,k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D),k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,k8_bvfunc_1(A,C,D)))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t18_bvfunc_8,t4_bvfunc_1,t11_bvfunc_1]),
    [file(bvfunc26,t65_bvfunc26),interesting(0.24)]).

fof(t12_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,B,k9_bvfunc_1(A,C,D)) = k15_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t11_bvfunc25,t12_bvfunc_8,t4_bvfunc_1]),
    [file(bvfunc26,t12_bvfunc26),interesting(0.19)]).

fof(t15_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,B,k15_bvfunc_1(A,C,D)) = k14_bvfunc_1(A,B,k9_bvfunc_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t17_bvfunc_1,t12_bvfunc25,t4_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc26,t15_bvfunc26),interesting(0.19)]).

fof(t14_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( k3_bvfunc26(A,B,k4_bvfunc26(A,C,D)) = k8_bvfunc_1(A,k8_bvfunc_1(A,k5_valuat_1(A,B),C),D)
                    & k3_bvfunc26(A,B,k4_bvfunc26(A,C,D)) = k14_bvfunc_1(A,B,k8_bvfunc_1(A,C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t2_bvfunc26,t17_bvfunc_1,t4_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc26,t14_bvfunc26),interesting(0.03)]).

fof(d5_valuat_1,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ( C = k5_valuat_1(A,B)
              <=> ! [D] : 
                    ( m1_subset_1(D,A)
                   => k8_funct_2(A,k6_margrel1,C,D) = k11_margrel1(k8_funct_2(A,k6_margrel1,B,D)) ) ) ) ) ) ),
    file(valuat_1,d5_valuat_1),
    [interesting(0.00)]).

fof(d6_valuat_1,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( D = k6_valuat_1(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,A)
                       => k8_funct_2(A,k6_margrel1,D,E) = k12_margrel1(k8_funct_2(A,k6_margrel1,B,E),k8_funct_2(A,k6_margrel1,C,E)) ) ) ) ) ) ) ),
    file(valuat_1,d6_valuat_1),
    [interesting(0.00)]).

fof(t4_binari_5,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => k9_margrel1(k1_binari_5(A,B)) = k10_margrel1(A,B) ) ) ),
    file(binari_5,t4_binari_5),
    [interesting(0.00)]).

fof(t40_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k9_margrel1(k9_margrel1(A)) = A ) ),
    file(margrel1,t40_margrel1),
    [interesting(0.00)]).

fof(d3_bvfunc26,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( D = k3_bvfunc26(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,A)
                       => k1_funct_1(D,E) = k1_binari_5(k1_funct_1(B,E),k1_funct_1(C,E)) ) ) ) ) ) ) ),
    file(bvfunc26,d3_bvfunc26),
    [interesting(0.00)]).

fof(d2_funct_2,definition,(
    ! [A,B,C] : 
      ( C = k1_funct_2(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E] : 
              ( v1_relat_1(E)
              & v1_funct_1(E)
              & D = E
              & k1_relat_1(E) = A
              & r1_tarski(k2_relat_1(E),B) ) ) ) ),
    file(funct_2,d2_funct_2),
    [interesting(0.00)]).

fof(t9_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( k1_relat_1(A) = k1_relat_1(B)
              & ! [C] : 
                  ( r2_hidden(C,k1_relat_1(A))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) ) )
           => A = B ) ) ) ),
    file(funct_1,t9_funct_1),
    [interesting(0.00)]).

fof(t11_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,B,k9_bvfunc_1(A,C,D)) = k9_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,B,D)) ) ) ) ) ),
    file(bvfunc25,t11_bvfunc25),
    [interesting(0.00)]).

fof(t12_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,C) = k5_valuat_1(A,k15_bvfunc_1(A,B,C)) ) ) ) ),
    file(bvfunc_8,t12_bvfunc_8),
    [interesting(0.00)]).

fof(t4_bvfunc_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_valuat_1(A) )
     => k3_valuat_1(k3_valuat_1(A)) = A ) ),
    file(bvfunc_1,t4_bvfunc_1),
    [interesting(0.00)]).

fof(t17_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k6_valuat_1(A,B,C)) = k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ),
    file(bvfunc_1,t17_bvfunc_1),
    [interesting(0.00)]).

fof(t8_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,C) = k8_bvfunc_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    file(bvfunc_4,t8_bvfunc_4),
    [interesting(0.00)]).

fof(t13_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( k3_bvfunc26(A,B,k3_bvfunc26(A,C,D)) = k8_bvfunc_1(A,k5_valuat_1(A,B),k6_valuat_1(A,C,D))
                    & k3_bvfunc26(A,B,k3_bvfunc26(A,C,D)) = k14_bvfunc_1(A,B,k6_valuat_1(A,C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t1_bvfunc26,t17_bvfunc_1,t4_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc26,t13_bvfunc26),interesting(0.00)]).

fof(d7_bvfunc_1,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( D = k8_bvfunc_1(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,A)
                       => k8_funct_2(A,k6_margrel1,D,E) = k3_binarith(k8_funct_2(A,k6_margrel1,B,E),k8_funct_2(A,k6_margrel1,C,E)) ) ) ) ) ) ) ),
    file(bvfunc_1,d7_bvfunc_1),
    [interesting(0.00)]).

fof(t13_binari_5,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => k9_margrel1(k3_binari_5(A,B)) = k1_binarith(A,B) ) ) ),
    file(binari_5,t13_binari_5),
    [interesting(0.00)]).

fof(d4_bvfunc26,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( D = k4_bvfunc26(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,A)
                       => k1_funct_1(D,E) = k3_binari_5(k1_funct_1(B,E),k1_funct_1(C,E)) ) ) ) ) ) ) ),
    file(bvfunc26,d4_bvfunc26),
    [interesting(0.00)]).

fof(t11_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D) = k8_bvfunc_1(A,B,k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t11_bvfunc_1),
    [interesting(0.00)]).

fof(t12_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k5_valuat_1(A,k9_bvfunc_1(A,B,C)) ) ) ) ),
    file(bvfunc25,t12_bvfunc25),
    [interesting(0.00)]).

fof(t7_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,k6_valuat_1(A,B,C),D) = k6_valuat_1(A,B,k6_valuat_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t7_bvfunc_1),
    [interesting(0.00)]).

fof(t9_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,B,k6_valuat_1(A,C,D)) = k5_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t7_bvfunc_1]),
    [file(bvfunc26,t9_bvfunc26),interesting(0.00)]).

fof(t10_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,B,k6_valuat_1(A,C,D)) = k3_bvfunc26(A,k6_valuat_1(A,B,C),D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t9_bvfunc26]),
    [file(bvfunc26,t10_bvfunc26),interesting(0.00)]).

fof(t6_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,B,B) = B ) ) ) ),
    file(bvfunc_1,t6_bvfunc_1),
    [interesting(0.00)]).

fof(t15_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,k8_bvfunc_1(A,B,C),D) = k8_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t15_bvfunc_1),
    [interesting(0.00)]).

fof(t16_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k8_bvfunc_1(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ),
    file(bvfunc_1,t16_bvfunc_1),
    [interesting(0.00)]).

fof(t11_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,B,k8_bvfunc_1(A,C,D)) = k6_valuat_1(A,k5_valuat_1(A,k6_valuat_1(A,B,C)),k5_valuat_1(A,k6_valuat_1(A,B,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t15_bvfunc_1,t16_bvfunc_1]),
    [file(bvfunc26,t11_bvfunc26),interesting(0.00)]).

fof(t17_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k3_bvfunc26(A,B,k8_bvfunc_1(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,k6_valuat_1(A,B,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_bvfunc26,t6_bvfunc_1]),
    [file(bvfunc26,t17_bvfunc26),interesting(0.00)]).

fof(t14_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k8_bvfunc_1(A,k6_valuat_1(A,B,C),D) = k6_valuat_1(A,k8_bvfunc_1(A,B,D),k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t14_bvfunc_1),
    [interesting(0.00)]).

fof(t6_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,k5_valuat_1(A,B)) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc_4,t6_bvfunc_4),
    [interesting(0.00)]).

fof(t9_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k6_valuat_1(A,B,k19_bvfunc_1(A)) = B ) ) ),
    file(bvfunc_1,t9_bvfunc_1),
    [interesting(0.00)]).

fof(t13_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,k19_bvfunc_1(A)) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc_1,t13_bvfunc_1),
    [interesting(0.00)]).

fof(t13_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,C) = k6_valuat_1(A,k8_bvfunc_1(A,B,C),k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C))) ) ) ) ),
    file(bvfunc_8,t13_bvfunc_8),
    [interesting(0.00)]).

fof(t10_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,B) = B ) ) ),
    file(bvfunc_1,t10_bvfunc_1),
    [interesting(0.00)]).

fof(t23_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k3_bvfunc26(A,k3_bvfunc26(A,B,C),k3_bvfunc26(A,B,D)) = k6_valuat_1(A,B,k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t1_bvfunc26,t1_bvfunc26,t17_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t15_bvfunc_1]),
    [file(bvfunc26,t23_bvfunc26),interesting(0.00)]).

fof(t12_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,k18_bvfunc_1(A)) = B ) ) ),
    file(bvfunc_1,t12_bvfunc_1),
    [interesting(0.00)]).

fof(t5_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( k5_valuat_1(A,k19_bvfunc_1(A)) = k18_bvfunc_1(A)
            & k5_valuat_1(A,k18_bvfunc_1(A)) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_1,t5_bvfunc_1),
    [interesting(0.00)]).

fof(t28_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( k4_bvfunc26(A,k18_bvfunc_1(A),k18_bvfunc_1(A)) = k19_bvfunc_1(A)
        & k4_bvfunc26(A,k18_bvfunc_1(A),k19_bvfunc_1(A)) = k18_bvfunc_1(A)
        & k4_bvfunc26(A,k19_bvfunc_1(A),k19_bvfunc_1(A)) = k18_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_bvfunc26,t5_bvfunc_1,t26_bvfunc26,t26_bvfunc26]),
    [file(bvfunc26,t28_bvfunc26),interesting(0.00)]).

fof(t9_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,C) = k8_bvfunc_1(A,k6_valuat_1(A,k5_valuat_1(A,B),C),k6_valuat_1(A,B,k5_valuat_1(A,C))) ) ) ) ),
    file(bvfunc_4,t9_bvfunc_4),
    [interesting(0.00)]).

fof(t5_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k6_valuat_1(A,B,k5_valuat_1(A,B)) = k18_bvfunc_1(A) ) ) ),
    file(bvfunc_4,t5_bvfunc_4),
    [interesting(0.00)]).

fof(t8_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k6_valuat_1(A,B,k18_bvfunc_1(A)) = k18_bvfunc_1(A) ) ) ),
    file(bvfunc_1,t8_bvfunc_1),
    [interesting(0.00)]).

fof(t33_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k4_bvfunc26(A,B,k6_valuat_1(A,C,D)) = k8_bvfunc_1(A,k5_valuat_1(A,k8_bvfunc_1(A,B,C)),k5_valuat_1(A,k8_bvfunc_1(A,B,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t14_bvfunc_1,t17_bvfunc_1]),
    [file(bvfunc26,t33_bvfunc26),interesting(0.00)]).

fof(t39_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k4_bvfunc26(A,B,k6_valuat_1(A,B,C)) = k5_valuat_1(A,k6_valuat_1(A,B,k8_bvfunc_1(A,B,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t33_bvfunc26,t10_bvfunc_1,t17_bvfunc_1]),
    [file(bvfunc26,t39_bvfunc26),interesting(0.00)]).

fof(t34_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k4_bvfunc26(A,B,k8_bvfunc_1(A,C,D)) = k5_valuat_1(A,k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t11_bvfunc_1]),
    [file(bvfunc26,t34_bvfunc26),interesting(0.00)]).

fof(t1_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k14_bvfunc_1(A,B,C)) = k6_valuat_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    file(bvfunc25,t1_bvfunc25),
    [interesting(0.00)]).

fof(t38_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k4_bvfunc26(A,B,k4_bvfunc26(A,C,D)) = k6_valuat_1(A,k5_valuat_1(A,B),k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t2_bvfunc26,t16_bvfunc_1,t4_bvfunc_1]),
    [file(bvfunc26,t38_bvfunc26),interesting(0.00)]).

fof(t13_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k9_bvfunc_1(A,B,B) = k18_bvfunc_1(A) ) ) ),
    file(bvfunc25,t13_bvfunc25),
    [interesting(0.00)]).

fof(t14_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k9_bvfunc_1(A,B,k5_valuat_1(A,B)) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc25,t14_bvfunc25),
    [interesting(0.00)]).

fof(t14_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k9_bvfunc_1(A,B,k19_bvfunc_1(A)) = k5_valuat_1(A,B) ) ) ),
    file(bvfunc_8,t14_bvfunc_8),
    [interesting(0.00)]).

fof(t50_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,B,k3_bvfunc26(A,C,D)) = k8_bvfunc_1(A,k6_valuat_1(A,B,k5_valuat_1(A,C)),k6_valuat_1(A,B,k5_valuat_1(A,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t17_bvfunc_1,t15_bvfunc_1]),
    [file(bvfunc26,t50_bvfunc26),interesting(0.00)]).

fof(t51_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k8_bvfunc_1(A,B,k3_bvfunc26(A,C,D)) = k8_bvfunc_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,C)),k5_valuat_1(A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_bvfunc26,t17_bvfunc_1,t11_bvfunc_1]),
    [file(bvfunc26,t51_bvfunc26),interesting(0.00)]).

fof(t19_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k8_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C))) ) ) ) ),
    file(bvfunc_8,t19_bvfunc_8),
    [interesting(0.00)]).

fof(t5_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( k3_bvfunc26(A,k18_bvfunc_1(A),k18_bvfunc_1(A)) = k19_bvfunc_1(A)
        & k3_bvfunc26(A,k18_bvfunc_1(A),k19_bvfunc_1(A)) = k19_bvfunc_1(A)
        & k3_bvfunc26(A,k19_bvfunc_1(A),k19_bvfunc_1(A)) = k18_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_bvfunc26,t4_bvfunc26,t3_bvfunc26,t5_bvfunc_1]),
    [file(bvfunc26,t5_bvfunc26),interesting(0.00)]).

fof(t62_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,B,k4_bvfunc26(A,C,D)) = k6_valuat_1(A,k6_valuat_1(A,B,k5_valuat_1(A,C)),k5_valuat_1(A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t16_bvfunc_1,t7_bvfunc_1]),
    [file(bvfunc26,t62_bvfunc26),interesting(0.00)]).

fof(t63_bvfunc26,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k8_bvfunc_1(A,B,k4_bvfunc26(A,C,D)) = k6_valuat_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,C)),k8_bvfunc_1(A,B,k5_valuat_1(A,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc26,t16_bvfunc_1,t14_bvfunc_1]),
    [file(bvfunc26,t63_bvfunc26),interesting(0.00)]).

fof(t18_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k6_valuat_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,C)),k8_bvfunc_1(A,k5_valuat_1(A,B),C)) ) ) ) ),
    file(bvfunc_8,t18_bvfunc_8),
    [interesting(0.00)]).