Talk:Gentzen

variation on cmp

A function similar to cmp would be:

cmpv : (*a |- *b; *a |- *c; *a |- *d) / ($1(|\|), $2(|\|), *a |- *b, *c, *d);

Maybe you can think of a use for this. I think you can define it in terms of cmp, but I'm not sure what the syntax for such a definition would be. --GreyKnight (talk) 14:44, 20 June 2014 (UTC)

I think it would be like this:

  cmpv : (*a |- $1(*b); *a |- $1(*c); *a |- $1(*d)) / ($1(|\|), $2(|\|), *a |- $3(*b), $4(*c), $5(*d));
  cmpv = [bb,cc,dd/x,y,b,c,d] cmp (bb b) (cc c) (dd d) x y;

--Zzo38 (talk) 08:28, 21 June 2014 (UTC)