User Manual for Rodin v.2.3: The Final Context

2.6.3 The Final Context

CONTEXT

agatha

SETS

$\tt persons$

CONSTANTS

$\tt Agatha$
$\tt butler$
$\tt Charles$
$\tt hates$
$\tt richer$
$\tt killer$

AXIOMS

$\tt person\_ partition :$: $\it partition(persons, \{ Agatha\} , \{ butler\} , \{ Charles\} )$
$\tt hate\_ relation :$: $\it hates \in persons \mathbin \leftrightarrow persons$
$\tt richer\_ relation :$: $\it richer \in persons \mathbin \leftrightarrow persons \land \\ \hspace*{3,4 cm} richer \mathbin {\mkern 1mu\cap \mkern 1mu}id = \emptyset \land \\ \hspace*{3,4 cm} (\forall x,y,z \mathord {\mkern 1mu\cdot \mkern 1mu}( x\mapsto y\in richer \land y\mapsto z\in richer) \mathbin \Rightarrow x\mapsto z\in richer) \land \\ \hspace*{3,4 cm} (\forall x,y \mathord {\mkern 1mu\cdot \mkern 1mu}x\in persons \land y\in persons \land x\neq y \mathbin \Rightarrow (x\mapsto y\in richer \mathbin \Leftrightarrow y\mapsto x \notin richer))$
$\tt killer\_ type :$: $\it killer \in persons$
$\tt killer\_ hates :$: $\it killer \mapsto Agatha \in hates$
$\tt killer\_ not\_ richer :$: $\it killer \mapsto Agatha \notin richer$
$\tt charles\_ hates :$: $\it hates[\{ Agatha\} ] \mathbin {\mkern 1mu\cap \mkern 1mu}hates[\{ Charles\} ] = \emptyset$
$\tt agatha\_ hates :$: $\it hates[\{ Agatha\} ] = persons \setminus \{ butler\}$
$\tt butler\_ hates\_ 1 :$: $\it \forall x\mathord {\mkern 1mu\cdot \mkern 1mu}( x\mapsto Agatha \notin richer \mathbin \Rightarrow butler\mapsto x \in hates)$
$\tt butler\_ hates\_ 2 :$: $\it hates[\{ Agatha\} ] \subseteq hates[\{ butler\} ] \land \\ \hspace*{3,2 cm} (\forall x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in persons \mathbin \Rightarrow hates[\{ x\} ] \neq persons)$
$\tt noone\_ hates\_ everyone :$: $\it \forall x \mathord {\mkern 1mu\cdot \mkern 1mu}x \in persons \land hates[\{ x\} ] \neq persons$
$\tt solution :$: $\it \fbox{theorem} ~ killer = Agatha$

END

Rodin Handbook

2.6.3 The Final Context