Nuprl - Pf vcs mng wf

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

vs:VCs{i}, ds,da:Collection{i}(dec()), de:sig(), rho:Decl{i}, e:{sig_mng{i:l}(de; rho)}, s:{[[ds]] rho}, tr:trace_env([[da]] rho). tc_vcs{i}(vs;ds;da;de) (vvs.trace_consistent_vc(rho;da;tr.proj;v)) [[vs]] rho ds da de e s tr Prop{i'}

By: Unfolds [`vcs`;`vcs_mng`] 0 THEN All (Unfolds [`decl`;`col`]) THEN Try ((AllHyps (Unfold `tc_vcs`)) THEN BackThruSomeHyp)

Generated subgoals:

1 1. vs: vc{i:l}()Prop{i'}
2. ds: dec()Prop{i}
3. da: dec()Prop{i}
4. de: sig()
5. rho: LabelType{i}
6. e: {sig_mng{i:l} (de; rho)}
7. s: {[[ds]] rho}
8. tr: trace_env([[da]] rho)
9. tc_vcs{i}(vs;ds;da;de)
10. (vvs.trace_consistent_vc(rho;da;tr.proj;v))
11. v: vc{i:l}()
12. v vs
trace_consistent_vc(rho;da;tr.proj;v)

2 1. vs: vc{i:l}()Prop{i'}
2. ds: dec()Prop{i}
3. da: dec()Prop{i}
4. de: sig()
5. rho: LabelType{i}
6. e: {sig_mng{i:l} (de; rho)}
7. s: {[[ds]] rho}
8. tr: trace_env([[da]] rho)
vs VCs{i}

About:

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

1	1. `vs:` `vc{i:l}()Prop{i'}` 2. `ds:` `dec()Prop{i}` 3. `da:` `dec()Prop{i}` 4. `de:` `sig()` 5. `rho:` `LabelType{i}` 6. `e:` `{sig_mng{i:l} (de; rho)}` 7. `s:` `{[[ds]] rho}` 8. `tr:` `trace_env([[da]] rho)` 9. `tc_vcs{i}(vs;ds;da;de)` 10. `(vvs.trace_consistent_vc(rho;da;tr.proj;v))` 11. `v:` `vc{i:l}()` 12. `v vs` `trace_consistent_vc(rho;da;tr.proj;v)`
2	1. `vs:` `vc{i:l}()Prop{i'}` 2. `ds:` `dec()Prop{i}` 3. `da:` `dec()Prop{i}` 4. `de:` `sig()` 5. `rho:` `LabelType{i}` 6. `e:` `{sig_mng{i:l} (de; rho)}` 7. `s:` `{[[ds]] rho}` 8. `tr:` `trace_env([[da]] rho)` `vs VCs{i}`