Step * of Lemma ancestral-logic-example1

(∀x,y:Dom.  ((P y)  (Q y)))  (∀x,y:Dom.  (TC(λa,b.P b)(x,y)  TC(λa,b.Q b)(x,y)))
BY
StartFO }

1
⊢ (∀x,y:Dom.  ((P y)  (Q y)))  (∀x,y:Dom.  (TC(λa,b.P b)(x,y)  TC(λa,b.Q b)(x,y)))


Latex:


(\mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  (Q  x  y)))  {}\mRightarrow{}  (\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.P  a  b)(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.Q  a  b)(x,y)))


By

StartFO




Home Index