Задача 5 Дать эквивалентное определение без использований вариантных определений

Начнем с простенького примера с коллоквиума прошлого года:
type Collection

empty | add (Collection <-> head, tail:Collection) [Знак <-> обозначает реконструктор. То есть то, что мы можем по созданной функцией add коллекции реконструировать (заменять) значение указанного аргумента. Выражение типа tail: Collection обозначает возможность однозначного конструирования этого "хвоста" из коллекции полученной функцией add, сиречь конструктор]

---

type Collection
value
empty : Collection,

add: Collection >< Collection -> Collection
head : Collection >< Collection -~-> Collection,
tail : Collection -~-> Collection

axiom

[disjoint - собственно, то, что конструироемое функцией add или head ни в коем случае не равно empty]
all c1, c2: Collection:-
empty ~= add(c1, c2)/\ empty ~= head(c1, c2)

[induction - читать как: для любого предиката над типом коллекция, если справедлив предикат над пустой коллекцией, и если для любых двух коллекций из справедливости предиката для них следуют справедливость предиката для add и head, то следует справедливость предиката для любой коллекции; по-моему разумеию мы формулируем свойство коллекции оставаться коллекцией при выполнении указанных функций]
all IsC: Collection -> Bool :-
IsC(empty) /\ (all c1, c2: Collection:- (IsC(c1) /\ IsC(c2)) => IsC(add(c1, c2)) /\ IsC(head(c1, c2))) => (all c: Collection :- IsC(c)),

[вот аксиома выражающая вышесказанное о реконструкторе]

all c1, c2, c3 : Collection :-
head (c1, add(c2, c3)) is add(c1, c3)

[вот аксиома выражающая вышесказанное об однозначном конструировании]

all c1, c2: Collection:- tail (add(c1,c2)) is c2

Пример, разобранный в варианте:
type Elem, Collection

empty | add(Collection <-> head, first: Elem, Elem <-> new_second)

---

type Elem, Collection
value empty: Collection,

add: Collection >< Elem >< Elem -> Collection,
head: Collection >< Collection -~-> Collection,
first: Collection -~-> Elem,
new_second: Elem >< Collection -~-> Collection

axiom

[disjoint - аналогично]
all c, c1: Collection, e1, e2: Elem :-
empty ~= add(c, e1, e2) /\ empty ~= head(c, c1) /\ empty ~= new_second(e1, c)

[induction и тут точно так же]
all IsC: Collection -> Bool :-
IsC(empty) /\ (all c1, c2: Collection, e1, e2: Elem :- ( (IsC(c1) /\ IsC(c2)) => IsC(add(c1, e1, e2)) /\ IsC(head(c1, c2)) /\ IsC(new_second(e1, c1)) ) => (all c: Collection :- IsC(c))

[head_add - указываем реконструироемость]
all c1, c2: Collection, e1, e2: Elem :-
head(c1, add(c2, e1, e2)) is add(c1, e1, e2)

[first_add - тоже самое]
all c: Collection, e1, e2: Elem :-
first(add(c, e1, e2)) is e1

[new_second_add - и тут тоже]
all c: Collection, e1, e2, e3: Elem :-
new_second(e1, add(c, e2, e3)) is add(c, e2, e1)

Еще пример из вариантов:
[вот тут небольшая заковыка - имя head указано трижды. Не бойтесь - это всего лишь перегруженная функция).
type Elem, Collection

empty | add1(head: Elem) | add2( Elem <-> head)
type

Elem, Collection

value

empty: Collection
add1: Elem -> Collection
add2: Elem -> Collection
head: Elem >< Collection -~-> Collection
head: Collection -~-> Element

axiom

[disjoint - аналогично]
all c: Collection, e1, e2, e3: Elem :-
empty ~= add1(e1) /\ empty ~= add2(e2) /\ empty ~= head(e3, c)

[induction и тут точно так же]
all IsC: Collection -> Bool :-
IsC(empty) /\ (all c: Collection, e1, e2, e3: Elem :- ( IsC(c) => IsC(add1(e1) /\ IsC(add2(e2)) /\ IsC(head(e3, c)) ) => (all c: Collection :- IsC(c))

[head_add1 - указываем конструироемость]
all e1, e2: Elem:- head(add1(e1)) is e1,

[head_add2 - указываем конструироемость и реконструироемость одновременно :) - ффтыкайте]
all c1, c2: Collection, e1, e2: Elem
head( head (e1, add(e2))) is e2

[ для тех кому непонятно, распишу в две аксиомы: реконструироемость all c1: Collection, e: Elem:- head(e1, add(e2)) is add(e1)
и конструироемость all e: Elem head (add(e)) is e ]