Nuprl - Pf decls_mng_member 1 1 1 2

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

1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. x: Label
4. rho: Decl
5. v: d:{d:dec()| d ds1 }. [[d]] rho(x)
6. d:dec(). d ds2 d.lbl = x d ds1
7. d: {d:dec()| d ds2 }
8. d.lbl = x

v [[d]] rho(x)

By: Analyze -2 THEN Analyze -3 THEN Unfold `dec_mng` 0 THEN Unfold `dbase` 0 THEN All Reduce

Generated subgoal:

1 7. lbl: Label
8. d1: SimpleType
9. < lbl,d1 > ds2
10. lbl = x
v if x = lbl [[d1]] rho else Top fi

About:

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