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 . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

1 Lemma Prop 3.10 3

2 Lemma Prop 3.11 3

[Prop 3.7a →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a}]

[Prop 3.7b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z+\underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{c}]

[Prop 3.7c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z+\underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a}]

[Prop 3.7d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z+\underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} + \underline{c} = \underline{b} + \underline{c}]

[Prop 3.7e →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} ⇒ \underline{a} = \underline{a}]

[Prop 3.7f →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{c} ⇒ \underline{a} = \underline{c}]

[Prop 3.7g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c}]

[Prop 3.7g′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b}]

[Prop 3.7h →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{c}]

[Prop 3.7i →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} ⇒ 0 = \underline{a}] [Prop 3.7j →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a}′]

[Prop 3.7k →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z+\underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a}′ = \underline{b} ⇒ \underline{a}′ = \underline{b}]

[Prop 3.7k′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a}′ = \underline{b} ⇒ \underline{a}′ = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b}]

[Prop 3.7l →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b}′]

[Prop 3.7l′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z+\underline{a} = \underline{b}′ ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b}]

[Prop 3.7m →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a}′]

[Prop 3.7o →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a}]

[Prop 3.7p →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a}]

[Prop 3.7q →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a} ⇒ \underline{b} = \underline{a}]

[Prop 3.7r →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} + \underline{b} ⇒ \underline{a} = \underline{a} + \underline{b}]

[Prop 3.7s →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} + \underline{b}]

[Prop 3.7t →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} · \underline{b} ⇒ \underline{a} = \underline{a} · \underline{b}]

[Prop 3.7u →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a}]

[Prop 3.7u′ →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} ⇒ ¬\underline{a} = 0]

[Prop 3.7v →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} · \underline{b}]

[Prop 3.7w →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0′ = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} · \underline{a}]

[Prop 3.7x →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a}]

[Prop 3.7x′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c}] [Prop 3.7y →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ \underline{b} · \underline{a} = \underline{c} · \underline{a}]

[Prop 3.7y′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c}]

[Prop 3.7z →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = 0]

[Prop 3.7z′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a} ⇒ \underline{b} = \underline{a} ⇒ \underline{a} = \underline{b}]

0.1 proof of Prop 3.7

1 Lemma Prop 3.10

[Prop 3.10a →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} = ∀\underline{a}: \underline{a} · z]

[Prop 3.10b →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} = ∀\underline{a}: 0′ · z]

[Prop 3.10c →^{stmt} S ⊢ ¬∀_{obj}z: ¬0 = ∀\underline{a}: \underline{a} · z]

[Prop 3.10d →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{c} = ¬∀_{obj}z: ¬\underline{c} ⇒ \underline{a} = ¬∀_{obj}z: ¬\underline{b} ∧ \underline{b} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z · z]

[Prop 3.10e →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} ⇒ \underline{a} = \underline{a} = ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} = 0 ⇒ ¬\underline{b} · z]

[Prop 3.10f →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} ⇒ \underline{a} = \underline{b} = ¬∀_{obj}z: ¬¬\underline{b} ⇒ ¬\underline{b} = ∀\underline{a}: ∀\underline{b}: \underline{a} · z · z]

[Prop 3.10g →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} · \underline{c} = ¬∀_{obj}z: ¬\underline{b} ⇒ \underline{a} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z]

[Prop 3.10h →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} + \underline{c} = ¬∀_{obj}z: ¬\underline{c} ⇒ \underline{a} = ¬∀_{obj}z: ¬\underline{b} ∧ \underline{a} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z · z]

2 Lemma Prop 3.11

[Prop 3.11 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}\underline{c}: ∀_{obj}\underline{d}: ¬¬¬\underline{b} = \underline{a} · \underline{c} + \underline{d} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{d} = \underline{a} ⇒ ¬∀_{obj}\underline{e}: ∀_{obj}\underline{f} : ¬\underline{b} = \underline{a} · \underline{e} + \underline{f} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{f} = \underline{a} ⇒ ¬\underline{c} = \underline{e} ⇒ ¬\underline{d} = \underline{f}]

References