§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)