(*** MAKROER BEGYNDER ***) [ph_{1} ¨= a_{Ph}] [ph_{2} ¨= b_{Ph}] [ph_{3} ¨= c_{Ph}] [ph_{4} ¨= d_{Ph}] [ph_{5} ¨= e_{Ph}] [ph_{6} ¨= f_{Ph}] [x ˙∧ y ¨= ˙¬ ((x ⇒ ˙¬ (y)n))n] [x ˙∨ y ¨= ˙¬ (x)n ⇒ y] [x ˙⇔ y ¨= (x ⇒ y) ˙∧ (y ⇒ x)] [x ≠ y ¨= ˙¬ (x==y)n] [x ∉ y ¨= ˙¬ (x ∈ y)n] [x ⊆ y ¨= ∀(S1ob): ((S1ob) ∈ x ⇒ (S1ob) ∈ y)] [{x} ¨= {x, x}] [x ∪ y ¨= ∪{{x}, {y}}] [x ∩ y ¨= {ph ∈ x ∪ y | ph_{3} ∈ x ˙∧ ph_{3} ∈ y}] [⟨x, y⟩ ¨= {{x}, {x, y}}] [r(x, y) ¨= ⟨x, y⟩ ∈ r] [ReflRel(r, x) ¨= ∀s: (s ∈ x ⇒ r(s, s))] [SymRel(r, x) ¨= ∀s, t: (s ∈ x ⇒ t ∈ x ⇒ r(s, t) ⇒ r(t, s))] [TransRel(r, x) ¨=

∀s, t, u: (s ∈ x ⇒ t ∈ x ⇒ u ∈ x ⇒ r(s, t) ⇒ r(t, u) ⇒ r(s, u))]

[EqRel(r, x) ¨= ReflRel(r, x) ˙∧ SymRel(r, x) ˙∧ TransRel(r, x)]

[BS ¨= \underline{bs}] [OBS ¨= \overline{bs}]

[[x ∈ bs]_{r} ¨= {ph ∈ bs | r(ph_{1}, x)}]

[bs/r ¨= {ph ∈ P(bs) | Ex_{20} ∈ bs ˙∧ [Ex_{20} ∈ bs]_{r} ==ph_{2}}]

[Partition(p, bs) ¨= (∀s: (s ∈ p ⇒ s ≠ Ø)) ˙∧

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

∪ p==bs]

(*** EKSISTENS-VARIABLE ***)

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

[Ex_{1} ¨= a_{Ex}]

[Ex_{2} ¨= b_{Ex}] [Ex_{10} ¨= j_{Ex}] [Ex_{20} ¨= t_{Ex}]

[⟨a≡b|x:==t⟩_{Ex} ¨= ⟨⌈a⌉≡^{0}⌈b⌉|⌈x⌉:==⌈t⌉⟩_{Ex}]

[⟨a≡^{0}b|x:==t⟩_{Ex} ˙= λc.x^{Ex} ∧ ⟨a≡^{1}b|x:==t⟩_{Ex}] [⟨a≡^{1}b|x:==t⟩_{Ex} ˙= a!x!t! if b =^{r} ⌈∀u: v⌉ then F else if b^{Ex} ∧ b =^{t} x then a =^{t} t else a =^{r} b ¨∧ ⟨a^{t}≡^{∗}b^{t}|x:==t⟩_{Ex}]

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

(*** AKSIOMATISK SYSTEM ***)

[Theory SystemQ]

[SystemQ rule MP: ΠA, B: A ⇒ B ⊢ A ⊢ B]

[SystemQ rule Gen: ΠX , A: A ⊢ ∀X: A]

[SystemQ rule Repetition: ΠA: A ⊢ A]

[SystemQ rule Neg: ΠA, B: ˙¬ (B)n ⇒ A ⊢ ˙¬ (B)n ⇒ ˙¬ (A)n ⊢ B]

[SystemQ rule Ded: ΠA, B: A ⊢ B]

[SystemQ rule ExistIntro: ΠX , T , A, B: ⟨A≡B|X:==T ⟩_{Ex} ⊢⊢ A ⊢ B]

[SystemQ rule Extensionality: ΠX , Y: X ==Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y)]

[SystemQ rule Ødef: ΠS: ˙¬ (S ∈ Ø)n]

[SystemQ rule PairDef: ΠS, X , Y: S ∈ {X , Y} ˙⇔ S ==X ˙∨ S ==Y]

[SystemQ rule UnionDef: ΠS, X: S ∈ ∪X ˙⇔ (S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X)]

[SystemQ rule PowerDef: ΠS, X: S ∈ P(X) ˙⇔ ∀s: (s ∈ S ⇒ s ∈ X)]

[SystemQ rule SeparationDef: ΠA, B, P, X , Z: P^{Ph} ∧ ⟨B≡A|P:==Z⟩_{Ph} ⊢⊢ Z ∈ {ph ∈ X | A} ˙⇔ Z ∈ X ˙∧ B]

————- RRRRRRRRRRRRRRR ————-

(*** import fra A.M. ***)

[SystemQ rule TimesCommutativity(R): ΠFX, FY: R(FX)∗∗R(FY) == R(FY)∗ ∗R(FX)]

(*** aksiomer ***)

[SystemQ rule leqReflexivity: ΠX: X <= X]

[SystemQ rule leqAntisymmetryAxiom: ΠX , Y: X <= Y ⇒ Y <= X ⇒ X = Y]

[SystemQ rule leqTransitivityAxiom: ΠX , Y, Z: X <= Y ⇒ Y <= Z ⇒ X <= Z]

[SystemQ rule leqTotality: ΠX , Y: X <= Y ˙∨ Y <= X]

[SystemQ rule leqAdditionAxiom: ΠX , Y, Z: X <= Y ⇒ (X + Z) <= (Y + Z)]

[SystemQ rule leqMultiplicationAxiom: ΠX , Y, Z: 0 <= Z ⇒ X <= Y ⇒ (X ∗ Z) <= (Y ∗ Z)]

[SystemQ rule plusAssociativity: ΠX , Y, Z: (((X + Y)) + Z) = (X + ((Y + Z)))]

[SystemQ rule plusCommutativity: ΠX , Y: (X + Y) = (Y + X)] [SystemQ rule Negative: ΠX: (X + ((−uX))) = 0] [SystemQ rule plus0: ΠX: (X + 0) = X] [SystemQ rule timesAssociativity: ΠX , Y, Z: (((X ∗Y))∗Z) = (X ∗((Y∗Z)))] [SystemQ rule timesCommutativity: ΠX , Y: (X ∗ Y) = (Y ∗ X)] [SystemQ rule ReciprocalAxiom: ΠX: X ≠ 0 ⇒ (X ∗ recX) = 1] [SystemQ rule times1: ΠX: (X ∗ 1) = X] [SystemQ rule Distribution: ΠX , Y, Z: (X ∗ ((Y + Z))) = (((X ∗ Y)) + ((X ∗

Z)))] [SystemQ rule 0not1: 0 ≠ 1] [SystemQ rule EqualityAxiom: ΠX , Y, Z: X = Y ⇒ X = Z ⇒ Y = Z] [SystemQ rule EqLeqAxiom: ΠX , Y: X = Y ⇒ X <= Y] [SystemQ rule EqAdditionAxiom: ΠX , Y, Z: X = Y ⇒ (X + Z) = (Y + Z)] [SystemQ rule EqMultiplicationAxiom: ΠX , Y, Z: X = Y ⇒ (X ∗ Z) = (Y ∗

Z)]

[SystemQ rule A4(Axiom): ΠX , V_{1}, A, B: ⟨A≡B|V_{1}:==X ⟩_{Me} ⊢⊢ ∀V_{1}: B ⇒ A]

(*** XX snydeaksiomer ***) [SystemQ rule ==Reflexivity: ΠRX: RX == RX] [SystemQ rule ==Symmetry: ΠRX, RY: RX == RY ⊢ RY == RX] [SystemQ rule == Transitivity: ΠRX, RY, RZ: RX == RY ⊢ RY == RZ ⊢

RX == RZ]

XX ikke 100procent identisk med originalen fra equivalence-relations [SystemQ rule SENC1: ΠFX, RX, RY: RX == RY ⊢ FX ∈ RX ⊢ FX ∈ RY]

XX boer bevises ud fra nummer 1 [SystemQ rule SENC2: ΠFX, RX, RY: RX == RY ⊢ FX ∈ RY ⊢ FX ∈ RX]

[SystemQ rule PlusF: ΠM, FX, FY: FX +_{f} FY[M] = (FX[M] + FY[M])] [SystemQ rule From ==: ΠFX, FY: R(FX) == R(FY) ⊢ SF(FX, FY)] [SystemQ rule To ==: ΠFX, FY: SF(FX, FY) ⊢ R(FX) == R(FY)] [SystemQ rule FromInR: ΠFX, FY: FX ∈ R(FY) ⊢ SF(FX, FY)] (*** makroer ***) KVANTI [M_{1} ¨= \underline{(m1)}] [M_{2} ¨= \underline{(m2)}] [N_{1} ¨= \underline{(n1)}] [N_{2} ¨= \underline{(n2)}] [N_{3} ¨= \underline{(n3)}] [ϵ ¨= \underline{(ϵ)}]

[ϵ1 ¨= \underline{(ϵ)_{1}}] [ϵ2 ¨= \underline{(ϵ2)}] [X_{1} ¨= \underline{(x1)}] [X_{2} ¨= \underline{(x2)}] [Y_{1} ¨= \underline{(y1)}] [Y_{2} ¨= \underline{(y2)}] [V_{1} ¨= \underline{(v1)}] [V_{2} ¨= \underline{(v2)}] [V_{3} ¨= \underline{(v3)}] [V_{4} ¨= \underline{(v4)}] [V_{2n} ¨= \underline{(v2n)}] [FX ¨= \underline{(fx)}] [FY ¨= \underline{(fy)}] [FZ ¨= \underline{(fz)}] [FU ¨= \underline{(fu)}] [FV ¨= \underline{(fv)}] [FW ¨= \underline{(fw)}] [FEP ¨= \underline{(fep)}] [RX ¨= \underline{(rx)}] [RY ¨= \underline{(ry)}] [RZ ¨= \underline{(rz)}] [RU ¨= \underline{(ru)}] [(SX) ¨= \underline{(sx)}] [(SX1) ¨= \underline{(sx1)}] [(SY) ¨= \underline{(sy)}] [(SY1) ¨= \underline{(sy1)}] [(SZ) ¨= \underline{(sz)}] [(SZ1) ¨= \underline{(sz1)}] [(SU) ¨= \underline{(su)}] [(SU1) ¨= \underline{(su1)}] [FXS ¨= \underline{(fxs)}] [FYS ¨= \underline{(fys)}] [(F1) ¨= \underline{(f1)}] [(F2) ¨= \underline{(f2)}] [(F3) ¨= \underline{(f3)}] [(F4) ¨= \underline{(f4)}] [(OP1) ¨= \underline{(op1)}] [(OP2) ¨= \underline{(op2)}] [(R1) ¨= \underline{(r1)}] [(S1) ¨= \underline{(s1)}] [(S2) ¨= \underline{(s2)}]

[(EPob) ¨= \overline{(ϵ)}] [(CRS1ob) ¨= \overline{(crs1)}] [(F1ob) ¨= \overline{(f1)}] [(F2ob) ¨= \overline{(f2)}] [(F3ob) ¨= \overline{(f3)}] [(F4ob) ¨= \overline{(f4)}] [(N1ob) ¨= \overline{(n1)}] [(N2ob) ¨= \overline{(n2)}] [(OP1ob) ¨= \overline{(op1)}] [(OP2ob) ¨= \overline{(op2)}] [(R1ob) ¨= \overline{(r1)}] [(S1ob) ¨= \overline{(s1)}] [(S2ob) ¨= \overline{(s2)}] [(fx) ≤_{f} (fy) ¨= (fx) <_{f} (fy) ˙∨ SF((fx), (fy))] [Ex3 ¨= c_{Ex}] [∃(v1): a ¨= ˙¬ (∀(v1): ˙¬ (a)n)n] [x <<== y ¨= x << y ˙∨ x == y] [(−1) ¨= (−u1)] [2 ¨= (1 + 1)] [3 ¨= (2 + 1)] [1/2 ¨= rec2] [1/3 ¨= rec3] [2/3 ¨= (2 ∗ 1/3)] [x < y ¨= x <= y ˙∧ x ≠ y] [x ≠ y ¨= ˙¬ (x = y)n] [(x − y) ¨= (x + (−uy))] [00 ¨= R(0f)] [01 ¨= R(1f)] [x!! == y ¨= ˙¬ (x == y)n] (*** REGELLEMMAER ***) (*** UDSAGNSLOGIK ***) [SystemQ lemma ToNegatedImply: ΠA, B: A ⊢ ˙¬ (B)n ⊢ ˙¬ ((A ⇒ B))n] SystemQ proof of ToNegatedImply:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  ˙¬ (B)n  ;
L05: Premise ≫  ˙¬ ( ˙¬ ((A ⇒ B))n)n  ;
L06: RemoveDoubleNeg ⊳ L05 ≫  A ⇒ B  ;
L07: MP ⊳ L06 ⊳ L03 ≫  B  ;

L08: FromContradiction ⊳ L07 ⊳

L04 ≫ ˙¬ ((A ⇒ B))n ;

L09: Block ≫  End  ;
L10: Arbitrary ≫  A, B  ;
L11: Ded ⊳ L09 ≫  {A ⇒ ˙¬ (B)n ⇒ ˙¬ ( ˙¬ ((A ⇒ \atop B))n)n ⇒ ˙¬ ((A ⇒ B))n  ;}
L12: Premise ≫  A  ;
L13: Premise ≫  ˙¬ (B)n  ;
L14: MP2 ⊳ L11 ⊳ L12 ⊳ L13 ≫  {˙¬ ( ˙¬ ((A ⇒ B))n)n ⇒ ˙¬ ((A ⇒ \atop B))n  ;}
L15: AutoImply ≫  {˙¬ ( ˙¬ ((A ⇒ B))n)n ⇒ \atop ˙¬ ( ˙¬ ((A ⇒ B))n)n  ;}
L16: Neg ⊳ L14 ⊳ L15 ≫  ˙¬ ((A ⇒ B))n  □

[SystemQ lemma TND: ΠA: A ˙∨ ˙¬ (A)n] SystemQ proof of TND:

L01: Arbitrary ≫  A  ;
L02: AutoImply ≫  ˙¬ (A)n ⇒ ˙¬ (A)n  ;
L03: Repetition ⊳ L02 ≫  A ˙∨ ˙¬ (A)n  □

[SystemQ lemma FromNegations: ΠA, B: A ⇒ B ⊢ ˙¬ (A)n ⇒ B ⊢ B]

SystemQ proof of FromNegations:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ˙¬ (A)n ⇒ B  ;
L04: TND ≫  A ˙∨ ˙¬ (A)n  ;

L05: FromDisjuncts ⊳ L04 ⊳ L02 ⊳

L03 ≫ B □

[SystemQ lemma prop lemma imply negation: ΠA: A ⇒ ˙¬ (A)n ⊢ ˙¬ (A)n] SystemQ proof of prop lemma imply negation:

L01: Arbitrary ≫  A  ;
L02: Premise ≫  A ⇒ ˙¬ (A)n  ;
L03: AutoImply ≫  ˙¬ (A)n ⇒ ˙¬ (A)n  ;
L04: TND ≫  A ˙∨ ˙¬ (A)n  ;

L05: FromDisjuncts ⊳ L04 ⊳ L02 ⊳

L03 ≫ ˙¬ (A)n □

[SystemQ lemma From3Disjuncts: ΠA, B, C, D: A ˙∨ B ˙∨ C ⊢ A ⇒ D ⊢ B ⇒ D ⊢ C ⇒ D ⊢ D]

SystemQ proof of From3Disjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C, D  ;
L03: Premise ≫  A ˙∨ B ˙∨ C  ;
L04: Premise ≫  B ⇒ D  ;
L05: Premise ≫  C ⇒ D  ;
L06: Premise ≫  ˙¬ (A)n  ;
L07: Repetition ⊳ L03 ≫  ˙¬ (A)n ⇒ (B ˙∨ C)  ;
L08: MP ⊳ L07 ⊳ L06 ≫  B ˙∨ C  ;

L09: FromDisjuncts ⊳ L08 ⊳ L04 ⊳

L05 ≫ D ;

L10: Block ≫  End  ;
L11: Arbitrary ≫  A, B, C, D  ;
L12: Ded ⊳ L10 ≫  {A ˙∨ B ˙∨ C ⇒ (B ⇒ D) ⇒ (C ⇒ \atop D) ⇒ ˙¬ (A)n ⇒ D  ;}
L13: AutoImply ≫  (A ⇒ D) ⇒ A ⇒ D  ;
L14: Premise ≫  A ˙∨ B ˙∨ C  ;
L15: Premise ≫  A ⇒ D  ;
L16: Premise ≫  B ⇒ D  ;
L17: Premise ≫  C ⇒ D  ;
L18: MP3⊳L12⊳L14⊳L16⊳L17 ≫ ˙¬ (A)n ⇒ D  ;
L19: MP ⊳ L13 ⊳ L15 ≫ A ⇒ D ;
L20: FromNegations ⊳ L19 ⊳ L18 ≫ D  □

[SystemQ lemma NegateDisjunct1: ΠA, B: A ˙∨ B ⊢ ˙¬ (A)n ⊢ B]

SystemQ proof of NegateDisjunct1:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙∨ B  ;
L03: Premise ≫  ˙¬ (A)n  ;
L04: Repetition ⊳ L02 ≫  ˙¬ (A)n ⇒ B  ;

L05: MP ⊳ L04 ⊳ L03 ≫  B  □

[SystemQ lemma NegateDisjunct2: ΠA, B: A ˙∨ B ⊢ ˙¬ (B)n ⊢ A]

SystemQ proof of NegateDisjunct2:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙∨ B  ;
L03: Premise ≫  ˙¬ (B)n  ;
L04: Repetition ⊳ L02 ≫  ˙¬ (A)n ⇒ B  ;
L05: NegativeMT ⊳ L04 ⊳ L03 ≫  A  □

(***)

[SystemQ lemma ExpandDisjuncts: ΠA, B, C, D: A ˙∨ B ⊢ C ˙∨ D ⊢ B ˙∨ D ˙∨ (A ˙∧ C)]

SystemQ proof of ExpandDisjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C, D  ;
L03: Premise ≫  A ˙∨ B  ;
L04: Premise ≫  C ˙∨ D  ;
L05: Premise ≫  ˙¬ (B)n  ;
L06: Premise ≫  ˙¬ (D)n  ;
L07: NegateDisjunct2⊳L03⊳L05 ≫ A  ;
L08: NegateDisjunct2⊳L04⊳L06 ≫ C  ;
L09: JoinConjuncts ⊳ L07 ⊳ L08 ≫ A ˙∧ C  ;
L10: Block ≫  End  ;
L11: Arbitrary ≫  A, B, C, D  ;
L12: Ded ⊳ L10 ≫  {A ˙∨ B ⇒ C ˙∨ D ⇒ ˙¬ (B)n ⇒ \atop ˙¬ (D)n ⇒ A ˙∧ C  ;}
L13: Premise ≫  A ˙∨ B  ;
L14: Premise ≫  C ˙∨ D  ;
L15: MP2 ⊳ L12 ⊳ L13 ⊳ L14 ≫  ˙¬ (B)n ⇒ ˙¬ (D)n ⇒ A ˙∧ C  ;
L16: Repetition ⊳ L15 ≫  B ˙∨ D ˙∨ (A ˙∧ C)  □

[SystemQ lemma From2 ∗ 2Disjuncts: ΠA, B, C, D, E: A ˙∨ B ⊢ C ˙∨ D ⊢ A ⇒ C ⇒ E ⊢ A ⇒ D ⇒ E ⊢ B ⇒ C ⇒ E ⊢ B ⇒ D ⇒ E ⊢ E]

SystemQ proof of From2 ∗ 2Disjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C, D, E  ;
L03: Premise ≫  C ˙∨ D  ;
L04: Premise ≫  A ⇒ C ⇒ E  ;
L05: Premise ≫  A ⇒ D ⇒ E  ;
L06: Premise ≫  A  ;
L07: MP ⊳ L04 ⊳ L06 ≫  C ⇒ E  ;
L08: MP ⊳ L05 ⊳ L06 ≫  D ⇒ E  ;

L09: FromDisjuncts ⊳ L03 ⊳ L07 ⊳

L08 ≫ E ;

L10: Block ≫  End  ;
L11: Block ≫  Begin  ;
L12: Arbitrary ≫  A, B, C, D, E  ;
L13: Premise ≫  A ˙∨ B  ;

L14: Premise ≫  C ˙∨ D  ;
L15: Premise ≫  B ⇒ C ⇒ E  ;
L16: Premise ≫  B ⇒ D ⇒ E  ;
L17: Premise ≫  ˙¬ (A)n  ;
L18: NegateDisjunct1⊳L13⊳L17 ≫ B  ;
L19: MP ⊳ L15 ⊳ L18 ≫  C ⇒ E  ;
L20: MP ⊳ L16 ⊳ L18 ≫  D ⇒ E  ;

L21: FromDisjuncts ⊳ L14 ⊳ L19 ⊳

L20 ≫ E ;

L22: Block ≫  End  ;
L23: Arbitrary ≫  A, B, C, D, E  ;
L24: Ded ⊳ L10 ≫  {C ˙∨ D ⇒ (A ⇒ C ⇒ E) ⇒ \atop (A ⇒ D ⇒ E) ⇒ A ⇒ E  ;}
L25: Ded ⊳ L22 ≫  A ˙∨ B ⇒ C ˙∨ D ⇒ (B ⇒ ; C ⇒ E) ⇒ (B ⇒ D ⇒ E) ⇒ ; ˙¬ (A)n ⇒ E  ;

L26: Premise ≫  A ˙∨ B  ;
L27: Premise ≫  C ˙∨ D  ;
L28: Premise ≫  A ⇒ C ⇒ E  ;
L29: Premise ≫  A ⇒ D ⇒ E  ;
L30: Premise ≫  B ⇒ C ⇒ E  ;
L31: Premise ≫  B ⇒ D ⇒ E  ;
L32: MP3⊳L24⊳L27⊳L28⊳L29 ≫ A ⇒ E  ;

L33: MP4 ⊳ L25 ⊳ L26 ⊳ L27 ⊳

L30 ⊳ L31 ≫ ˙¬ (A)n ⇒ E ;

L34: FromNegations ⊳ L32 ⊳ L33 ≫ E  □

(*** SAME-F ***) XX-am

(*** R-AFDELINGEN ***) XX-am

(*******************)

[SystemQ lemma FromNegatedImply: ΠA, B: ˙¬ ((A ⇒ B))n ⊢ A ˙∧ ˙¬ (B)n] SystemQ proof of FromNegatedImply:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A ⇒ ˙¬ ( ˙¬ (B)n)n  ;
L04: Premise ≫  A  ;
L05: MP ⊳ L03 ⊳ L04 ≫  ˙¬ ( ˙¬ (B)n)n  ;
L06: RemoveDoubleNeg ⊳ L05 ≫  B  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  A, B  ;
L03: Ded ⊳ L07 ≫  (A ⇒ ˙¬ ( ˙¬ (B)n)n) ⇒ (A ⇒ B) ;
L04: Premise ≫  ˙¬ ((A ⇒ B))n  ;
L05: MT ⊳ L03 ⊳ L04 ≫  ˙¬ ((A ⇒ ˙¬ ( ˙¬ (B)n)n))n  ;
L09: Repetition ⊳ L05 ≫  A ˙∧ ˙¬ (B)n  □

(***)

[SystemQ lemma FromNegated(2 ∗ Imply): ΠA, B, C: ˙¬ ((A ⇒ B ⇒ C))n ⊢ A ˙∧ B ˙∧ ˙¬ (C)n]

SystemQ proof of FromNegated(2 ∗ Imply):

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  ˙¬ ((A ⇒ B ⇒ C))n  ;
L03: FromNegatedImply ⊳ L02 ≫  A ˙∧ ˙¬ ((B ⇒ C))n  ;
L04: FirstConjunct ⊳ L03 ≫  A  ;
L05: SecondConjunct ⊳ L03 ≫  ˙¬ ((B ⇒ C))n  ;
L06: FromNegatedImply ⊳ L05 ≫  B ˙∧ ˙¬ (C)n  ;
L07: FirstConjunct ⊳ L06 ≫  B  ;
L08: SecondConjunct ⊳ L06 ≫  ˙¬ (C)n  ;
L09: JoinConjuncts ⊳ L04 ⊳ L07 ≫ A ˙∧ B  ;
L10: JoinConjuncts ⊳ L09 ⊳ L08 ≫ A ˙∧ B ˙∧ ˙¬ (C)n  □

[SystemQ lemma FromNegatedOr: ΠA, B: ˙¬ ((A ˙∨ B))n ⊢ ˙¬ (A)n ˙∧ ˙¬ (B)n] SystemQ proof of FromNegatedOr:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  ˙¬ ((A ˙∨ B))n  ;
L03: Repetition ⊳ L02 ≫  ˙¬ (( ˙¬ (A)n ⇒ B))n  ;
L04: FromNegatedImply ⊳ L03 ≫  ˙¬ (A)n ˙∧ ˙¬ (B)n  □

[SystemQ rule InductionAxiom: ΠV_{1}, A, B, C: ⟨B≡A|V_{1}:==0⟩_{Me} ⊢⊢ ⟨C≡A|V_{1}:==(V_{1}+ 1)⟩_{Me} ⊢⊢ B ⇒ ∀V_{1}: (A ⇒ C) ⇒ ∀V_{1}: A]

[SystemQ rule LessMinus1(N): ΠM, N: Nat(M) ⊢⊢ Nat(N) ⊢⊢ M < (N +

1) ⊢ M <= N] [SystemQ rule Nonnegative(N): ΠM: Nat(M) ⊢⊢ 0 <= M] ————– [SystemQ rule Cauchy: ΠV_{1}, V_{2}, N , ϵ, FX: ∀ϵ: ∃N: ∀V_{1}, V_{2}: (0 < ϵ ⇒ N <=

V_{1} ⇒ N <= V_{2} ⇒ |(FX[V_{1}] − FX[V_{2}])| < ϵ)] ————- ————– [SystemQ lemma JoinConjuncts(2conditions): ΠA, B, C, D: A ⇒ B ⇒ C ⊢

A ⇒ B ⇒ D ⊢ A ⇒ B ⇒ C ˙∧ D]

SystemQ proof of JoinConjuncts(2conditions):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C, D  ;
L03: Premise ≫  A ⇒ B ⇒ C  ;
L04: Premise ≫  A ⇒ B ⇒ D  ;
L05: Premise ≫  A  ;
L06: Premise ≫  B  ;
L07: MP2 ⊳ L03 ⊳ L05 ⊳ L06 ≫  C  ;
L08: MP2 ⊳ L04 ⊳ L05 ⊳ L06 ≫  D  ;
L09: JoinConjuncts ⊳ L07 ⊳ L08 ≫ C ˙∧ D  ;
L10: Block ≫  End  ;
L11: Arbitrary ≫  A, B, C, D  ;
L03: Ded ⊳ L10 ≫  {(A ⇒ B ⇒ C) ⇒ (A ⇒ B ⇒ \atop D) ⇒ A ⇒ B ⇒ C ˙∧ D  ;}
L04: Premise ≫  A ⇒ B ⇒ C  ;
L05: Premise ≫  A ⇒ B ⇒ D  ;
L12: MP2 ⊳ L03 ⊳ L04 ⊳ L05 ≫  A ⇒ B ⇒ C ˙∧ D  □

—————-

[SystemQ lemma FromNegatedAnd: ΠA, B: ˙¬ ((A ˙∧ B))n ⊢ A ⊢ ˙¬ (B)n]

SystemQ proof of FromNegatedAnd:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  ˙¬ ((A ˙∧ B))n  ;
L03: Premise ≫  A  ;
L04: Repetition ⊳ L02 ≫  ˙¬ ( ˙¬ ((A ⇒ ˙¬ (B)n))n)n  ;
L05: RemoveDoubleNeg ⊳ L04 ≫  A ⇒ ˙¬ (B)n  ;
L06: MP ⊳ L05 ⊳ L03 ≫  ˙¬ (B)n  □

——–

———-

[SystemQ lemma ToNegatedOr: ΠA, B: ˙¬ (A)n ˙∧ ˙¬ (B)n ⊢ ˙¬ ((A ˙∨ B))n]

SystemQ proof of ToNegatedOr:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  ˙¬ (A)n ˙∧ ˙¬ (B)n  ;
L04: Premise ≫  A ˙∨ B  ;
L05: FirstConjunct ⊳ L03 ≫  ˙¬ (A)n  ;
L06: SecondConjunct ⊳ L03 ≫  ˙¬ (B)n  ;
L07: NegateDisjunct1⊳L04⊳L05 ≫ B  ;

L08: FromContradiction ⊳ L07 ⊳

L06 ≫ ˙¬ ((A ˙∨ B))n ;

L09: Block ≫  End  ;
L10: Arbitrary ≫  A, B  ;
L03: Ded ⊳ L09 ≫  {˙¬ (A)n ˙∧ ˙¬ (B)n ⇒ A ˙∨ B ⇒ \atop ˙¬ ((A ˙∨ B))n  ;}
L04: Premise ≫  ˙¬ (A)n ˙∧ ˙¬ (B)n  ;
L05: MP ⊳ L03 ⊳ L04 ≫  A ˙∨ B ⇒ ˙¬ ((A ˙∨ B))n  ;

L11: prop lemma imply negation ⊳

L05 ≫ ˙¬ ((A ˙∨ B))n □

——————–

[SystemQ rule NextXS(UpperBound): ΠM: UB(01//02∗∗(xs[M]++us[M]), SetOfReals) ⊢ xs[(M + 1)] == xs[M]]

[SystemQ rule NextXS(NoUpperBound): ΠM: ˙¬ (UB(01//02∗∗(xs[M]++us[M]), SetOfReals))n ⊢ xs[(M + 1)] == 01//02 ∗ ∗(xs[M] + +us[M])]

[SystemQ rule NextUS(UpperBound): ΠM: UB(01//02∗∗(xs[M]++us[M]), SetOfReals) ⊢ us[(M + 1)] == 01//02 ∗ ∗(xs[M] + +us[M])]

[SystemQ rule NextUS(NoUpperBound): ΠM: ˙¬ (UB(01//02∗∗(xs[M]++us[M]), SetOfReals))n ⊢ us[(M + 1)] == us[M]]

[SystemQ rule US0: us[0] == xs[0] + +01]

[SystemQ rule ExpZero: ΠM, X: M = 0 ⊢ X (exp)M = 1]

[SystemQ rule ExpPositive: ΠM, X: 0 < M ⊢ X (exp)M = (X ∗X (exp)((M− 1)))]

————–

[SystemQ rule BSzero: ΠM, N: N = 0 ⊢ BS(M, N) = 1/2(exp)M]

[SystemQ rule BSpositive: ΠM, N: 0 < N ⊢ BS(M, N) = (1/2(exp)((M + N)) + BS(M, (N − 1)))]

———— [SystemQ rule UStelescope(Zero): ΠM, N: N = 0 ⊢ UStelescope(M, N) =

|(us[M] − us[(M + 1)])|]

[SystemQ rule UStelescope(Positive): ΠM, N: 0 < N ⊢ UStelescope(M, N) = (|(us[(M + N)] − us[(M + ((N + 1)))])| + UStelescope(M, (N − 1)))]

[(x) ¨= (x)] ———- [SystemQ rule EqAddition(R): ΠFX, FY, FZ: R(FX) = R(FY) ⊢ R(FX) +

+R(FZ) = R(FY) + +R(FZ)]

[SystemQ rule PlusCommutativity(R): ΠFX, FY: R(FX)++R(FY) == R(FY)+ +R(FX)]

————— [SystemQ rule PlusAssociativity(R): ΠFX, FY, FZ: R(FX)++R(FY)++R(FZ) =

R(FX) + +(R(FY) + +R(FZ))]

[SystemQ rule PlusAssociativity(R)XX: ΠFX, FY, FZ: R(FX+_{f}FY+_{f}FZ) == R(FX +_{f} (FY +_{f} FZ))]

[SystemQ rule Plus0(R): ΠFX: R(FX) + +00 == R(FX)] [SystemQ rule Negative(R): ΠM, FX: R(FX) + +(− − R(FX)) == 00] [SystemQ rule TimesAssociativity(R): ΠFX, FY, FZ: R(FX)∗∗R(FY)∗∗R(FZ) ==

R(FX) ∗ ∗(R(FY) ∗ ∗R(FZ))] [SystemQ rule Times1(R): ΠFX: R(FX) ∗ ∗01 == R(FX)] ———–(21.10.06) [SystemQ rule lessAddition(R): ΠM, ϵ, FX, FY, FZ: R(FX) << R(FY) ⊢ R(FX)+

+R(FZ) << R(FY) + +R(FZ)] ————–(23.10.06) [SystemQ rule LeqAntisymmetry(R): ΠFX, FY: R(FX) <<== R(FY) ⊢ R(FY) <<==

R(FX) ⊢ R(FX) = R(FY)]

[SystemQ rule LeqTransitivity(R): ΠFX, FY, FZ: R(FX) <<== R(FY) ⊢ R(FY) <<== R(FZ) ⊢ R(FX) <<== R(FZ)]

————–(24.10.06) [SystemQ rule leqAddition(R): ΠFX, FY, FZ: R(FX) <<== R(FY) ⊢ R(FX)+

+R(FZ) <<== R(FY) + +R(FZ)]

[SystemQ rule Distribution(R): ΠFX, FY, FZ: R(FX)∗∗(R(FY)++R(FZ)) = R(FX) ∗ ∗R(FY) + +R(FX) ∗ ∗R(FZ)]

[(− − 01) ¨= (− − 01)] ————-(24.10.06) [SystemQ rule FromLimit: ΠM, N , FEP, FX, FYS: Limit(FX, FYS) ⊢ ∀FEP: ∃M: ∀N: (00 <<

FEP ⇒ M <= N ⇒ |rFX + +(− − FYS[N])| << FEP)]

[SystemQ rule ToUpperBound: ΠFX, FY, FXS: FX ∈ FXS ⇒ FX <<== FY ⊢ UB(FY, FXS)]

[SystemQ rule FromUpperBound: ΠFX, FY, FXS: UB(FY, FXS) ⊢ FX ∈ FXS ⊢ FX <<== FY]

[SystemQ rule USisUpperBound: ΠM: UB(usFoelge[M], SetOfFxs)] ———(25.10.06)

[SystemQ rule 0not1(R): 00 ≠ 01] ———(25.10.06) [SystemQ rule ExpZero(R): ΠM, FX: M = 0 ⊢ FX(exp)M = 01] [SystemQ rule ExpPositive(R): ΠM, FX: 0 < M ⊢ FX(exp)M == FX ∗

∗FX(exp)((M − 1))] —–(26.10.06) [02 ¨= 01 + +01] [01//02 ¨= 01//temp02] ——(28.10.06) [SystemQ rule ExpUnbounded(R): ΠM, FX: ∃M: FX << 02(exp)M] ——(30.10.06) [SystemQ rule FromLeq(Advanced)(N): ΠM, M_{1}, N: M <= N ⊢ ∃M_{1}: (M+

M_{1}) = N] ——-(3.11.06) [usFoelge ¨= us] [SystemQ rule FromLeastUpperBound: LUB(FX, FYS) ⊢ UB(FX, FYS) ˙∧

(UB(FZ, FYS) ⇒ FX <<== FZ)]

[SystemQ rule ToLeastUpperBound: ΠFX, FZ, FYS: UB(FX, FYS) ⊢ UB(FZ, FYS) ⇒ FX <<== FZ ⊢ LUB(FX, FYS)]

[SystemQ rule XSisNotUpperBound: ΠM: ˙¬ (UB(xs[M], SetOfFxs))n] ——-(4.11.06) [xaF ¨= xs] [SystemQ rule ysFGreater: ΠM: xaF[M] < ysF[M]] [SystemQ rule ysFLess: ΠM: ysF[M] < (xaF[M] + recM)] [SystemQ rule SmallInverse: ΠM, X: 0 < X ⊢ ∃M: recM < X] ——-(6.11.06) [x == y ¨= x = y] [OrderedPair(x, y) ¨= ⟨x, y⟩] [SystemQ rule MemberOfSeries(Imply): ΠM, FX, (SY): M ∈ N ⇒ IsSeries(FX, (SY)) ⇒

OrderedPair(M, FX[M]) ∈ FX]

[SystemQ lemma MemberOfSeries: ΠM, FX, (SY): M ∈ N ⊢ IsSeries(FX, (SY)) ⊢ OrderedPair(M, FX[M]) ∈ FX]

SystemQ proof of MemberOfSeries:

L01: Arbitrary ≫  M, FX, (SY)  ;
L02: Premise ≫  M ∈ N  ;
L03: Premise ≫  IsSeries(FX, (SY))  ;

L04: MemberOfSeries(Imply) ≫

M  ∈  N  ⇒

IsSeries(FX, (SY)) ⇒ OrderedPair(M, FX[M]) ∈ FX ;

L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫  OrderedPair(M, FX[M]) ∈ FX □

[SystemQ lemma memberOfSeries(Type): ΠM, FX, (SY): TypeNat(M) ⊢⊢ TypeSeries(FX, (SY)) ⊢⊢ OrderedPair(M, FX[M]) ∈ FX]

SystemQ proof of memberOfSeries(Type):

L01: Arbitrary ≫  M, FX, (SY)  ;
L02: Side-condition ≫  TypeNat(M)  ;
L03: Side-condition ≫  TypeSeries(FX, (SY))  ;
L04: NatType ⊳ ⊳ L02 ≫  M ∈ N  ;

L05: SeriesType ⊳ ⊳ L03 ≫  IsSeries(FX, (SY))  ;
L06: MemberOfSeries⊳L04⊳L05 ≫ OrderedPair(M, FX[M]) ∈ FX □

[SystemQ rule NatType: ΠM: TypeNat(M) ⊢⊢ M ∈ N] [SystemQ rule RationalType: ΠX: TypeRational(X) ⊢⊢ X ∈ Q] [SystemQ rule SeriesType: ΠFX, (SY): TypeSeries(FX, (SY)) ⊢⊢ IsSeries(FX, (SY))] [IsOrderedPair((sx), (sy), (sz)) ¨= ∃(OP1ob): ∃(OP2ob): (OP1ob) ∈ (sy) ˙∧

(OP2ob) ∈ (sz) ˙∧ (sx) = OrderedPair((OP1ob), (OP2ob))] [IsRelation((sx), (sy), (sz)) ¨= ∀(R1ob): ((R1ob) ∈ (sx) ⇒ IsOrderedPair((R1ob), (sy), (sz)))] [isFunction((sx), (sy), (sz)) ¨= IsRelation((sx), (sy), (sz)) ˙∧ ∀(F1ob), (F2ob),

(F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ (sx) ⇒ OrderedPair((F3ob), (F4ob)) ∈ (sx) ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob))]

[IsSeries((fx), (fy)) ¨= isFunction((fx), N, (fy)) ˙∧ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ (fx))]

XXhertype [TypeNat(x) ¨= λc.TypeNat0(⌈x⌉)] [TypeNat0(x) ˙= x ∈_{t} (⌈0⌉ : : ⌈V_{2n}⌉ : : ⌈M⌉ : : ⌈N ⌉ : : ⌈(N +1)⌉ : : ⌈(M+0)⌉ : :

⌈(M + N)⌉ : : ⌈O⌉ : : ⌈P⌉ : : ⌈((M + N) + 1)⌉ : : ⌈(M + M_{1})⌉ : : ⌈(M + ((N + 1)))⌉ : : ⌈M_{1}⌉ : : ⌈M_{2}⌉ : : ⌈N_{1}⌉ : : ⌈N_{2}⌉ : : ⌈m⌉ : : ⌈n⌉ : : T)]

[TypeSeries(x, y) ¨= λc.Typeseries0(⌈x⌉, ⌈y⌉)] [Typeseries0(x, y) ˙= y!x ∈_{t} (⌈FX⌉ : : ⌈FY⌉ : : ⌈FZ⌉ : : ⌈us⌉ : : ⌈FX +_{f} FY⌉ : :

⌈0f⌉ : : ⌈1f⌉ : : ⌈FX ∗_{f} 0f⌉ : : ⌈1f/FX⌉ : : T)] [TypeRational(x) ¨= λc.TypeRational0(⌈x⌉)] [TypeRational0(x) ˙= x ∈_{t} (⌈X ⌉ : : ⌈Y⌉ : : ⌈Z⌉ : : ⌈0⌉ : : ⌈1⌉ : : T)] [Max(x, y) ¨= if(y <= x, x, y)] —–(7.11.06) [SystemQ rule ReciprocalF: ΠM, FX: 1f/FX[M] = if(FX[M] = 0, 0, recFX[M])] ——–(11.11.06) [0f ¨= constantRationalSeries(0)] [1f ¨= constantRationalSeries(1)] [cartProd((sx)) ¨=

{ph ∈ Power(Power(binaryUnion((sx), (sy)))) | IsOrderedPair(ph_{1}, (sx), (sy))}] [constantRationalSeries(x) ¨= {ph ∈ cartProd(N) | ∃(CRS1ob): ph_{3} = OrderedPair((CRS1ob), x)}] [SystemQ rule Sep2Formula: ΠA, B, X , Y: Y ∈ {ph ∈ X | A} ⊢ Y ∈ X ˙∧ B] [Power(x) ¨= P(x)] ——-(12.11.06) [IsSubset(x, y) ¨= x ⊆ y] ——(12.11.06) [SystemQ rule Formula2Sep: ΠA, B, X , Y: Y ∈ X ⊢ B ⊢ Y ∈ {ph ∈ X | A}] ——(13.11.06) [SystemQ lemma SameSeries: ΠM, N , FX, (SY): TypeNat(M) ⊢⊢ TypeNat(N) ⊢⊢

TypeSeries(FX, (SY)) ⊢⊢ M = N ⊢ FX[M] = FX[N]]

SystemQ proof of SameSeries:

L01: Arbitrary ≫  M, N , FX, (SY)  ;
L02: Side-condition ≫  TypeNat(M)  ;
L03: Side-condition ≫  TypeNat(N)  ;
L04: Side-condition ≫  TypeSeries(FX, (SY))  ;
L05: Premise ≫  M = N  ;

L06: memberOfSeries(Type) ⊳ ⊳ L02 ⊳ ⊳ L04 ≫ OrderedPair(M, FX[M]) ∈ FX ; L07: memberOfSeries(Type) ⊳ ⊳

L03 ⊳ ⊳ L04 ≫

OrderedPair(N , FX[N]) ∈ FX ;

L08: UniqueMember(Type) ⊳ ⊳ L04 ⊳ L06 ⊳ L07 ⊳ L05 ≫

FX[M] = FX[N] □

[SystemQ lemma UniqueMember(Type): ΠFX, (SX), (SX1), (SY), (SY1), (SZ): TypeSeries(FX, (SZ)) ⊢⊢ OrderedPair((SX), (SX1)) ∈ FX ⊢ OrderedPair((SY), (SY1)) ∈ FX ⊢ (SX) = (SY) ⊢ (SX1) = (SY1)]

SystemQ proof of UniqueMember(Type): L01: Arbitrary ≫ FX, (SX), (SX1), (SY), (SY1),

(SZ) ;

L02: Side-condition ≫ TypeSeries(FX, (SZ)) ;

L03: Premise ≫ OrderedPair((SX), (SX1)) ∈

FX ;

L04: Premise ≫ OrderedPair((SY), (SY1)) ∈

FX ;

L05: Premise ≫  (SX) = (SY)  ;
L06: SeriesType ⊳ ⊳ L02 ≫  IsSeries(FX, (SZ))  ;

L07: UniqueMember ⊳ L06 ⊳ L03 ⊳

L04 ⊳ L05 ≫ (SX1) = (SY1) □

[SystemQ lemma UniqueMember: ΠFX, (SX), (SX1), (SY), (SY1), (SZ): IsSeries(FX, (SZ)) ⊢ OrderedPair((SX), (SX1)) ∈ FX ⊢ OrderedPair((SY), (SY1)) ∈ FX ⊢ (SX) = (SY) ⊢ (SX1) = (SY1)]

SystemQ proof of UniqueMember: L01: Arbitrary ≫ FX, (SX), (SX1), (SY), (SY1),

(SZ) ;

L02: Premise ≫ IsSeries(FX, (SZ)) ;

L03: Premise ≫ OrderedPair((SX), (SX1)) ∈

FX ;

L04: Premise ≫ OrderedPair((SY), (SY1)) ∈

FX ;

L05: Premise ≫ (SX) = (SY) ;

L06: Repetition ⊳ L02 ≫

isFunction(FX, N, (SZ))  ˙∧

∀(S1ob): ((S1ob) ∈ N ⇒

∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) ;

L07: FirstConjunct ⊳ L06 ≫ isFunction(FX, N, (SZ)) ;

L08: Repetition ⊳ L07 ≫

IsRelation(FX, N, (SZ))  ˙∧

∀(F1ob), (F2ob), (F3ob),

(F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob)) ; L09: SecondConjunct ⊳ L08 ≫ ∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob)) ;

L10: A4 @(SX) ⊳ L09 ≫ ∀(F2ob), (F3ob), (F4ob): (OrderedPair((SX), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (SX) = (F3ob) ⇒ (F2ob) = (F4ob)) ;

L11: A4 @(SX1) ⊳ L10 ≫ ∀(F3ob), (F4ob): (OrderedPair((SX), (SX1)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (SX) = (F3ob) ⇒ (SX1) = (F4ob)) ;

L12: A4 @(SY) ⊳ L11 ≫ ∀(F4ob): (OrderedPair((SX), (SX1)) ∈ FX ⇒ OrderedPair((SY), (F4ob)) ∈ FX ⇒ (SX) = (SY) ⇒ (SX1) = (F4ob)) ;

L13: A4 @(SY1) ⊳ L12 ≫ OrderedPair((SX), (SX1)) ∈ FX ⇒ OrderedPair((SY), (SY1)) ∈ FX ⇒ (SX) = (SY) ⇒ (SX1) = (SY1) ;

L14: MP3⊳L13⊳L03⊳L04⊳L05 ≫ (SX1) = (SY1)  □

[SystemQ lemma A4: ΠX , V_{1}, A, B: ⟨A≡B|V_{1}:==X ⟩_{Me} ⊢⊢ ∀V_{1}: B ⊢ A] KVANTI SystemQ proof of A4:

L01: Arbitrary ≫  X , V_{1}, A, B  ;
L02: Side-condition ≫  ⟨A≡B|V_{1}:==X ⟩_{Me}  ;
L03: Premise ≫  ∀V_{1}: B  ;
L04: A4(Axiom) ⊳ ⊳ L02 ≫  ∀V_{1}: B ⇒ A  ;
L05: MP ⊳ L04 ⊳ L03 ≫  A  □

——(16.11.06) [SystemQ rule SameMember: Π(SX), (SY), (SZ): (SX) = (SY) ⊢ (SX) ∈ (SZ) ⊢

(SY) ∈ (SZ)]

[SystemQ rule ToSetEquality: Π(SX), FY: IsSubset(FX, FY) ⊢ IsSubset(FY, FX) ⊢ FX = FY]

[(px, y) ¨= {x, y}] [SystemQ rule SamePair: Π(SX), (SX1), (SY), (SY1): (SX) = (SX1) ⊢ (SY) =

(SY1) ⊢ (p(SX), (SY)) = (p(SX1), (SY1))] [(sx) ¨= {x}] [SystemQ rule SameSingleton: Π(SX), (SY): (SX) = (SY) ⊢ (s(SX)) = (s(SY))] ——-(17.11.06) [(fx) +_{f} (fy) ¨= {ph ∈ cartProd(N) | ∃M: ph_{4} = OrderedPair(M, ((fx)[M] +

(fy)[M]))}] [SystemQ rule Qclosed(Addition): ΠX , Y: X ∈ Q ⊢ Y ∈ Q ⊢ (X + Y) ∈ Q] [SystemQ rule FromCartProd(1): Π(SX), (SX1), (SY), (SY1): OrderedPair((SX), (SY)) ∈

cartProd((SX1)) ⊢ (SX) ∈ (SX1)]

[SystemQ rule 1rule fromCartProd(2): Π(SX), (SX1), (SY), (SY1): OrderedPair((SX), (SY)) ∈ cartProd((SX1)) ⊢ (SY) ∈ (SY1)]

——-(18.11.06) [(fx) ∗_{f} (fy) ¨= {ph ∈ cartProd(N) | ∃M: ph_{5} = OrderedPair(M, ((fx)[M] ∗

(fy)[M]))}]

[SystemQ rule Qclosed(Multiplication): ΠX , Y: X ∈ Q ⊢ Y ∈ Q ⊢ (X ∗ Y) ∈ Q]

——-(19.11.06) [SystemQ rule Pair2Formula: Π(SX), (SY), (SZ): (SX) ∈ (p(SY), (SZ)) ⊢ (SX) =

(SY) ˙∨ (SX) = (SZ)]

[SystemQ rule Formula2Pair: Π(SX), (SY), (SZ): (SX) = (SY) ˙∨ (SX) = (SZ) ⊢ (SX) ∈ (p(SY), (SZ))]

—-(23.11.06) [binaryUnion(x, y) ¨= Union((px, y))] [SystemQ rule Formula2Union: Π(SX), (SY), (SZ): ∃(SY): (SX) ∈ (SY) ˙∧ (SY) ∈

(SZ) ⊢ (SX) ∈ Union((SZ))]

[SystemQ rule Formula2Power: Π(SX), (SY): IsSubset((SX), (SY)) ⊢ (SX) ∈ Power((SY))]

——-(28.11.06) [SetOfRationalSeries ¨= {ph ∈ Power(cartProd(N)) | IsSeries(ph_{2}, Q)}] [1f/(fx) ¨= {ph ∈ cartProd(N) | ∃M: ((fx)[M] ≠ 0 ˙∧ ph_{6} = OrderedPair(M, rec(fx)[M])) ˙∨

((fx)[M] = 0 ˙∧ ph_{6} = OrderedPair(M, 0))}]

[SystemQ rule Max: ΠX , Y: (Y <= X ˙∧ Max(X , Y) = X) ˙∨ ( ˙¬ (Y <= X)n ˙∧ Max(X , Y) = Y)]

[SystemQ rule Numerical: ΠX: (0 <= X ˙∧ |X | = X) ˙∨ ( ˙¬ (0 <= X)n ˙∧ |X | = (−uX))]

[SystemQ rule Separation2formula(1): ΠA, B, X , Y: Y ∈ {ph ∈ X | A} ⊢ Y ∈ X]

[SystemQ rule Separation2formula(2): ΠA, B, X , Y: Y ∈ {ph ∈ X | A} ⊢ B] [SystemQ rule QisClosed(Reciprocal)(Imply): ΠX: X ≠ 0 ⇒ X ∈ Q ⇒

recX ∈ Q] [SystemQ lemma QisClosed(Reciprocal): ΠX: X ≠ 0 ⊢ X ∈ Q ⊢ recX ∈ Q] SystemQ proof of QisClosed(Reciprocal):

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X ≠ 0  ;
L03: Premise ≫  X ∈ Q  ;
L04: QisClosed(Reciprocal)(Imply) ≫ X ≠ 0 ⇒ X ∈ Q ⇒ recX ∈ Q ;
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫ recX ∈ Q □

——(1.12.06)

[SystemQ rule QisClosed(Negative)(Imply): ΠX: X ∈ Q ⇒ (−uX) ∈ Q] [SystemQ lemma QisClosed(Negative): ΠX: X ∈ Q ⊢ (−uX) ∈ Q] SystemQ proof of QisClosed(Negative):

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X ∈ Q  ;
L03: QisClosed(Negative)(Imply) ≫ X ∈ Q ⇒ (−uX) ∈ Q  ;
L04: MP ⊳ L03 ⊳ L02 ≫ (−uX) ∈ Q □

[−_{f}(fx) ¨= {ph ∈ cartProd(N) | ∃M: ph_{6} = OrderedPair(M, (−u(fx)[M]))}] [SF((fx), (fy)) ¨= ∀(EPob): ∃n: ∀m: (0 < (EPob) ⇒ n <= m ⇒ |((fx)[m] −

(fy)[m])| < (EPob))] ——(2.12.06) [(fx) <_{f} (fy) ¨= ∃(EPob): ∃n: ∀m: 0 < (EPob) ˙∧ (n <= m ⇒ (fx)[m] <=

((fy)[m] − (EPob)))] ——(2.12.06) [extractSeries(t) ˙= t^{2}^{2}^{1}^{2}^{1}^{2}^{2}^{2}^{1}^{1}^{1}^{1}^{1}^{1}] [SetOfSeries((sx)) ¨= {ph ∈ Power(cartProd(N)) | IsSeries(ph_{6}, (sx))}] [R((fx)) ¨= {ph ∈ Power(SetOfSeries(Q)) | SF((fx), ph_{4})}] [ExpandList(t, s, c) ˙= t!s!c!if t^{a} then T else StateExpand(t^{h}, s, c) : : ExpandList(t^{t}, s, c)] (***) ([x ∗ ∗y →^{macro} λt.λs.λc. ∗ ∗Macro(t^{h} : : ExpandList(t^{t}, s, c))])^{p} [∗∗Macro(t) →^{val} Q̃(t, ⌈R(x∗_{f}y)⌉, (⌈x⌉ : : extractSeries(t^{1})) : : (⌈y⌉ : : extractSeries(t^{2})) : :

T)] (***) ([x + +y →^{macro} λt.λs.λc. + +Macro(t^{h} : : ExpandList(t^{t}, s, c))])^{p} [++Macro(t) →^{val} Q̃(t, ⌈R(x+_{f}y)⌉, (⌈x⌉ : : extractSeries(t^{1})) : : (⌈y⌉ : : extractSeries(t^{2})) : :

T)] (***) ([(− − x) →^{macro} λt.λs.λc. − −Macro(t^{h} : : ExpandList(t^{t}, s, c))])^{p} [− − Macro(t) →^{val} Q̃(t, ⌈R(−_{f}x)⌉, (⌈x⌉ : : extractSeries(t^{1})) : : T)] (****) ([x << y →^{macro} λt.λs.λc. << Macro(t^{h} : : ExpandList(t^{t}, s, c))])^{p} [<< Macro(t) →^{val} Q̃(t, ⌈x <_{f} y⌉, (⌈x⌉ : : extractSeries(t^{1})) : : (⌈y⌉ : : extractSeries(t^{2})) : :

T)] —–(3.12.06) [StateExpand(t, s, c) ˙= t!s!c!U^{M}(s^{h} ‘ t ‘ s ‘ c)] —–(5.12.06) [SystemQ lemma lemma eqLeq(R): ΠFX, FY: R(FX) = R(FY) ⊢ R(FX) <<==

R(FY)]

SystemQ proof of lemma eqLeq(R):

L01: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  R(FX) = R(FY)  ;

L03: WeakenOr1 ⊳ L02 ≫ R(FX) << R(FY) ˙∨ R(FX) = R(FY) ;

L04: Repetition ⊳ L03 ≫  R(FX) <<== R(FY)  □

—–(5.12.06)

[SystemQ lemma LessLeq(R): ΠFX, FY: R(FX) << R(FY) ⊢ R(FX) <<== R(FY)]

SystemQ proof of LessLeq(R):

L01: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  R(FX) << R(FY)  ;

L03: WeakenOr2 ⊳ L02 ≫ R(FX) << R(FY) ˙∨ R(FX) = R(FY) ;

L04: Repetition ⊳ L03 ≫ R(FX) <<== R(FY) □

——(7.12.06)

[SystemQ lemma MP2: ΠA, B, C: A ⇒ B ⇒ C ⊢ A ⊢ B ⊢ C]

SystemQ proof of MP2:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ⇒ B ⇒ C  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: MP ⊳ L02 ⊳ L03 ≫  B ⇒ C  ;
L06: MP ⊳ L05 ⊳ L04 ≫  C  □

[SystemQ lemma MP3: ΠA, B, C, D: A ⇒ B ⇒ C ⇒ D ⊢ A ⊢ B ⊢ C ⊢ D] SystemQ proof of MP3:

L01: Arbitrary ≫  A, B, C, D  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: MP2 ⊳ L02 ⊳ L03 ⊳ L04 ≫  C ⇒ D  ;
L07: MP ⊳ L06 ⊳ L05 ≫  D  □

[SystemQ lemma MP4: ΠA, B, C, D, E: A ⇒ B ⇒ C ⇒ D ⇒ E ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E]

SystemQ proof of MP4:

L01: Arbitrary ≫  A, B, C, D, E  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D ⇒ E  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: Premise ≫  D  ;
L07: MP2 ⊳ L02 ⊳ L03 ⊳ L04 ≫  C ⇒ D ⇒ E  ;
L08: MP2 ⊳ L07 ⊳ L05 ⊳ L06 ≫  E  □

[SystemQ lemma MP5: ΠA, B, C, D, E, F: A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E ⊢ F]

SystemQ proof of MP5:

L01: Arbitrary ≫  A, B, C, D, E, F  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;

L05: Premise ≫  C  ;
L06: Premise ≫  D  ;
L07: Premise ≫  E  ;
L08: MP3⊳L02⊳L03⊳L04⊳L05 ≫ D ⇒ E ⇒ F  ;
L09: MP2 ⊳ L08 ⊳ L06 ⊳ L07 ≫ F □

[SystemQ lemma AutoImply: ΠA: A ⇒ A]

SystemQ proof of AutoImply:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A  ;
L03: Premise ≫  A  ;
L04: Repetition ⊳ L03 ≫  A  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A  ;
L07: Ded ⊳ L05 ≫  A ⇒ A  □

[SystemQ lemma ImplyTransitivity: ΠA, B, C: A ⇒ B ⊢ B ⇒ C ⊢ A ⇒ C] SystemQ proof of ImplyTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  B ⇒ C  ;
L05: Premise ≫  A  ;
L06: MP ⊳ L03 ⊳ L05 ≫  B  ;
L07: MP ⊳ L04 ⊳ L06 ≫  C  ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  A, B, C  ;
L10: Premise ≫  A ⇒ B  ;
L11: Premise ≫  B ⇒ C  ;
L12: Ded ⊳ L08 ≫  (A ⇒ B) ⇒ (B ⇒ C) ⇒ A ⇒ C ;
L13: MP2 ⊳ L12 ⊳ L10 ⊳ L11 ≫ A ⇒ C □

[SystemQ lemma Weakening: ΠA, B: B ⊢ A ⇒ B]

SystemQ proof of Weakening:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  B  ;
L04: Premise ≫  A  ;
L05: Repetition ⊳ L03 ≫  B  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  B ⇒ A ⇒ B  ;
L09: Premise ≫  B  ;
L10: MP ⊳ L08 ⊳ L09 ≫  A ⇒ B  □

[SystemQ lemma FromContradiction: ΠA, B: A ⊢ ˙¬ (A)n ⊢ B] SystemQ proof of FromContradiction:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A  ;
L03: Premise ≫  ˙¬ (A)n  ;

L04: Weakening ⊳ L02 ≫  ˙¬ (B)n ⇒ A  ;
L05: Weakening ⊳ L03 ≫  ˙¬ (B)n ⇒ ˙¬ (A)n  ;
L06: Neg ⊳ L04 ⊳ L05 ≫  B  □

[SystemQ lemma RemoveDoubleNeg: ΠA: ˙¬ ( ˙¬ (A)n)n ⊢ A] SystemQ proof of RemoveDoubleNeg:

L01: Arbitrary ≫  A  ;
L02: Premise ≫  ˙¬ ( ˙¬ (A)n)n  ;
L03: Weakening ⊳ L02 ≫  ˙¬ (A)n ⇒ ˙¬ ( ˙¬ (A)n)n  ;
L04: AutoImply ≫  ˙¬ (A)n ⇒ ˙¬ (A)n  ;
L05: Neg ⊳ L04 ⊳ L03 ≫  A  □

[SystemQ lemma AddDoubleNeg: ΠA: A ⊢ ˙¬ ( ˙¬ (A)n)n] SystemQ proof of AddDoubleNeg:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A  ;
L03: Premise ≫  ˙¬ ( ˙¬ ( ˙¬ (A)n)n)n  ;
L04: RemoveDoubleNeg ⊳ L03 ≫  ˙¬ (A)n  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A  ;
L07: Ded ⊳ L05 ≫  ˙¬ ( ˙¬ ( ˙¬ (A)n)n)n ⇒ ˙¬ (A)n  ;
L08: Premise ≫  A  ;
L09: Weakening ⊳ L08 ≫  ˙¬ ( ˙¬ ( ˙¬ (A)n)n)n ⇒ A  ;
L10: Neg ⊳ L09 ⊳ L07 ≫  ˙¬ ( ˙¬ (A)n)n  □

——(10.12.06)

[SystemQ lemma Technicality: ΠA, B: A ⇒ B ⊢ ˙¬ ( ˙¬ (A)n)n ⇒ B] SystemQ proof of Technicality:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ˙¬ ( ˙¬ (A)n)n  ;
L05: RemoveDoubleNeg ⊳ L04 ≫  A  ;
L06: MP ⊳ L03 ⊳ L05 ≫  B  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  A, B  ;
L09: Ded ⊳ L07 ≫  (A ⇒ B) ⇒ ˙¬ ( ˙¬ (A)n)n ⇒ B  ;
L10: Premise ≫  A ⇒ B  ;
L11: MP ⊳ L09 ⊳ L10 ≫  ˙¬ ( ˙¬ (A)n)n ⇒ B  □

[SystemQ lemma NegativeMT: ΠA, B: ˙¬ (A)n ⇒ B ⊢ ˙¬ (B)n ⊢ A] SystemQ proof of NegativeMT:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  ˙¬ (A)n ⇒ B  ;
L03: Premise ≫  ˙¬ (B)n  ;
L04: Weakening ⊳ L03 ≫  ˙¬ (A)n ⇒ ˙¬ (B)n  ;
L05: Neg ⊳ L02 ⊳ L04 ≫  A  □

[SystemQ lemma MT: ΠA, B: A ⇒ B ⊢ ˙¬ (B)n ⊢ ˙¬ (A)n] SystemQ proof of MT:

L01: Arbitrary ≫  A, B  ;

L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ˙¬ (B)n  ;
L04: Technicality ≫  ˙¬ ( ˙¬ (A)n)n ⇒ B  ;
L05: NegativeMT ⊳ L04 ⊳ L03 ≫  ˙¬ (A)n  □

[SystemQ lemma Contrapositive: ΠA, B: A ⇒ B ⊢ ˙¬ (B)n ⇒ ˙¬ (A)n] SystemQ proof of Contrapositive:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ˙¬ (B)n  ;
L05: MT ⊳ L03 ⊳ L04 ≫  ˙¬ (A)n  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Premise ≫  A ⇒ B  ;
L09: Ded ⊳ L06 ≫  (A ⇒ B) ⇒ ˙¬ (B)n ⇒ ˙¬ (A)n  ;
L10: MP ⊳ L09 ⊳ L08 ≫  ˙¬ (B)n ⇒ ˙¬ (A)n  □

[SystemQ lemma JoinConjuncts: ΠA, B: A ⊢ B ⊢ A ˙∧ B]

SystemQ proof of JoinConjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  A ⇒ ˙¬ (B)n  ;
L05: MP ⊳ L04 ⊳ L03 ≫  ˙¬ (B)n  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  A ⇒ (A ⇒ ˙¬ (B)n) ⇒ ˙¬ (B)n  ;
L09: Premise ≫  A  ;
L10: Premise ≫  B  ;
L11: MP ⊳ L08 ⊳ L09 ≫  (A ⇒ ˙¬ (B)n) ⇒ ˙¬ (B)n  ;
L12: AddDoubleNeg ⊳ L10 ≫  ˙¬ ( ˙¬ (B)n)n  ;
L13: MT ⊳ L11 ⊳ L12 ≫  ˙¬ ((A ⇒ ˙¬ (B)n))n  ;
L14: Repetition ⊳ L13 ≫  A ˙∧ B  □

[SystemQ lemma SecondConjunct: ΠA, B: A ˙∧ B ⊢ B]

SystemQ proof of SecondConjunct:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  ˙¬ (B)n  ;
L04: Weakening ⊳ L03 ≫  A ⇒ ˙¬ (B)n  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A, B  ;
L07: Ded ⊳ L05 ≫  ˙¬ (B)n ⇒ A ⇒ ˙¬ (B)n  ;
L08: Premise ≫  A ˙∧ B  ;
L09: Repetition ⊳ L08 ≫  ˙¬ ((A ⇒ ˙¬ (B)n))n  ;
L10: NegativeMT ⊳ L07 ⊳ L09 ≫  B  □

——(10.12.06)

[SystemQ lemma AndCommutativity: ΠA, B: A ˙∧ B ⊢ B ˙∧ A]

SystemQ proof of AndCommutativity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  B ⇒ ˙¬ (A)n  ;
L04: Premise ≫  A  ;
L05: AddDoubleNeg ⊳ L04 ≫  ˙¬ ( ˙¬ (A)n)n  ;
L06: MT ⊳ L03 ⊳ L05 ≫  ˙¬ (B)n  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  A, B  ;
L09: Ded ⊳ L07 ≫  (B ⇒ ˙¬ (A)n) ⇒ A ⇒ ˙¬ (B)n  ;
L10: Premise ≫  A ˙∧ B  ;
L11: Repetition ≫  ˙¬ ((A ⇒ ˙¬ (B)n))n  ;
L12: MT ⊳ L09 ⊳ L11 ≫  ˙¬ ((B ⇒ ˙¬ (A)n))n  ;
L13: Repetition ⊳ L12 ≫  B ˙∧ A  □

[SystemQ lemma FirstConjunct: ΠA, B: A ˙∧ B ⊢ A]

SystemQ proof of FirstConjunct:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙∧ B  ;
L03: AndCommutativity ⊳ L02 ≫  B ˙∧ A  ;
L04: SecondConjunct ⊳ L03 ≫  A  □

[SystemQ lemma IffFirst: ΠA, B: A ˙⇔ B ⊢ B ⊢ A]

SystemQ proof of IffFirst:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Premise ≫  B  ;
L04: SecondConjunct ⊳ L02 ≫  B ⇒ A  ;
L05: MP ⊳ L04 ⊳ L03 ≫  A  □

[SystemQ lemma IffSecond: ΠA, B: A ˙⇔ B ⊢ A ⊢ B] SystemQ proof of IffSecond:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Premise ≫  A  ;
L04: FirstConjunct ⊳ L02 ≫  A ⇒ B  ;
L05: MP ⊳ L04 ⊳ L03 ≫  B  □

[SystemQ lemma IffCommutativity: ΠA, B: A ˙⇔ B ⊢ B ˙⇔ A] SystemQ proof of IffCommutativity:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Repetition ⊳ L02 ≫  (A ⇒ B) ˙∧ (B ⇒ A)  ;
L04: AndCommutativity ⊳ L03 ≫  (B ⇒ A) ˙∧ (A ⇒ B)  ;
L05: Repetition ⊳ L04 ≫  B ˙⇔ A  □

—-(10.12.06)

[SystemQ lemma WeakenOr1: ΠA, B: B ⊢ A ˙∨ B]

SystemQ proof of WeakenOr1:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  B  ;

L03: Weakening ⊳ L02 ≫  ˙¬ (A)n ⇒ B  ;
L04: Repetition ⊳ L03 ≫  A ˙∨ B  □

[SystemQ lemma WeakenOr2: ΠA, B: A ⊢ A ˙∨ B]

SystemQ proof of WeakenOr2:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  ˙¬ (A)n  ;

L05: FromContradiction ⊳ L03 ⊳

L04 ≫ B ;

L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  A ⇒ ˙¬ (A)n ⇒ B  ;
L09: Premise ≫  A  ;
L10: MP ⊳ L08 ⊳ L09 ≫  ˙¬ (A)n ⇒ B  ;
L11: Repetition ⊳ L10 ≫  A ˙∨ B  □

[SystemQ lemma FromDisjuncts: ΠA, B, C: A ˙∨ B ⊢ A ⇒ C ⊢ B ⇒ C ⊢ C] SystemQ proof of FromDisjuncts:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ˙∨ B  ;
L03: Premise ≫  A ⇒ C  ;
L04: Premise ≫  B ⇒ C  ;
L05: Repetition ⊳ L02 ≫  ˙¬ (A)n ⇒ B  ;
L06: Contrapositive ⊳ L05 ≫  ˙¬ (B)n ⇒ ˙¬ ( ˙¬ (A)n)n  ;
L07: Technicality ⊳ L03 ≫  ˙¬ ( ˙¬ (A)n)n ⇒ C  ;
L08: ImplyTransitivity⊳L06⊳L07 ≫ ˙¬ (B)n ⇒ C  ;
L09: Contrapositive ⊳ L08 ≫  ˙¬ (C)n ⇒ ˙¬ ( ˙¬ (B)n)n  ;
L10: Contrapositive ⊳ L04 ≫  ˙¬ (C)n ⇒ ˙¬ (B)n  ;
L11: Neg ⊳ L10 ⊳ L09 ≫  C  □

[SystemQ rule NumericalF: ΠFX: (0f ≤_{f} FX ⇒ |fFX| = FX) ˙∧ ( ˙¬ (0f ≤_{f} FX)n ⇒ |fFX| = −_{f}FX)]

([|rx| →^{macro} λt.λs.λc.||Macro(t^{h} : : ExpandList(t^{t}, s, c))])^{p}

[||Macro(t) →^{val} Q̃(t, ⌈R(|fx|)⌉, (⌈x⌉ : : extractSeries(t^{1})) : : T)]

—–(11.12.06)

[SystemQ rule (Adgic)SameR: ΠFX, FY: FX = FY ⊢ R(FX) = R(FY)] ——-(11.12.06) ([01//tempx →^{macro} λt.λs.λc.01//Macro(t^{h} : : ExpandList(t^{t}, s, c))])^{p} [01//Macro(t) →^{val} Q̃(t, ⌈R(1f/x)⌉, (⌈x⌉ : : extractSeries(t^{1})) : : T)] venter——-

Priority table 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] ∗], [∗\\∗]; End table

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”] )^{p}

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”]

70