mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ma-is-empty(M)
Def == fpf-is-empty(1of(M))fpf-is-empty(1of(2of(M)))
Def == fpf-is-empty(1of(2of(2of(M))))fpf-is-empty(1of(2of(2of(2of(M)))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(M))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(M)))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(M))))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(2of(M)))))))))

is mentioned by

Thm* D:Dsys, L:Id List.
Thm* (i:Id. (i  L)  ma-is-empty(M(i)))
Thm* 
Thm* (i:Id. Feasible(M(i)))
Thm* 
Thm* (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L)
Thm* (iL.(ltgma-outlinks(M(i);i).
Thm* interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
Thm* 
Thm* d-feasible(D)		[finite-support-feasible]
Thm* L:MsgA List. ma-is-empty((L))  reduce(M,x. ma-is-empty(M) & x;True;L)[assert-ma-join-list-is-empty]
Thm* L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L)[ma-join-list-is-empty]

In prior sections: mb event system 5

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 6 Sections EventSystems Doc