1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. Top
19. d3 : x:Id fp-> Type
20. d4 : a:Knd fp-> Type
21. i2 : x:Id fp-> d3(x)?Void
22. p2 : a:Id fp-> State(d3)d4(locl(a))?TopProp
23. e2 : kx:KndId fp-> State(d3)d4(1of(kx))?Topd3(2of(kx))?Void
24. s3 : 
24. kl:KndIdLnk fp-> (tg:Id
24. kl:KndIdLnk fp-> (State(d3)d4(1of(kl))?Top
24. kl:KndIdLnk fp-> ((d4(rcv(2of(kl); tg))?Void List)) List
25. f2 : x:Id fp-> Knd List
26. s4 : ltg:IdLnkId fp-> Knd List
27. Top
28. ds || d1 & da || d2
28. & init || i1
28. & pre || p1
28. & ef || e1
28. & send || s1
28. & frame || f1
28. & sframe || s2
29. kx:(KndId). 
29. (kx  dom(ef)
29. (
29. (2of(kx)  dom(frame)
29. (
29. (2of(kx)  dom(f1)  deq-member(KindDeq;1of(kx);f1(2of(kx))))
29. & (kx  dom(e1)
29. & (
29. & (2of(kx)  dom(f1)
29. & (
29. & (2of(kx)  dom(frame)  deq-member(KindDeq;1of(kx);frame(2of(kx))))
30. kl:(KndIdLnk), tg:Id.
30. (kl  dom(send)
30. (
30. ((tg  map(p.1of(p);send(kl)))
30. (
30. (<2of(kl),tg>  dom(sframe)
30. (
30. (<2of(kl),tg>  dom(s2)  deq-member(KindDeq;1of(kl);s2(<2of(kl),tg>)))
30. & (kl  dom(s1)
30. & (
30. & ((tg  map(p.1of(p);s1(kl)))
30. & (
30. & (<2of(kl),tg>  dom(s2)
30. & (
30. & (<2of(kl),tg>  dom(sframe)
30. & (
30. & (deq-member(KindDeq;1of(kl);sframe(<2of(kl),tg>)))
31. d3 || ds & d4 || da
31. & i2 || init
31. & p2 || pre
31. & e2 || ef
31. & s3 || send
31. & f2 || frame
31. & s4 || sframe
32. kx:(KndId). 
32. (kx  dom(e2)
32. (
32. (2of(kx)  dom(f2)
32. (
32. (2of(kx)  dom(frame)  deq-member(KindDeq;1of(kx);frame(2of(kx))))
32. & (kx  dom(ef)
32. & (
32. & (2of(kx)  dom(frame)
32. & (
32. & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))
33. kl:(KndIdLnk), tg:Id.
33. (kl  dom(s3)
33. (
33. ((tg  map(p.1of(p);s3(kl)))
33. (
33. (<2of(kl),tg>  dom(s4)
33. (
33. (<2of(kl),tg>  dom(sframe)
33. (
33. (deq-member(KindDeq;1of(kl);sframe(<2of(kl),tg>)))
33. & (kl  dom(send)
33. & (
33. & ((tg  map(p.1of(p);send(kl)))
33. & (
33. & (<2of(kl),tg>  dom(sframe)
33. & (
33. & (<2of(kl),tg>  dom(s4)  deq-member(KindDeq;1of(kl);s4(<2of(kl),tg>)))
34. d3 || d1 & d4 || d2
34. & i2 || i1
34. & p2 || p1
34. & e2 || e1
34. & s3 || s1
34. & f2 || f1
34. & s4 || s2
35. kx:(KndId). 
35. (kx  dom(e2)
35. (
35. (2of(kx)  dom(f2)
35. (
35. (2of(kx)  dom(f1)  deq-member(KindDeq;1of(kx);f1(2of(kx))))
35. & (kx  dom(e1)
35. & (
35. & (2of(kx)  dom(f1)
35. & (
35. & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))
36. kl:(KndIdLnk), tg:Id.
36. (kl  dom(s3)
36. (
36. ((tg  map(p.1of(p);s3(kl)))
36. (
36. (<2of(kl),tg>  dom(s4)
36. (
36. (<2of(kl),tg>  dom(s2)  deq-member(KindDeq;1of(kl);s2(<2of(kl),tg>)))
36. & (kl  dom(s1)
36. & (
36. & ((tg  map(p.1of(p);s1(kl)))
36. & (
36. & (<2of(kl),tg>  dom(s2)
36. & (
36. & (<2of(kl),tg>  dom(s4)  deq-member(KindDeq;1of(kl);s4(<2of(kl),tg>)))
  kx:(KndId). 
  (kx  dom(e2)
  (
  (2of(kx)  dom(f2)
  (
  (2of(kx)  dom(frame  f1)
  (
  (deq-member(KindDeq;1of(kx);frame  f1(2of(kx))))
  & (kx  dom(ef  e1)
  & (
  & (2of(kx)  dom(frame  f1)
  & (
  & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))

By:

Auto THEN Try (RWO (Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. (Thm* x  dom(f  g)  x  dom(f)  x  dom(g) (-3 (THEN (Analyze -3 (THEN (AllHyps ((h. ((BackThru h THEN ParallelOp -2 ((THEN ((RWO ((Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. ((Thm* x  dom(f  g)  x  dom(f)  x  dom(g) ((0 ((THEN ((((OrRight THEN Complete Auto) ORELSE (OrLeft THEN Complete Auto)))) THEN Try (RWO (Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A. (Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi (0 (THEN (RWO (Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. (Thm* x  dom(f  g)  x  dom(f)  x  dom(g) (-1 (THEN (SplitOnConclITE (THEN (BackThruSomeHyp (THEN (SplitOrHyps)

None

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