(*** MAKROER BEGYNDER ***) [ph_{1} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ph_{1} ¨= a_{Ph}]⌉)] [ph_{2} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ph_{2} ¨= b_{Ph}]⌉)] [ph_{3} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ph_{3} ¨= c_{Ph}]⌉)] [ph_{4} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ph_{4} ¨= d_{Ph}]⌉)] [ph_{5} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ph_{5} ¨= e_{Ph}]⌉)] [ph_{6} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ph_{6} ¨= f_{Ph}]⌉)] [x ˙∧ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙∧ y ¨= ˙¬ ((x ⇒ ˙¬ (y)n))n]⌉)] [x ˙∨ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙∨ y ¨= ˙¬ (x)n ⇒ y]⌉)] [x ˙⇔ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙⇔ y ¨= (x ⇒ y) ˙∧ (y ⇒ x)]⌉)] [x ≠ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≠ y ¨= ˙¬ (x==y)n]⌉)] [x ∉ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ∉ y ¨= ˙¬ (x ∈ y)n]⌉)] [x ⊆ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ⊆ y ¨= ∀(S1ob): ((S1ob) ∈ x ⇒ (S1ob) ∈ y)]⌉)]

[{x} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[{x} ¨= {x, x}]⌉)]

[x ∪ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ∪ y ¨= ∪{{x}, {y}}]⌉)]

[x ∩ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ∩ y ¨= {ph ∈ x ∪ y | ph_{3} ∈ x ˙∧ ph_{3} ∈ y}]⌉)]

[⟨x, y⟩ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[⟨x, y⟩ ¨= {{x}, {x, y}}]⌉)]

[r(x, y) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[r(x, y) ¨= ⟨x, y⟩ ∈ r]⌉)] [ReflRel(r, x) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ReflRel(r, x) ¨= ∀s: (s ∈ x ⇒ r(s, s))]⌉)] [SymRel(r, x) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[SymRel(r, x) ¨= ∀s, t: (s ∈ x ⇒ t ∈ x ⇒ r(s, t) ⇒ r(t, s))]⌉)] [TransRel(r, x) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[TransRel(r, x) ¨= ∀s, t, u: (s ∈ x ⇒ t ∈ x ⇒ u ∈ x ⇒ r(s, t) ⇒ r(t, u) ⇒ r(s, u))]⌉)]

[EqRel(r, x) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[EqRel(r, x) ¨= ReflRel(r, x) ˙∧ SymRel(r, x) ˙∧ TransRel(r, x)]⌉)]

[BS →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[BS ¨= \underline{bs}]⌉)] [OBS →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[OBS ¨= \overline{bs}]⌉)]

[[x ∈ bs]_{r} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x ∈ bs]_{r} ¨= {ph ∈ bs | r(ph_{1}, x)}]⌉)]

[bs/r →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[bs/r ¨= {ph ∈ P(bs) | Ex_{20} ∈ bs ˙∧ [Ex_{20} ∈

bs]_{r} ==ph_{2}}]⌉)]

[Partition(p, bs) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Partition(p, bs) ¨= (∀s: (s ∈

p ⇒ s ≠ Ø)) ˙∧
(∀s, t: (s ∈ p ⇒ t ∈ p ⇒ s ≠ t ⇒ s ∩ t ==Ø)) ˙∧
∪ p==bs]⌉)]

(*** EKSISTENS-VARIABLE ***)

[x^{Ex} →^{val} x =^{r} ⌈x_{Ex}⌉]

[Ex_{1} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Ex_{1} ¨= a_{Ex}]⌉)]

[Ex_{2} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Ex_{2} ¨= b_{Ex}]⌉)] [Ex_{10} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Ex_{10} ¨= j_{Ex}]⌉)] [Ex_{20} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Ex_{20} ¨= t_{Ex}]⌉)] [⟨a≡b|x:==t⟩_{Ex} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[⟨a≡b|x:==t⟩_{Ex} ¨= ⟨⌈a⌉≡^{0}⌈b⌉|⌈x⌉:==⌈t⌉⟩_{Ex}]⌉)]

[⟨a≡^{0}b|x:==t⟩_{Ex} →^{val} λc.x^{Ex} ∧ ⟨a≡^{1}b|x:==t⟩_{Ex}]

[⟨a≡^{1}b|x:==t⟩_{Ex} →^{val} a!x!t! If(b =^{r} ⌈∀_{obj}u: v⌉, F, If(b^{Ex} ∧ b =^{t} x, a =^{t} t, If( a =^{r} b, ⟨a^{t}≡^{∗}b^{t}|x:==t⟩_{Ex}, F)))]

[⟨a≡^{∗}b|x:==t⟩_{Ex} →^{val} b!x!t!If(a, T, If(⟨a^{h}≡^{1}b^{h}|x:==t⟩_{Ex}, ⟨a^{t}≡^{∗}b^{t}|x:==t⟩_{Ex}, F))]

(*** AKSIOMATISK SYSTEM ***) [SystemQ →^{stmt} ∀\underline{(fx)}: ∀\underline{(fy)}: R(\underline{(fx)}) + +R(\underline{(fy)}) == R(\underline{(fy)}) + +R(\underline{(fx)}) ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)})∗∗R(\underline{(fy)})∗∗R(\underline{(fz)}) == R(\underline{(fx)})∗∗R(\underline{(fy)})∗∗R(\underline{(fz)}) ⊕ ∀\underline{(fx)}: ∀\underline{(rx)}: ∀\underline{(ry)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(fx)} ∈ \underline{(rx)} ⊢ \underline{(fx)} ∈ \underline{(ry)} ⊕ ∀\underline{m}: UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals) ⊢ xs[(\underline{m} + 1)] == xs[\underline{m}] ⊕ ∀\underline{x}: ∀\underline{y}: \underline{x} <= \underline{y} ⇒ \underline{y} <= \underline{x} ⇒ \underline{x} = \underline{y} ⊕ ∀\underline{s}: ∀\underline{x}: ∀\underline{y}: ˙¬ (\underline{s} ∈ \{\underline{x}, \underline{y}\} ⇒ ˙¬ (\underline{s}==\underline{x})n ⇒ \underline{s}==\underline{y} ⇒ ˙¬ ( ˙¬ (\underline{s}== \underline{x})n ⇒ \underline{s}==\underline{y} ⇒ \underline{s} ∈ \{\underline{x}, \underline{y}\})n)n ⊕ ∀\underline{m}: ∀\underline{n}: \underline{n} = 0 ⊢ BS(\underline{m}, \underline{n}) = rec(1+1)(exp)\underline{m} ⊕ ∀\underline{x}: (\underline{x} + 0) = \underline{x} ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: R(\underline{(fx)}) == R(\underline{(fy)}) ⊢ SF(\underline{(fx)}, \underline{(fy)}) ⊕ ∀\underline{x}: ∀\underline{y}: \underline{x} = \underline{y} ⇒ \underline{x} <= \underline{y} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b} ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)}) = R(\underline{(fy)}) ⊢ R(\underline{(fx)}) + +R(\underline{(fz)}) = R(\underline{(fy)}) + +R(\underline{(fz)}) ⊕ ∀\underline{(fx)}: R(\underline{(fx)}) + +R(0f) == R(\underline{(fx)}) ⊕ ∀\underline{x}: (\underline{x} ∗ 1) = \underline{x} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ⊕ ∀\underline{(rx)}: ∀\underline{(ry)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(ry)} == \underline{(rx)} ⊕ ∀\underline{m}: ∀\underline{x}: \underline{m} = 0 ⊢ \underline{x}(exp)\underline{m} = 1 ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: 0 <= \underline{z} ⇒ \underline{x} <= \underline{y} ⇒ (\underline{x} ∗ \underline{z}) <= (\underline{y} ∗ \underline{z}) ⊕ ∀\underline{(fx)}: R(\underline{(fx)}) ∗ ∗R(1f) == R(\underline{(fx)}) ⊕ ˙¬ (0 = 1)n ⊕ ∀\underline{m}: Nat(\underline{m}) ⊢⊢ 0 <= \underline{m} ⊕ ∀\underline{x}: ∀\underline{y}: ˙¬ (\underline{x}==\underline{y} ⇒ ∀_{obj}\overline{s}: ˙¬ (\overline{s} ∈ \underline{x} ⇒ \overline{s} ∈ \underline{y} ⇒ ˙¬ (\overline{s} ∈ \underline{y} ⇒ \overline{s} ∈ \underline{x})n)n ⇒ ˙¬ (∀_{obj}\overline{s}: ˙¬ (\overline{s} ∈ \underline{x} ⇒ \overline{s} ∈ \underline{y} ⇒ ˙¬ (\overline{s} ∈ \underline{y} ⇒ \overline{s} ∈ \underline{x})n)n ⇒ \underline{x}== \underline{y})n)n ⊕ ∀\underline{(rx)}: ∀\underline{(ry)}: ∀\underline{(rz)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(ry)} == \underline{(rz)} ⊢ \underline{(rx)} == \underline{(rz)} ⊕ ∀\underline{x}: ∀\underline{y}: (\underline{x} + \underline{y}) = (\underline{y} + \underline{x}) ⊕ ∀\underline{m}: ∀\underline{(fx)}: ∀\underline{(fy)}: \underline{(fx)} +_{f} \underline{(fy)}[\underline{m}] = (\underline{(fx)}[\underline{m}] + \underline{(fy)}[\underline{m}]) ⊕ ∀\underline{(v1)}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ⟨\underline{b}≡\underline{a}|\underline{(v1)}:==0⟩_{Me} ⊢⊢ ⟨\underline{c}≡\underline{a}|\underline{(v1)}:==(\underline{(v1)} + 1)⟩_{Me} ⊢⊢ \underline{b} ⇒ ∀_{obj}\underline{(v1)}: \underline{a} ⇒ \underline{c} ⇒ ∀_{obj}\underline{(v1)}: \underline{a} ⊕ ∀\underline{m}: ∀\underline{n}: \underline{n} = 0 ⊢ UStelescope(\underline{m}, \underline{n}) = |(us[\underline{m}] + (−uus[(\underline{m} + 1)]))| ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)}) + +R(\underline{(fy)}) + +R(\underline{(fz)}) = R(\underline{(fx)}) + +R(\underline{(fy)}) + +R(\underline{(fz)}) ⊕ ∀\underline{x}: ∀\underline{y}: (\underline{x} ∗ \underline{y}) = (\underline{y} ∗ \underline{x}) ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: \underline{(fx)} ∈ R(\underline{(fy)}) ⊢ SF(\underline{(fx)}, \underline{(fy)}) ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} = \underline{y} ⇒ (\underline{x} ∗ \underline{z}) = (\underline{y} ∗ \underline{z}) ⊕ ∀\underline{a}: \underline{a} ⊢ \underline{a} ⊕ ∀\underline{m}: UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals) ⊢ us[(\underline{m} + 1)] == 01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}] ⊕ ∀\underline{x}: ∀\underline{y}: ˙¬ (\underline{x} <= \underline{y})n ⇒ \underline{y} <= \underline{x} ⊕ ∀\underline{s}: ∀\underline{x}: ˙¬ (\underline{s} ∈ P(\underline{x}) ⇒ ∀_{obj}\overline{s}: \overline{s} ∈ \underline{s} ⇒ \overline{s} ∈ \underline{x} ⇒ ˙¬ (∀_{obj}\overline{s}: \overline{s} ∈ \underline{s} ⇒ \overline{s} ∈ \underline{x} ⇒ \underline{s} ∈ P(\underline{x}))n)n ⊕ us[0] == xs[0] + +R(1f) ⊕ ∀\underline{x}: \underline{x} <= \underline{x} ⊕ ∀\underline{s}: ˙¬ (\underline{s} ∈ Ø)n ⊕ ∀\underline{x}: (\underline{x} + (−u\underline{x})) = 0 ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} = \underline{y} ⇒ \underline{x} = \underline{z} ⇒ \underline{y} = \underline{z} ⊕ ∀\underline{m}: ∀\underline{n}: ˙¬ (0 <= \underline{n} ⇒ ˙¬ ( ˙¬ (0 = \underline{n})n)n)n ⊢ UStelescope(\underline{m}, \underline{n}) = (|(us[(\underline{m}+\underline{n})]+(−uus[(\underline{m}+(\underline{n}+1))]))|+UStelescope(\underline{m}, (\underline{n}+ (−u1)))) ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)} +_{f} \underline{(fy)} +_{f} \underline{(fz)}) == R(\underline{(fx)} +_{f} \underline{(fy)} +_{f} \underline{(fz)}) ⊕ ∀\underline{x}: ˙¬ (\underline{x} = 0)n ⇒ (\underline{x} ∗ rec\underline{x}) = 1 ⊕ ∀\underline{a}: ∀\underline{b}: ˙¬ (\underline{b})n ⇒ \underline{a} ⊢ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{a})n ⊢ \underline{b} ⊕ ∀\underline{(rx)}: \underline{(rx)} == \underline{(rx)} ⊕ ∀\underline{m}: ˙¬ (UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals))n ⊢ us[(\underline{m} + 1)] == us[\underline{m}] ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} <= \underline{y} ⇒ (\underline{x} + \underline{z}) <= (\underline{y} + \underline{z}) ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{p}: ∀\underline{x}: ∀\underline{z}: \underline{p}^{Ph} ∧ ⟨\underline{b}≡\underline{a}|\underline{p}:==\underline{z}⟩_{Ph} ⊢⊢ ˙¬ (\underline{z} ∈ \{ph ∈ \underline{x} | \underline{a}\} ⇒ ˙¬ (\underline{z} ∈ \underline{x} ⇒ ˙¬ (\underline{b})n)n ⇒ ˙¬ ( ˙¬ (\underline{z} ∈ \underline{x} ⇒ ˙¬ (\underline{b})n)n ⇒ \underline{z} ∈ \{ph ∈ \underline{x} | \underline{a}\})n)n ⊕ ∀\underline{m}: ∀\underline{(fx)}: R(\underline{(fx)}) + +(− − R(\underline{(fx)})) == R(0f) ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: (\underline{x} ∗ (\underline{y} + \underline{z})) = ((\underline{x} ∗ \underline{y}) + (\underline{x} ∗ \underline{z})) ⊕ ∀\underline{m}: ∀\underline{n}: Nat(\underline{m}) ⊢⊢ Nat(\underline{n}) ⊢⊢ ˙¬ (\underline{m} <= (\underline{n} + 1) ⇒ ˙¬ ( ˙¬ (\underline{m} = (\underline{n} + 1))n)n)n ⊢ \underline{m} <= \underline{n} ⊕ ∀\underline{x}: ∀\underline{t}: ∀\underline{a}: ∀\underline{b}: ⟨⌈\underline{a}⌉≡^{0}⌈\underline{b}⌉|⌈\underline{x}⌉:==⌈\underline{t}⌉⟩_{Ex} ⊢⊢ \underline{a} ⊢ \underline{b} ⊕ ∀\underline{m}: ∀\underline{x}: ˙¬ (0 <= \underline{m} ⇒ ˙¬ ( ˙¬ (0 = \underline{m})n)n)n ⊢ \underline{x}(exp)\underline{m} = (\underline{x} ∗ \underline{x}(exp)(\underline{m} + (−u1))) ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: ((\underline{x} + \underline{y}) + \underline{z}) = (\underline{x} + (\underline{y} + \underline{z})) ⊕ ∀\underline{(v1)}: ∀\underline{(v2)}: ∀\underline{n}: ∀\underline{(ϵ)}: ∀\underline{(fx)}: ∀_{obj}\underline{(ϵ)}: ˙¬ (∀_{obj}\underline{n}: ˙¬ (∀_{obj}\underline{(v1)}: ∀_{obj}\underline{(v2)}: ˙¬ (0 <= \underline{(ϵ)} ⇒ ˙¬ ( ˙¬ (0 = \underline{(ϵ)})n)n)n ⇒ \underline{n} <= \underline{(v1)} ⇒ \underline{n} <= \underline{(v2)} ⇒ ˙¬ (|(\underline{(fx)}[\underline{(v1)}] + (−u\underline{(fx)}[\underline{(v2)}]))| <= \underline{(ϵ)} ⇒ ˙¬ ( ˙¬ (|(\underline{(fx)}[\underline{(v1)}] + (−u\underline{(fx)}[\underline{(v2)}]))| = \underline{(ϵ)})n)n)n)n)n ⊕ ∀\underline{x}: ∀\underline{(v1)}: ∀\underline{a}: ∀\underline{b}: ⟨\underline{a}≡\underline{b}|\underline{(v1)}:==\underline{x}⟩_{Me} ⊢⊢ ∀_{obj}\underline{(v1)}: \underline{b} ⇒ \underline{a} ⊕ ∀\underline{m}: ∀\underline{n}: ˙¬ (0 <= \underline{n} ⇒ ˙¬ ( ˙¬ (0 = \underline{n})n)n)n ⊢ BS(\underline{m}, \underline{n}) = (rec(1 + 1)(exp)(\underline{m} + \underline{n}) + BS(\underline{m}, (\underline{n} + (−u1)))) ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: ((\underline{x} ∗ \underline{y}) ∗ \underline{z}) = (\underline{x} ∗ (\underline{y} ∗ \underline{z})) ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: SF(\underline{(fx)}, \underline{(fy)}) ⊢ R(\underline{(fx)}) == R(\underline{(fy)}) ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} = \underline{y} ⇒ (\underline{x} + \underline{z}) = (\underline{y} + \underline{z}) ⊕ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ∀_{obj}\underline{x}: \underline{a} ⊕ ∀\underline{m}: ˙¬ (UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals))n ⊢ xs[(\underline{m} + 1)] == 01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}] ⊕ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} <= \underline{y} ⇒ \underline{y} <= \underline{z} ⇒ \underline{x} <= \underline{z} ⊕ ∀\underline{s}: ∀\underline{x}: ˙¬ (\underline{s} ∈ ∪\underline{x} ⇒ ˙¬ (\underline{s} ∈ j_{Ex} ⇒ ˙¬ (j_{Ex} ∈ \underline{x})n)n ⇒ ˙¬ ( ˙¬ (\underline{s} ∈ j_{Ex} ⇒ ˙¬ (j_{Ex} ∈ \underline{x})n)n ⇒ \underline{s} ∈ ∪\underline{x})n)n ⊕ ∀\underline{(fx)}: ∀\underline{(fy)}: R(\underline{(fx)}) ∗ ∗R(\underline{(fy)}) == R(\underline{(fy)}) ∗ ∗R(\underline{(fx)}) ⊕ ∀\underline{(fx)}: ∀\underline{(rx)}: ∀\underline{(ry)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(fx)} ∈ \underline{(ry)} ⊢ \underline{(fx)} ∈ \underline{(rx)}]

[MP →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b}][MP →^{proof} Rule tactic]

[Gen →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ∀_{obj}\underline{x}: \underline{a}][Gen →^{proof} Rule tactic]

[Repetition →^{stmt} SystemQ ⊢ ∀\underline{a}: \underline{a} ⊢ \underline{a}][Repetition →^{proof} Rule tactic]

[Neg →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ (\underline{b})n ⇒ \underline{a} ⊢ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{a})n ⊢ \underline{b}][Neg →^{proof} Rule tactic]

[Ded →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b}][Ded →^{proof} Rule tactic]

[ExistIntro →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{t}: ∀\underline{a}: ∀\underline{b}: ⟨⌈\underline{a}⌉≡^{0}⌈\underline{b}⌉|⌈\underline{x}⌉:==⌈\underline{t}⌉⟩_{Ex} ⊢⊢ \underline{a} ⊢ \underline{b}][ExistIntro →^{proof} Rule tactic]

[Extensionality →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ˙¬ (\underline{x}==\underline{y} ⇒ ∀_{obj}\overline{s}: ˙¬ (\overline{s} ∈ \underline{x} ⇒ \overline{s} ∈ \underline{y} ⇒ ˙¬ (\overline{s} ∈ \underline{y} ⇒ \overline{s} ∈ \underline{x})n)n ⇒ ˙¬ (∀_{obj}\overline{s}: ˙¬ (\overline{s} ∈ \underline{x} ⇒ \overline{s} ∈ \underline{y} ⇒ ˙¬ (\overline{s} ∈ \underline{y} ⇒ \overline{s} ∈ \underline{x})n)n ⇒

\underline{x}==\underline{y})n)n][Extensionality →^{proof} Rule tactic]

[Ødef →^{stmt} SystemQ ⊢ ∀\underline{s}: ˙¬ (\underline{s} ∈ Ø)n][Ødef →^{proof} Rule tactic]

[PairDef →^{stmt} SystemQ ⊢ ∀\underline{s}: ∀\underline{x}: ∀\underline{y}: ˙¬ (\underline{s} ∈ \{\underline{x}, \underline{y}\} ⇒ ˙¬ (\underline{s}==\underline{x})n ⇒ \underline{s}==\underline{y} ⇒

˙¬ ( ˙¬ (\underline{s}==\underline{x})n ⇒ \underline{s}==\underline{y} ⇒ \underline{s} ∈ \{\underline{x}, \underline{y}\})n)n][PairDef →^{proof} Rule tactic] [UnionDef →^{stmt} SystemQ ⊢ ∀\underline{s}: ∀\underline{x}: ˙¬ (\underline{s} ∈ ∪\underline{x} ⇒ ˙¬ (\underline{s} ∈ j_{Ex} ⇒ ˙¬ (j_{Ex} ∈ \underline{x})n)n ⇒ ˙¬ ( ˙¬ (\underline{s} ∈ j_{Ex} ⇒ ˙¬ (j_{Ex} ∈ \underline{x})n)n ⇒ \underline{s} ∈ ∪\underline{x})n)n][UnionDef →^{proof} Rule tactic]

[PowerDef →^{stmt} SystemQ ⊢ ∀\underline{s}: ∀\underline{x}: ˙¬ (\underline{s} ∈ P(\underline{x}) ⇒ ∀_{obj}\overline{s}: \overline{s} ∈ \underline{s} ⇒ \overline{s} ∈ \underline{x} ⇒ ˙¬ (∀_{obj}\overline{s}: \overline{s} ∈ \underline{s} ⇒ \overline{s} ∈ \underline{x} ⇒ \underline{s} ∈ P(\underline{x}))n)n][PowerDef →^{proof} Rule tactic]

[SeparationDef →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{p}: ∀\underline{x}: ∀\underline{z}: \underline{p}^{Ph} ∧ ⟨\underline{b}≡\underline{a}|\underline{p}:==\underline{z}⟩_{Ph} ⊢⊢ ˙¬ (\underline{z} ∈ \{ph ∈ \underline{x} | \underline{a}\} ⇒ ˙¬ (\underline{z} ∈ \underline{x} ⇒ ˙¬ (\underline{b})n)n ⇒ ˙¬ ( ˙¬ (\underline{z} ∈ \underline{x} ⇒ ˙¬ (\underline{b})n)n ⇒ \underline{z} ∈ \{ph ∈ \underline{x} | \underline{a}\})n)n][SeparationDef →^{proof} Rule tactic] ————- RRRRRRRRRRRRRRR ————- (*** import fra A.M. ***) [TimesCommutativity(R) →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: R(\underline{(fx)}) ∗ ∗R(\underline{(fy)}) == R(\underline{(fy)}) ∗ ∗R(\underline{(fx)})][TimesCommutativity(R) →^{proof} Rule tactic] (*** aksiomer ***) [leqReflexivity →^{stmt} SystemQ ⊢ ∀\underline{x}: \underline{x} <= \underline{x}][leqReflexivity →^{proof} Rule tactic] [leqAntisymmetryAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: \underline{x} <= \underline{y} ⇒ \underline{y} <= \underline{x} ⇒ \underline{x} = \underline{y}][leqAntisymmetryAxiom →^{proof} Rule tactic] [leqTransitivityAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} <= \underline{y} ⇒ \underline{y} <= \underline{z} ⇒ \underline{x} <= \underline{z}][leqTransitivityAxiom →^{proof} Rule tactic] [leqTotality →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ˙¬ (\underline{x} <= \underline{y})n ⇒ \underline{y} <= \underline{x}][leqTotality →^{proof} Rule tactic] [leqAdditionAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} <= \underline{y} ⇒ (\underline{x} + \underline{z}) <= (\underline{y} + \underline{z})][leqAdditionAxiom →^{proof} Rule tactic] [leqMultiplicationAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: 0 <= \underline{z} ⇒ \underline{x} <= \underline{y} ⇒ (\underline{x} ∗ \underline{z}) <= (\underline{y} ∗ \underline{z})][leqMultiplicationAxiom →^{proof} Rule tactic] [plusAssociativity →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: ((\underline{x} + \underline{y}) + \underline{z}) = (\underline{x} + (\underline{y} + \underline{z}))][plusAssociativity →^{proof} Rule tactic] [plusCommutativity →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: (\underline{x} + \underline{y}) = (\underline{y} + \underline{x})][plusCommutativity →^{proof} Rule tactic] [Negative →^{stmt} SystemQ ⊢ ∀\underline{x}: (\underline{x} + (−u\underline{x})) = 0][Negative →^{proof} Rule tactic] [plus0 →^{stmt} SystemQ ⊢ ∀\underline{x}: (\underline{x} + 0) = \underline{x}][plus0 →^{proof} Rule tactic] [timesAssociativity →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: ((\underline{x} ∗ \underline{y}) ∗ \underline{z}) = (\underline{x} ∗ (\underline{y} ∗ \underline{z}))][timesAssociativity →^{proof} Rule tactic] [timesCommutativity →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: (\underline{x} ∗ \underline{y}) = (\underline{y} ∗ \underline{x})][timesCommutativity →^{proof} Rule tactic] [ReciprocalAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ˙¬ (\underline{x} = 0)n ⇒ (\underline{x} ∗ rec\underline{x}) = 1][ReciprocalAxiom →^{proof} Rule tactic] [times1 →^{stmt} SystemQ ⊢ ∀\underline{x}: (\underline{x} ∗ 1) = \underline{x}][times1 →^{proof} Rule tactic] [Distribution →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: (\underline{x} ∗ (\underline{y} + \underline{z})) = ((\underline{x} ∗ \underline{y}) + (\underline{x} ∗ \underline{z}))][Distribution →^{proof} Rule tactic] [0not1 →^{stmt} SystemQ ⊢ ˙¬ (0 = 1)n][0not1 →^{proof} Rule tactic] [EqualityAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} = \underline{y} ⇒ \underline{x} = \underline{z} ⇒ \underline{y} = \underline{z}][EqualityAxiom →^{proof} Rule tactic] [EqLeqAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: \underline{x} = \underline{y} ⇒ \underline{x} <= \underline{y}][EqLeqAxiom →^{proof} Rule tactic] [EqAdditionAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} = \underline{y} ⇒ (\underline{x} + \underline{z}) = (\underline{y} + \underline{z})][EqAdditionAxiom →^{proof} Rule tactic] [EqMultiplicationAxiom →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{y}: ∀\underline{z}: \underline{x} = \underline{y} ⇒ (\underline{x} ∗ \underline{z}) = (\underline{y} ∗ \underline{z})][EqMultiplicationAxiom →^{proof} Rule tactic] [A4(Axiom) →^{stmt} SystemQ ⊢ ∀\underline{x}: ∀\underline{(v1)}: ∀\underline{a}: ∀\underline{b}: ⟨\underline{a}≡\underline{b}|\underline{(v1)}:==\underline{x}⟩_{Me} ⊢⊢ ∀_{obj}\underline{(v1)}: \underline{b} ⇒ \underline{a}][A4(Axiom) →^{proof} Rule tactic] (*** XX snydeaksiomer ***) [==Reflexivity →^{stmt} SystemQ ⊢ ∀\underline{(rx)}: \underline{(rx)} == \underline{(rx)}][==Reflexivity →^{proof} Rule tactic] [==Symmetry →^{stmt} SystemQ ⊢ ∀\underline{(rx)}: ∀\underline{(ry)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(ry)} == \underline{(rx)}][== Symmetry →^{proof} Rule tactic] [==Transitivity →^{stmt} SystemQ ⊢ ∀\underline{(rx)}: ∀\underline{(ry)}: ∀\underline{(rz)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(ry)} == \underline{(rz)} ⊢ \underline{(rx)} == \underline{(rz)}][==Transitivity →^{proof} Rule tactic] XX ikke 100procent identisk med originalen fra equivalence-relations [SENC1 →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(rx)}: ∀\underline{(ry)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(fx)} ∈ \underline{(rx)} ⊢ \underline{(fx)} ∈ \underline{(ry)}][SENC1 →^{proof} Rule tactic] XX boer bevises ud fra nummer 1 [SENC2 →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(rx)}: ∀\underline{(ry)}: \underline{(rx)} == \underline{(ry)} ⊢ \underline{(fx)} ∈ \underline{(ry)} ⊢ \underline{(fx)} ∈ \underline{(rx)}][SENC2 →^{proof} Rule tactic] [PlusF →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{(fx)}: ∀\underline{(fy)}: \underline{(fx)} +_{f} \underline{(fy)}[\underline{m}] = (\underline{(fx)}[\underline{m}] + \underline{(fy)}[\underline{m}])][PlusF →^{proof} Rule tactic] [From == →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: R(\underline{(fx)}) == R(\underline{(fy)}) ⊢ SF(\underline{(fx)}, \underline{(fy)})][From == →^{proof} Rule tactic] [To == →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: SF(\underline{(fx)}, \underline{(fy)}) ⊢ R(\underline{(fx)}) == R(\underline{(fy)})][To == →^{proof} Rule tactic] [FromInR →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: \underline{(fx)} ∈ R(\underline{(fy)}) ⊢ SF(\underline{(fx)}, \underline{(fy)})][FromInR →^{proof} Rule tactic] (*** makroer ***) KVANTI [M_{1} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[M_{1} ¨= \underline{(m1)}]⌉)] [M_{2} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[M_{2} ¨= \underline{(m2)}]⌉)] [N_{1} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[N_{1} ¨= \underline{(n1)}]⌉)] [N_{2} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[N_{2} ¨= \underline{(n2)}]⌉)] [N_{3} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[N_{3} ¨= \underline{(n3)}]⌉)]

[ϵ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ϵ ¨= \underline{(ϵ)}]⌉)]

[ϵ1 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ϵ1 ¨= \underline{(ϵ)_{1}}]⌉)]

[ϵ2 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ϵ2 ¨= \underline{(ϵ2)}]⌉)]

[X_{1} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[X_{1} ¨= \underline{(x1)}]⌉)] [X_{2} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[X_{2} ¨= \underline{(x2)}]⌉)] [Y_{1} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Y_{1} ¨= \underline{(y1)}]⌉)] [Y_{2} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Y_{2} ¨= \underline{(y2)}]⌉)] [V_{1} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[V_{1} ¨= \underline{(v1)}]⌉)] [V_{2} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[V_{2} ¨= \underline{(v2)}]⌉)] [V_{3} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[V_{3} ¨= \underline{(v3)}]⌉)] [V_{4} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[V_{4} ¨= \underline{(v4)}]⌉)] [V_{2n} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[V_{2n} ¨= \underline{(v2n)}]⌉)] [FX →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FX ¨= \underline{(fx)}]⌉)] [FY →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FY ¨= \underline{(fy)}]⌉)] [FZ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FZ ¨= \underline{(fz)}]⌉)] [FU →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FU ¨= \underline{(fu)}]⌉)] [FV →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FV ¨= \underline{(fv)}]⌉)] [FW →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FW ¨= \underline{(fw)}]⌉)] [FEP →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FEP ¨= \underline{(fep)}]⌉)] [RX →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[RX ¨= \underline{(rx)}]⌉)] [RY →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[RY ¨= \underline{(ry)}]⌉)] [RZ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[RZ ¨= \underline{(rz)}]⌉)] [RU →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[RU ¨= \underline{(ru)}]⌉)] [(SX) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SX) ¨= \underline{(sx)}]⌉)] [(SX1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SX1) ¨= \underline{(sx1)}]⌉)] [(SY) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SY) ¨= \underline{(sy)}]⌉)] [(SY1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SY1) ¨= \underline{(sy1)}]⌉)] [(SZ) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SZ) ¨= \underline{(sz)}]⌉)] [(SZ1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SZ1) ¨= \underline{(sz1)}]⌉)] [(SU) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SU) ¨= \underline{(su)}]⌉)] [(SU1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(SU1) ¨= \underline{(su1)}]⌉)] [FXS →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FXS ¨= \underline{(fxs)}]⌉)] [FYS →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[FYS ¨= \underline{(fys)}]⌉)] [(F1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F1) ¨= \underline{(f1)}]⌉)] [(F2) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F2) ¨= \underline{(f2)}]⌉)] [(F3) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F3) ¨= \underline{(f3)}]⌉)] [(F4) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F4) ¨= \underline{(f4)}]⌉)] [(OP1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(OP1) ¨= \underline{(op1)}]⌉)] [(OP2) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(OP2) ¨= \underline{(op2)}]⌉)] [(R1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(R1) ¨= \underline{(r1)}]⌉)] [(S1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(S1) ¨= \underline{(s1)}]⌉)] [(S2) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(S2) ¨= \underline{(s2)}]⌉)] [(EPob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(EPob) ¨= \overline{(ϵ)}]⌉)] [(CRS1ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(CRS1ob) ¨= \overline{(crs1)}]⌉)] [(F1ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F1ob) ¨= \overline{(f1)}]⌉)] [(F2ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F2ob) ¨= \overline{(f2)}]⌉)] [(F3ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F3ob) ¨= \overline{(f3)}]⌉)] [(F4ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(F4ob) ¨= \overline{(f4)}]⌉)] [(N1ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(N1ob) ¨= \overline{(n1)}]⌉)] [(N2ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(N2ob) ¨= \overline{(n2)}]⌉)] [(OP1ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(OP1ob) ¨= \overline{(op1)}]⌉)] [(OP2ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(OP2ob) ¨= \overline{(op2)}]⌉)] [(R1ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(R1ob) ¨= \overline{(r1)}]⌉)] [(S1ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(S1ob) ¨= \overline{(s1)}]⌉)] [(S2ob) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(S2ob) ¨= \overline{(s2)}]⌉)] [(fx) ≤_{f} (fy) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(fx) ≤_{f} (fy) ¨= (fx) <_{f} (fy) ˙∨ SF((fx), (fy))]⌉)] [Ex3 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Ex3 ¨= c_{Ex}]⌉)] [∃(v1): a →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[∃(v1): a ¨= ˙¬ (∀(v1): ˙¬ (a)n)n]⌉)] [x <<== y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x <<== y ¨= x << y ˙∨ x == y]⌉)] [(−1) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(−1) ¨= (−u1)]⌉)] [2 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[2 ¨= (1 + 1)]⌉)] [3 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[3 ¨= (2 + 1)]⌉)] [1/2 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[1/2 ¨= rec2]⌉)] [1/3 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[1/3 ¨= rec3]⌉)] [2/3 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[2/3 ¨= (2 ∗ 1/3)]⌉)] [x < y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x < y ¨= x <= y ˙∧ x ≠ y]⌉)] [x ≠ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≠ y ¨= ˙¬ (x = y)n]⌉)] [(x − y) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(x − y) ¨= (x + (−uy))]⌉)] [00 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[00 ¨= R(0f)]⌉)] [01 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[01 ¨= R(1f)]⌉)] [x!! == y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x!! == y ¨= ˙¬ (x == y)n]⌉)] (*** REGELLEMMAER ***) (*** UDSAGNSLOGIK ***) [ToNegatedImply →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ ˙¬ (\underline{b})n ⊢ ˙¬ (\underline{a} ⇒ \underline{b})n] [ToNegatedImply →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ ˙¬ (\underline{b})n ⊢ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⊢ RemoveDoubleNeg ⊳ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ≫ \underline{a} ⇒ \underline{b}; MP ⊳ \underline{a} ⇒ \underline{b} ⊳ \underline{a} ≫ \underline{b}; FromContradiction ⊳ \underline{b} ⊳ ˙¬ (\underline{b})n ≫ ˙¬ (\underline{a} ⇒ \underline{b})n; ∀\underline{a}: ∀\underline{b}: Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ ˙¬ (\underline{b})n ⊢ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⊢ ˙¬ (\underline{a} ⇒ \underline{b})n ≫ \underline{a} ⇒ ˙¬ (\underline{b})n ⇒ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⇒ ˙¬ (\underline{a} ⇒ \underline{b})n; \underline{a} ⊢ ˙¬ (\underline{b})n ⊢ MP2 ⊳ \underline{a} ⇒ ˙¬ (\underline{b})n ⇒ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⇒ ˙¬ (\underline{a} ⇒ \underline{b})n ⊳ \underline{a} ⊳ ˙¬ (\underline{b})n ≫ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⇒ ˙¬ (\underline{a} ⇒ \underline{b})n; AutoImply ≫ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⇒ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n; Neg ⊳ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⇒ ˙¬ (\underline{a} ⇒ \underline{b})n ⊳ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ⇒ ˙¬ ( ˙¬ (\underline{a} ⇒ \underline{b})n)n ≫ ˙¬ (\underline{a} ⇒ \underline{b})n⌉, p_{0}, c)] [TND →^{stmt} SystemQ ⊢ ∀\underline{a}: ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n] [TND →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: AutoImply ≫ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n; Repetition ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n ≫ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n⌉, p_{0}, c)] [FromNegations →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ \underline{b}] [FromNegations →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ TND ≫ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n; FromDisjuncts ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n ⊳ \underline{a} ⇒ \underline{b} ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ≫ \underline{b}⌉, p_{0}, c)] [prop lemma imply negation →^{stmt} SystemQ ⊢ ∀\underline{a}: \underline{a} ⇒ ˙¬ (\underline{a})n ⊢ ˙¬ (\underline{a})n] [prop lemma imply negation →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: \underline{a} ⇒ ˙¬ (\underline{a})n ⊢ AutoImply ≫ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n; TND ≫ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n; FromDisjuncts ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n ⊳ \underline{a} ⇒ ˙¬ (\underline{a})n ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{a})n ≫ ˙¬ (\underline{a})n⌉, p_{0}, c)] [From3Disjuncts →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{d} ⊢ \underline{b} ⇒ \underline{d} ⊢ \underline{c} ⇒ \underline{d} ⊢ \underline{d}] [From3Disjuncts →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⊢ \underline{b} ⇒ \underline{d} ⊢ \underline{c} ⇒ \underline{d} ⊢ ˙¬ (\underline{a})n ⊢ Repetition ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ≫ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c}; MP ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⊳ ˙¬ (\underline{a})n ≫ ˙¬ (\underline{b})n ⇒ \underline{c}; FromDisjuncts ⊳ ˙¬ (\underline{b})n ⇒ \underline{c} ⊳ \underline{b} ⇒ \underline{d} ⊳ \underline{c} ⇒ \underline{d} ≫ \underline{d}; ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⊢ \underline{b} ⇒ \underline{d} ⊢ \underline{c} ⇒ \underline{d} ⊢ ˙¬ (\underline{a})n ⊢ \underline{d} ≫ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⇒ \underline{b} ⇒ \underline{d} ⇒ \underline{c} ⇒ \underline{d} ⇒ ˙¬ (\underline{a})n ⇒ \underline{d}; AutoImply ≫ \underline{a} ⇒ \underline{d} ⇒ \underline{a} ⇒ \underline{d}; ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{d} ⊢ \underline{b} ⇒ \underline{d} ⊢ \underline{c} ⇒ \underline{d} ⊢ MP3 ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⇒ \underline{b} ⇒ \underline{d} ⇒ \underline{c} ⇒ \underline{d} ⇒ ˙¬ (\underline{a})n ⇒ \underline{d} ⊳ ˙¬ (\underline{a})n ⇒ ˙¬ (\underline{b})n ⇒ \underline{c} ⊳ \underline{b} ⇒ \underline{d} ⊳ \underline{c} ⇒ \underline{d} ≫ ˙¬ (\underline{a})n ⇒ \underline{d}; MP ⊳ \underline{a} ⇒ \underline{d} ⇒ \underline{a} ⇒ \underline{d} ⊳ \underline{a} ⇒ \underline{d} ≫ \underline{a} ⇒ \underline{d}; FromNegations ⊳ \underline{a} ⇒ \underline{d} ⊳ ˙¬ (\underline{a})n ⇒ \underline{d} ≫ \underline{d}⌉, p_{0}, c)] [NegateDisjunct1 →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{a})n ⊢ \underline{b}] [NegateDisjunct1 →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{a})n ⊢ Repetition ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ≫ ˙¬ (\underline{a})n ⇒ \underline{b}; MP ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⊳ ˙¬ (\underline{a})n ≫ \underline{b}⌉, p_{0}, c)] [NegateDisjunct2 →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{b})n ⊢ \underline{a}] [NegateDisjunct2 →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{b})n ⊢ Repetition ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ≫ ˙¬ (\underline{a})n ⇒ \underline{b}; NegativeMT ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⊳ ˙¬ (\underline{b})n ≫ \underline{a}⌉, p_{0}, c)] (***) [ExpandDisjuncts →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{d})n ⇒ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n] [ExpandDisjuncts →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ ˙¬ (\underline{b})n ⊢ ˙¬ (\underline{d})n ⊢ NegateDisjunct2 ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⊳ ˙¬ (\underline{b})n ≫ \underline{a}; NegateDisjunct2 ⊳ ˙¬ (\underline{c})n ⇒ \underline{d} ⊳ ˙¬ (\underline{d})n ≫ \underline{c}; JoinConjuncts ⊳ \underline{a} ⊳ \underline{c} ≫ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n; ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ ˙¬ (\underline{b})n ⊢ ˙¬ (\underline{d})n ⊢ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n ≫ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ (\underline{c})n ⇒ \underline{d} ⇒ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{d})n ⇒ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n; ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ MP2 ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ (\underline{c})n ⇒ \underline{d} ⇒ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{d})n ⇒ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⊳ ˙¬ (\underline{c})n ⇒ \underline{d} ≫ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{d})n ⇒ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n; Repetition ⊳ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{d})n ⇒ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n ≫ ˙¬ (\underline{b})n ⇒ ˙¬ (\underline{d})n ⇒ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{c})n)n⌉, p_{0}, c)] [From2 ∗ 2Disjuncts →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ∀\underline{e}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ⊢ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ⊢ \underline{e}] [From2 ∗ 2Disjuncts →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ∀\underline{e}: ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ⊢ \underline{a} ⊢ MP ⊳ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⊳ \underline{a} ≫ \underline{c} ⇒ \underline{e}; MP ⊳ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ⊳ \underline{a} ≫ \underline{d} ⇒ \underline{e}; FromDisjuncts ⊳ ˙¬ (\underline{c})n ⇒ \underline{d} ⊳ \underline{c} ⇒ \underline{e} ⊳ \underline{d} ⇒ \underline{e} ≫ \underline{e}; ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ∀\underline{e}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ⊢ ˙¬ (\underline{a})n ⊢ NegateDisjunct1 ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⊳ ˙¬ (\underline{a})n ≫ \underline{b}; MP ⊳ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⊳ \underline{b} ≫ \underline{c} ⇒ \underline{e}; MP ⊳ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ⊳ \underline{b} ≫ \underline{d} ⇒ \underline{e}; FromDisjuncts ⊳ ˙¬ (\underline{c})n ⇒ \underline{d} ⊳ \underline{c} ⇒ \underline{e} ⊳ \underline{d} ⇒ \underline{e} ≫ \underline{e}; ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ∀\underline{e}: Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ∀\underline{e}: ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ⊢ \underline{a} ⊢ \underline{e} ≫ ˙¬ (\underline{c})n ⇒ \underline{d} ⇒ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⇒ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ⇒ \underline{a} ⇒ \underline{e}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: ∀\underline{e}: ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ⊢ ˙¬ (\underline{a})n ⊢ \underline{e} ≫ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ (\underline{c})n ⇒ \underline{d} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⇒ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ⇒ ˙¬ (\underline{a})n ⇒ \underline{e}; ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ (\underline{c})n ⇒ \underline{d} ⊢ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ⊢ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⊢ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ⊢ MP3 ⊳ ˙¬ (\underline{c})n ⇒ \underline{d} ⇒ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⇒ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ⇒ \underline{a} ⇒ \underline{e} ⊳ ˙¬ (\underline{c})n ⇒ \underline{d} ⊳ \underline{a} ⇒ \underline{c} ⇒ \underline{e} ⊳ \underline{a} ⇒ \underline{d} ⇒ \underline{e} ≫ \underline{a} ⇒ \underline{e}; MP4 ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ (\underline{c})n ⇒ \underline{d} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⇒ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ⇒ ˙¬ (\underline{a})n ⇒ \underline{e} ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⊳ ˙¬ (\underline{c})n ⇒ \underline{d} ⊳ \underline{b} ⇒ \underline{c} ⇒ \underline{e} ⊳ \underline{b} ⇒ \underline{d} ⇒ \underline{e} ≫ ˙¬ (\underline{a})n ⇒ \underline{e}; FromNegations ⊳ \underline{a} ⇒ \underline{e} ⊳ ˙¬ (\underline{a})n ⇒ \underline{e} ≫ \underline{e}⌉, p_{0}, c)] (*** SAME-F ***) XX-am (*** R-AFDELINGEN ***) XX-am (*******************) [FromNegatedImply →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ (\underline{a} ⇒ \underline{b})n ⊢ ˙¬ (\underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n] [FromNegatedImply →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n ⊢ \underline{a} ⊢ MP ⊳ \underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n ⊳ \underline{a} ≫ ˙¬ ( ˙¬ (\underline{b})n)n; RemoveDoubleNeg ⊳ ˙¬ ( ˙¬ (\underline{b})n)n ≫ \underline{b}; ∀\underline{a}: ∀\underline{b}: Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n ⊢ \underline{a} ⊢ \underline{b} ≫ \underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n ⇒ \underline{a} ⇒ \underline{b}; ˙¬ (\underline{a} ⇒ \underline{b})n ⊢ MT ⊳ \underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n ⇒ \underline{a} ⇒ \underline{b} ⊳ ˙¬ (\underline{a} ⇒ \underline{b})n ≫ ˙¬ (\underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n; Repetition ⊳ ˙¬ (\underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ≫ ˙¬ (\underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n⌉, p_{0}, c)] (***)

[FromNegated(2 ∗ Imply) →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ˙¬ (\underline{a} ⇒ \underline{b} ⇒ \underline{c})n ⊢ ˙¬ ( ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n ⇒ ˙¬ ( ˙¬ (\underline{c})n)n)n] [FromNegated(2 ∗ Imply) →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ˙¬ (\underline{a} ⇒ \underline{b} ⇒ \underline{c})n ⊢ FromNegatedImply ⊳ ˙¬ (\underline{a} ⇒ \underline{b} ⇒ \underline{c})n ≫ ˙¬ (\underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b} ⇒ \underline{c})n)n)n; FirstConjunct ⊳ ˙¬ (\underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b} ⇒ \underline{c})n)n)n ≫ \underline{a}; SecondConjunct ⊳ ˙¬ (\underline{a} ⇒ ˙¬ ( ˙¬ (\underline{b} ⇒ \underline{c})n)n)n ≫ ˙¬ (\underline{b} ⇒ \underline{c})n; FromNegatedImply ⊳ ˙¬ (\underline{b} ⇒ \underline{c})n ≫ ˙¬ (\underline{b} ⇒ ˙¬ ( ˙¬ (\underline{c})n)n)n; FirstConjunct ⊳ ˙¬ (\underline{b} ⇒ ˙¬ ( ˙¬ (\underline{c})n)n)n ≫ \underline{b}; SecondConjunct ⊳ ˙¬ (\underline{b} ⇒ ˙¬ ( ˙¬ (\underline{c})n)n)n ≫ ˙¬ (\underline{c})n; JoinConjuncts ⊳ \underline{a} ⊳ \underline{b} ≫ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n; JoinConjuncts ⊳ ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n ⊳ ˙¬ (\underline{c})n ≫ ˙¬ ( ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n ⇒ ˙¬ ( ˙¬ (\underline{c})n)n)n⌉, p_{0}, c)] [FromNegatedOr →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n ⊢ ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n] [FromNegatedOr →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n ⊢ Repetition ⊳ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n ≫ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n; FromNegatedImply ⊳ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n ≫ ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n⌉, p_{0}, c)] [InductionAxiom →^{stmt} SystemQ ⊢ ∀\underline{(v1)}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ⟨\underline{b}≡\underline{a}|\underline{(v1)}:==0⟩_{Me} ⊢⊢ ⟨\underline{c}≡\underline{a}|\underline{(v1)}:==(\underline{(v1)} + 1)⟩_{Me} ⊢⊢ \underline{b} ⇒ ∀_{obj}\underline{(v1)}: \underline{a} ⇒ \underline{c} ⇒

∀_{obj}\underline{(v1)}: \underline{a}][InductionAxiom →^{proof} Rule tactic]

[LessMinus1(N) →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{n}: Nat(\underline{m}) ⊢⊢ Nat(\underline{n}) ⊢⊢ ˙¬ (\underline{m} <= (\underline{n} + 1) ⇒ ˙¬ ( ˙¬ (\underline{m} = (\underline{n} + 1))n)n)n ⊢ \underline{m} <= \underline{n}][LessMinus1(N) →^{proof} Rule tactic] [Nonnegative(N) →^{stmt} SystemQ ⊢ ∀\underline{m}: Nat(\underline{m}) ⊢⊢ 0 <= \underline{m}][Nonnegative(N) →^{proof} Rule tactic] ————– [Cauchy →^{stmt} SystemQ ⊢ ∀\underline{(v1)}: ∀\underline{(v2)}: ∀\underline{n}: ∀\underline{(ϵ)}: ∀\underline{(fx)}: ∀_{obj}\underline{(ϵ)}: ˙¬ (∀_{obj}\underline{n}: ˙¬ (∀_{obj}\underline{(v1)}: ∀_{obj}\underline{(v2)}: ˙¬ (0 <= \underline{(ϵ)} ⇒ ˙¬ ( ˙¬ (0 = \underline{(ϵ)})n)n)n ⇒ \underline{n} <= \underline{(v1)} ⇒ \underline{n} <= \underline{(v2)} ⇒ ˙¬ (|(\underline{(fx)}[\underline{(v1)}] + (−u\underline{(fx)}[\underline{(v2)}]))| <= \underline{(ϵ)} ⇒

˙¬ ( ˙¬ (|(\underline{(fx)}[\underline{(v1)}] + (−u\underline{(fx)}[\underline{(v2)}]))| = \underline{(ϵ)})n)n)n)n)n][Cauchy →^{proof} Rule tactic] ————- ————– [JoinConjuncts(2conditions) →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ⊢ \underline{a} ⇒ \underline{b} ⇒ ˙¬ (\underline{c} ⇒ ˙¬ (\underline{d})n)n] [JoinConjuncts(2conditions) →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ⊢ \underline{a} ⊢ \underline{b} ⊢ MP2 ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊳ \underline{a} ⊳ \underline{b} ≫ \underline{c}; MP2 ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ⊳ \underline{a} ⊳ \underline{b} ≫ \underline{d}; JoinConjuncts ⊳ \underline{c} ⊳ \underline{d} ≫ ˙¬ (\underline{c} ⇒ ˙¬ (\underline{d})n)n; ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ⊢ \underline{a} ⊢ \underline{b} ⊢ ˙¬ (\underline{c} ⇒ ˙¬ (\underline{d})n)n ≫ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ⇒ \underline{a} ⇒ \underline{b} ⇒ ˙¬ (\underline{c} ⇒ ˙¬ (\underline{d})n)n; \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ⊢ MP2 ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ⇒ \underline{a} ⇒ \underline{b} ⇒ ˙¬ (\underline{c} ⇒ ˙¬ (\underline{d})n)n ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{d} ≫ \underline{a} ⇒ \underline{b} ⇒ ˙¬ (\underline{c} ⇒ ˙¬ (\underline{d})n)n⌉, p_{0}, c)] —————- [FromNegatedAnd →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ ( ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n)n ⊢ \underline{a} ⊢ ˙¬ (\underline{b})n] [FromNegatedAnd →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ ( ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n)n ⊢ \underline{a} ⊢ Repetition ⊳ ˙¬ ( ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n)n ≫ ˙¬ ( ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n)n; RemoveDoubleNeg ⊳ ˙¬ ( ˙¬ (\underline{a} ⇒ ˙¬ (\underline{b})n)n)n ≫ \underline{a} ⇒ ˙¬ (\underline{b})n; MP ⊳ \underline{a} ⇒ ˙¬ (\underline{b})n ⊳ \underline{a} ≫ ˙¬ (\underline{b})n⌉, p_{0}, c)] ——– ———- [ToNegatedOr →^{stmt} SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ⊢ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n] [ToNegatedOr →^{proof} λc.λx.P(⌈SystemQ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ⊢ ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ FirstConjunct ⊳ ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ≫ ˙¬ (\underline{a})n; SecondConjunct ⊳ ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ≫ ˙¬ (\underline{b})n; NegateDisjunct1 ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⊳ ˙¬ (\underline{a})n ≫ \underline{b}; FromContradiction ⊳ \underline{b} ⊳ ˙¬ (\underline{b})n ≫ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n; ∀\underline{a}: ∀\underline{b}: Ded ⊳ ∀\underline{a}: ∀\underline{b}: ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ⊢ ˙¬ (\underline{a})n ⇒ \underline{b} ⊢ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n ≫ ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ⇒ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n; ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ⊢ MP ⊳ ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ⇒ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n ⊳ ˙¬ ( ˙¬ (\underline{a})n ⇒ ˙¬ ( ˙¬ (\underline{b})n)n)n ≫ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n; prop lemma imply negation ⊳ ˙¬ (\underline{a})n ⇒ \underline{b} ⇒ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n ≫ ˙¬ ( ˙¬ (\underline{a})n ⇒ \underline{b})n⌉, p_{0}, c)] ——————– [NextXS(UpperBound) →^{stmt} SystemQ ⊢ ∀\underline{m}: UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals) ⊢ xs[(\underline{m} + 1)] == xs[\underline{m}]][NextXS(UpperBound) →^{proof} Rule tactic] [NextXS(NoUpperBound) →^{stmt} SystemQ ⊢ ∀\underline{m}: ˙¬ (UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals))n ⊢ xs[(\underline{m} + 1)] == 01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}]][NextXS(NoUpperBound) →^{proof} Rule tactic] [NextUS(UpperBound) →^{stmt} SystemQ ⊢ ∀\underline{m}: UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals) ⊢ us[(\underline{m} + 1)] == 01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}]][NextUS(UpperBound) →^{proof} Rule tactic] [NextUS(NoUpperBound) →^{stmt} SystemQ ⊢ ∀\underline{m}: ˙¬ (UB(01//02 ∗ ∗xs[\underline{m}] + +us[\underline{m}], SetOfReals))n ⊢ us[(\underline{m} + 1)] == us[\underline{m}]][NextUS(NoUpperBound) →^{proof} Rule tactic] [US0 →^{stmt} SystemQ ⊢ us[0] == xs[0] + +R(1f)][US0 →^{proof} Rule tactic] [ExpZero →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{x}: \underline{m} = 0 ⊢ \underline{x}(exp)\underline{m} = 1][ExpZero →^{proof} Rule tactic] [ExpPositive →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{x}: ˙¬ (0 <= \underline{m} ⇒ ˙¬ ( ˙¬ (0 = \underline{m})n)n)n ⊢ \underline{x}(exp)\underline{m} = (\underline{x} ∗ \underline{x}(exp)(\underline{m} + (−u1)))][ExpPositive →^{proof} Rule tactic] ————– [BSzero →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{n}: \underline{n} = 0 ⊢ BS(\underline{m}, \underline{n}) = rec(1 + 1)(exp)\underline{m}][BSzero →^{proof} Rule tactic] [BSpositive →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{n}: ˙¬ (0 <= \underline{n} ⇒ ˙¬ ( ˙¬ (0 = \underline{n})n)n)n ⊢ BS(\underline{m}, \underline{n}) = (rec(1 + 1)(exp)(\underline{m} + \underline{n}) + BS(\underline{m}, (\underline{n} + (−u1))))][BSpositive →^{proof} Rule tactic] ———— [UStelescope(Zero) →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{n}: \underline{n} = 0 ⊢ UStelescope(\underline{m}, \underline{n}) = |(us[\underline{m}] + (−uus[(\underline{m} + 1)]))|][UStelescope(Zero) →^{proof} Rule tactic] [UStelescope(Positive) →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{n}: ˙¬ (0 <= \underline{n} ⇒ ˙¬ ( ˙¬ (0 = \underline{n})n)n)n ⊢ UStelescope(\underline{m}, \underline{n}) = (|(us[(\underline{m} + \underline{n})] + (−uus[(\underline{m} + (\underline{n} + 1))]))| + UStelescope(\underline{m}, (\underline{n} + (−u1))))][UStelescope(Positive) →^{proof} Rule tactic] [(x) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(x) ¨= (x)]⌉)] ———- [EqAddition(R) →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)}) = R(\underline{(fy)}) ⊢

R(\underline{(fx)}) + +R(\underline{(fz)}) = R(\underline{(fy)}) + +R(\underline{(fz)})][EqAddition(R) →^{proof} Rule tactic]

[PlusCommutativity(R) →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: R(\underline{(fx)}) + +R(\underline{(fy)}) ==

R(\underline{(fy)}) + +R(\underline{(fx)})][PlusCommutativity(R) →^{proof} Rule tactic] ————— [PlusAssociativity(R) →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)}) + +R(\underline{(fy)}) + +R(\underline{(fz)}) =

R(\underline{(fx)}) + +R(\underline{(fy)}) + +R(\underline{(fz)})][PlusAssociativity(R) →^{proof} Rule tactic]

[PlusAssociativity(R)XX →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)} +_{f} \underline{(fy)} +_{f}

\underline{(fz)}) == R(\underline{(fx)} +_{f} \underline{(fy)} +_{f} \underline{(fz)})][PlusAssociativity(R)XX →^{proof} Rule tactic]

[Plus0(R) →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: R(\underline{(fx)}) + +R(0f) == R(\underline{(fx)})][Plus0(R) →^{proof} Rule tactic] [Negative(R) →^{stmt} SystemQ ⊢ ∀\underline{m}: ∀\underline{(fx)}: R(\underline{(fx)}) + +(− − R(\underline{(fx)})) ==

R(0f)][Negative(R) →^{proof} Rule tactic] [TimesAssociativity(R) →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: ∀\underline{(fy)}: ∀\underline{(fz)}: R(\underline{(fx)}) ∗ ∗R(\underline{(fy)}) ∗ ∗R(\underline{(fz)}) ==

R(\underline{(fx)}) ∗ ∗R(\underline{(fy)}) ∗ ∗R(\underline{(fz)})][TimesAssociativity(R) →^{proof} Rule tactic]

[Times1(R) →^{stmt} SystemQ ⊢ ∀\underline{(fx)}: R(\underline{(fx)}) ∗ ∗R(1f) == R(\underline{(fx)})][Times1(R) →^{proof} Rule tactic] a venter——-

[kvanti →^{prio} Preassociative [kvanti], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)], [S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)],

[S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)], [S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)],

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [check], [[∗ =^{∘} ∗]], [RootVisible(∗)], [A], [R], [C], [T], [L], [\{∗\}], [\overline{∗}], [a], [b], [c], [d], [e], [f ], [g], [h], [i], [j ], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [x], [y], [z], [⟨∗≡ ∗ | ∗:=∗⟩], [⟨∗≡^{0} ∗ | ∗:=∗⟩], [⟨∗≡^{1} ∗ | ∗:=∗⟩], [⟨∗≡^{∗} ∗ | ∗:=∗⟩], [Ded(∗, ∗)], [Ded_{0}(∗, ∗)], [Ded_{1}(∗, ∗, ∗)], [Ded_{2}(∗, ∗, ∗)], [Ded_{3}(∗, ∗, ∗, ∗)], [Ded_{4}(∗, ∗, ∗, ∗)], [Ded_{4}^{∗}(∗, ∗, ∗, ∗)], [Ded_{5}(∗, ∗, ∗)], [Ded_{6}(∗, ∗, ∗, ∗)], [Ded_{6}^{∗}(∗, ∗, ∗, ∗)], [Ded_{7}(∗)], [Ded_{8}(∗, ∗)], [Ded_{8}^{∗}(∗, ∗)], [S], [Neg], [MP], [Gen], [Ded], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [Repetition], [A1′], [A2′], [A4′], [A5′], [Prop 3.2a], [Prop 3.2b], [Prop 3.2c], [Prop 3.2d], [Prop 3.2e_{1}], [Prop 3.2e_{2}], [Prop 3.2e], [Prop 3.2f_{1}], [Prop 3.2f_{2}], [Prop 3.2f], [Prop 3.2g_{1}], [Prop 3.2g_{2}], [Prop 3.2g], [Prop 3.2h_{1}], [Prop 3.2h_{2}], [Prop 3.2h], [Block_{1}(∗, ∗, ∗)], [Block_{2}(∗)], [UniqueMember], [UniqueMember(Type)], [SameSeries], [A4], [SameMember], [Qclosed(Addition)], [Qclosed(Multiplication)], [FromCartProd(1)], [1rule fromCartProd(2)], [constantRationalSeries(∗)], [cartProd(∗)], [Power(∗)], [binaryUnion(∗, ∗)], [SetOfRationalSeries], [IsSubset(∗, ∗)], [(p∗, ∗)], [(s∗)], [(⋯)], [Objekt-var], [Ex-var], [Ph-var], [Værdi], [Variabel], [Op(∗)], [Op(∗, ∗)], [∗ ¨ == ∗], [ContainsEmpty(∗)], [Nat(∗)], [Dedu(∗, ∗)], [Dedu_{0}(∗, ∗)], [Dedu_{s}(∗, ∗, ∗)], [Dedu_{1}(∗, ∗, ∗)], [Dedu_{2}(∗, ∗, ∗)], [Dedu_{3}(∗, ∗, ∗, ∗)], [Dedu_{4}(∗, ∗, ∗, ∗)], [Dedu_{4}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{5}(∗, ∗, ∗)], [Dedu_{6}(∗, ∗, ∗, ∗)], [Dedu_{6}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{7}(∗)], [Dedu_{8}(∗, ∗)], [Dedu_{8}^{∗}(∗, ∗)], [Ex_{1}], [Ex_{2}], [Ex3], [Ex_{10}], [Ex_{20}], [∗_{Ex}], [∗^{Ex}], [⟨∗≡ ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ex}], [ph_{1}], [ph_{2}], [ph_{3}], [∗_{Ph}], [∗^{Ph}], [⟨∗≡ ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡ ∗ | ∗:==∗⟩_{Me}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Me}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Me}], [bs], [OBS], [BS], [Ø], [SystemQ], [MP], [Gen], [Repetition], [Neg], [Ded], [ExistIntro], [Extensionality], [Ødef], [PairDef], [UnionDef], [PowerDef], [SeparationDef], [AddDoubleNeg], [RemoveDoubleNeg], [AndCommutativity], [AutoImply], [Contrapositive], [FirstConjunct], [SecondConjunct], [FromContradiction], [FromDisjuncts], [IffCommutativity], [IffFirst], [IffSecond], [ImplyTransitivity], [JoinConjuncts], [MP2], [MP3], [MP4], [MP5], [MT], [NegativeMT], [Technicality], [Weakening], [WeakenOr1], [WeakenOr2], [Formula2Pair], [Pair2Formula], [Formula2Union], [Union2Formula], [Formula2Sep], [Sep2Formula], [Formula2Power], [SubsetInPower], [HelperPowerIsSub], [PowerIsSub], [(Switch)HelperPowerIsSub], [(Switch)PowerIsSub], [ToSetEquality], [HelperToSetEquality(t)], [ToSetEquality(t)], [HelperFromSetEquality], [FromSetEquality], [HelperReflexivity], [Reflexivity], [HelperSymmetry], [Symmetry], [HelperTransitivity], [Transitivity], [ERisReflexive], [ERisSymmetric], [ERisTransitive], [ØisSubset], [HelperMemberNotØ], [MemberNotØ], [HelperUniqueØ], [UniqueØ], [==Reflexivity], [==Symmetry], [Helper==Transitivity], [==Transitivity], [HelperTransferNotEq], [TransferNotEq], [HelperPairSubset], [Helper(2)PairSubset], [PairSubset], [SamePair], [SameSingleton], [UnionSubset], [SameUnion], [SeparationSubset], [SameSeparation], [SameBinaryUnion], [IntersectionSubset], [SameIntersection], [AutoMember], [HelperEqSysNotØ], [EqSysNotØ], [HelperEqSubset], [EqSubset], [HelperEqNecessary], [EqNecessary], [HelperNoneEqNecessary], [Helper(2)NoneEqNecessary], [NoneEqNecessary], [EqClassIsSubset], [EqClassesAreDisjoint], [AllDisjoint], [AllDisjointImply], [BSsubset], [Union(BS/R)subset], [UnionIdentity], [EqSysIsPartition], [(x1)], [(x2)], [(y1)], [(y2)], [(v1)], [(v2)], [(v3)], [(v4)], [(v2n)], [(m1)], [(m2)], [(n1)], [(n2)], [(n3)], [(ϵ)], [(ϵ)_{1}], [(ϵ2)], [(fep)], [(fx)], [(fy)], [(fz)], [(fu)], [(fv)], [(fw)], [(rx)], [(ry)], [(rz)], [(ru)], [(sx)], [(sx1)], [(sy)], [(sy1)], [(sz)], [(sz1)], [(su)], [(su1)], [(fxs)], [(fys)], [(crs1)], [(f1)], [(f2)], [(f3)], [(f4)], [(op1)], [(op2)], [(r1)], [(s1)], [(s2)], [X_{1}], [X_{2}], [Y_{1}], [Y_{2}], [V_{1}], [V_{2}], [V_{3}], [V_{4}], [V_{2n}], [M_{1}], [M_{2}], [N_{1}], [N_{2}], [N_{3}], [ϵ], [ϵ1], [ϵ2], [FX], [FY], [FZ], [FU], [FV], [FW], [FEP], [RX], [RY], [RZ], [RU], [(SX)], [(SX1)], [(SY)], [(SY1)], [(SZ)], [(SZ1)], [(SU)], [(SU1)], [FXS], [FYS], [(F1)], [(F2)], [(F3)], [(F4)], [(OP1)], [(OP2)], [(R1)], [(S1)], [(S2)], [(EPob)], [(CRS1ob)], [(F1ob)], [(F2ob)], [(F3ob)], [(F4ob)], [(N1ob)], [(N2ob)], [(OP1ob)], [(OP2ob)], [(R1ob)], [(S1ob)], [(S2ob)], [ph_{4}], [ph_{5}], [ph_{6}], [NAT], [RATIONAL_{S}ERIES], [SERIES], [SetOfReals], [SetOfFxs], [N], [Q], [X], [xs], [xaF], [ysF], [us], [usFoelge], [0], [1], [(−1)], [2], [3], [1/2], [1/3], [2/3], [0f], [1f], [00], [01], [(− − 01)], [02], [01//02], [PlusAssociativity(R)], [PlusAssociativity(R)XX], [Plus0(R)], [Negative(R)], [Times1(R)], [lessAddition(R)], [PlusCommutativity(R)], [LeqAntisymmetry(R)], [LeqTransitivity(R)], [leqAddition(R)], [Distribution(R)], [A4(Axiom)], [InductionAxiom], [EqualityAxiom], [EqLeqAxiom], [EqAdditionAxiom], [EqMultiplicationAxiom], [QisClosed(Reciprocal)(Imply)], [QisClosed(Reciprocal)], [QisClosed(Negative)(Imply)], [QisClosed(Negative)], [leqReflexivity], [leqAntisymmetryAxiom], [leqTransitivityAxiom], [leqTotality], [leqAdditionAxiom], [leqMultiplicationAxiom], [plusAssociativity], [plusCommutativity], [Negative], [plus0], [timesAssociativity], [timesCommutativity], [ReciprocalAxiom], [times1], [Distribution], [0not1], [lemma eqLeq(R)], [TimesAssociativity(R)], [TimesCommutativity(R)], [(Adgic)SameR], [Separation2formula(1)], [Separation2formula(2)], [Cauchy], [PlusF], [ReciprocalF], [From ==], [To ==], [FromInR], [PlusR(Sym)], [ReciprocalR(Axiom)], [LessMinus1(N)], [Nonnegative(N)], [US0], [NextXS(UpperBound)], [NextXS(NoUpperBound)], [NextUS(UpperBound)], [NextUS(NoUpperBound)], [ExpZero], [ExpPositive], [ExpZero(R)], [ExpPositive(R)], [BSzero], [BSpositive], [UStelescope(Zero)], [UStelescope(Positive)], [EqAddition(R)], [FromLimit], [ToUpperBound], [FromUpperBound], [USisUpperBound], [0not1(R)], [ExpUnbounded(R)], [FromLeq(Advanced)(N)], [FromLeastUpperBound], [ToLeastUpperBound], [XSisNotUpperBound], [ysFGreater], [ysFLess], [SmallInverse], [NatType], [RationalType], [SeriesType], [Max], [Numerical], [NumericalF], [MemberOfSeries(Imply)], [JoinConjuncts(2conditions)], [prop lemma imply negation], [TND], [FromNegatedImply], [ToNegatedImply], [FromNegated(2 ∗ Imply)], [FromNegatedAnd], [FromNegatedOr], [ToNegatedOr], [FromNegations], [From3Disjuncts], [From2 ∗ 2Disjuncts], [NegateDisjunct1], [NegateDisjunct2], [ExpandDisjuncts], [SENC1], [SENC2], [LessLeq(R)], [MemberOfSeries], [memberOfSeries(Type)]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)], [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗^{hide}]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], ["∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗], [MacroIndent(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗(exp)∗]; Preassociative [∗′], [R(∗)], [− − R(∗)], [rec∗]; Preassociative [∗/∗], [∗ ∩ ∗], [∗[∗]]; Preassociative [∪∗], [∗ ∪ ∗], [P(∗)]; Preassociative [{∗}], [StateExpand(∗, ∗, ∗)], [extractSeries(∗)], [SetOfSeries(∗)], [− − Macro(∗)], [ExpandList(∗, ∗, ∗)], [∗ ∗ Macro(∗)], [+ + Macro(∗)], [<< Macro(∗)], [||Macro(∗)], [01//Macro(∗)], [UB(∗, ∗)], [LUB(∗, ∗)], [BS(∗, ∗)], [UStelescope(∗, ∗)], [(∗)], [|f ∗ |], [|r ∗ |], [Limit(∗, ∗)], [Union(∗)], [IsOrderedPair(∗, ∗, ∗)], [IsRelation(∗, ∗, ∗)], [isFunction(∗, ∗, ∗)], [IsSeries(∗, ∗)], [IsNatural(∗, ∗)], [OrderedPair(∗, ∗)], [TypeNat(∗)], [TypeNat0(∗)], [TypeRational(∗)], [TypeRational0(∗)], [TypeSeries(∗, ∗)], [Typeseries0(∗, ∗)]; Preassociative [{∗, ∗}], [⟨∗, ∗⟩], [(−u∗)], [−_{f}∗], [(− − ∗)], [1f/∗], [01//temp∗]; Preassociative [∗(∗, ∗)], [ReflRel(∗, ∗)], [SymRel(∗, ∗)], [TransRel(∗, ∗)], [EqRel(∗, ∗)], [[∗ ∈ ∗]_{∗}], [Partition(∗, ∗)]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [(∗ ∗ ∗)], [∗ ∗_{f} ∗], [∗ ∗ ∗∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [(∗ + ∗)], [(∗ − ∗)], [∗ +_{f} ∗], [∗ −_{f} ∗], [∗ + +∗], [R(∗) − −R(∗)]; Preassociative [∗ ∈ ∗]; Preassociative [| ∗ |], [if(∗, ∗, ∗)], [Max(∗, ∗)], [Max(∗, ∗)]; Preassociative [∗ = ∗], [∗ ≠ ∗], [∗ <= ∗], [∗ < ∗], [∗ <_{f} ∗], [∗ ≤_{f} ∗], [SF(∗, ∗)], [∗ == ∗], [∗!! == ∗], [∗ << ∗], [∗ <<== ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗], [∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ = ∗], [∗ ≠ ∗], [∗^{var}], [∗#^{0}∗], [∗#^{1}∗], [∗#^{∗}∗], [∗==∗], [∗ ⊆ ∗]; Preassociative [¬∗], [ ˙¬ (∗)n], [∗ ∉ ∗], [∗ ≠ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗]; Postassociative [∗ ˙∨ ∗]; Preassociative [∃∗: ∗], [∀∗: ∗], [∀_{obj}∗: ∗], [∃∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗], [∗ ⇔ ∗], [∗ ˙⇔ ∗]; Preassociative [{ph ∈ ∗ | ∗}]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗#∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗], [∗ ⊵ ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗], [Π∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗], [Begin ∗; ∗ : End; ∗], [Last block line ∗ ≫ ∗; ], [Arbitrary ≫ ∗; ∗]; Postassociative [∗ | ∗]; Postassociative [∗ , ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗], [∗ linebreak[4] ∗], [∗\\∗]; ]

A Pyk definitioner

[UniqueMember →^{pyk} “lemma uniqueMember”] [UniqueMember(Type) →^{pyk} “lemma uniqueMember(Type)”] [SameSeries →^{pyk} “lemma sameSeries”] [A4 →^{pyk} “lemma a4”] [SameMember →^{pyk} “lemma sameMember”] [Qclosed(Addition) →^{pyk} “1rule Qclosed(Addition)”] [Qclosed(Multiplication) →^{pyk} “1rule Qclosed(Multiplication)”] [FromCartProd(1) →^{pyk} “1rule fromCartProd(1)”] [1rule fromCartProd(2) →^{pyk} “1rule fromCartProd(2)”] [constantRationalSeries(∗) →^{pyk} “constantRationalSeries( " )”] [cartProd(∗) →^{pyk} “cartProd( " , " )”] [Power(∗) →^{pyk} “P( " )”] [binaryUnion(∗, ∗) →^{pyk} “binaryUnion( " , " )”] [SetOfRationalSeries →^{pyk} “setOfRationalSeries”] [IsSubset(∗, ∗) →^{pyk} “isSubset( " , " )”]

[(p∗, ∗) →^{pyk} “(p " , " )”]

[(s∗) →^{pyk} “(s " )”]

[(⋯) →^{pyk} “cdots”] [Objekt-var →^{pyk} “object-var”] [Ex-var →^{pyk} “ex-var”] [Ph-var →^{pyk} “ph-var”] [Værdi →^{pyk} “vaerdi”] [Variabel →^{pyk} “variabel”] [Op(∗) →^{pyk} “op " end op”] [Op(∗, ∗) →^{pyk} “op2 " comma " end op2”] [∗ ¨ == ∗ →^{pyk} “define-equal " comma " end equal”] [ContainsEmpty(∗) →^{pyk} “contains-empty " end empty”] [Nat(∗) →^{pyk} “Nat( " )”] [Dedu(∗, ∗) →^{pyk} “1deduction " conclude " end 1deduction”] [Dedu_{0}(∗, ∗) →^{pyk} “1deduction zero " conclude " end 1deduction”] [Dedu_{s}(∗, ∗, ∗) →^{pyk} “1deduction side " conclude " condition " end 1deduction”] [Dedu_{1}(∗, ∗, ∗) →^{pyk} “1deduction one " conclude " condition " end 1deduction”] [Dedu_{2}(∗, ∗, ∗) →^{pyk} “1deduction two " conclude " condition " end 1deduction”] [Dedu_{3}(∗, ∗, ∗, ∗) →^{pyk} “1deduction three " conclude " condition " bound " end 1deduction”] [Dedu_{4}(∗, ∗, ∗, ∗) →^{pyk} “1deduction four " conclude " condition " bound " end 1deduction”] [Dedu_{4}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “1deduction four star " conclude " condition " bound " end 1deduction”] [Dedu_{5}(∗, ∗, ∗) →^{pyk} “1deduction five " condition " bound " end 1deduction”] [Dedu_{6}(∗, ∗, ∗, ∗) →^{pyk} “1deduction six " conclude " exception " bound " end 1deduction”] [Dedu_{6}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “1deduction six star " conclude " exception " bound " end 1deduction”] [Dedu_{7}(∗) →^{pyk} “1deduction seven " end 1deduction”] [Dedu_{8}(∗, ∗) →^{pyk} “1deduction eight " bound " end 1deduction”] [Dedu_{8}^{∗}(∗, ∗) →^{pyk} “1deduction eight star " bound " end 1deduction”]

[Ex_{1} →^{pyk} “ex1”]

[Ex_{2} →^{pyk} “ex2”]

[Ex3 →^{pyk} “ex3”]

[Ex_{10} →^{pyk} “ex10”]

[Ex_{20} →^{pyk} “ex20”]

[∗_{Ex} →^{pyk} “existential var " end var”] [∗^{Ex} →^{pyk} “" is existential var”] [⟨∗≡ ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub " is " where " is " end sub”] [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub0 " is " where " is " end sub”] [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub1 " is " where " is " end sub”] [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub∗ " is " where " is " end sub”]

[ph_{1} →^{pyk} “ph1”]

[ph_{2} →^{pyk} “ph2”]

[ph_{3} →^{pyk} “ph3”]

[∗_{Ph} →^{pyk} “placeholder-var " end var”] [∗^{Ph} →^{pyk} “" is placeholder-var”] [⟨∗≡ ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub " is " where " is " end sub”] [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub0 " is " where " is " end sub”] [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub1 " is " where " is " end sub”] [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub∗ " is " where " is " end sub”] [⟨∗≡ ∗ | ∗:==∗⟩_{Me} →^{pyk} “meta-sub " is " where " is " end sub”] [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Me} →^{pyk} “meta-sub1 " is " where " is " end sub”] [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Me} →^{pyk} “meta-sub∗ " is " where " is " end sub”] [bs →^{pyk} “var big set”] [OBS →^{pyk} “object big set”] [BS →^{pyk} “meta big set”] [Ø →^{pyk} “zermelo empty set”] [SystemQ →^{pyk} “system Q”] [MP →^{pyk} “1rule mp”] [Gen →^{pyk} “1rule gen”] [Repetition →^{pyk} “1rule repetition”] [Neg →^{pyk} “1rule ad absurdum”] [Ded →^{pyk} “1rule deduction”] [ExistIntro →^{pyk} “1rule exist intro”] [Extensionality →^{pyk} “axiom extensionality”] [Ødef →^{pyk} “axiom empty set”] [PairDef →^{pyk} “axiom pair definition”] [UnionDef →^{pyk} “axiom union definition”] [PowerDef →^{pyk} “axiom power definition”] [SeparationDef →^{pyk} “axiom separation definition”] [AddDoubleNeg →^{pyk} “prop lemma add double neg”] [RemoveDoubleNeg →^{pyk} “prop lemma remove double neg”] [AndCommutativity →^{pyk} “prop lemma and commutativity”] [AutoImply →^{pyk} “prop lemma auto imply”] [Contrapositive →^{pyk} “prop lemma contrapositive”] [FirstConjunct →^{pyk} “prop lemma first conjunct”] [SecondConjunct →^{pyk} “prop lemma second conjunct”] [FromContradiction →^{pyk} “prop lemma from contradiction”] [FromDisjuncts →^{pyk} “prop lemma from disjuncts”] [IffCommutativity →^{pyk} “prop lemma iff commutativity”] [IffFirst →^{pyk} “prop lemma iff first”] [IffSecond →^{pyk} “prop lemma iff second”] [ImplyTransitivity →^{pyk} “prop lemma imply transitivity”] [JoinConjuncts →^{pyk} “prop lemma join conjuncts”] [MP2 →^{pyk} “prop lemma mp2”] [MP3 →^{pyk} “prop lemma mp3”] [MP4 →^{pyk} “prop lemma mp4”] [MP5 →^{pyk} “prop lemma mp5”] [MT →^{pyk} “prop lemma mt”] [NegativeMT →^{pyk} “prop lemma negative mt”] [Technicality →^{pyk} “prop lemma technicality”] [Weakening →^{pyk} “prop lemma weakening”] [WeakenOr1 →^{pyk} “prop lemma weaken or first”] [WeakenOr2 →^{pyk} “prop lemma weaken or second”] [Formula2Pair →^{pyk} “lemma formula2pair”] [Pair2Formula →^{pyk} “lemma pair2formula”] [Formula2Union →^{pyk} “lemma formula2union”] [Union2Formula →^{pyk} “lemma union2formula”] [Formula2Sep →^{pyk} “lemma formula2separation”] [Sep2Formula →^{pyk} “lemma separation2formula”] [Formula2Power →^{pyk} “lemma formula2power”] [SubsetInPower →^{pyk} “lemma subset in power set”] [HelperPowerIsSub →^{pyk} “lemma power set is subset0”] [PowerIsSub →^{pyk} “lemma power set is subset”] [(Switch)HelperPowerIsSub →^{pyk} “lemma power set is subset0-switch”] [(Switch)PowerIsSub →^{pyk} “lemma power set is subset-switch”] [ToSetEquality →^{pyk} “lemma set equality suff condition”] [HelperToSetEquality(t) →^{pyk} “lemma set equality suff condition(t)0”] [ToSetEquality(t) →^{pyk} “lemma set equality suff condition(t)”] [HelperFromSetEquality →^{pyk} “lemma set equality skip quantifier”] [FromSetEquality →^{pyk} “lemma set equality nec condition”] [HelperReflexivity →^{pyk} “lemma reflexivity0”] [Reflexivity →^{pyk} “lemma reflexivity”] [HelperSymmetry →^{pyk} “lemma symmetry0”] [Symmetry →^{pyk} “lemma symmetry”] [HelperTransitivity →^{pyk} “lemma transitivity0”] [Transitivity →^{pyk} “lemma transitivity”] [ERisReflexive →^{pyk} “lemma er is reflexive”] [ERisSymmetric →^{pyk} “lemma er is symmetric”] [ERisTransitive →^{pyk} “lemma er is transitive”] [ØisSubset →^{pyk} “lemma empty set is subset”] [HelperMemberNotØ →^{pyk} “lemma member not empty0”] [MemberNotØ →^{pyk} “lemma member not empty”] [HelperUniqueØ →^{pyk} “lemma unique empty set0”] [UniqueØ →^{pyk} “lemma unique empty set”] [==Reflexivity →^{pyk} “lemma ==Reflexivity”] [==Symmetry →^{pyk} “lemma ==Symmetry”] [Helper==Transitivity →^{pyk} “lemma ==Transitivity0”] [==Transitivity →^{pyk} “lemma ==Transitivity”] [HelperTransferNotEq →^{pyk} “lemma transfer ˜ is0”] [TransferNotEq →^{pyk} “lemma transfer ˜ is”] [HelperPairSubset →^{pyk} “lemma pair subset0”] [Helper(2)PairSubset →^{pyk} “lemma pair subset1”] [PairSubset →^{pyk} “lemma pair subset”] [SamePair →^{pyk} “lemma same pair”] [SameSingleton →^{pyk} “lemma same singleton”] [UnionSubset →^{pyk} “lemma union subset”] [SameUnion →^{pyk} “lemma same union”] [SeparationSubset →^{pyk} “lemma separation subset”] [SameSeparation →^{pyk} “lemma same separation”] [SameBinaryUnion →^{pyk} “lemma same binary union”] [IntersectionSubset →^{pyk} “lemma intersection subset”] [SameIntersection →^{pyk} “lemma same intersection”] [AutoMember →^{pyk} “lemma auto member”] [HelperEqSysNotØ →^{pyk} “lemma eq-system not empty0”] [EqSysNotØ →^{pyk} “lemma eq-system not empty”] [HelperEqSubset →^{pyk} “lemma eq subset0”] [EqSubset →^{pyk} “lemma eq subset”] [HelperEqNecessary →^{pyk} “lemma equivalence nec condition0”] [EqNecessary →^{pyk} “lemma equivalence nec condition”] [HelperNoneEqNecessary →^{pyk} “lemma none-equivalence nec condition0”] [Helper(2)NoneEqNecessary →^{pyk} “lemma none-equivalence nec condition1”] [NoneEqNecessary →^{pyk} “lemma none-equivalence nec condition”] [EqClassIsSubset →^{pyk} “lemma equivalence class is subset”] [EqClassesAreDisjoint →^{pyk} “lemma equivalence classes are disjoint”] [AllDisjoint →^{pyk} “lemma all disjoint”] [AllDisjointImply →^{pyk} “lemma all disjoint-imply”] [BSsubset →^{pyk} “lemma bs subset union(bs/r)”] [Union(BS/R)subset →^{pyk} “lemma union(bs/r) subset bs”] [UnionIdentity →^{pyk} “lemma union(bs/r) is bs”] [EqSysIsPartition →^{pyk} “theorem eq-system is partition”] [(x1) →^{pyk} “var x1”] [(x2) →^{pyk} “var x2”] [(y1) →^{pyk} “var y1”] [(y2) →^{pyk} “var y2”] [(v1) →^{pyk} “var v1”] [(v2) →^{pyk} “var v2”] [(v3) →^{pyk} “var v3”] [(v4) →^{pyk} “var v4”] [(v2n) →^{pyk} “var v2n”] [(m1) →^{pyk} “var m1”] [(m2) →^{pyk} “var m2”] [(n1) →^{pyk} “var n1”] [(n2) →^{pyk} “var n2”] [(n3) →^{pyk} “var n3”] [(ϵ) →^{pyk} “var ep”] [(ϵ)_{1} →^{pyk} “var ep1”] [(ϵ2) →^{pyk} “var ep2”] [(fep) →^{pyk} “var fep”] [(fx) →^{pyk} “var fx”] [(fy) →^{pyk} “var fy”] [(fz) →^{pyk} “var fz”] [(fu) →^{pyk} “var fu”] [(fv) →^{pyk} “var fv”] [(fw) →^{pyk} “var fw”] [(rx) →^{pyk} “var rx”] [(ry) →^{pyk} “var ry”] [(rz) →^{pyk} “var rz”] [(ru) →^{pyk} “var ru”] [(sx) →^{pyk} “var sx”] [(sx1) →^{pyk} “var sx1”] [(sy) →^{pyk} “var sy”] [(sy1) →^{pyk} “var sy1”] [(sz) →^{pyk} “var sz”] [(sz1) →^{pyk} “var sz1”] [(su) →^{pyk} “var su”] [(su1) →^{pyk} “var su1”] [(fxs) →^{pyk} “var fxs”] [(fys) →^{pyk} “var fys”] [(crs1) →^{pyk} “var crs1”] [(f1) →^{pyk} “var f1”] [(f2) →^{pyk} “var f2”] [(f3) →^{pyk} “var f3”] [(f4) →^{pyk} “var f4”] [(op1) →^{pyk} “var op1”] [(op2) →^{pyk} “var op2”] [(r1) →^{pyk} “var r1”] [(s1) →^{pyk} “var s1”] [(s2) →^{pyk} “var s2”] [X_{1} →^{pyk} “meta x1”] [X_{2} →^{pyk} “meta x2”] [Y_{1} →^{pyk} “meta y1”] [Y_{2} →^{pyk} “meta y2”] [V_{1} →^{pyk} “meta v1”] [V_{2} →^{pyk} “meta v2”] [V_{3} →^{pyk} “meta v3”] [V_{4} →^{pyk} “meta v4”] [V_{2n} →^{pyk} “meta v2n”] [M_{1} →^{pyk} “meta m1”] [M_{2} →^{pyk} “meta m2”] [N_{1} →^{pyk} “meta n1”] [N_{2} →^{pyk} “meta n2”] [N_{3} →^{pyk} “meta n3”] [ϵ →^{pyk} “meta ep”] [ϵ1 →^{pyk} “meta ep1”] [ϵ2 →^{pyk} “meta ep2”] [FX →^{pyk} “meta fx”] [FY →^{pyk} “meta fy”] [FZ →^{pyk} “meta fz”] [FU →^{pyk} “meta fu”] [FV →^{pyk} “meta fv”] [FW →^{pyk} “meta fw”] [FEP →^{pyk} “meta fep”] [RX →^{pyk} “meta rx”] [RY →^{pyk} “meta ry”] [RZ →^{pyk} “meta rz”] [RU →^{pyk} “meta ru”] [(SX) →^{pyk} “meta sx”] [(SX1) →^{pyk} “meta sx1”] [(SY) →^{pyk} “meta sy”] [(SY1) →^{pyk} “meta sy1”] [(SZ) →^{pyk} “meta sz”] [(SZ1) →^{pyk} “meta sz1”] [(SU) →^{pyk} “meta su”] [(SU1) →^{pyk} “meta su1”] [FXS →^{pyk} “meta fxs”] [FYS →^{pyk} “meta fys”] [(F1) →^{pyk} “meta f1”] [(F2) →^{pyk} “meta f2”] [(F3) →^{pyk} “meta f3”] [(F4) →^{pyk} “meta f4”] [(OP1) →^{pyk} “meta op1”] [(OP2) →^{pyk} “meta op2”] [(R1) →^{pyk} “meta r1”] [(S1) →^{pyk} “meta s1”] [(S2) →^{pyk} “meta s2”] [(EPob) →^{pyk} “object ep”] [(CRS1ob) →^{pyk} “object crs1”] [(F1ob) →^{pyk} “object f1”] [(F2ob) →^{pyk} “object f2”] [(F3ob) →^{pyk} “object f3”] [(F4ob) →^{pyk} “object f4”] [(N1ob) →^{pyk} “object n1”] [(N2ob) →^{pyk} “object n2”] [(OP1ob) →^{pyk} “object op1”] [(OP2ob) →^{pyk} “object op2”] [(R1ob) →^{pyk} “object r1”] [(S1ob) →^{pyk} “object s1”] [(S2ob) →^{pyk} “object s2”]

[ph_{4} →^{pyk} “ph4”]

[ph_{5} →^{pyk} “ph5”]

[ph_{6} →^{pyk} “ph6”]

[NAT →^{pyk} “NAT”] [RATIONAL_{S}ERIES →^{pyk} “RATIONAL SERIES”] [SERIES →^{pyk} “SERIES”] [SetOfReals →^{pyk} “setOfReals”] [SetOfFxs →^{pyk} “setOfFxs”]

[N →^{pyk} “N”]

[Q →^{pyk} “Q”]

[X →^{pyk} “X”]

[xs →^{pyk} “xs”]

[xaF →^{pyk} “xsF”] [ysF →^{pyk} “ysF”]

[us →^{pyk} “us”]

[usFoelge →^{pyk} “usF”]

[0 →^{pyk} “0”]

[1 →^{pyk} “1”]

[(−1) →^{pyk} “(-1)”]

[2 →^{pyk} “2”]

[3 →^{pyk} “3”]

[1/2 →^{pyk} “1/2”]

[1/3 →^{pyk} “1/3”]

[2/3 →^{pyk} “2/3”]

[0f →^{pyk} “0f”]

[1f →^{pyk} “1f”]

[00 →^{pyk} “00”]

[01 →^{pyk} “01”]

[(− − 01) →^{pyk} “(--01)”]

[02 →^{pyk} “02”]

[01//02 →^{pyk} “01//02”]

[PlusAssociativity(R) →^{pyk} “lemma plusAssociativity(R)”] [PlusAssociativity(R)XX →^{pyk} “lemma plusAssociativity(R)XX”] [Plus0(R) →^{pyk} “lemma plus0(R)”] [Negative(R) →^{pyk} “lemma negative(R)”] [Times1(R) →^{pyk} “lemma times1(R)”] [lessAddition(R) →^{pyk} “lemma lessAddition(R)”] [PlusCommutativity(R) →^{pyk} “lemma plusCommutativity(R)”] [LeqAntisymmetry(R) →^{pyk} “lemma leqAntisymmetry(R)”] [LeqTransitivity(R) →^{pyk} “lemma leqTransitivity(R)”] [leqAddition(R) →^{pyk} “lemma leqAddition(R)”] [Distribution(R) →^{pyk} “lemma distribution(R)”] [A4(Axiom) →^{pyk} “axiom a4”] [InductionAxiom →^{pyk} “axiom induction”] [EqualityAxiom →^{pyk} “axiom equality”] [EqLeqAxiom →^{pyk} “axiom eqLeq”] [EqAdditionAxiom →^{pyk} “axiom eqAddition”] [EqMultiplicationAxiom →^{pyk} “axiom eqMultiplication”] [QisClosed(Reciprocal)(Imply) →^{pyk} “axiom QisClosed(reciprocal)”] [QisClosed(Reciprocal) →^{pyk} “lemma QisClosed(reciprocal)”] [QisClosed(Negative)(Imply) →^{pyk} “axiom QisClosed(negative)”] [QisClosed(Negative) →^{pyk} “lemma QisClosed(negative)”] [leqReflexivity →^{pyk} “axiom leqReflexivity”] [leqAntisymmetryAxiom →^{pyk} “axiom leqAntisymmetry”] [leqTransitivityAxiom →^{pyk} “axiom leqTransitivity”] [leqTotality →^{pyk} “axiom leqTotality”] [leqAdditionAxiom →^{pyk} “axiom leqAddition”] [leqMultiplicationAxiom →^{pyk} “axiom leqMultiplication”] [plusAssociativity →^{pyk} “axiom plusAssociativity”] [plusCommutativity →^{pyk} “axiom plusCommutativity”] [Negative →^{pyk} “axiom negative”] [plus0 →^{pyk} “axiom plus0”] [timesAssociativity →^{pyk} “axiom timesAssociativity”] [timesCommutativity →^{pyk} “axiom timesCommutativity”] [ReciprocalAxiom →^{pyk} “axiom reciprocal”] [times1 →^{pyk} “axiom times1”] [Distribution →^{pyk} “axiom distribution”] [0not1 →^{pyk} “axiom 0not1”] [lemma eqLeq(R) →^{pyk} “lemma eqLeq(R)”] [TimesAssociativity(R) →^{pyk} “lemma timesAssociativity(R)”] [TimesCommutativity(R) →^{pyk} “lemma timesCommutativity(R)”] [(Adgic)SameR →^{pyk} “1rule adhoc sameR”] [Separation2formula(1) →^{pyk} “lemma separation2formula(1)”] [Separation2formula(2) →^{pyk} “lemma separation2formula(2)”] [Cauchy →^{pyk} “axiom cauchy”] [PlusF →^{pyk} “axiom plusF”] [ReciprocalF →^{pyk} “axiom reciprocalF”] [From == →^{pyk} “1rule from==”] [To == →^{pyk} “1rule to==”] [FromInR →^{pyk} “1rule fromInR”] [PlusR(Sym) →^{pyk} “lemma plusR(Sym)”] [ReciprocalR(Axiom) →^{pyk} “axiom reciprocalR”] [LessMinus1(N) →^{pyk} “1rule lessMinus1(N)”] [Nonnegative(N) →^{pyk} “axiom nonnegative(N)”] [US0 →^{pyk} “axiom US0”] [NextXS(UpperBound) →^{pyk} “1rule nextXS(upperBound)”] [NextXS(NoUpperBound) →^{pyk} “1rule nextXS(noUpperBound)”] [NextUS(UpperBound) →^{pyk} “1rule nextUS(upperBound)”] [NextUS(NoUpperBound) →^{pyk} “1rule nextUS(noUpperBound)”] [ExpZero →^{pyk} “1rule expZero”] [ExpPositive →^{pyk} “1rule expPositive”] [ExpZero(R) →^{pyk} “1rule expZero(R)”] [ExpPositive(R) →^{pyk} “1rule expPositive(R)”] [BSzero →^{pyk} “1rule base(1/2)Sum zero”] [BSpositive →^{pyk} “1rule base(1/2)Sum positive”] [UStelescope(Zero) →^{pyk} “1rule UStelescope zero”] [UStelescope(Positive) →^{pyk} “1rule UStelescope positive”] [EqAddition(R) →^{pyk} “1rule adhoc eqAddition(R)”] [FromLimit →^{pyk} “1rule fromLimit”] [ToUpperBound →^{pyk} “1rule toUpperBound”] [FromUpperBound →^{pyk} “1rule fromUpperBound”] [USisUpperBound →^{pyk} “axiom USisUpperBound”] [0not1(R) →^{pyk} “axiom 0not1(R)”] [ExpUnbounded(R) →^{pyk} “1rule expUnbounded”] [FromLeq(Advanced)(N) →^{pyk} “1rule fromLeq(Advanced)(N)”] [FromLeastUpperBound →^{pyk} “1rule fromLeastUpperBound”] [ToLeastUpperBound →^{pyk} “1rule toLeastUpperBound”] [XSisNotUpperBound →^{pyk} “axiom XSisNotUpperBound”] [ysFGreater →^{pyk} “axiom ysFGreater”] [ysFLess →^{pyk} “axiom ysFLess”] [SmallInverse →^{pyk} “1rule smallInverse”] [NatType →^{pyk} “axiom natType”] [RationalType →^{pyk} “axiom rationalType”] [SeriesType →^{pyk} “axiom seriesType”] [Max →^{pyk} “axiom max”] [Numerical →^{pyk} “axiom numerical”] [NumericalF →^{pyk} “axiom numericalF”] [MemberOfSeries(Imply) →^{pyk} “axiom memberOfSeries”] [JoinConjuncts(2conditions) →^{pyk} “prop lemma doubly conditioned join conjuncts”] [prop lemma imply negation →^{pyk} “prop lemma imply negation”] [TND →^{pyk} “prop lemma tertium non datur”] [FromNegatedImply →^{pyk} “prop lemma from negated imply”] [ToNegatedImply →^{pyk} “prop lemma to negated imply”] [FromNegated(2 ∗ Imply) →^{pyk} “prop lemma from negated double imply”] [FromNegatedAnd →^{pyk} “prop lemma from negated and”] [FromNegatedOr →^{pyk} “prop lemma from negated or”] [ToNegatedOr →^{pyk} “prop lemma to negated or”] [FromNegations →^{pyk} “prop lemma from negations”] [From3Disjuncts →^{pyk} “prop lemma from three disjuncts”] [From2 ∗ 2Disjuncts →^{pyk} “prop lemma from two times two disjuncts”] [NegateDisjunct1 →^{pyk} “prop lemma negate first disjunct”] [NegateDisjunct2 →^{pyk} “prop lemma negate second disjunct”] [ExpandDisjuncts →^{pyk} “prop lemma expand disjuncts”] [SENC1 →^{pyk} “lemma set equality nec condition(1)”] [SENC2 →^{pyk} “lemma set equality nec condition(2)”] [LessLeq(R) →^{pyk} “lemma lessLeq(R)”] [MemberOfSeries →^{pyk} “lemma memberOfSeries”] [memberOfSeries(Type) →^{pyk} “lemma memberOfSeries(Type)”]

[∗(exp)∗ →^{pyk} “" ˆ "”]

[R(∗) →^{pyk} “R( " )”]

[− − R(∗) →^{pyk} “--R( " )”]

[rec∗ →^{pyk} “1/ "”]

[∗/∗ →^{pyk} “eq-system of " modulo "”] [∗ ∩ ∗ →^{pyk} “intersection " comma " end intersection”]

[∗[∗] →^{pyk} “[ " ; " ]”]

[∪∗ →^{pyk} “union " end union”] [∗ ∪ ∗ →^{pyk} “binary-union " comma " end union”] [P(∗) →^{pyk} “power " end power”] [{∗} →^{pyk} “zermelo singleton " end singleton”] [StateExpand(∗, ∗, ∗) →^{pyk} “stateExpand( " , " , " )”] [extractSeries(∗) →^{pyk} “extractSeries( " )”] [SetOfSeries(∗) →^{pyk} “setOfSeries( " )”] [− − Macro(∗) →^{pyk} “--Macro( " )”] [ExpandList(∗, ∗, ∗) →^{pyk} “expandList( " , " , " )”] [∗ ∗ Macro(∗) →^{pyk} “∗∗Macro( " )”] [+ + Macro(∗) →^{pyk} “++Macro( " )”] [<< Macro(∗) →^{pyk} “<<Macro( " )”] [||Macro(∗) →^{pyk} “||Macro( " )”] [01//Macro(∗) →^{pyk} “01//Macro( " )”] [UB(∗, ∗) →^{pyk} “upperBound( " , " )”] [LUB(∗, ∗) →^{pyk} “leastUpperBound( " , " )”] [BS(∗, ∗) →^{pyk} “base(1/2)Sum( " , " )”] [UStelescope(∗, ∗) →^{pyk} “UStelescope( " , " )”]

[(∗) →^{pyk} “( " )”]

[|f ∗ | →^{pyk} “|f " |”]

[|r ∗ | →^{pyk} “|r " |”]

[Limit(∗, ∗) →^{pyk} “limit( " , " )”] [Union(∗) →^{pyk} “U( " )”] [IsOrderedPair(∗, ∗, ∗) →^{pyk} “isOrderedPair( " , " , " )”] [IsRelation(∗, ∗, ∗) →^{pyk} “isRelation( " , " , " )”] [isFunction(∗, ∗, ∗) →^{pyk} “isFunction( " , " , " )”] [IsSeries(∗, ∗) →^{pyk} “isSeries( " , " )”] [IsNatural(∗, ∗) →^{pyk} “isNatural( " )”] [OrderedPair(∗, ∗) →^{pyk} “(o " , " )”] [TypeNat(∗) →^{pyk} “typeNat( " )”] [TypeNat0(∗) →^{pyk} “typeNat0( " )”] [TypeRational(∗) →^{pyk} “typeRational( " )”] [TypeRational0(∗) →^{pyk} “typeRational0( " )”] [TypeSeries(∗, ∗) →^{pyk} “typeSeries( " , " )”] [Typeseries0(∗, ∗) →^{pyk} “typeSeries0( " , " )”] [{∗, ∗} →^{pyk} “zermelo pair " comma " end pair”] [⟨∗, ∗⟩ →^{pyk} “zermelo ordered pair " comma " end pair”]

[(−u∗) →^{pyk} “- "”]

[−_{f}∗ →^{pyk} “-f "”]

[(− − ∗) →^{pyk} “-- "”]

[1f/∗ →^{pyk} “1f/ "”]

[01//temp∗ →^{pyk} “01// "”]

[∗(∗, ∗) →^{pyk} “" is related to " under "”] [ReflRel(∗, ∗) →^{pyk} “" is reflexive relation in "”] [SymRel(∗, ∗) →^{pyk} “" is symmetric relation in "”] [TransRel(∗, ∗) →^{pyk} “" is transitive relation in "”] [EqRel(∗, ∗) →^{pyk} “" is equivalence relation in "”] [[∗ ∈ ∗]_{∗} →^{pyk} “equivalence class of " in " modulo "”] [Partition(∗, ∗) →^{pyk} “" is partition of "”]

[(∗ ∗ ∗) →^{pyk} “" ∗ "”]

[∗ ∗_{f} ∗ →^{pyk} “" ∗f "”]

[∗ ∗ ∗∗ →^{pyk} “" ∗∗ "”]

[(∗ + ∗) →^{pyk} “" + "”]

[(∗ − ∗) →^{pyk} “" - "”]

[∗ +_{f} ∗ →^{pyk} “" +f "”]

[∗ −_{f} ∗ →^{pyk} “" -f "”]

[∗ + +∗ →^{pyk} “" ++ "”]

[R(∗) − −R(∗) →^{pyk} “R( " ) -- R( " )”]

[∗ ∈ ∗ →^{pyk} “" in0 "”]

[| ∗ | →^{pyk} “| " |”]

[if(∗, ∗, ∗) →^{pyk} “if( " , " , " )”]

[Max(∗, ∗) →^{pyk} “max( " , " )”] [Max(∗, ∗) →^{pyk} “maxR( " , " )”]

[∗ = ∗ →^{pyk} “" = "”]

[∗ ≠ ∗ →^{pyk} “" != "”]

[∗ <= ∗ →^{pyk} “" <= "”]

[∗ < ∗ →^{pyk} “" < "”]

[∗ <_{f} ∗ →^{pyk} “" <f "”]

[∗ ≤_{f} ∗ →^{pyk} “" <=f "”]

[SF(∗, ∗) →^{pyk} “" sameF "”]

[∗ == ∗ →^{pyk} “" == "”]

[∗!! == ∗ →^{pyk} “" !!== "”]

[∗ << ∗ →^{pyk} “" << "”]

[∗ <<== ∗ →^{pyk} “" <<== "”]

[∗==∗ →^{pyk} “" zermelo is "”] [∗ ⊆ ∗ →^{pyk} “" is subset of "”]

[ ˙¬ (∗)n →^{pyk} “not0 "”]

[∗ ∉ ∗ →^{pyk} “" zermelo ˜ in "”] [∗ ≠ ∗ →^{pyk} “" zermelo ˜ is "”]

[∗ ˙∧ ∗ →^{pyk} “" and0 "”]

[∗ ˙∨ ∗ →^{pyk} “" or0 "”]

[∃∗: ∗ →^{pyk} “exist0 " indeed "”]

[∗ ˙⇔ ∗ →^{pyk} “" iff "”]

[{ph ∈ ∗ | ∗} →^{pyk} “the set of ph in " such that " end set”] [kvanti →^{pyk} “kvanti”]

B TEX definitioner

[kvanti →^{tex} “kvanti”]

[(⋯) →^{tex} “(\cdots{})”]

[Objekt-var →^{tex} “\texttt{Objekt-var}”]

[Ex-var →^{tex} “\texttt{Ex-var}”]

[Ph-var →^{tex} “\texttt{Ph-var}”]

[Værdi →^{tex} “\texttt{V\ae{}rdi}”]

[Variabel →^{tex} “\texttt{Variabel}”]

[Op(x) →^{tex} “Op(#1. )”]

[Op(x, y) →^{tex} “Op(#1. , #2. )”]

[x ¨ == y →^{tex} “#1.

\mathrel {\ddot {==}} #2.”]

[ContainsEmpty(x) →^{tex} “ContainsEmpty(#1. )”]

[Dedu(x, y) →^{tex} “ Dedu(#1. , #2. )”]

[Dedu_{0}(x, y) →^{tex} “ Dedu 0(#1. , #2. )”]

[Dedu_{s}(x, y, z) →^{tex} “Dedu {s}(#1. , #2. , #3. )”]

[Dedu_{1}(x, y, z) →^{tex} “ Dedu 1(#1. , #2.

, #3. )”]

[Dedu_{2}(x, y, z) →^{tex} “ Dedu 2(#1. , #2. , #3. )”]

[Dedu_{3}(x, y, z, u) →^{tex} “ Dedu 3(#1. , #2. , #3. , #4. )”]

[Dedu_{4}(x, y, z, u) →^{tex} “ Dedu 4(#1. , #2. , #3. , #4. )”]

[Dedu_{4}^{∗}(x, y, z, u) →^{tex} “ Dedu 4ˆ ∗(#1. , #2. , #3. , #4. )”]

[Dedu_{5}(x, y, z) →^{tex} “ Dedu 5(#1. , #2. , #3. )”]

[Dedu_{6}(p, c, e, b) →^{tex} “ Dedu 6(#1. , #2. , #3. , #4. )”]

[Dedu_{6}^{∗}(p, c, e, b) →^{tex} “ Dedu 6ˆ ∗(#1. , #2. , #3.

[Dedu_{7}(p) →^{tex} “ Dedu 7(#1. )”]

[Dedu_{8}(p, b) →^{tex} “ Dedu 8(#1. , #2. )”]

[Dedu_{8}^{∗}(p, b) →^{tex} “ Dedu 8ˆ ∗(#1. , #2. )”]

[Ex_{1} →^{tex} “Ex {1}”]

[Ex_{2} →^{tex} “Ex {2}”]

[Ex_{10} →^{tex} “Ex {10}”]

[Ex_{20} →^{tex} “Ex {20}”]

[x_{Ex} →^{tex} “#1.

{Ex}”]

[x^{Ex} →^{tex} “#1.

ˆ {Ex}”]

[⟨x≡y|z:==u⟩_{Ex} →^{tex} “\langle #1. {\equiv} #2. | #3. {:==} #4. \rangle {Ex} ”]

[⟨x≡^{0}y|z:==u⟩_{Ex} →^{tex} “\langle #1. {\equiv}ˆ 0 #2. | #3. {:==} #4. \rangle {Ex} ”]

[⟨x≡^{1}y|z:==u⟩_{Ex} →^{tex} “\langle #1. {\equiv}ˆ 1 #2. | #3. {:==} #4. \rangle {Ex} ”] [⟨x≡^{∗}y|z:==u⟩_{Ex} →^{tex} “\langle #1. {\equiv}ˆ ∗ #2. | #3. {:==} #4. \rangle {Ex} ”]

[ph_{1} →^{tex} “ph {1}”]

[ph_{2} →^{tex} “ph {2}”]

[ph_{3} →^{tex} “ph {3}”]

[ph_{4} →^{tex} “ph {4}”]

[ph_{5} →^{tex} “ph {5}”]

[ph_{6} →^{tex} “ph {6}”]

[∗_{Ph} →^{tex} “#1.

{Ph} ”]

[x^{Ph} →^{tex} “#1.

ˆ {Ph}”]

[⟨x≡y|z:==u⟩_{Ph} →^{tex} “\langle #1. {\equiv} #2. | #3. {:==} #4. \rangle {Ph} ”]

[⟨x≡^{0}y|z:==u⟩_{Ph} →^{tex} “\langle #1. {\equiv}ˆ 0 #2. | #3. {:==} #4. \rangle {Ph} ”]

[⟨x≡^{1}y|z:==u⟩_{Ph} →^{tex} “\langle #1. {\equiv}ˆ 1 #2. | #3. {:==} #4. \rangle {Ph} ”]

[⟨x≡^{∗}y|z:==u⟩_{Ph} →^{tex} “\langle #1. {\equiv}ˆ ∗ #2. | #3. {:==} #4. \rangle {Ph} ”] [bs →^{tex} “\mathsf {bs}”] [OBS →^{tex} “ \mathsf {OBS}”] [BS →^{tex} “{\cal BS}”] [Ø →^{tex} “\mathrm{\O}”] [SystemQ →^{tex} “SystemQ”]

[MP →^{tex} “MP”]

[Gen →^{tex} “Gen”] [Repetition →^{tex} “Repetition”] [Neg →^{tex} “Neg”] [Ded →^{tex} “Ded”] [ExistIntro →^{tex} “ExistIntro”] [Extensionality →^{tex} “Extensionality”] [Ødef →^{tex} “\O{}def”] [PairDef →^{tex} “PairDef”] [UnionDef →^{tex} “UnionDef”] [PowerDef →^{tex} “PowerDef”] [SeparationDef →^{tex} “SeparationDef”] [AddDoubleNeg →^{tex} “AddDoubleNeg”] [RemoveDoubleNeg →^{tex} “RemoveDoubleNeg”] [AndCommutativity →^{tex} “AndCommutativity”] [AutoImply →^{tex} “AutoImply”] [Contrapositive →^{tex} “Contrapositive”] [FirstConjunct →^{tex} “FirstConjunct”] [SecondConjunct →^{tex} “SecondConjunct”] [FromContradiction →^{tex} “FromContradiction”] [FromDisjuncts →^{tex} “FromDisjuncts”] [IffCommutativity →^{tex} “IffCommutativity”] [IffFirst →^{tex} “IffFirst”] [IffSecond →^{tex} “IffSecond”] [ImplyTransitivity →^{tex} “ImplyTransitivity”] [JoinConjuncts →^{tex} “JoinConjuncts”]

[MP2 →^{tex} “MP2”]

[MP3 →^{tex} “MP3”]

[MP4 →^{tex} “MP4”]

[MP5 →^{tex} “MP5”]

[MT →^{tex} “MT”]

[NegativeMT →^{tex} “NegativeMT”] [Technicality →^{tex} “Technicality”] [Weakening →^{tex} “Weakening”] [WeakenOr1 →^{tex} “WeakenOr1”] [WeakenOr2 →^{tex} “WeakenOr2”] [Pair2Formula →^{tex} “Pair2Formula”] [Formula2Pair →^{tex} “Formula2Pair”] [Union2Formula →^{tex} “Union2Formula”] [Formula2Union →^{tex} “Formula2Union”] [Formula2Power →^{tex} “Formula2Power”] [Sep2Formula →^{tex} “Sep2Formula”] [Formula2Sep →^{tex} “Formula2Sep”] [SubsetInPower →^{tex} “SubsetInPower”] [HelperPowerIsSub →^{tex} “HelperPowerIsSub”] [PowerIsSub →^{tex} “PowerIsSub”] [(Switch)HelperPowerIsSub →^{tex} “(Switch)HelperPowerIsSub”] [(Switch)PowerIsSub →^{tex} “(Switch)PowerIsSub”] [ToSetEquality →^{tex} “ToSetEquality”] [HelperToSetEquality(t) →^{tex} “HelperToSetEquality(t)”] [ToSetEquality(t) →^{tex} “ToSetEquality(t)”] [HelperFromSetEquality →^{tex} “HelperFromSetEquality”] [FromSetEquality →^{tex} “FromSetEquality”] [HelperReflexivity →^{tex} “HelperReflexivity”] [Reflexivity →^{tex} “Reflexivity”] [HelperSymmetry →^{tex} “HelperSymmetry”] [Symmetry →^{tex} “Symmetry”] [HelperTransitivity →^{tex} “HelperTransitivity”] [Transitivity →^{tex} “Transitivity”], [ERisReflexive →^{tex} “ERisReflexive”] [ERisSymmetric →^{tex} “ERisSymmetric”] [ERisTransitive →^{tex} “ERisTransitive”] [ØisSubset →^{tex} “\O{}isSubset”] [HelperMemberNotØ →^{tex} “HelperMemberNot\O{}”] [MemberNotØ →^{tex} “MemberNot\O{}”] [HelperUniqueØ →^{tex} “HelperUnique\O{}”] [UniqueØ →^{tex} “Unique\O{}”] [==Reflexivity →^{tex} “==\!{}Reflexivity”] [==Symmetry →^{tex} “==\!{}Symmetry”] [Helper==Transitivity →^{tex} “Helper\!{}==\!{}Transitivity”] [==Transitivity →^{tex} “\!{}==\!{}Transitivity”] [HelperTransferNotEq →^{tex} “HelperTransferNotEq”] [TransferNotEq →^{tex} “TransferNotEq”] [HelperPairSubset →^{tex} “HelperPairSubset”] [Helper(2)PairSubset →^{tex} “Helper(2)PairSubset”] [PairSubset →^{tex} “PairSubset”] [SamePair →^{tex} “SamePair”] [SameSingleton →^{tex} “SameSingleton”] [UnionSubset →^{tex} “UnionSubset”] [SameUnion →^{tex} “SameUnion”] [SeparationSubset →^{tex} “SeparationSubset”] [SameSeparation →^{tex} “SameSeparation”] [SameBinaryUnion →^{tex} “SameBinaryUnion”] [IntersectionSubset →^{tex} “IntersectionSubset”] [SameIntersection →^{tex} “SameIntersection”] [AutoMember →^{tex} “AutoMember”] [HelperEqSysNotØ →^{tex} “HelperEqSysNot\O{}”] [EqSysNotØ →^{tex} “EqSysNot\O{}”] [HelperEqSubset →^{tex} “HelperEqSubset”] [EqSubset →^{tex} “EqSubset”] [EqNecessary →^{tex} “EqNecessary”] [HelperEqNecessary →^{tex} “HelperEqNecessary”] [HelperNoneEqNecessary →^{tex} “HelperNoneEqNecessary”] [Helper(2)NoneEqNecessary →^{tex} “Helper(2)NoneEqNecessary”] [NoneEqNecessary →^{tex} “NoneEqNecessary”] [EqClassIsSubset →^{tex} “EqClassIsSubset”] [EqClassesAreDisjoint →^{tex} “EqClassesAreDisjoint”] [AllDisjoint →^{tex} “AllDisjoint”] [AllDisjointImply →^{tex} “AllDisjointImply”] [BSsubset →^{tex} “BSsubset”] [Union(BS/R)subset →^{tex} “Union(BS/R)subset”] [UnionIdentity →^{tex} “UnionIdentity”] [EqSysIsPartition →^{tex} “EqSysIsPartition”]

[x/y →^{tex} “#1.

/ #2.”]

[x ∩ y →^{tex} “#1.

\cap #2.”]

[∪x →^{tex} “\cup #1.”]

[x ∪ y →^{tex} “#1.

\mathrel{\cup} #2.”]

[P(x) →^{tex} “P(#1.

)”]

[{x} →^{tex} “\{#1.

\}”]

[{x, y} →^{tex} “\{#1.

, #2. \}”] [⟨x, y⟩ →^{tex} “\langle #1. , #2. \rangle”],

[x ∈ y →^{tex} “#1.

\mathrel{\in} #2.”]

[z(x, y) →^{tex} “#3.

(#1. , #2. )”] [ReflRel(r, x) →^{tex} “ReflRel(#1. , #2. )”]

[SymRel(r, x) →^{tex} “SymRel(#1. , #2. )”]

[TransRel(r, x) →^{tex} “TransRel(#1. , #2. )”]

[EqRel(r, x) →^{tex} “EqRel(#1. , #2. )”]

[[x ∈ bs]_{r} →^{tex} “[#1.

\mathrel{\in} #2. ] {#3. }”]

[Partition(x, y) →^{tex} “Partition(#1. , #2. )”]

[x==y →^{tex} “#1.

\!\mathrel{==}\! #2.”]

[x ⊆ y →^{tex} “#1.

\mathrel{\subseteq} #2.”]

[ ˙¬ (x)n →^{tex} “\dot{\neg}\, (#1. )n”]

[x ∉ y →^{tex} “#1.

\mathrel{\notin} #2.”]

[x ≠ y →^{tex} “#1.

\mathrel{\neq} #2.”]

[x ˙∧ y →^{tex} “#1.

\mathrel{\dot{\wedge}} #2.”]

[x ˙∨ y →^{tex} “#1.

\mathrel{\dot{\vee}} #2.”]

[x ˙⇔ y →^{tex} “#1.

\mathrel{\dot{\Leftrightarrow}} #2.”] [{ph ∈ x | a} →^{tex} “ \{ ph \mathrel{\in} #1. \mid #2. \}”]

[x ⇒ y →^{tex} “(i#1.

\Rightarrow #2. )i”]

[Nat(x) →^{tex} “Nat(#1. )”]

[⟨x≡y|z:==u⟩_{Me} →^{tex} “\langle #1. {\equiv} #2. | #3. {:==} #4. \rangle {Me}”]

[⟨x≡^{1}y|z:==u⟩_{Me} →^{tex} “\langle #1. {\equiv}ˆ 1 #2. | #3. {:==} #4. \rangle {Me} ”]

[⟨x≡^{∗}y|z:==u⟩_{Me} →^{tex} “\langle #1. {\equiv}ˆ ∗ #2. | #3. {:==} #4. \rangle {Me} ”]

[∃x: y →^{tex} “

\exists #1. \colon #2.”]

[(x1) →^{tex} “(x1)”]

[(x2) →^{tex} “(x2)”]

[(y1) →^{tex} “(y1)”]

[(y2) →^{tex} “(y2)”]

[(v1) →^{tex} “(v1)”]

[(v2) →^{tex} “(v2)”]

[(v3) →^{tex} “(v3)”]

[(v4) →^{tex} “(v4)”]

[(v2n) →^{tex} “(v2n)”]

[(n1) →^{tex} “(n1)”]

[(n2) →^{tex} “(n2)”]

[(n3) →^{tex} “(n3)”]

[(m1) →^{tex} “(m1)”]

[(m2) →^{tex} “(m2)”]

[(ϵ) →^{tex} “(\epsilon)”]

[(ϵ)_{1} →^{tex} “(\epsilon) {1}”]

[(ϵ2) →^{tex} “(\epsilon 2)”]

[(fx) →^{tex} “(fx)”]

[(fy) →^{tex} “(fy)”]

[(fz) →^{tex} “(fz)”]

[(fu) →^{tex} “(fu)”]

[(fv) →^{tex} “(fv)”]

[(fw) →^{tex} “(fw)”]

[(fep) →^{tex} “(fep)”]

[(rx) →^{tex} “(rx)”]

[(ry) →^{tex} “(ry)”]

[(rz) →^{tex} “(rz)”]

[(ru) →^{tex} “(ru)”]

[(sx) →^{tex} “(sx)”]

[(sx1) →^{tex} “(sx1)”]

[(sy) →^{tex} “(sy)”]

[(sy1) →^{tex} “(sy1)”]

[(sz) →^{tex} “(sz)”]

[(sz1) →^{tex} “(sz1)”]

[(su) →^{tex} “(su)”]

[(su1) →^{tex} “(su1)”]

[(fxs) →^{tex} “(fxs)”]

[(fys) →^{tex} “(fys)”]

[(crs1) →^{tex} “(crs1)”]

[(f1) →^{tex} “(f1)”]

[(f2) →^{tex} “(f2)”]

[(f3) →^{tex} “(f3)”]

[(f4) →^{tex} “(f4)”]

[(op1) →^{tex} “(op1)”]

[(op2) →^{tex} “(op2)”]

[(r1) →^{tex} “(r1)”]

[(s1) →^{tex} “(s1)”]

[(s2) →^{tex} “(s2)”]

[X_{1} →^{tex} “X {1}”]

[X_{2} →^{tex} “X {2}”]

[Y_{1} →^{tex} “Y {1}”]

[Y_{2} →^{tex} “Y {2}”]

[V_{1} →^{tex} “V {1}”]

[V_{2} →^{tex} “V {2}”]

[V_{3} →^{tex} “V {3}”]

[V_{4} →^{tex} “V {4}”]

[V_{2n} →^{tex} “V {2n}”]

[ϵ →^{tex} “\epsilon”]

[M_{1} →^{tex} “M {1}”]

[M_{2} →^{tex} “M {2}”]

[N_{1} →^{tex} “N {1} ”]

[N_{2} →^{tex} “N {2} ”]

[N_{3} →^{tex} “N {3} ”]

[ϵ1 →^{tex} “\epsilon 1”]

[ϵ2 →^{tex} “\epsilon 2”]

[FX →^{tex} “FX”]

[FY →^{tex} “FY”]

[FZ →^{tex} “FZ”]

[FU →^{tex} “FU”]

[FV →^{tex} “FV”]

[FW →^{tex} “FW”]

[FEP →^{tex} “FEP”]

[RX →^{tex} “RX”]

[RY →^{tex} “RY”]

[RZ →^{tex} “RZ”]

[RU →^{tex} “RU”]

[(SX) →^{tex} “(SX)”]

[(SX1) →^{tex} “(SX1)”]

[(SY) →^{tex} “(SY)”]

[(SY1) →^{tex} “(SY1)”]

[(SZ) →^{tex} “(SZ)”]

[(SZ1) →^{tex} “(SZ1)”]

[(SU) →^{tex} “(SU)”]

[(SU1) →^{tex} “(SU1)”]

[FXS →^{tex} “FXS”]

[FYS →^{tex} “FYS”]

[(F1) →^{tex} “(F1)”]

[(F2) →^{tex} “(F2)”]

[(F3) →^{tex} “(F3)”]

[(F4) →^{tex} “(F4)”]

[(OP1) →^{tex} “(OP1)”]

[(OP2) →^{tex} “(OP2)”]

[(R1) →^{tex} “(R1)”]

[(S1) →^{tex} “(S1)”]

[(S2) →^{tex} “(S2)”]

[(EPob) →^{tex} “(EPob)”]

[(CRS1ob) →^{tex} “(CRS1ob)”]

[(F1ob) →^{tex} “(F1ob)”]

[(F2ob) →^{tex} “(F2ob)”]

[(F3ob) →^{tex} “(F3ob)”]

[(F4ob) →^{tex} “(F4ob)”]

[(N1ob) →^{tex} “(N1ob)”]

[(N2ob) →^{tex} “(N2ob)”]

[(OP1ob) →^{tex} “(OP1ob)”]

[(OP2ob) →^{tex} “(OP2ob)”]

[(R1ob) →^{tex} “(R1ob)”]

[(S1ob) →^{tex} “(S1ob)”]

[(S2ob) →^{tex} “(S2ob)”]

[Ex3 →^{tex} “Ex3”]

[NAT →^{tex} “NAT”] [RATIONAL_{S}ERIES →^{tex} “RATIONAL SERIES”] [SERIES →^{tex} “SERIES”] [SetOfReals →^{tex} “SetOfReals”] [SetOfFxs →^{tex} “SetOfFxs”]

[N →^{tex} “N”]

[Q →^{tex} “Q”]

[X →^{tex} “X”]

[xs →^{tex} “xs”]

[xaF →^{tex} “xaF”] [ysF →^{tex} “ysF”]

[us →^{tex} “us”]

[usFoelge →^{tex} “usFoelge”]

[0 →^{tex} “0”]

[1 →^{tex} “1”]

[(−1) →^{tex} “(-1)”]

[2 →^{tex} “2”]

[3 →^{tex} “3”]

[1/2 →^{tex} “1/2”]

[1/3 →^{tex} “1/3”]

[2/3 →^{tex} “2/3”]

[0f →^{tex} “0f”]

[00 →^{tex} “00”]

[(− − 01) →^{tex} “(--01)”]

[02 →^{tex} “02”]

[01//02 →^{tex} “01//02”]

[x = y →^{tex} “#1.

= #2.”]

[x ≠ y →^{tex} “#1.

\neq #2.”]

[x < y →^{tex} “#1.

< #2.”]

[x <= y →^{tex} “#1.

<= #2.”]

[x <_{f} y →^{tex} “#1.

< {f}#2.”]

[x ≤_{f} y →^{tex} “#1.

\leq {f}#2.”] [SF(x, y) →^{tex} “SF(#1. , #2. )”]

[x == y →^{tex} “#1.

== #2.”]

[x!! == y →^{tex} “#1.

!!== #2.”]

[x << y →^{tex} “#1.

<< #2.”]

[x <<== y →^{tex} “#1.

<<== #2.”]

[x[y] →^{tex} “#1.

[#2. ]”]

[(−ux) →^{tex} “(-u#1.

)”]

[−_{f}x →^{tex} “- {f}#1.”]

[(− − x) →^{tex} “(--#1.

)”]

[1f/x →^{tex} “1f/#1.”]

[01//tempx →^{tex} “01//temp#1.”]

[(x + y) →^{tex} “(#1.

+#2. )”]

[(x − y) →^{tex} “(#1.

-#2. )”]

[(fx) +_{f} (fy) →^{tex} “#1. + {f}#2.”]

[(fx) −_{f} (fy) →^{tex} “#1.

- {f}#2.”]

[(fx) ∗_{f} (fy) →^{tex} “#1.

∗ {f}#2.”]

[x + +y →^{tex} “#1.

++#2.”]

[R((fx)) − −R((fy)) →^{tex} “R(#1. ) -- R(#2. )”]

[(x ∗ y) →^{tex} “(#1.

∗#2. )”]

[x ∗ ∗y →^{tex} “#1.

∗∗#2.”]

[x(exp)y →^{tex} “ #1. (exp) #2.”]

[leqReflexivity →^{tex} “leqReflexivity”]

[recx →^{tex} “rec#1.”]

[|x| →^{tex} “|#1.

|”] [StateExpand(t, s, c) →^{tex} “StateExpand(#1. , #2. , #3. )”]

[extractSeries(t) →^{tex} “extractSeries(#1. )”]

[|fx| →^{tex} “|f#1.

|”]

[|rx| →^{tex} “|r#1.

|”]

[SetOfSeries(x) →^{tex} “SetOfSeries(#1. )”]

[ExpandList(x, y, z) →^{tex} “ExpandList(#1. , #2. , #3. )”]

[∗ ∗ Macro(x) →^{tex} “∗∗Macro(#1. )”]

[+ + Macro(x) →^{tex} “++Macro(#1. )”]

[− − Macro(x) →^{tex} “--Macro(#1. )”]

[<< Macro(x) →^{tex} “<<Macro(#1. )”]

[||Macro(x) →^{tex} “||Macro(#1. )”]

[01//Macro(x) →^{tex} “01//Macro(#1. )”]

[Max(x, y) →^{tex} “Max(#1. , #2. )”]

[Max(x, y) →^{tex} “Max(#1. , #2. )”] [Limit(x, y) →^{tex} “Limit(#1. , #2. )”]

[Union(x) →^{tex} “Union(#1. )”]

[if(x, y, z) →^{tex} “if(#1. , #2. , #3. )”]

[IsOrderedPair(x, y, z) →^{tex} “IsOrderedPair(#1. , #2. , #3. )”]

[IsRelation(x, y, z) →^{tex} “IsRelation(#1. , #2. , #3. )”]

[isFunction(x, y, z) →^{tex} “isFunction(#1. , #2. , #3. )”]

[TypeNat(x) →^{tex} “TypeNat(#1. )”]

[TypeNat0(x) →^{tex} “TypeNat0(#1. )”]

[TypeRational(x) →^{tex} “TypeRational(#1. )”]

[TypeRational0(x) →^{tex} “TypeRational0(#1. )”]

[TypeSeries(x, y) →^{tex} “TypeSeries(#1. , #2. )”]

[Typeseries0(x, y) →^{tex} “Typeseries0(#1. , #2. )”] [UB(x, y) →^{tex} “UB(#1. , #2. )”]

[LUB(x, y) →^{tex} “LUB(#1. , #2. )”]

[BS(x, y) →^{tex} “BS(#1. , #2. )”]

[UStelescope(x, y) →^{tex} “UStelescope(#1. , #2. )”]

[(x) →^{tex} “(#1.

)”]

[R(x) →^{tex} “R(#1.

)”]

[− − R(x) →^{tex} “--R(#1.

)”]

[IsSeries(x, y) →^{tex} “IsSeries(#1. , #2. )”]

[IsNatural(xy, ∗) →^{tex} “IsNatural(#1. , #2. )”]

[OrderedPair(x, y) →^{tex} “OrderedPair(#1. , #2. )”]

[leqAntisymmetryAxiom →^{tex} “leqAntisymmetryAxiom”]

[leqTransitivityAxiom →^{tex} “leqTransitivityAxiom”]

[leqTotality →^{tex} “leqTotality”]

[leqAdditionAxiom →^{tex} “leqAdditionAxiom”]

[leqMultiplicationAxiom →^{tex} “leqMultiplicationAxiom”]

[plusAssociativity →^{tex} “plusAssociativity”] [plusCommutativity →^{tex} “plusCommutativity”] [Negative →^{tex} “Negative”] [plus0 →^{tex} “plus0”] [timesAssociativity →^{tex} “timesAssociativity”] [timesCommutativity →^{tex} “timesCommutativity”] [ReciprocalAxiom →^{tex} “ReciprocalAxiom”] [times1 →^{tex} “times1”] [plusAssociativity →^{tex} “plusAssociativity”] [plusCommutativity →^{tex} “plusCommutativity”] [Negative →^{tex} “Negative”] [Distribution →^{tex} “Distribution”] [0not1 →^{tex} “0not1”] [A4(Axiom) →^{tex} “A4(Axiom)”] [InductionAxiom →^{tex} “InductionAxiom”] [EqualityAxiom →^{tex} “EqualityAxiom”] [EqLeqAxiom →^{tex} “EqLeqAxiom”] [EqAdditionAxiom →^{tex} “EqAdditionAxiom”] [EqMultiplicationAxiom →^{tex} “EqMultiplicationAxiom”] [SENC1 →^{tex} “SENC1”] [SENC2 →^{tex} “SENC2”] [Cauchy →^{tex} “Cauchy”] [PlusF →^{tex} “PlusF”] [ReciprocalF →^{tex} “ReciprocalF”] [From ==→^{tex} “From==”]

[To ==→^{tex} “To==”]

[FromInR →^{tex} “FromInR”] [ReciprocalR(Axiom) →^{tex} “ReciprocalR(Axiom)”]

[US0 →^{tex} “US0”]

[NextXS(UpperBound) →^{tex} “NextXS(UpperBound)”] [NextXS(NoUpperBound) →^{tex} “NextXS(NoUpperBound)”] [NextUS(UpperBound) →^{tex} “NextUS(UpperBound)”] [NextUS(NoUpperBound) →^{tex} “NextUS(NoUpperBound)”] [ExpZero →^{tex} “ExpZero”] [ExpPositive →^{tex} “ExpPositive”] [ExpZero(R) →^{tex} “ExpZero(R)”] [ExpPositive(R) →^{tex} “ExpPositive(R)”] [LessMinus1(N) →^{tex} “LessMinus1(N)”] [Nonnegative(N) →^{tex} “Nonnegative(N)”] [BSzero →^{tex} “BSzero”] [BSpositive →^{tex} “BSpositive”] [UStelescope(Zero) →^{tex} “UStelescope(Zero)”] [UStelescope(Positive) →^{tex} “UStelescope(Positive)”] [EqAddition(R) →^{tex} “EqAddition(R)”] [FromLimit →^{tex} “FromLimit”] [ToUpperBound →^{tex} “ToUpperBound”] [FromUpperBound →^{tex} “FromUpperBound”] [USisUpperBound →^{tex} “USisUpperBound”] [0not1(R) →^{tex} “0not1(R)”] [ExpUnbounded(R) →^{tex} “ExpUnbounded(R)”] [FromLeq(Advanced)(N) →^{tex} “FromLeq(Advanced)(N)”] [FromLeastUpperBound →^{tex} “FromLeastUpperBound”] [ToLeastUpperBound →^{tex} “ToLeastUpperBound”] [XSisNotUpperBound →^{tex} “XSisNotUpperBound”] [ysFGreater →^{tex} “ysFGreater”] [ysFLess →^{tex} “ysFLess”] [SmallInverse →^{tex} “SmallInverse”] [MemberOfSeries(Imply) →^{tex} “MemberOfSeries(Imply)”] [NatType →^{tex} “NatType”] [RationalType →^{tex} “RationalType”] [SeriesType →^{tex} “SeriesType”] [JoinConjuncts(2conditions) →^{tex} “JoinConjuncts(2conditions)”] [TND →^{tex} “TND”] [FromNegatedImply →^{tex} “FromNegatedImply”] [ToNegatedImply →^{tex} “ToNegatedImply”] [FromNegated(2 ∗ Imply) →^{tex} “FromNegated(2∗Imply)”] [FromNegatedAnd →^{tex} “FromNegatedAnd”] [FromNegatedOr →^{tex} “FromNegatedOr”] [ToNegatedOr →^{tex} “ToNegatedOr”] [FromNegations →^{tex} “FromNegations”] [From3Disjuncts →^{tex} “From3Disjuncts”] [NegateDisjunct1 →^{tex} “NegateDisjunct1”] [NegateDisjunct2 →^{tex} “NegateDisjunct2”] [ExpandDisjuncts →^{tex} “ExpandDisjuncts”] [From2 ∗ 2Disjuncts →^{tex} “From2∗2Disjuncts”] [PlusR(Sym) →^{tex} “PlusR(Sym)”] [LessLeq(R) →^{tex} “LessLeq(R)”] [LeqAntisymmetry(R) →^{tex} “LeqAntisymmetry(R)”] [LeqTransitivity(R) →^{tex} “LeqTransitivity(R)”] [Plus0(R) →^{tex} “Plus0(R)”] [lessAddition(R) →^{tex} “lessAddition(R)”] [leqAddition(R) →^{tex} “leqAddition(R)”] [PlusAssociativity(R)XX →^{tex} “PlusAssociativity(R)XX”] [PlusAssociativity(R) →^{tex} “PlusAssociativity(R)”] [Negative(R) →^{tex} “Negative(R)”] [PlusCommutativity(R) →^{tex} “PlusCommutativity(R)”] [Times1(R) →^{tex} “Times1(R)”] [TimesAssociativity(R) →^{tex} “TimesAssociativity(R)”] [TimesCommutativity(R) →^{tex} “TimesCommutativity(R)”] [Distribution(R) →^{tex} “Distribution(R)”] [∃x: y →^{tex} “(AARRGGHH!-exist-bug!)”] [constantRationalSeries(x) →^{tex} “constantRationalSeries(#1. )”] [Power(x) →^{tex} “Power(#1. )”] [cartProd(x) →^{tex} “cartProd(#1. )”] [binaryUnion(x, y) →^{tex} “binaryUnion(#1. , #2. )”] [SetOfRationalSeries →^{tex} “SetOfRationalSeries”] [MemberOfSeries →^{tex} “MemberOfSeries”] [IsSubset(x, y) →^{tex} “IsSubset(#1. , #2. )”] [memberOfSeries(Type) →^{tex} “memberOfSeries(Type)”] [UniqueMember →^{tex} “UniqueMember”] [UniqueMember(Type) →^{tex} “UniqueMember(Type)”] [SameSeries →^{tex} “SameSeries”]

[A4 →^{tex} “A4”]

[(sx) →^{tex} “(s#1.

)”]

[(px, y) →^{tex} “(p#1.

, #2. )”] [SameMember →^{tex} “SameMember”] [Qclosed(Addition) →^{tex} “Qclosed(Addition)”] [Qclosed(Multiplication) →^{tex} “Qclosed(Multiplication)”] [FromCartProd(1) →^{tex} “FromCartProd(1)”] [FromCartProd(1) →^{tex} “FromCartProd(1)”] [Max →^{tex} “Max”] [Numerical →^{tex} “Numerical”] [NumericalF →^{tex} “NumericalF”] [Separation2formula(1) →^{tex} “Separation2formula(1)”] [Separation2formula(2) →^{tex} “Separation2formula(2)”] [QisClosed(Reciprocal)(Imply) →^{tex} “QisClosed(Reciprocal)(Imply)”] [QisClosed(Reciprocal) →^{tex} “QisClosed(Reciprocal)”] [QisClosed(Negative)(Imply) →^{tex} “QisClosed(Negative)(Imply)”] [QisClosed(Negative) →^{tex} “QisClosed(Negative)”] [(Adgic)SameR →^{tex} “(Adgic)SameR”]

60