| changeset 1108 | e97bdbc84421 |
| parent 1105 | 576a95f4c918 |
| child 1109 | 86093c201bac |
| 1105:576a95f4c918 | 1108:e97bdbc84421 |
|---|---|
935 primrec |
935 primrec |
936 rbv6 |
936 rbv6 |
937 where |
937 where |
938 "rbv6 (rVr6 x) = {atom x}" |
938 "rbv6 (rVr6 x) = {atom x}" |
939 | "rbv6 (rAp6 l r) = rbv6 l \<union> rbv6 r" |
939 | "rbv6 (rAp6 l r) = rbv6 l \<union> rbv6 r" |
940 | "rbv6 (rFo6 l r) = rbv6 l - rbv6 r" |
940 | "rbv6 (rFo6 l r) = rbv6 r - rbv6 l" |
941 |
941 |
942 primrec |
942 primrec |
943 rfv_trm6 |
943 rfv_trm6 |
944 where |
944 where |
945 "rfv_trm6 (rVr6 n) = {atom n}" |
945 "rfv_trm6 (rVr6 n) = {atom n}" |