Nuprl - Pf trace consistent init 1

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

1. A: ioa{i:l}()
2. rho: Decl
3. te: LabelLabel
4. ioa_mentions_trace(A)
5. r: rel()
6. r A.init

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 OrRight THEN InstConcl [r]

Generated subgoals:

None

About:

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