Extra rhs terms in formal equations

[siddhartha-gadgil]

• These are tracked by the logging.
• Problem may be domain of a Pi-type or a lambda
• Here is the first part of the logs.

  2020.06.05 11:34:49 [ERROR] provingground.learning.LocalProverStep.$anonfun:414:42 - for type: (`c : M ) ~> ((((eqM) (n)) (`c)) → (((eqM) (((mul) (n)) (n))) (((mul) (`c)) (n))))
  P₁(M ∈ Typs)
  orphan in generated (P₁((`c : M ) ~> ((((eqM) (n)) (`c)) → (((eqM) (((mul) (n)) (n))) (((mul) (`c)) (n)))) ∈ Typs) =) ((Coeff(FlatMap(Typs,PiIsle,Typs))) * (P₁(M ∈ Typs))) * (P₁(InIsle((((eqM) (n)) (`c)) → (((eqM) (((mul) (n)) (n))) (((mul) (`c)) (n))) ∈ Typs,`c,Island(Typs,Typs,AddVar,Pi,EnterIsle))))
  2020.06.05 11:34:49 [ERROR] provingground.learning.LocalProverStep.$anonfun:414:42 - for type: (`c : M ) ~> ((((eqM) (n)) (`c)) → (((eqM) (((mul) (n)) (n))) (((mul) (`c)) (n))))
  P₁(InIsle(((eqM) (n)) (`c) ∈ Typs,`c,Island(Typs,Typs,AddVar,Pi,EnterIsle)))
  orphan in generated (P₁(InIsle((((eqM) (n)) (`c)) → (((eqM) (((mul) (n)) (n))) (((mul) (`c)) (n))) ∈ Typs,`c,Island(Typs,Typs,AddVar,Pi,EnterIsle))) =) ((Coeff(FlatMap(Typs,PiIsle,Typs))) * (P₁(InIsle(((eqM) (n)) (`c) ∈ Typs,`c,Island(Typs,Typs,AddVar,Pi,EnterIsle))))) * (P₁(InIsle(InIsle(((eqM) (((mul) (n)) (n))) (((mul) (`c)) (n)) ∈ Typs,@a,Island(Typs,Typs,AddVar,Pi,EnterIsle)),`c,Island(Typs,Typs,AddVar,Pi,EnterIsle))))
  2020.06.05 11:34:49 [ERROR] provingground.learning.LocalProverStep.$anonfun:414:42 - for type: (`b : M ) ~> ((`c : M ) ~> ((((eqM) (`b)) (`c)) → (((eqM) (((mul) (`b)) (((mul) (m)) (n)))) (((mul) (`c)) (((mul) (m)) (n))))))
  P₁(M ∈ Typs)
  orphan in generated (P₁((`b : M ) ~> ((`c : M ) ~> ((((eqM) (`b)) (`c)) → (((eqM) (((mul) (`b)) (((mul) (m)) (n)))) (((mul) (`c)) (((mul) (m)) (n)))))) ∈ Typs) =) ((Coeff(FlatMap(Typs,PiIsle,Typs))) * (P₁(M ∈ Typs))) * (P₁(InIsle((`c : M ) ~> ((((eqM) (`b)) (`c)) → (((eqM) (((mul) (`b)) (((mul) (m)) (n)))) (((mul) (`c)) (((mul) (m)) (n))))) ∈ Typs,`b,Island(Typs,Typs,AddVar,Pi,EnterIsle))))

[siddhartha-gadgil]

There are still events that are not in the lhs, this time for generated equations. It was not noticed because sub-terms ignored quotients. A sample log is as follows.

2020.06.05 13:44:42 [ERROR] provingground.learning.LocalProverStep.$anonfun:414:42 - for type: (`c : M ) ~> ((((eqM) (n)) (`c)) → (((eqM) (((mul) (n)) (n))) (((mul) (`c)) (n))))
P₁(InIsle({Terms ∈ Restrict(FuncOpt)},`c,Island(Typs,Typs,AddVar,Pi,EnterIsle)))
 orphan in generated (P₁(InIsle(Wrap(eqM) ∈ Funcs,`c,Island(Typs,Typs,AddVar,Pi,EnterIsle))) =) (P₁(InIsle(eqM ∈ Terms,`c,Island(Typs,Typs,AddVar,Pi,EnterIsle)))) / (P₁(InIsle({Terms ∈ Restrict(FuncOpt)},`c,Island(Typs,Typs,AddVar,Pi,EnterIsle))))

[siddhartha-gadgil]

A simpler example, showing this is not because of islands.

2020.06.05 13:44:42 [ERROR] provingground.learning.LocalProverStep.$anonfun:414:42 - for type:
 (((eqM) (m)) (n)) → (((eqM) (n)) (m))
P₁({Terms ∈ Restrict(FuncOpt)})
 orphan in generated (P₁(Wrap(eqM) ∈ Funcs) =) (P₁(eqM ∈ Terms)) / (P₁({Terms ∈ Restrict(FuncOpt)}))