(16steps 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: sframe-rule 1 1
...
By: Thin -4 THEN Analyze -3 THEN Analyze -4 THEN All Reduce THEN RenameVar `j' -5
THEN
RenameVar `t' -4
THEN
Decide isnull(a(j;t))
THEN
Try (Assert False THEN Unhide THEN Complete Auto)

Generated subgoal:

1 13. j : Id
14. t : 
15. isnull(a(j;t))  [not for witness]
16. j = i
17. null(filter(m.mtag(m) = tg;sends(l;<j,t>)))
18. isnull(a(j;t))
  (kind(<j,t>)  L)
12 steps

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

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