# Appendix 1: Sample Mizar Proofs

We used to have a bunch of Mizar proofs from the past assignments in this section. Now they are spread all over the notes.

## 1.1: A murder mystery

```== The following puzzle is due to L. Schubert
==
== A mysterious death at Dreadbury Mansion ...
==
==  1: Someone who lives at Dreadbury Mansion killed Aunt Agatha.
==  2: Only Agatha, the butler and Charles has lived at Dreadbury Mansion.
==  3: A killer always hates their victim.
==  4: A killer is never richer than their victim.
==  5: Charles hates no-one that Aunt Agatha hates.
==  6: Aunt Agatha hates everyone but the butler.
==  7: The butler hates everyone who is not richer than Aunt Agatha.
==  8: The butler hates everyone Aunt Agatha hates.
==  9: No-one hates everyone.
== 10: Aunt Agatha is not identical with the butler, of course.
==
== Question: Who killed Aunt Agatha?
==

environ reserve x1,x2,z,u,v,w for Person;
given Agatha, butler, Charles being Person;
1:  ex x1 st LivesatDBM[x1] & Killed[x1,Agatha];
2:  for x1 st LivesatDBM[x1] holds x1=Agatha or x1=butler or x1=Charles;
3:  for x1,x2 st Killed[x1,x2] holds Hates[x1,x2];
4:  for x1,x2 st Killed[x1,x2] holds not Richer[x1,x2];
5:  for x1 st Hates[Agatha,x1] holds not Hates[Charles,x1];
6:  for x1 st x1<>butler holds Hates[Agatha,x1];
7:  for x1 st not Richer[x1,Agatha] holds Hates[butler,x1];
8:  for x1 st Hates[Agatha,x1] holds Hates[butler,x1];
9: for x1 ex x2 st not Hates[x1,x2];
10: Agatha<>butler

begin

Killed[Agatha, Agatha]
proof

11: for x1 st x1<>butler holds Hates[butler,x1] proof
let u be Person;
assume 11a: u<>butler;
thus Hates[butler,u] proof
11b: Hates[Agatha,u] by 11a,6;
thus thesis by 8,11b;
end;
end;

12: ex x2 st not Hates[butler,x2] by 9;
consider u such that
13: not Hates[butler,u] by 12;

14: u=butler proof
assume 14a: u<>butler;
14b: Hates[butler,u] by 11,14a;
end;

15: not Hates[butler,butler] by 13,14;
16: Richer[butler,Agatha] by 7,15;
17: not Killed[butler,Agatha] by 4,16;

18: Hates[Agatha,Agatha] by 6,10;
19: not Hates[Charles,Agatha] by 5,18;
20: not Killed[Charles,Agatha] by 3,19;

consider u such that
21: LivesatDBM[u] & Killed[u,Agatha] by 1;
22: u=Agatha or u=butler or u=Charles by 2,21;
23: u<>butler & u<>Charles by 17,20,21;
24: u=Agatha by 22,23;

thus thesis by 21,24;

end
```

## 1.2: K. Schubert's Steamroller

```environ

== The following example is due to L. Schubert.
==
== Wolves, foxes, birds, caterpillars, and snails are animals, and there
== are some of each of them.

reserve x, y, w, f, b, c, s for animal;

A: ex w, f, b, c, s st
wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s];

==  Also, there are some grains, and grains are plants.

reserve p, g for plants;

P: ex g st grain[g];

== Every animal either likes to eat all plants or all animals much smaller
== than itself that like to eat some plants.

1LIKES: for x holds
(for p holds likes[x,p])
or
(for y st smaller[y,x] &
(ex p st likes[y,p])
holds likes[x,y]);

== Caterpillars and snails are much smaller than birds, which are much smaller
== than foxes, which in turn are much smaller than wolves.

1SMALLER: for x, y st (caterpillar[x] or snail[x]) & bird[y]
holds smaller[x,y];
2SMALLER: for x, y st bird[x] & fox[y] holds smaller[x,y];
3SMALLER: for x, y st fox[x] & wolf[y] holds smaller[x,y];

== Wolves do not like to eat foxes or grains, while birds like to eat
== caterpillars but not snails.

2LIKES: for x, y, p st wolf[x] & fox[y] & grain[p]
holds not likes[x,y] & not likes[x,p];
3LIKES: for x, y st bird[x]
holds (caterpillar[y] implies likes[x,y]) &
(snail[y] implies not likes[x,y]);

== Caterpillars and snails like to eat some plants.

4LIKES: for x st caterpillar[x] or snail[x]
ex p st likes[x,p]

== Therefore there is an animal that likes to eat a grain-eating animal.

begin

ex x, y, p st likes[x,y] & likes[y,p] & grain[p]

proof
consider w, f, b, c, s such that
WFBCS: wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s] by A;
consider g such that G: grain[g] by P;
0: not likes[b,s] & (ex p st likes[s,p]) & smaller[s,b]
by 3LIKES, 4LIKES, 1SMALLER, WFBCS;
1: likes[b,g] by 0, 1LIKES;
2: smaller[f,w] & not likes[w,f] & not likes[w,g]
by 3SMALLER, 2LIKES, G, WFBCS;
3: not likes[f,g] by 2, 1LIKES;
4: smaller[b,f] by 2SMALLER, WFBCS;
5: likes[f,b] by 1, 3, 4, 1LIKES;
thus thesis by G, 1, 5
end;

== A bit shorter, but messier.

ex x, y, p st likes[x,y] & likes[y,p] & grain[p]

proof
consider w, f, b, c, s such that
WFBCS: wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s] by A;
consider g such that G: grain[g] by P;
1: not likes[b,s] & (ex p st likes[s,p]) & smaller[s,b] &
smaller[f,w] & not likes[w,f] & not likes[w,g] & smaller[b,f]
by 1SMALLER, 2SMALLER, 3SMALLER, 2LIKES,
3LIKES, 4LIKES, G, WFBCS;
2: likes[b,g] & not likes[f,g] by 1, 1LIKES;
3: likes[b,g] & likes[f,b] by 1, 2, 1LIKES;
thus thesis by G, 3
end

== Who will make it any shorter?
```