29 lines
682 B
Plaintext
29 lines
682 B
Plaintext
mybabyre: THEORY
|
|
BEGIN
|
|
% 'person' is an inhabited Type
|
|
% The '+' means that there is at least one term of the type 'person'
|
|
person: TYPE+
|
|
|
|
% 'me' and 'mybaby' are people
|
|
% ie, they are values of the type 'person'
|
|
me, mybaby: person
|
|
|
|
% A few variables of type 'person'
|
|
x, y, z: VAR person
|
|
|
|
% A predicate accepting two values of type 'person'
|
|
loves(x, y): boolean
|
|
|
|
% Everyone loves my baby
|
|
everybodyLovesMyBaby: AXIOM
|
|
forall x: loves(x, mybaby)
|
|
|
|
% If my baby loves somebody, that is me
|
|
mybabyLovesOnlyMe: AXIOM
|
|
loves(mybaby, x) IMPLIES x = me
|
|
|
|
% We this, we can prove that mybaby and me are same!
|
|
mybabyIsMe: LEMMA
|
|
mybaby = me
|
|
END mybabyre
|