Nuprl - Pf decls_mng_singleton 1 1 1

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

1. d: dec()
2. rho: Decl
3. s: l:Labeldecl_type([[d]] rho;l)
4. x1: Label
5. x: decl_type([[d]] rho;x1)
6. d1: dec()
7. d1 = d

x decl_type([[d1]] rho;x1)

By: All (Unfolds [`decl_type`;`dec_mng`]) THEN All (Unfold `dbase`) THEN Analyze -2 THEN Analyze 1 THEN All Reduce

Generated subgoal:

1 1. l1: Label
2. d3: SimpleType
3. rho: Decl
4. s: l:Labelif l = l1 [[d3]] rho else Top fi
5. x1: Label
6. x: if x1 = l1 [[d3]] rho else Top fi
7. lbl: Label
8. d2: SimpleType
9. < lbl,d2 > = < l1,d3 > dec()
x if x1 = lbl [[d2]] rho else Top fi

About:

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