Nuprl - Pf tc ioa inv vc

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

A:ioa{i:l}(), I:Fmla, de:sig(). tc_ioa(A;de) tc_pred(I;A.ds; < > ;de) covers_pred(A;I) closed_pred(I) single_valued_decls(A.ds) tc_vcs{i}(VCs(A;I);A.ds;A.da;de)

By: Auto THEN Unfolds [`tc_vcs`;`ioa_inv_vc`] 0 THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 1. A: ioa{i:l}()
2. I: Fmla
3. de: sig()
4. tc_ioa(A;de)
5. tc_pred(I;A.ds; < > ;de)
6. covers_pred(A;I)
7. closed_pred(I)
8. single_valued_decls(A.ds)
9. v: vc{i:l}()
10. v < *vc_imp(mk_imp(A.init, I))* > +* ioa_trans_all{i}(A;I)
tc_vc(v;A.ds;A.da;de)

2 1. A: ioa{i:l}()
2. I: Fmla{i}
3. de: sig()
4. tc_ioa(A;de)
5. tc_pred(I;A.ds; < > ;de)
6. covers_pred(A;I)
7. closed_pred(I)
8. single_valued_decls(A.ds)
9. v: vc{i:l}()
( < *vc_imp(mk_imp(A.init, I))* > {i} +* ioa_trans_all{i}(A;I)) Collection{i'}(vc{i:l}())

About:

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

1	1. `A:` `ioa{i:l}()` 2. `I:` `Fmla` 3. `de:` `sig()` 4. `tc_ioa(A;de)` 5. `tc_pred(I;A.ds; < > ;de)` 6. `covers_pred(A;I)` 7. `closed_pred(I)` 8. `single_valued_decls(A.ds)` 9. `v:` `vc{i:l}()` 10. `v < vc_imp(mk_imp(A.init, I)) > +* ioa_trans_all{i}(A;I)` `tc_vc(v;A.ds;A.da;de)`
2	1. `A:` `ioa{i:l}()` 2. `I:` `Fmla{i}` 3. `de:` `sig()` 4. `tc_ioa(A;de)` 5. `tc_pred(I;A.ds; < > ;de)` 6. `covers_pred(A;I)` 7. `closed_pred(I)` 8. `single_valued_decls(A.ds)` 9. `v:` `vc{i:l}()` `( < vc_imp(mk_imp(A.init, I)) > {i} +* ioa_trans_all{i}(A;I)) Collection{i'}(vc{i:l}())`