X2.casl.output revision 2f2237571ed7885b0f1ccb2c17996e8922f3d12d
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder(sorts a, s, s1, s2, t
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder sorts s1, s2 < s
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder op a : s -> t
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski op b : s -> t
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski op c : a -> s
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder op c : a * t * t * t -> s
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder op d : s -> t,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski [forall v1 : a; v2, v3, v4 : t . a(c(v1, v2, v3, v4)) = v2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %(ga_selector_a)%,
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder forall v1 : a; v2, v3, v4 : t . b(c(v1, v2, v3, v4)) = v3
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder %(ga_selector_b)%,
0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski forall v1 : a; v2, v3, v4 : t . d(c(v1, v2, v3, v4)) = v4
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder %(ga_selector_d)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall v1 : a; v2, v3, v4 : t; v5 : a; v6, v7, v8 : t
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . c(v1, v2, v3, v4) = c(v5, v6, v7, v8)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder <=> v1 = v5 /\ v2 = v6 /\ v3 = v7 /\ v4 = v8 %(ga_injective_c)%,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder forall v1, v2 : a . c(v1) = c(v2) <=> v1 = v2 %(ga_injective_c)%,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder forall v1 : s . not (v1 in s2 /\ v1 in s1)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %(ga_disjoint_sorts_s2_s1)%,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder not c in s2 %(ga_disjoint_c_sort_s2)%,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder not c in s1 %(ga_disjoint_c_sort_s1)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall v1 : a; v2, v3, v4 : t . not c(v1, v2, v3, v4) in s2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %(ga_disjoint_c_sort_s2)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall v1 : a; v2, v3, v4 : t . not c(v1, v2, v3, v4) in s1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %(ga_disjoint_c_sort_s1)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall v1 : a . not c(v1) in s2 %(ga_disjoint_c_sort_s2)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall v1 : a . not c(v1) in s1 %(ga_disjoint_c_sort_s1)%,
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder forall v1 : a; v2, v3, v4 : t . not c = c(v1, v2, v3, v4)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder %(ga_disjoint_c_c)%,
cf31aaf25d0fe96b0578755e7ee18b732e337343Christian Maeder forall v1 : a . not c = c(v1) %(ga_disjoint_c_c)%,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder forall v1 : a; v2, v3, v4 : t; v5 : a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . not c(v1, v2, v3, v4) = c(v5) %(ga_disjoint_c_c)%,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder not def a(c) %(ga_selector_undef_a_c)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall v1 : a . not def a(c(v1)) %(ga_selector_undef_a_c)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski not def b(c) %(ga_selector_undef_b_c)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall v1 : a . not def b(c(v1)) %(ga_selector_undef_b_c)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski not def d(c) %(ga_selector_undef_d_c)%,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder forall v1 : a . not def d(c(v1)) %(ga_selector_undef_d_c)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski op c : a ->? s;
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder op c : a * t * t * t -> s;
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder op gn_inj : s1 -> s;
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder op gn_inj : s2 -> s
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder } %(ga_generated_s)%,
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder forall v1 : a; v2, v3, v4 : t . a(c(v1, v2, v3, v4)) = v2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder %(ga_selector_a)%,
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder forall v1 : a; v2, v3, v4 : t . b(c(v1, v2, v3, v4)) = v3
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder %(ga_selector_b)%,
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder forall v1 : a; v2, v3, v4 : t . d(c(v1, v2, v3, v4)) = v4
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %(ga_selector_d)%,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski op c : a ->? s;
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski op c : a * t * t * t -> s;
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski op gn_inj : s1 -> s;
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski op gn_inj : s2 -> s
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski } %(ga_generated_s)%])
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder*** Error 3.30, total selectors 'a : s -> t,b : s -> t,d : s -> t'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder must appear in alternative 'c : s'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder*** Error 3.53, total selectors 'a : s -> t,b : s -> t,d : s -> t'
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder must appear in alternative 'c : a ->? s'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hint 4.16, redeclared sort 's'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hint 4.27, redeclared subsort 's2 < s'
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder### Hint 4.30, redeclared subsort 's1 < s'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hint 4.35, redeclared op 'c'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 4.39, redeclared as total 'c'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hint 4.46, redeclared op 'c'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hint 4.51, redeclared op 'a'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hint 4.53, redeclared op 'b'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hint 4.58, redeclared op 'd'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Warning 4.65, partially redeclared 'c'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski*** Error 4.39, duplicates at '(4,65)' for 'c : a -> s'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski*** Error 4.35, total selectors 'a : s -> t,b : s -> t,d : s -> t'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder must appear in alternative 'c : s'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski*** Error 4.39, total selectors 'a : s -> t,b : s -> t,d : s -> t'
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski must appear in alternative 'c : a -> s'
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder*** Error 4.65, total selectors 'a : s -> t,b : s -> t,d : s -> t'
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder must appear in alternative 'c : a ->? s'