SHOW:
|
|
- or go back to the newest paste.
| 1 | - | SomeFunnyRel(R1,R2,x,y) = (forall x y z . (R1(x,y) & R1(y,z) -> R1(x,z))) & (forall p q . R2(p,q) -> R1(p,q)) & (forall Q . ((forall a b c . (Q(a,b) & Q(b,c) -> Q(a,c))) & (forall m n . R2(m,n) -> Q(m,n)) -> (forall l g . R1(l,g) -> Q(l,g)))) |
| 1 | + | createTC(R1,RPlus) <-> |
| 2 | exists(RPlus, | |
| 3 | trans(R1,x,y) -> RPlus(x,y)) | |
| 4 | ||
| 5 | trans(R,x,z) <-> | |
| 6 | ( R(x,z) | |
| 7 | v (R(x,y) & R(y,z) -> R(x,z)))) |
