Nuprl - Pf trace consistent ioa inv vc

(2steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

A:ioa{i:l}(), I:Fmla, rho:Decl, te:(LabelLabel). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;I) (vVCs(A;I).trace_consistent_vc(rho;A.da;te;v))

By: Unfold `col_all` 0 THEN Try (Fold `vcs` 0) THEN Reduce 0

Generated subgoal:

1 1. A: ioa{i:l}()
2. I: Fmla
3. rho: Decl
4. te: LabelLabel
5. ioa_mentions_trace(A)
6. trace_consistent_pred(rho;A.da;te;I)
7. v: vc{i:l}()
8. v VCs(A;I)
trace_consistent_vc(rho;A.da;te;v)

About:

(2steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc