equal
deleted
inserted
replaced
29 "qfst(p) == THE a. EX b. p=<a;b>" |
29 "qfst(p) == THE a. EX b. p=<a;b>" |
30 |
30 |
31 qsnd :: "i => i" |
31 qsnd :: "i => i" |
32 "qsnd(p) == THE b. EX a. p=<a;b>" |
32 "qsnd(p) == THE b. EX a. p=<a;b>" |
33 |
33 |
34 qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*) |
34 qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for pattern-matching*) |
35 "qsplit(c,p) == c(qfst(p), qsnd(p))" |
35 "qsplit(c,p) == c(qfst(p), qsnd(p))" |
36 |
36 |
37 qconverse :: "i => i" |
37 qconverse :: "i => i" |
38 "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}" |
38 "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}" |
39 |
39 |