By:	Thin -4 THEN HypSubst -3 -1 THEN AllHyps (h.InstHyp [i;t] h THENA Complete Auto) THEN ThinForallHyps THEN Subst ((eqof(IdDeq)(i,i)) ~ true) -1 THEN Reduce -1 THEN Try (BackThru Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true) THEN ExRepD

1

8. j : Id 9. t :  10. j = i 11. null(filter(m.mtag(m) = tg;sends(l;<j,t>))) 12. isnull(a(i;t)) 13. islocal(kind(a(i;t))) 13.  13. deq-member(IdDeq;act(kind(a(i;t)));1of()) 13.  13. 2of()(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))) 14. x:Id.  14. deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of()) 14.  14. s(i;t+1).x 14. = 14. 2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t))) 14.  if deq-member(IdDeq;x;1of()) 2of()(x) else Top fi 15. l@0:IdLnk.  15. deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l@0>;1of()) 15.  15. withlnk(l@0;m(i;t)) 15. = 15. if source(l@0) = i 15. if concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf) 15. if concat(map(tgf.map(x.<1of(tgf),x>;((x.s(i;t).x) 15. if concat(map(tgf.map(x.<1of(tgf),x>;,val(a(i;t))));2of() 15. if concat(map(tgf.map(x.<1of(tgf),x>;,val(a(i;t))));(<kind(a(i;t)),l@0>))) 15. else nil fi 15.  (tg@0:Id 15.  (if source(l@0) = i <,,,,,,,<[<l,tg>],x.L>,>.da(rcv(l@0; tg@0)) 15.  (else Top fi) List 16. x:Id.  16. (deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x))) 16.  16. s(i;t).x = s(i;t+1).x  if deq-member(IdDeq;x;1of()) 2of()(x) else Top fi 17. l@0:IdLnk, tg@0:Id. 17. ((eqof(product-deq(IdLnk;Id;IdLnkDeq;IdDeq))(<l,tg>,<l@0,tg@0>)  false) 17. ( 17. (deq-member(KindDeq;kind(a(i;t));L)) 17.  17. w-tagged(tg@0; onlnk(l@0;m(i;t))) = nil  Msg List   (kind(<j,t>)  L)

11 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html