(40steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-support-feasible
  D:Dsys, L:Id List.
  (i:Id. (i  L)  ma-is-empty(M(i)))
  
  (i:Id. Feasible(M(i)))
  
  (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L)
  (iL.(ltgma-outlinks(M(i);i).
  interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
  
  d-feasible(D)
By: Auto THEN Analyze 0 THEN Try Trivial THEN Analyze 0

Generated subgoals:

1 1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
5. (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L)
5. (iL.(ltgma-outlinks(M(i);i).
5. interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
  l:IdLnk, tg:Id. M(source(l)).dout(l,tg) r M(destination(l)).din(l,tg)
28 steps
2 1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
5. (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L)
5. (iL.(ltgma-outlinks(M(i);i).
5. interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
  i:Id. 
  finite-type({l:IdLnk| destination(l) = i & M(source(l)) sends on link l })
11 steps

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

(40steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc