Nuprl - Pf ioa all mng state 1 1 1 1

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

1. I: Type
2. A: Iioa{i:l}()
3. rho: Decl
4. de: sig()
5. e: {[[de]] rho}
6. s: l:Labeldecl_type([[ioa_all(I; i.A(i)).ds]] rho;l)
7. i: I
8. x1: Label
9. x: [[ioa_all(I; i.A(i)).ds]] rho(x1)

x [[A(i).ds]] rho(x1)

By: Using [`ds1',ioa_all(I; i.A(i)).ds] (BackThru Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x))

Generated subgoal:

1 10. d: dec()
11. d A(i).ds
12. d.lbl = x1
d ioa_all(I; i.A(i)).ds

About:

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