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
|