Nuprl - mb_automata_1 Citations of case_relname

Def Case x = > body(x) cont(x1,z) == (

x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1])

is mentioned by

Def rel_arg_typ(rn;i;de) == Case(rn) Case eq(Q) = > Q Case R = > (de.rel(R))[i] Default = > False [rel_arg_typ]

Def tc1(r;de) == Case(r.name) Case eq(Q) = > ||r.args|| = 2 Case R = > ||de.rel(R)|| = ||r.args|| Default = > False [tc1]

Try larger context: GenAutomata

mb automata 1 Sections GenAutomata Doc

`Def rel_arg_typ(rn;i;de) == Case(rn) Case eq(Q) = > Q Case R = > (de.rel(R))[i] Default = > False`	[rel_arg_typ]
`Def tc1(r;de) == Case(r.name) Case eq(Q) = > \|\|r.args\|\| = 2 Case R = > \|\|de.rel(R)\|\| = \|\|r.args\|\| Default = > False`	[tc1]