Nuprl Lemma : ancestral-logic-induction

(∀x,y:Dom.  ((R y)  (B x)  (B y)))  (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (B x)  (B 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-min-uniform
(\mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y)))  {}\mRightarrow{}  (\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y)))



Date html generated: 2015_07_17-AM-07_52_56
Last ObjectModification: 2015_01_30-AM-09_47_11

Home Index