Udvidedlse af S-reglerne, Appendix

Maja Hanne Tønnesen, Rune Christoffer Kildetoft Andresen

& Niels Peter Meyn Milthers GRD-2006-06-30.UTC:01:48:56.562305

Contents

0.1 proof of Prop 3.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1 Lemma Prop 3.10 2 2 Lemma Prop 3.11 3 [S lemma Prop 3.7a: ΠA: A ≮ A] [S lemma Prop 3.7b: ΠA, B, C: A < B ⇒ B < C ⇒ A < C] [S lemma Prop 3.7c: ΠA, B: A < B ⇒ B ≮ A] [S lemma Prop 3.7d: ΠA, B, C: A < B ⇒ A + C < B + C] [S lemma Prop 3.7e: ΠA: A ≤ A] [S lemma Prop 3.7f : ΠA, B, C: A ≤ B ⇒ B ≤ C ⇒ A ≤ C] [S lemma Prop 3.7g: ΠA, B, C: A ≤ B ⇒ A + C ≤ B + C] [S lemma Prop 3.7g′: ΠA, B, C: A + C ≤ B + C ⇒ A ≤ B] [S lemma Prop 3.7h: ΠA, B, C: A ≤ B ⇒ B < C ⇒ A < C] [S lemma Prop 3.7i: ΠA: 0 ≤ A] [S lemma Prop 3.7j: ΠA: 0 < A′] [S lemma Prop 3.7k: ΠA, B: A < B ⇒ A′ ≤ B] [S lemma Prop 3.7k′: ΠA, B: A′ ≤ B ⇒ A < B] [S lemma Prop 3.7l: ΠA, B: A ≤ B ⇒ A < B′] [S lemma Prop 3.7l′: ΠA, B: A < B′ ⇒ A ≤ B] [S lemma Prop 3.7m: ΠA: A < A′] [S lemma Prop 3.7o: ΠA, B: A ≠ B ⇒ (A < B ∨ B < A)] [S lemma Prop 3.7p: ΠA, B: A = B ∨ A < B ∨ B < A] [S lemma Prop 3.7q: ΠA, B: A ≤ B ∨ B ≤ A] [S lemma Prop 3.7r: ΠA, B: A + B ≥ A] [S lemma Prop 3.7s: ΠA, B: B ≠ 0 ⇒ A + B > A] [S lemma Prop 3.7t: ΠA, B: B ≠ 0 ⇒ A · B ≥ A] [S lemma Prop 3.7u: ΠA: A ≠ 0 ⇒ A > 0] [S lemma Prop 3.7u′: ΠA: A > 0 ⇒ A ≠ 0] [S lemma Prop 3.7v: ΠA, B: A > 0 ⇒ B > 0 ⇒ A · B > 0] [S lemma Prop 3.7w: ΠA, B: A ≠ 0 ⇒ B > \overline{1} ⇒ B · A > A] [S lemma Prop 3.7x: ΠA, B, C: A ≠ 0 ⇒ B < C ⇒ B · A < C · A] [S lemma Prop 3.7x′: ΠA, B, C: A ≠ 0 ⇒ B · A < C · A ⇒ B < C] [S lemma Prop 3.7y: ΠA, B, C: A ≠ 0 ⇒ B ≤ C ⇒ B · A ≤ C · A] [S lemma Prop 3.7y′: ΠA, B, C: A ≠ 0 ⇒ B · A ≤ C · A ⇒ B ≤ C] [S lemma Prop 3.7z: ΠA: A ≮ 0] [S lemma Prop 3.7z′: ΠA, B: A ≤ B ∧ B ≤ A ⇒ A = B]

0.1 proof of Prop 3.7

1 Lemma Prop 3.10

[S lemma Prop 3.10a: ΠA: A | A] [S lemma Prop 3.10b: ΠA: \overline{1} | A] [S lemma Prop 3.10c: ΠA: A | 0] [S lemma Prop 3.10d: ΠA, B, C: A | B ∧ B | C ⇒ A | C] [S lemma Prop 3.10e: ΠA, B: A ≠ 0 ∧ B | B ⇒ A ≤ A] [S lemma Prop 3.10f : ΠA, B: A | B ∧ B | A ⇒ A = B] [S lemma Prop 3.10g: ΠA, B, C: A | B ⇒ A | (B · C)] [S lemma Prop 3.10h: ΠA, B, C: A | B ∧ A | C ⇒ A | (B + C)]

2 Lemma Prop 3.11

[S lemma Prop 3.11: ΠA, B: A ≠ 0 ⇒ ∃C, D: (B = A · C + D ∧ D < A ∧ ∀E, F: ((B = A · E + F ∧ F < A) ⇒ C = E ∧ D = F))]

References