Atom
inl(*); inr(*) fi ; x1/x2@1,x1@1. InjCase(if x1@1=1 inl(*) ; inr(*) fi ; body(x1@0;x2@1); cont(z,z)); cont(z,z))| No mentions to report in GenAutomata | |
| case_pattern1 | Def < < "a", b > , c, 1 > = > body(b;c) cont(x,z) == x/x2,x1. x2/x2@0,x1@0. InjCase(if x2@0="a"Atominl(*); inr(*) fi ; x1/x2@1,x1@1. InjCase(if x1@1=1 inl(*) ; inr(*) fi ; body(x1@0;x2@1); cont(z,z)); cont(z,z)) |
| Syntax: | < < "a", b > , c, 1 > = > body(b;c) cont | has structure: | case_pattern1(b,c.body(b;c); cont) |
About:
 |  |  |  |  |
 |  |  |  |  |  |