Definitions GenAutomata Sections NuprlLIB Doc

No mentions to report in GenAutomata
right_ptnDef right_ptn(l) == Case(l) Case ptn_pr( < x, y > ) = > y Default = > l
Thm* l:Pattern. right_ptn(l) Pattern
case_default Def Default = > body(value,value) == body
case_lbl_pair Def Case ptn_pr( < x, y > ) = > body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. InjCase(x2; _. cont(z,z); x2@0. InjCase(x2@0; _. cont(z,z); x2@1. x2@1/x3,x2@2. body(x3;x2@2))))
case Def Case(value) body == body(value,value)

About:
spreaddecide
applymemberall!abstraction

Definitions GenAutomata Sections NuprlLIB Doc