Nuprl - mb automata 4 LEMMAs for trace consistent wp

Rank	Theorem	Name
5			Thm* A:ioa{i:l}(), Q:Fmla, rho:Decl, R:(LabelLabel), k:Label. ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;R;Q) trace_consistent_pred(rho;A.da;R;wp(A;k;Q))	[trace_consistent_wp]
cites
4			Thm* A:ioa{i:l}(), rho:Decl, r:rel(), R:(LabelLabel), k:Label. ioa_mentions_trace(A) trace_consistent_rel(rho;A.da;R;r) trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r))	[trace_consistent_wp_rel]