23 lines
410 B
Plaintext
23 lines
410 B
Plaintext
mybabynn: THEORY
|
|
BEGIN
|
|
person: TYPE+
|
|
me, mybaby: person
|
|
p, p1, p2: VAR person
|
|
loves(p1, p2): boolean
|
|
|
|
nonNarcissism: AXIOM
|
|
forall p1, p2: loves(p1, p2) IMPLIES p1 /= p2
|
|
|
|
everybodyLovesMyBaby: AXIOM
|
|
forall p: loves(p, mybaby)
|
|
|
|
mybabyLovesMe: AXIOM
|
|
loves(mybaby, me)
|
|
|
|
mybabyLovesOnlyMe: AXIOM
|
|
loves(mybaby, p) IMPLIES p = me
|
|
|
|
mybabyIsNotMe: LEMMA
|
|
mybaby /= me
|
|
END mybabynn
|