Nuprl - Pf trace consistent action pre 1

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

1. A: ioa{i:l}()
2. rho: Decl
3. te: LabelLabel
4. k: Label
5. ioa_mentions_trace(A)
6. r: rel()
7. r action_pre(k;A.pre)

trace_consistent_rel(rho;A.da;te;r)

By: BackThru Thm* rho:Decl, r:rel(), da:Collection(dec()), R:(LabelLabel). rel_mentions_trace(r) trace_consistent_rel(rho;da;R;r) THEN AllHyps (h.(Unfold `ioa_mentions_trace` h) THEN (ParallelOp h)) THEN OrLeft THEN OrRight

Generated subgoal:

1 5. r: rel()
6. r action_pre(k;A.pre)
7. rel_mentions_trace(r)
p:pre(). p A.pre & rel_mentions_trace(p.rel)

About:

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