th_G: THEORY
BEGIN

%%%
%%% Solve the problem below and prove your solution in PVS.  This will involve
%%% building the appropriate PVS theory.
%%%
% 
% Taken from _Algebra 1_, Glencoe/McGraw-Hill, New York, New York, 1998 
% pg. 411, Problem 56
% 
% There are 8 houses on McArthur St, all in a row.  These houses
% are numbered from 1 to 8.
% 
% Allison, whose house number is greater than 2, lives next door
% to her best friend, Adrienne.  Belinda, whose house number is
% greater than 5, lives 2 doors away from her boyfriend, Benito.
% Cheri, whose house number is greater than Benito's, lives
% three doors away from her piano teacher, Mr. Crawford.  Daryl,
% whose house number is less than 4, lives 4 doors from his
% teammate, Don.  Who lives in each house?
% 
%%%
%%%
%%%
%%%
PPL: TYPE = {a, b, c, d, e, f, g, h}
ADR: TYPE = {i:int | 0 < i & i < 9}

H: {fn:[PPL -> ADR] | (forall (x,y:PPL): fn(x) = fn(y) => x = y)}



a1: axiom H(a) > 2
a2: axiom H(b) = H(a) + 1 OR H(b) = H(a) - 1
a3: axiom H(c) > 5
a4: axiom H(d) = H(c) + 2 OR H(d) = H(c) - 2
a5: axiom H(h) > H(d)
a6: axiom H(e) = H(h) + 3 OR H(e) = H(h) - 3
a7: axiom H(f) < 4
a8: axiom H(g) = H(f) + 4 OR H(g) = H(f) - 4
%%
%% l9 is obviously true, but is it easy to prove in PVS?
%%
l9: lemma forall (k:ADR) : k = 1 or k = 2 or k = 3 or k = 4
                        or k = 5 or k = 6 or k = 7 or k = 8
%%
%% Even if you can't prove it you might need to use it,
%% or maybe ASSERT understands it...?
%%
a9: axiom forall (k:ADR) : k = 1 or k = 2 or k = 3 or k = 4
                        or k = 5 or k = 6 or k = 7 or k = 8

l10: lemma forall (k:ADR) : (exists (p:PPL): H(p) = k)

%%
%% Solve the problem
%%

END th_G