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


Proof




Definitions occuring in Statement :  TC: TC(λx,y.F[x; y])(a,b) language1: language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) all: x:A. B[x] implies:  Q apply: a
Lemmas :  all_wf TC-base TC-min-uniform TC_wf TC-trans
(\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)))



Date html generated: 2015_07_17-AM-07_53_00
Last ObjectModification: 2015_01_30-AM-09_47_13

Home Index