inv_mul_cancel_left.p

inv_mul_cancel_left.p

fof(ccanonically__ordered__comm__semiring_o_to__comm__semiring, axiom,
 (![X_ga_n2]: (p(ccanonically__ordered__comm__semiring(X_ga_n2)) => p(ccomm__semiring(X_ga_n2))))).

fof(ccanonically__ordered__comm__semiring_o_to__zero__ne__one__class, axiom,
 (![X_ga_n3]: (p(ccanonically__ordered__comm__semiring(X_ga_n3)) => p(czero__ne__one__class(X_ga_n3))))).

fof(ccomm__group_o_to__comm__monoid, axiom, (![X_ga_n5]: (p(ccomm__group(X_ga_n5)) => p(ccomm__monoid(X_ga_n5))))).

fof(ccomm__group_o_to__group, axiom, (![X_ga_n6]: (p(ccomm__group(X_ga_n6)) => p(cgroup(X_ga_n6))))).

fof(ccomm__monoid_o_to__comm__semigroup, axiom,
 (![X_ga_n8]: (p(ccomm__monoid(X_ga_n8)) => p(ccomm__semigroup(X_ga_n8))))).

fof(ccomm__monoid_o_to__monoid, axiom, (![X_ga_n9]: (p(ccomm__monoid(X_ga_n9)) => p(cmonoid(X_ga_n9))))).

fof(ccomm__ring_o_to__comm__semigroup, axiom,
 (![X_ga_n11]: (p(ccomm__ring(X_ga_n11)) => p(ccomm__semigroup(X_ga_n11))))).

fof(ccomm__ring_o_to__comm__semiring, axiom, (![X_ga_n12]: (p(ccomm__ring(X_ga_n12)) => p(ccomm__semiring(X_ga_n12))))).

fof(ccomm__ring_o_to__ring, axiom, (![X_ga_n13]: (p(ccomm__ring(X_ga_n13)) => p(cring(X_ga_n13))))).

fof(ccomm__semigroup_o_to__semigroup, axiom, (![X_ga_n15]: (p(ccomm__semigroup(X_ga_n15)) => p(csemigroup(X_ga_n15))))).

fof(ccomm__semigroup__to__is__commutative, axiom,
 (![X_ga_n16]: (p(ccomm__semigroup(X_ga_n16)) => p(cis__commutative(chas__mul_o_mul(X_ga_n16)))))).

fof(ccomm__semiring_o_to__comm__monoid, axiom,
 (![X_ga_n18]: (p(ccomm__semiring(X_ga_n18)) => p(ccomm__monoid(X_ga_n18))))).

fof(ccomm__semiring_o_to__semiring, axiom, (![X_ga_n19]: (p(ccomm__semiring(X_ga_n19)) => p(csemiring(X_ga_n19))))).

fof(cdecidable__linear__ordered__comm__ring_o_to__decidable__linear__ordered__semiring, axiom,
 (![X_ga_n21]:
  (p(cdecidable__linear__ordered__comm__ring(X_ga_n21)) => p(cdecidable__linear__ordered__semiring(X_ga_n21))))).

fof(cdecidable__linear__ordered__comm__ring_o_to__linear__ordered__comm__ring, axiom,
 (![X_ga_n22]: (p(cdecidable__linear__ordered__comm__ring(X_ga_n22)) => p(clinear__ordered__comm__ring(X_ga_n22))))).

fof(cdecidable__linear__ordered__semiring_o_to__linear__ordered__semiring, axiom,
 (![X_ga_n24]: (p(cdecidable__linear__ordered__semiring(X_ga_n24)) => p(clinear__ordered__semiring(X_ga_n24))))).

fof(cdiscrete__field_o_to__field, axiom, (![X_ga_n29]: (p(cdiscrete__field(X_ga_n29)) => p(cfield(X_ga_n29))))).

fof(cdiscrete__field_o_to__integral__domain, axiom,
 (![X_ga_n30]: (p(cdiscrete__field(X_ga_n30)) => (p(cdiscrete__field(X_ga_n30)) => p(cintegral__domain(X_ga_n30)))))).

fof(cdiscrete__linear__ordered__field_o_to__decidable__linear__ordered__comm__ring, axiom,
 (![X_ga_n32]:
  (p(cdiscrete__linear__ordered__field(X_ga_n32)) => p(cdecidable__linear__ordered__comm__ring(X_ga_n32))))).

fof(cdiscrete__linear__ordered__field_o_to__discrete__field, axiom,
 (![X_ga_n33]: (p(cdiscrete__linear__ordered__field(X_ga_n33)) => p(cdiscrete__field(X_ga_n33))))).

fof(cdiscrete__linear__ordered__field_o_to__linear__ordered__field, axiom,
 (![X_ga_n34]: (p(cdiscrete__linear__ordered__field(X_ga_n34)) => p(clinear__ordered__field(X_ga_n34))))).

fof(cdistrib_o_to__has__mul, axiom, (![X_ga_n36]: (p(cdistrib(X_ga_n36)) => p(chas__mul(X_ga_n36))))).

fof(cdivision__ring_o_to__has__inv, axiom, (![X_ga_n38]: (p(cdivision__ring(X_ga_n38)) => p(chas__inv(X_ga_n38))))).

fof(cdivision__ring_o_to__ring, axiom, (![X_ga_n39]: (p(cdivision__ring(X_ga_n39)) => p(cring(X_ga_n39))))).

fof(cdivision__ring_o_to__zero__ne__one__class, axiom,
 (![X_ga_n40]: (p(cdivision__ring(X_ga_n40)) => p(czero__ne__one__class(X_ga_n40))))).

fof(cdomain_o_to__no__zero__divisors, axiom, (![X_ga_n42]: (p(cdomain(X_ga_n42)) => p(cno__zero__divisors(X_ga_n42))))).

fof(cdomain_o_to__ring, axiom, (![X_ga_n43]: (p(cdomain(X_ga_n43)) => p(cring(X_ga_n43))))).

fof(cdomain_o_to__zero__ne__one__class, axiom,
 (![X_ga_n44]: (p(cdomain(X_ga_n44)) => p(czero__ne__one__class(X_ga_n44))))).

fof(ceq_o_mpr, axiom,
 (![X_ga_n48]:
  (![X_gb_n49]:
   ((X_ga_n48 = X_gb_n49) =>
    (![Xa_n51]: (t(Xa_n51, X_gb_n49) => t(a(ceq_o_mpr(X_ga_n48, X_gb_n49), Xa_n51), X_ga_n48))))))).

fof(ceq_o_mpr_o___proof__1, axiom, (![X_ga_n52]: (![X_gb_n53]: ((X_ga_n52 = X_gb_n53) => (X_gb_n53 = X_ga_n52))))).

fof(c__lambda_n58_o_eqn, axiom, (![X__x_n60]: (a(c__lambda_n58, X__x_n60) = X__x_n60))).

fof(ceq_o_mpr_o_equations_o___eqn__1, axiom,
 (![X_ga_n54]:
  (![X_gb_n55]:
   (![Xh_l1_n56]:
    (((ctrue_o_intro = ctrue_o_intro) & (X_ga_n54 = X_gb_n55)) =>
     (![Xh_l2_n57]:
      (t(Xh_l2_n57, X_gb_n55) =>
       (a(ceq_o_mpr(X_ga_n54, X_gb_n55), Xh_l2_n57) =
        a(a(ceq_o_rec__on(X_gb_n55, X_ga_n54), c__lambda_n58), Xh_l2_n57))))))))).

fof(ceq_o_rec, axiom,
 (![X_ga_n61]:
  (![Xa_n62]:
   (t(Xa_n62, X_ga_n61) =>
    (![XC_n63]:
     (![Xe__1_n64]:
      (t(Xe__1_n64, a(XC_n63, Xa_n62)) =>
       (![Xa_n65]:
        (t(Xa_n65, X_ga_n61) => ((Xa_n62 = Xa_n65) => t(a(ceq_o_rec(Xa_n65), Xe__1_n64), a(XC_n63, Xa_n65)))))))))))).

fof(ceq_o_rec__on, axiom,
 (![X_ga_n68]:
  (![Xa_n69]:
   (t(Xa_n69, X_ga_n68) =>
    (![XC_n70]:
     (![Xa_n71]:
      (t(Xa_n71, X_ga_n68) =>
       ((Xa_n69 = Xa_n71) =>
        (![Xe__1_n73]:
         (t(Xe__1_n73, a(XC_n70, Xa_n69)) =>
          t(a(a(ceq_o_rec__on(Xa_n69, Xa_n71), XC_n70), Xe__1_n73), a(XC_n70, Xa_n71)))))))))))).

fof(ceq_o_refl, axiom, (![X_ga_n75]: (![Xa_n76]: (t(Xa_n76, X_ga_n75) => (Xa_n76 = Xa_n76))))).

fof(ceq_o_symm, axiom,
 (![X_ga_n77]:
  (![Xa_n78]:
   (t(Xa_n78, X_ga_n77) => (![Xb_n79]: (t(Xb_n79, X_ga_n77) => ((Xa_n78 = Xb_n79) => (Xb_n79 = Xa_n78)))))))).

fof(cfield_o_to__comm__ring, axiom, (![X_ga_n81]: (p(cfield(X_ga_n81)) => p(ccomm__ring(X_ga_n81))))).

fof(cfield_o_to__division__ring, axiom, (![X_ga_n82]: (p(cfield(X_ga_n82)) => p(cdivision__ring(X_ga_n82))))).

fof(cgroup_o_to__has__inv, axiom, (![X_ga_n84]: (p(cgroup(X_ga_n84)) => p(chas__inv(X_ga_n84))))).

fof(cgroup_o_to__left__cancel__semigroup, axiom,
 (![X_ga_n85]: (p(cgroup(X_ga_n85)) => p(cleft__cancel__semigroup(X_ga_n85))))).

fof(cgroup_o_to__monoid, axiom, (![X_ga_n86]: (p(cgroup(X_ga_n86)) => p(cmonoid(X_ga_n86))))).

fof(cgroup_o_to__right__cancel__semigroup, axiom,
 (![X_ga_n87]: (p(cgroup(X_ga_n87)) => p(cright__cancel__semigroup(X_ga_n87))))).

fof(chas__inv_o_inv, axiom,
 (![X_ga_n89]:
  (p(chas__inv(X_ga_n89)) => (![Xa_n91]: (t(Xa_n91, X_ga_n89) => t(a(chas__inv_o_inv(X_ga_n89), Xa_n91), X_ga_n89)))))).

fof(chas__mul_o_mul, axiom,
 (![X_ga_n93]:
  (p(chas__mul(X_ga_n93)) =>
   (![Xa_n95]:
    (t(Xa_n95, X_ga_n93) =>
     (![Xa_n96]: (t(Xa_n96, X_ga_n93) => t(a(a(chas__mul_o_mul(X_ga_n93), Xa_n95), Xa_n96), X_ga_n93)))))))).

fof(chas__one_o_one, axiom, (![X_ga_n98]: (p(chas__one(X_ga_n98)) => t(chas__one_o_one(X_ga_n98), X_ga_n98)))).

fof(cid, axiom, (![X_ga_n100]: (![Xa_n101]: (t(Xa_n101, X_ga_n100) => t(a(a(cid, X_ga_n100), Xa_n101), X_ga_n100))))).

fof(cid_o_equations_o___eqn__1, axiom,
 (![X_ga_n102]: (![Xa_n103]: (t(Xa_n103, X_ga_n102) => (a(a(cid, X_ga_n102), Xa_n103) = Xa_n103))))).

fof(cintegral__domain_o_to__comm__ring, axiom,
 (![X_ga_n105]: (p(cintegral__domain(X_ga_n105)) => p(ccomm__ring(X_ga_n105))))).

fof(cintegral__domain_o_to__domain, axiom, (![X_ga_n106]: (p(cintegral__domain(X_ga_n106)) => p(cdomain(X_ga_n106))))).

fof(cintegral__domain_o_to__no__zero__divisors, axiom,
 (![X_ga_n107]: (p(cintegral__domain(X_ga_n107)) => p(cno__zero__divisors(X_ga_n107))))).

fof(cintegral__domain_o_to__nonzero__comm__ring, axiom,
 (![X_ga_n108]: (p(cintegral__domain(X_ga_n108)) => p(cnonzero__comm__ring(X_ga_n108))))).

fof(cintegral__domain_o_to__zero__ne__one__class, axiom,
 (![X_ga_n109]: (p(cintegral__domain(X_ga_n109)) => p(czero__ne__one__class(X_ga_n109))))).

fof(cleft__cancel__semigroup_o_to__semigroup, axiom,
 (![X_ga_n115]: (p(cleft__cancel__semigroup(X_ga_n115)) => p(csemigroup(X_ga_n115))))).

fof(clinear__nonneg__ring_o_to__decidable__linear__ordered__comm__ring, axiom,
 (![X_ga_n120]:
  (p(clinear__nonneg__ring(X_ga_n120)) =>
   (p(cis__commutative(chas__mul_o_mul(X_ga_n120))) => p(cdecidable__linear__ordered__comm__ring(X_ga_n120)))))).

fof(clinear__nonneg__ring_o_to__domain, axiom,
 (![X_ga_n121]: (p(clinear__nonneg__ring(X_ga_n121)) => p(cdomain(X_ga_n121))))).

fof(clinear__nonneg__ring_o_to__linear__ordered__ring, axiom,
 (![X_ga_n122]: (p(clinear__nonneg__ring(X_ga_n122)) => p(clinear__ordered__ring(X_ga_n122))))).

fof(clinear__nonneg__ring_o_to__nonneg__ring, axiom,
 (![X_ga_n123]: (p(clinear__nonneg__ring(X_ga_n123)) => p(cnonneg__ring(X_ga_n123))))).

fof(clinear__ordered__comm__ring_o_to__comm__monoid, axiom,
 (![X_ga_n125]: (p(clinear__ordered__comm__ring(X_ga_n125)) => p(ccomm__monoid(X_ga_n125))))).

fof(clinear__ordered__comm__ring_o_to__integral__domain, axiom,
 (![X_ga_n126]: (p(clinear__ordered__comm__ring(X_ga_n126)) => p(cintegral__domain(X_ga_n126))))).

fof(clinear__ordered__comm__ring_o_to__linear__ordered__ring, axiom,
 (![X_ga_n127]: (p(clinear__ordered__comm__ring(X_ga_n127)) => p(clinear__ordered__ring(X_ga_n127))))).

fof(clinear__ordered__field_o_to__field, axiom,
 (![X_ga_n129]: (p(clinear__ordered__field(X_ga_n129)) => p(cfield(X_ga_n129))))).

fof(clinear__ordered__field_o_to__linear__ordered__ring, axiom,
 (![X_ga_n130]: (p(clinear__ordered__field(X_ga_n130)) => p(clinear__ordered__ring(X_ga_n130))))).

fof(clinear__ordered__ring_o_to__domain, axiom,
 (![X_ga_n132]: (p(clinear__ordered__ring(X_ga_n132)) => p(cdomain(X_ga_n132))))).

fof(clinear__ordered__ring_o_to__linear__ordered__semiring, axiom,
 (![X_ga_n133]: (p(clinear__ordered__ring(X_ga_n133)) => p(clinear__ordered__semiring(X_ga_n133))))).

fof(clinear__ordered__ring_o_to__ordered__ring, axiom,
 (![X_ga_n134]: (p(clinear__ordered__ring(X_ga_n134)) => p(cordered__ring(X_ga_n134))))).

fof(clinear__ordered__semiring_o_to__ordered__semiring, axiom,
 (![X_ga_n136]: (p(clinear__ordered__semiring(X_ga_n136)) => p(cordered__semiring(X_ga_n136))))).

fof(cmonoid_o_to__has__one, axiom, (![X_ga_n138]: (p(cmonoid(X_ga_n138)) => p(chas__one(X_ga_n138))))).

fof(cmonoid_o_to__semigroup, axiom, (![X_ga_n139]: (p(cmonoid(X_ga_n139)) => p(csemigroup(X_ga_n139))))).

fof(cmul__assoc, axiom,
 (![X_ga_n140]:
  (p(csemigroup(X_ga_n140)) =>
   (![Xa_n141]:
    (t(Xa_n141, X_ga_n140) =>
     (![Xb_n142]:
      (t(Xb_n142, X_ga_n140) =>
       (![Xc_n143]:
        (t(Xc_n143, X_ga_n140) =>
         (a(a(chas__mul_o_mul(X_ga_n140), a(a(chas__mul_o_mul(X_ga_n140), Xa_n141), Xb_n142)), Xc_n143) =
          a(a(chas__mul_o_mul(X_ga_n140), Xa_n141), a(a(chas__mul_o_mul(X_ga_n140), Xb_n142), Xc_n143)))))))))))).

fof(cmul__left__inv, axiom,
 (![X_ga_n144]:
  (p(cgroup(X_ga_n144)) =>
   (![Xa_n145]:
    (t(Xa_n145, X_ga_n144) =>
     (a(a(chas__mul_o_mul(X_ga_n144), a(chas__inv_o_inv(X_ga_n144), Xa_n145)), Xa_n145) =
      chas__one_o_one(X_ga_n144))))))).

fof(cmul__zero__class_o_to__has__mul, axiom,
 (![X_ga_n147]: (p(cmul__zero__class(X_ga_n147)) => p(chas__mul(X_ga_n147))))).

fof(cno__zero__divisors_o_to__has__mul, axiom,
 (![X_ga_n149]: (p(cno__zero__divisors(X_ga_n149)) => p(chas__mul(X_ga_n149))))).

fof(cnonneg__ring_o_to__ordered__ring, axiom,
 (![X_ga_n151]: (p(cnonneg__ring(X_ga_n151)) => p(cordered__ring(X_ga_n151))))).

fof(cnonneg__ring_o_to__ring, axiom, (![X_ga_n152]: (p(cnonneg__ring(X_ga_n152)) => p(cring(X_ga_n152))))).

fof(cnonneg__ring_o_to__zero__ne__one__class, axiom,
 (![X_ga_n153]: (p(cnonneg__ring(X_ga_n153)) => p(czero__ne__one__class(X_ga_n153))))).

fof(cnonzero__comm__ring_o_to__comm__ring, axiom,
 (![X_ga_n155]: (p(cnonzero__comm__ring(X_ga_n155)) => p(ccomm__ring(X_ga_n155))))).

fof(cnonzero__comm__ring_o_to__nonzero__comm__semiring, axiom,
 (![X_ga_n156]: (p(cnonzero__comm__ring(X_ga_n156)) => p(cnonzero__comm__semiring(X_ga_n156))))).

fof(cnonzero__comm__ring_o_to__zero__ne__one__class, axiom,
 (![X_ga_n157]: (p(cnonzero__comm__ring(X_ga_n157)) => p(czero__ne__one__class(X_ga_n157))))).

fof(cnonzero__comm__semiring_o_to__comm__semiring, axiom,
 (![X_ga_n159]: (p(cnonzero__comm__semiring(X_ga_n159)) => p(ccomm__semiring(X_ga_n159))))).

fof(cnonzero__comm__semiring_o_to__zero__ne__one__class, axiom,
 (![X_ga_n160]: (p(cnonzero__comm__semiring(X_ga_n160)) => p(czero__ne__one__class(X_ga_n160))))).

fof(cone__mul, axiom,
 (![X_ga_n161]:
  (p(cmonoid(X_ga_n161)) =>
   (![Xa_n162]:
    (t(Xa_n162, X_ga_n161) => (a(a(chas__mul_o_mul(X_ga_n161), chas__one_o_one(X_ga_n161)), Xa_n162) = Xa_n162)))))).

fof(cordered__ring_o_to__ordered__semiring, axiom,
 (![X_ga_n164]: (p(cordered__ring(X_ga_n164)) => p(cordered__semiring(X_ga_n164))))).

fof(cordered__ring_o_to__ring, axiom, (![X_ga_n165]: (p(cordered__ring(X_ga_n165)) => p(cring(X_ga_n165))))).

fof(cordered__ring_o_to__zero__ne__one__class, axiom,
 (![X_ga_n166]: (p(cordered__ring(X_ga_n166)) => p(czero__ne__one__class(X_ga_n166))))).

fof(cordered__semiring_o_to__semiring, axiom,
 (![X_ga_n168]: (p(cordered__semiring(X_ga_n168)) => p(csemiring(X_ga_n168))))).

fof(cright__cancel__semigroup_o_to__semigroup, axiom,
 (![X_ga_n170]: (p(cright__cancel__semigroup(X_ga_n170)) => p(csemigroup(X_ga_n170))))).

fof(cring_o_to__distrib, axiom, (![X_ga_n172]: (p(cring(X_ga_n172)) => p(cdistrib(X_ga_n172))))).

fof(cring_o_to__monoid, axiom, (![X_ga_n173]: (p(cring(X_ga_n173)) => p(cmonoid(X_ga_n173))))).

fof(cring_o_to__semiring, axiom, (![X_ga_n174]: (p(cring(X_ga_n174)) => p(csemiring(X_ga_n174))))).

fof(csemigroup_o_to__has__mul, axiom, (![X_ga_n176]: (p(csemigroup(X_ga_n176)) => p(chas__mul(X_ga_n176))))).

fof(csemiring_o_to__distrib, axiom, (![X_ga_n178]: (p(csemiring(X_ga_n178)) => p(cdistrib(X_ga_n178))))).

fof(csemiring_o_to__monoid, axiom, (![X_ga_n179]: (p(csemiring(X_ga_n179)) => p(cmonoid(X_ga_n179))))).

fof(csemiring_o_to__mul__zero__class, axiom,
 (![X_ga_n180]: (p(csemiring(X_ga_n180)) => p(cmul__zero__class(X_ga_n180))))).

fof(czero__ne__one__class_o_to__has__one, axiom,
 (![X_ga_n182]: (p(czero__ne__one__class(X_ga_n182)) => p(chas__one(X_ga_n182))))).

fof(c__inst__1_n184, axiom, p(cgroup(c_ga_n183))).

fof(ca_n185, axiom, t(ca_n185, c_ga_n183)).

fof(cb_n186, axiom, t(cb_n186, c_ga_n183)).

fof(c__goal, conjecture,
 (a(a(chas__mul_o_mul(c_ga_n183), a(chas__inv_o_inv(c_ga_n183), ca_n185)),
   a(a(chas__mul_o_mul(c_ga_n183), ca_n185), cb_n186)) =
  cb_n186)).