Nuprl - Pf tc ioa inv vc 1 2 2 2 1 1 1

(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. a: dec()
11. a A.da
12. r: rel()
13. r (rI.smts_eff_rel(action_effect(a.lbl;A.eff;A.frame);r))
14. r1: rel()
15. r1 I
16. as: (LabelTerm) List
17. 1of(unzip(as)) = rel_vars(r1)
18. i:. i < ||as|| 2of(as[i]) (x.smts_eff(action_effect(a.lbl;A.eff;A.frame);x))(1of(as[i]))
19. r = rel_subst(as;r1)

tc(r1;A.ds;dec_lookup(A.da;a.lbl);de)

By: AllHyps (i.(Unfolds [`closed_pred`;`tc_pred`] i) THEN (InstHyp [r1] i)) THEN Using [`da1', < > ] (BackThru Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de))

Generated subgoals:

None

About:

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