Nuprl - Pf trace consistent action pre

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

A:ioa{i:l}(), rho:Decl, te:(LabelLabel), k:Label. ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;action_pre(k;A.pre))

By: Unfold `trace_consistent_pred` 0 THEN Unfold `col_all` 0 THEN Try (Fold `pred` 0)

Generated subgoal:

1 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)

About:

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