Total order


Definition

Let \((S, \mathcal{R})\) be a relational structure. Then \(\mathcal{R}\) is a total order on \(S\) if and only if:

\(\mathcal{R}\) is an ordering:
\(\mathcal{R}\) is reflexive:
\(\forall x \in S : x{\mathcal{R}}x\)
\(\mathcal{R}\) is transitive:
\(\forall x,y,z \in S : x{\mathcal{R}}y \wedge y{\mathcal{R}}z \Rightarrow x{\mathrel{R}}z\)
\(\mathcal{R}\) is anti-symmetric:
\(\forall x,y \in S : x{\mathcal{R}}y \wedge y{\mathcal{R}}x \Rightarrow x = y\)
\(\mathcal{R}\) is connex:
\(\forall x,y \in S : x{\mathcal{R}}y \vee y{\mathcal{R}}x\)

Axioms

   order_refl: ?x ≤ ?x
  order_trans: ?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?z
order_antisym: ?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?x \(\Longrightarrow\) ?x = ?y
       linear: ?x ≤ ?y \(\vee\) ?y ≤ ?x
THEOREM    $$\forall x,y \in S : (x \le y \Rightarrow P) \wedge (y \le x \Rightarrow P) \Rightarrow P$$
le_cases:
(?x ≤ ?y \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?y ≤ ?x \(\Longrightarrow\) ?P) \(\Longrightarrow\) ?P

Proof available

THEOREM    $$\begin{alignat}{3} \forall x,y,z \in S :&\ (x \le y \wedge y \le z \Rightarrow P)&&\ \wedge\\ &\ (x \le z \wedge z \le y \Rightarrow P)&&\ \wedge\\ &\ (y \le x \wedge x \le z \Rightarrow P)&&\ \wedge\\ &\ (y \le z \wedge z \le x \Rightarrow P)&&\ \wedge\\ &\ (z \le x \wedge x \le y \Rightarrow P)&&\ \wedge\\ &\ (z \le y \wedge y \le x \Rightarrow P)&& \Rightarrow P \end{alignat}$$
le_cases3:
(?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?z \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?y ≤ ?x \(\Longrightarrow\) ?x ≤ ?z \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?x ≤ ?z \(\Longrightarrow\) ?z ≤ ?y \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?z ≤ ?y \(\Longrightarrow\) ?y ≤ ?x \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?y ≤ ?z \(\Longrightarrow\) ?z ≤ ?x \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?z ≤ ?x \(\Longrightarrow\) ?x ≤ ?y \(\Longrightarrow\) ?P) \(\Longrightarrow\) ?P

Proof available