§5.4 BCK Games for LCM and Cut.                     Version with Constructive Implication.

LCM with Constructive Implication and Cut rule: using Minimum Principle, prove that the unequation f(x)≤f(x+27) has a solution.
A Cut between: ∃x.∀y.f(x)≤f(y) and (∃x.∀y.f(x)≤f(y) ⇒ ∃x.(  f(x)≤f(x+27)  )

LCM with Constructive Implication and Cut rule: using Minimum Principle, prove that the system f(x)≤f(g(x))∧f(x)≤f(h(x)) has a solution.
A Cut between: ∃x.∀y.f(x)≤f(y) and (∃x.∀y.f(x)≤f(y) ⇒ ∃x.(  f(x)≤f(g(x))  ∧  f(x)≤f(h(x)) ))


Created by Mathematica  (November 11, 2006)