Nuprl Lemma : ancestral-logic-example2

x,y:Dom.  (TC(λa,b.TC(λi,j.P j)(a,b))(x,y)  TC(λa,b.P 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 :  TC_wf TC-min-uniform TC-trans
\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.TC(\mlambda{}i,j.P  i  j)(a,b))(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,y))



Date html generated: 2015_07_17-AM-07_53_02
Last ObjectModification: 2015_01_30-AM-09_47_08

Home Index