17 lines
311 B
Plaintext
17 lines
311 B
Plaintext
mybabyv2: THEORY
|
|
BEGIN
|
|
person: TYPE+
|
|
me, mybaby: person
|
|
x, y: VAR person
|
|
loves(x, y): boolean
|
|
|
|
everybodyLovesMyBaby: AXIOM
|
|
forall x: x /= mybaby IMPLIES loves(x, mybaby)
|
|
|
|
mybabyLovesOnlyMe: AXIOM
|
|
loves(mybaby, x) IMPLIES x = me
|
|
% comment
|
|
mybabyIsMe: LEMMA
|
|
mybaby /= me
|
|
END mybabyv2
|