Nuprl - Pf tc ioa inv vc 1 2

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

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 ioa_trans_all{i}(A;I)

tc_vc(v;A.ds;A.da;de)

By: All (Unfold `ioa_trans_all`) THEN RWW "member_col_map" -1 THEN ExRepD THEN HypSubst -1 0

Generated subgoals:

1 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}()
10. v < ioa_trans(A;a.lbl;I) | a A.da >
A ioa{i':l}

2 10. a: dec()
11. a A.da
12. v = ioa_trans(A;a.lbl;I)
tc_vc(ioa_trans(A;a.lbl;I);A.ds;A.da;de)

About:

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

1	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}()` 10. `v < ioa_trans(A;a.lbl;I) \| a A.da >` `A ioa{i':l}`
2	10. `a:` `dec()` 11. `a A.da` 12. `v = ioa_trans(A;a.lbl;I)` `tc_vc(ioa_trans(A;a.lbl;I);A.ds;A.da;de)`