SUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUP [SystemQ lemma ToNegatedDoubleImply: ΠA, B, C: A ⊢ B ⊢ ˙¬ (C)n ⊢ ˙¬ ((A ⇒

B ⇒ C))n]

SystemQ proof of ToNegatedDoubleImply:

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

L08: FromContradiction ⊳ L07 ⊳

L05 ≫ ˙¬ ((A ⇒ B ⇒ C))n ;

L09: Block ≫  End  ;
L10: Arbitrary ≫  A, B, C  ;
L03: Ded ⊳ L09 ≫  {A ⇒ B ⇒ ˙¬ (C)n ⇒ (A ⇒ B ⇒ \atop C) ⇒ ˙¬ ((A ⇒ B ⇒ C))n  ;}
L04: Premise ≫  A  ;
L05: Premise ≫  B  ;
L06: Premise ≫  ˙¬ (C)n  ;
L07: MP3⊳L03⊳L04⊳L05⊳L06 ≫ {(A ⇒ B ⇒ C) ⇒ ˙¬ ((A ⇒ B ⇒ \atop C))n  ;}

L11: prop lemma imply negation ⊳

L07 ≫ ˙¬ ((A ⇒ B ⇒ C))n □

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

SystemQ proof of FromNegatedAnd(Imply):

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

L05: FromNegatedAnd ⊳ L03 ⊳

L04 ≫ ˙¬ (B)n ;

L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  ˙¬ ((A ˙∧ B))n ⇒ A ⇒ ˙¬ (B)n  □

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

SystemQ proof of RemoveDoubleNeg(Consequent):

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)n  ;
L09: MP ⊳ L03 ⊳ L04 ≫  A ⇒ B  □

[SystemQ lemma (A)to( E )(Imply): ΠV_{1}, A: ∀V_{1}: A ⇒ ˙¬ (∃V_{1}: ˙¬ (A)n)n] SystemQ proof of (A)to( E )(Imply):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  V_{1}, A  ;
L03: Premise ≫  ∀V_{1}: A  ;
L04: A4 @ V_{1} ⊳ L03 ≫  A  ;
L05: AddDoubleNeg ⊳ L04 ≫  ˙¬ ( ˙¬ (A)n)n  ;
L06: Gen ⊳ L05 ≫  ∀V_{1}: ˙¬ ( ˙¬ (A)n)n  ;
L07: AddDoubleNeg ⊳ L06 ≫  ˙¬ ( ˙¬ (∀V_{1}: ˙¬ ( ˙¬ (A)n)n)n)n  ;
L08: Repetition ⊳ L07 ≫  ˙¬ (∃V_{1}: ˙¬ (A)n)n  ;
L09: Block ≫  End  ;
L10: Arbitrary ≫  V_{1}, A  ;
L11: Ded ⊳ L09 ≫  ∀V_{1}: A ⇒ ˙¬ (∃V_{1}: ˙¬ (A)n)n  □

[SystemQ lemma (E)to( A )(Imply): ΠV_{1}, A: ∃V_{1}: A ⇒ ˙¬ (∀V_{1}: ˙¬ (A)n)n] SystemQ proof of (E)to( A )(Imply):

L01: Arbitrary ≫  V_{1}, A  ;
L02: AutoImply ≫  {˙¬ (∀V_{1}: ˙¬ (A)n)n  ⇒ \atop ˙¬ (∀V_{1}: ˙¬ (A)n)n  ;}
L03: Repetition ⊳ L02 ≫  ∃V_{1}: A ⇒ ˙¬ (∀V_{1}: ˙¬ (A)n)n  □

[SystemQ lemma (E )to( A)(Imply): ΠV_{1}, A: ∃V_{1}: ˙¬ (A)n ⇒ ˙¬ (∀V_{1}: A)n] SystemQ proof of (E )to( A)(Imply):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  V_{1}, A  ;
L03: Premise ≫  ∃V_{1}: ˙¬ (A)n  ;
L04: AddDoubleNeg ⊳ L03 ≫  ˙¬ ( ˙¬ (∃V_{1}: ˙¬ (A)n)n)n  ;
L05: (A)to( E )(Imply) ≫  ∀V_{1}: A ⇒ ˙¬ (∃V_{1}: ˙¬ (A)n)n  ;
L06: MT ⊳ L05 ⊳ L04 ≫  ˙¬ (∀V_{1}: A)n  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  V_{1}, A  ;
L09: Ded ⊳ L07 ≫  ∃V_{1}: ˙¬ (A)n ⇒ ˙¬ (∀V_{1}: A)n  □

[SystemQ lemma AddNegatedAll: ΠV_{1}, A, B: B ⇒ A ⊢ ˙¬ (∀V_{1}: A)n ⇒ ˙¬ (∀V_{1}: B)n] SystemQ proof of AddNegatedAll:

L01: Arbitrary ≫  V_{1}, A, B  ;
L02: Premise ≫  B ⇒ A  ;
L03: AddAll ⊳ L02 ≫  ∀V_{1}: B ⇒ ∀V_{1}: A  ;
L04: Contrapositive ⊳ L03 ≫  ˙¬ (∀V_{1}: A)n ⇒ ˙¬ (∀V_{1}: B)n  □

[SystemQ lemma ToNegatedAEA: ΠV_{1}, V_{2}, V_{3}, A: ∃V_{1}: ∀V_{2}: ∃V_{3}: ˙¬ (A)n ⊢ ˙¬ (∀V_{1}: ∃V_{2}: ∀V_{3}: A)n]

SystemQ proof of ToNegatedAEA:

L01: Arbitrary ≫  V_{1}, V_{2}, V_{3}, A  ;
L02: Premise ≫  ∃V_{1}: ∀V_{2}: ∃V_{3}: ˙¬ (A)n  ;
L03: (E )to( A)(Imply) ≫  ∃V_{3}: ˙¬ (A)n ⇒ ˙¬ (∀V_{3}: A)n  ;

L04: AddNegatedAll ⊳ L03 ≫

˙¬ (∀V_{2}: ˙¬ (∀V_{3}: A)n)n ⇒
˙¬ (∀V_{2}: ∃V_{3}: ˙¬ (A)n)n ;
L05: (E)to( A )(Imply) ≫  {∃V_{2}: ∀V_{3}: A  ⇒ \atop ˙¬ (∀V_{2}: ˙¬ (∀V_{3}: A)n)n  ;}

L06: ImplyTransitivity⊳L05⊳L04 ≫ {∃V_{2}: ∀V_{3}: A  ⇒ \atop ˙¬ (∀V_{2}: ∃V_{3}: ˙¬ (A)n)n  ;}

L07: AddNegatedAll ⊳ L06 ≫

˙¬ (∀V_{1}: ˙¬ (∀V_{2}: ∃V_{3}: ˙¬ (A)n)n)n ⇒
˙¬ (∀V_{1}: ∃V_{2}: ∀V_{3}: A)n ;

L08: (E)to( A )(Imply) ≫ ∃V_{1}: ∀V_{2}: ∃V_{3}: ˙¬ (A)n ⇒ ˙¬ (∀V_{1}: ˙¬ (∀V_{2}: ∃V_{3}: ˙¬ (A)n)n)n

;

L09: ImplyTransitivity⊳L08⊳L07 ≫

∃V_{1}: ∀V_{2}: ∃V_{3}: ˙¬ (A)n ⇒

˙¬ (∀V_{1}: ∃V_{2}: ∀V_{3}: A)n ;

L10: MP ⊳ L09 ⊳ L02 ≫ ˙¬ (∀V_{1}: ∃V_{2}: ∀V_{3}: A)n □

[SystemQ lemma (A )to( E): ΠV_{1}, A: ∀V_{1}: ˙¬ (A)n ⊢ ˙¬ (∃V_{1}: A)n] SystemQ proof of (A )to( E):

L01: Arbitrary ≫  V_{1}, A  ;
L02: Premise ≫  ∀V_{1}: ˙¬ (A)n  ;
L03: AddDoubleNeg ⊳ L02 ≫  ˙¬ ( ˙¬ (∀V_{1}: ˙¬ (A)n)n)n  ;
L04: Repetition ⊳ L03 ≫  ˙¬ (∃V_{1}: A)n  □

[SystemQ lemma ExistMP3: ΠV_{1}, V_{2}, V_{3}, A, B, C, D: A ⇒ B ⇒ C ⇒ D ⊢ ∃V_{1}: A ⊢ ∃V_{2}: B ⊢ ∃V_{3}: C ⊢ D]

SystemQ proof of ExistMP3:

L01: Arbitrary ≫  V_{1}, V_{2}, V_{3}, A, B, C, D  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D  ;
L03: Premise ≫  ∃V_{1}: A  ;
L04: Premise ≫  ∃V_{2}: B  ;
L05: Premise ≫  ∃V_{3}: C  ;
L06: ExistMP2⊳L02⊳L03⊳L04 ≫ C ⇒ D  ;
L07: ExistMP ⊳ L06 ⊳ L05 ≫ D □

[SystemQ lemma PositiveToLeft(Eq): ΠX , Y, Z: X = (Y + Z) ⊢ (X − Z) = Y]

SystemQ proof of PositiveToLeft(Eq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = (Y + Z)  ;
L03: eqAddition ⊳ L02 ≫  (X − Z) = ((Y + Z) − Z)  ;
L04: x = x + y − y ≫  Y = ((Y + Z) − Z)  ;
L05: eqSymmetry ⊳ L04 ≫  ((Y + Z) − Z) = Y  ;
L06: eqTransitivity ⊳ L03 ⊳ L05 ≫ (X − Z) = Y  □

——–

[SystemQ lemma ExpZero(Exact): ΠX: X (exp)0 = 1]

SystemQ proof of ExpZero(Exact):

L01: Arbitrary ≫  X  ;
L02: eqReflexivity ≫  0 = 0  ;

L03: ExpZero ⊳ L02 ≫  X (exp)0 = 1  □

[SystemQ lemma (+1)IsPositive(N): ΠM: Nat(M) ⊢⊢ 0 < (M + 1)]

SystemQ proof of (+1)IsPositive(N):

L01: Arbitrary ≫  M  ;
L02: Side-condition ≫  Nat(M)  ;
L03: Nonnegative(N) ⊳ ⊳ L02 ≫  0 <= M  ;
L04: Leq + 1 ⊳ L03 ≫  0 < (M + 1)  □

[SystemQ lemma SameExp(Base): ΠN , X: ∀N: (0 = N ⇒ X (exp)0 = X (exp)N)] SystemQ proof of SameExp(Base):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  N , X  ;
L03: Premise ≫  0 = N  ;
L04: ExpZero(Exact) ≫  X (exp)0 = 1  ;
L05: eqSymmetry ⊳ L03 ≫  N = 0  ;
L06: ExpZero ⊳ L05 ≫  X (exp)N = 1  ;
L07: eqSymmetry ⊳ L06 ≫  1 = X (exp)N  ;
L08: eqTransitivity ⊳ L04 ⊳ L07 ≫ X (exp)0 = X (exp)N  ;
L09: Block ≫  End  ;
L10: Arbitrary ≫  N , X  ;
L03: Ded ⊳ L09 ≫  0 = N ⇒ X (exp)0 = X (exp)N ;
L11: Gen ⊳ L03 ≫  {∀N: (0 = N ⇒ X (exp)0 = \atop X (exp)N)  □}

[SystemQ lemma SameExp(Indu): ΠM, N , X: ∀N: (M = N ⇒ X (exp)M = X (exp)N) ⇒ ∀N: ((M + 1) = N ⇒ X (exp)((M + 1)) = X (exp)N)]

SystemQ proof of SameExp(Indu):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N , X  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  M, N , X  ;
L05: Premise ≫  {∀N: (M = N ⇒ X (exp)M = \atop X (exp)N)  ;}
L06: Premise ≫  (M + 1) = N  ;
L07: (+1)IsPositive(N) ≫  0 < (M + 1)  ;
L08: ExpPositive ⊳ L07 ≫  {X (exp)((M + 1)) = (X ∗ \atop X (exp)(((M + 1) − 1)))  ;}
L09: x = x + y − y ≫  M = ((M + 1) − 1)  ;
L10: A4 @((M + 1) − 1) ⊳ L05 ≫  M = ((M + 1) − 1) ⇒ ; X (exp)M = X (exp)(((M+1)− ; 1))  ;

L11: MP ⊳ L10 ⊳ L09 ≫  {X (exp)M = X (exp)(((M+1)− \atop 1))  ;}
L12: eqSymmetry ⊳ L11 ≫  {X (exp)(((M + 1) − 1)) = \atop X (exp)M  ;}
L13: EqMultiplicationLeft ⊳ L12 ≫ {(X ∗ X (exp)(((M + 1) − 1))) = \atop (X ∗ X (exp)M)  ;}

L14: A4 @(N − 1) ⊳ L05 ≫  {M = (N − 1) ⇒ X (exp)M = \atop X (exp)((N − 1))  ;}
L15: PositiveToRight(Eq) ⊳ L06 ≫ M = (N − 1)  ;
L16: MP ⊳ L14 ⊳ L15 ≫  X (exp)M = X (exp)((N − 1)) ;
L17: EqMultiplicationLeft ⊳ L16 ≫ {(X ∗ X (exp)M) = (X ∗ \atop X (exp)((N − 1)))  ;}
L18: SubLessRight ⊳ L06 ⊳ L07 ≫ 0 < N  ;
L19: ExpPositive ⊳ L18 ≫  {X (exp)N = (X ∗ X (exp)((N − \atop 1)))  ;}
L20: eqSymmetry ⊳ L19 ≫  {(X ∗ X (exp)((N − 1))) = \atop X (exp)N  ;}

L21: eqTransitivity5 ⊳ L08 ⊳ L13 ⊳ L17 ⊳ L20 ≫

X (exp)((M + 1)) = X (exp)N ;
L22: Block ≫ End ;

L05: Ded ⊳ L22 ≫

∀N: (M = N ⇒ X (exp)M =
X (exp)N) ⇒ (M + 1) = N ⇒
X (exp)((M + 1)) = X (exp)N ;
L06: Premise ≫  {∀N: (M = N ⇒ X (exp)M = \atop X (exp)N)  ;}
L07: MP ⊳ L05 ⊳ L06 ≫  {(M + 1) = N ⇒ X (exp)((M + \atop 1)) = X (exp)N  ;}
L23: Gen ⊳ L07 ≫  {∀N: ((M + 1) = N ⇒ \atop X (exp)((M + 1)) = X (exp)N) ;}
L24: Block ≫  End  ;
L25: Arbitrary ≫  M, N , X  ;

L26: Ded ⊳ L24 ≫

∀N: (M = N ⇒ X (exp)M =
X (exp)N) ⇒ ∀N: ((M + 1) =
N ⇒ X (exp)((M + 1)) =
X (exp)N) □

[SystemQ lemma SameExp: ΠM, N , X: M = N ⊢ X (exp)M = X (exp)N] SystemQ proof of SameExp:

L01: Arbitrary ≫  M, N , X  ;
L02: Premise ≫  M = N  ;
L03: SameExp(Base) ≫  {∀N: (0 = N ⇒ X (exp)0 = \atop X (exp)N)  ;}

L04: SameExp(Indu) ≫

∀N: (M = N ⇒ X (exp)M =
X (exp)N) ⇒ ∀N: ((M + 1) =
N ⇒ X (exp)((M + 1)) =
X (exp)N) ;
L05: Induction ⊳ L03 ⊳ L04 ≫  {∀N: (M = N ⇒ X (exp)M = \atop X (exp)N)  ;}
L06: A4 @ N ⊳ L05 ≫  {M = N ⇒ X (exp)M = \atop X (exp)N  ;}
L07: MP ⊳ L06 ⊳ L02 ≫  X (exp)M = X (exp)N  □

————

[SystemQ lemma Exp(+1): ΠM, X: X (exp)((M + 1)) = (X ∗ X (exp)M)] SystemQ proof of Exp(+1):

L01: Arbitrary ≫  M, X  ;
L02: (+1)IsPositive(N) ≫  0 < (M + 1)  ;
L03: ExpPositive ⊳ L02 ≫  {X (exp)((M + 1)) = (X ∗ \atop X (exp)(((M + 1) − 1)))  ;}
L04: x = x + y − y ≫  M = ((M + 1) − 1)  ;
L05: SameExp ⊳ L04 ≫  {X (exp)M = X (exp)(((M+1)− \atop 1))  ;}
L06: EqMultiplicationLeft ⊳ L05 ≫ {(X ∗ X (exp)M) = (X ∗ \atop X (exp)(((M + 1) − 1)))  ;}
L07: eqSymmetry ⊳ L06 ≫  {(X ∗ X (exp)(((M + 1) − 1))) = \atop (X ∗ X (exp)M)  ;}
L08: eqTransitivity ⊳ L03 ⊳ L07 ≫ {X (exp)((M + 1)) = (X ∗ \atop X (exp)M)  □}

[SystemQ lemma DistributionOut(Minus): ΠX , Y, Z: ((X ∗ Y) − (X ∗ Z)) = (X ∗ ((Y − Z)))]

SystemQ proof of DistributionOut(Minus):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Times(−1)Left ≫  {((−1) ∗ ((X ∗ Z))) = (−u((X ∗ \atop Z)))  ;}
L03: eqSymmetry ⊳ L02 ≫  {(−u((X ∗ Z))) = ((−1) ∗ ((X ∗ \atop Z)))  ;}
L04: timesCommutativity ≫  {((−1) ∗ ((X ∗ Z))) = ((X ∗ Z) ∗ \atop (−1))  ;}
L05: timesAssociativity ≫  {((X ∗ Z) ∗ (−1)) = (X ∗ ((Z ∗ \atop (−1))))  ;}
L06: Times(−1) ≫  (Z ∗ (−1)) = (−uZ)  ;
L07: EqMultiplicationLeft ⊳ L06 ≫ {(X ∗ ((Z ∗ (−1)))) = (X ∗ \atop ((−uZ)))  ;}

L08: eqTransitivity5 ⊳ L03 ⊳ L04 ⊳

L05 ⊳ L07 ≫ (−u((X ∗ Z))) = (X ∗ ((−uZ))) ;

L09: EqAdditionLeft ⊳ L08 ≫  {((X ∗Y)−(X ∗Z)) = ((X ∗Y)+ \atop (X ∗ ((−uZ))))  ;}
L10: DistributionOut ≫  {((X ∗Y)+(X ∗((−uZ)))) = (X ∗ \atop ((Y − Z)))  ;}
L11: eqTransitivity ⊳ L09 ⊳ L10 ≫ {((X ∗Y)−(X ∗Z)) = (X ∗((Y − \atop Z)))  □}

[SystemQ lemma (1/2)(x+y)−x = (1/2)(y−x): ΠX , Y: ((1/2∗((X +Y)))− X) = (1/2 ∗ ((Y − X)))]

SystemQ proof of (1/2)(x + y) − x = (1/2)(y − x):

L01: Arbitrary ≫  X , Y  ;
L02: Distribution ≫  {(1/2 ∗ ((X + Y))) = ((1/2 ∗ X) + \atop (1/2 ∗ Y))  ;}
L03: eqAddition ⊳ L02 ≫  {((1/2∗((X +Y)))−X) = (((1/2∗ \atop X) + (1/2 ∗ Y)) − X)  ;}
L04: plusCommutativity ≫  {((1/2 ∗ X) + (1/2 ∗ Y)) = ((1/2 ∗ \atop Y) + (1/2 ∗ X))  ;}

L05: eqAddition ⊳ L04 ≫  {(((1/2 ∗ X) + (1/2 ∗ Y)) − X) = \atop (((1/2 ∗ Y) + (1/2 ∗ X)) − X) ;}
L06: plusAssociativity ≫  {(((1/2 ∗ Y) + (1/2 ∗ X)) − X) = \atop ((1/2 ∗ Y) + (((1/2 ∗ X) − X))) ;}
L07: TwoHalves ≫  ((1/2 ∗ X) + (1/2 ∗ X)) = X  ;
L08: PositiveToRight(Eq) ⊳ L07 ≫ (1/2 ∗ X) = (X − (1/2 ∗ X))  ;
L09: EqNegated ⊳ L08 ≫  {(−u((1/2 ∗ X))) = (−u((X − \atop (1/2 ∗ X))))  ;}
L10: MinusNegated ≫  {(−u((X − (1/2 ∗ X)))) = ((1/2 ∗ \atop X) − X)  ;}
L11: eqTransitivity ⊳ L09 ⊳ L10 ≫ {(−u((1/2 ∗ X))) = ((1/2 ∗ X) − \atop X)  ;}
L12: eqSymmetry ⊳ L11 ≫  {((1/2 ∗ X) − X) = (−u((1/2 ∗ \atop X)))  ;}
L13: EqAdditionLeft ⊳ L12 ≫  {((1/2∗Y)+(((1/2∗X)−X))) = \atop ((1/2 ∗ Y) − (1/2 ∗ X))  ;}
L14: DistributionOut(Minus) ≫  {((1/2 ∗ Y) − (1/2 ∗ X)) = (1/2 ∗ \atop ((Y − X)))  ;}

L15: eqTransitivity6 ⊳ L03 ⊳ L05 ⊳

L06 ⊳ L13 ⊳ L14 ≫ ((1/2 ∗ ((X + Y))) − X) = (1/2 ∗ ((Y − X))) □

[SystemQ lemma y − (1/2)(x + y) = (1/2)(y − x): ΠX , Y: (Y − (1/2 ∗ ((X + Y)))) = (1/2 ∗ ((Y − X)))]

SystemQ proof of y − (1/2)(x + y) = (1/2)(y − x):

L01: Arbitrary ≫  X , Y  ;
L02: Distribution ≫  {(1/2 ∗ ((X + Y))) = ((1/2 ∗ X) + \atop (1/2 ∗ Y))  ;}
L03: EqNegated ⊳ L02 ≫  {(−u((1/2 ∗ ((X + Y))))) = \atop (−u(((1/2 ∗ X) + (1/2 ∗ Y)))) ;}
L04: EqAdditionLeft ⊳ L03 ≫  {(Y − (1/2 ∗ ((X + Y)))) = (Y − \atop (((1/2 ∗ X) + (1/2 ∗ Y))))  ;}
L05: plusCommutativity ≫  {((1/2 ∗ X) + (1/2 ∗ Y)) = ((1/2 ∗ \atop Y) + (1/2 ∗ X))  ;}
L06: EqNegated ⊳ L05 ≫  {(−u(((1/2 ∗ X) + (1/2 ∗ Y)))) = \atop (−u(((1/2 ∗ Y) + (1/2 ∗ X)))) ;}
L07: −x − y = −(x + y) ≫  {((−u((1/2 ∗ Y))) − (1/2 ∗ X)) = \atop (−u(((1/2 ∗ Y) + (1/2 ∗ X)))) ;}
L08: eqSymmetry ⊳ L07 ≫  {(−u(((1/2 ∗ Y) + (1/2 ∗ X)))) = \atop ((−u((1/2 ∗ Y))) − (1/2 ∗ X)) ;}
L09: eqTransitivity ⊳ L06 ⊳ L08 ≫ {(−u(((1/2 ∗ X) + (1/2 ∗ Y)))) = \atop ((−u((1/2 ∗ Y))) − (1/2 ∗ X)) ;}
L10: EqAdditionLeft ⊳ L09 ≫  (Y −(((1/2∗X)+(1/2∗Y)))) = ; (Y + (((−u((1/2 ∗ Y))) − (1/2 ∗ ; X))))  ;

L11: plusAssociativity ≫  ((Y − (1/2 ∗ Y)) − (1/2 ∗ X)) = ; (Y + (((−u((1/2 ∗ Y))) − (1/2 ∗ ; X))))  ;

L12: eqSymmetry ⊳ L11 ≫  (Y + (((−u((1/2 ∗ Y))) − (1/2 ∗ ; X)))) = ((Y −(1/2∗Y))−(1/2∗ ; X))  ;

L13: TwoHalves ≫  ((1/2 ∗ Y) + (1/2 ∗ Y)) = Y  ;
L14: PositiveToRight(Eq) ⊳ L13 ≫ (1/2 ∗ Y) = (Y − (1/2 ∗ Y))  ;
L15: eqSymmetry ⊳ L14 ≫  (Y − (1/2 ∗ Y)) = (1/2 ∗ Y)  ;
L16: eqAddition ⊳ L15 ≫  {((Y − (1/2 ∗ Y)) − (1/2 ∗ X)) = \atop ((1/2 ∗ Y) − (1/2 ∗ X))  ;}
L17: DistributionOut(Minus) ≫  {((1/2 ∗ Y) − (1/2 ∗ X)) = (1/2 ∗ \atop ((Y − X)))  ;}

L18: eqTransitivity6 ⊳ L04 ⊳ L10 ⊳

L12 ⊳ L16 ⊳ L17 ≫ (Y − (1/2 ∗ ((X + Y)))) = (1/2 ∗ ((Y − X))) □

————–

[SystemQ lemma PositiveBase(Base): ΠX: 0 < X (exp)0]

SystemQ proof of PositiveBase(Base):

L01: Arbitrary ≫  X  ;
L02: ExpZero(Exact) ≫  X (exp)0 = 1  ;
L03: eqSymmetry ⊳ L02 ≫  1 = X (exp)0  ;
L04: 0 < 1 ≫  0 < 1  ;
L05: SubLessRight ⊳ L03 ⊳ L04 ≫ 0 < X (exp)0  □

[SystemQ lemma PositiveBase(Indu): ΠM, X: 0 < X ⊢ 0 < X (exp)M ⇒ 0 < X (exp)((M + 1))]

SystemQ proof of PositiveBase(Indu):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, X  ;
L03: Premise ≫  0 < X  ;
L04: Premise ≫  0 < X (exp)M  ;
L05: Exp(+1) ≫  {X (exp)((M + 1)) = (X ∗ \atop X (exp)M)  ;}
L06: eqSymmetry ⊳ L05 ≫  {(X ∗X (exp)M) = X (exp)((M+ \atop 1))  ;}
L07: PositiveFactors ⊳ L03 ⊳ L04 ≫ 0 < (X ∗ X (exp)M)  ;
L08: SubLessRight ⊳ L06 ⊳ L07 ≫ 0 < X (exp)((M + 1))  ;
L09: Block ≫  End  ;
L10: Arbitrary ≫  M, X  ;
L03: Ded ⊳ L09 ≫  {0 < X ⇒ 0 < X (exp)M ⇒ 0 < \atop X (exp)((M + 1))  ;}
L04: Premise ≫  0 < X  ;
L11: MP ⊳ L03 ⊳ L04 ≫  {0 < X (exp)M ⇒ 0 < \atop X (exp)((M + 1))  □}

[SystemQ lemma PositiveBase: ΠM, X: 0 < X ⊢ 0 < X (exp)M] SystemQ proof of PositiveBase:

L01: Arbitrary ≫  M, X  ;
L02: Premise ≫  0 < X  ;
L03: PositiveBase(Base) ≫  0 < X (exp)0  ;

L04: PositiveBase(Indu) ⊳ L02 ≫  {0 < X (exp)M ⇒ 0 < \atop X (exp)((M + 1))  ;}
L05: Induction ⊳ L03 ⊳ L04 ≫  0 < X (exp)M  □

[SystemQ lemma PositiveToRight(Eq)(1term): ΠX , Y: X = Y ⊢ 0 = (Y − X)]

SystemQ proof of PositiveToRight(Eq)(1term):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: eqSymmetry ⊳ L02 ≫  Y = X  ;

L04: PositiveToLeft(Eq)(1term) ⊳

L03 ≫ (Y − X) = 0 ;

L05: eqSymmetry ⊳ L04 ≫ 0 = (Y − X) □

———

[SystemQ lemma BSzero(Exact): ΠM: BS(M, 0) = 1/2(exp)M]

SystemQ proof of BSzero(Exact):

L01: Arbitrary ≫  M  ;
L02: eqReflexivity ≫  0 = 0  ;
L03: BSzero ⊳ L02 ≫  BS(M, 0) = 1/2(exp)M  □

[SystemQ lemma SameBS(2)(Base): ΠM, N_{2}: ∀N_{2}: (0 = N_{2} ⇒ BS(M, 0) = BS(M, N_{2}))]

SystemQ proof of SameBS(2)(Base):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N_{2}  ;
L03: Premise ≫  0 = N_{2}  ;
L04: eqSymmetry ⊳ L03 ≫  N_{2} = 0  ;
L05: BSzero ⊳ L04 ≫  BS(M, N_{2}) = 1/2(exp)(M)  ;
L06: eqSymmetry ⊳ L05 ≫  1/2(exp)(M) = BS(M, N_{2})  ;
L07: BSzero(Exact) ≫  BS(M, 0) = 1/2(exp)(M)  ;
L08: eqTransitivity ⊳ L07 ⊳ L06 ≫ BS(M, 0) = BS(M, N_{2})  ;
L09: Block ≫  End  ;
L10: Arbitrary ≫  M, N_{2}  ;
L03: Ded ⊳ L09 ≫  {0 = N_{2} ⇒ BS(M, 0) = \atop BS(M, N_{2})  ;}
L11: Gen ⊳ L03 ≫  {∀N_{2}: (0 = N_{2} ⇒ BS(M, 0) = \atop BS(M, N_{2}))  □}

[SystemQ lemma SameBS(2)(Indu): ΠM, N_{1}, N_{2}: ∀N_{2}: (N_{1} = N_{2} ⇒ BS(M, N_{1}) = BS(M, N_{2})) ⇒ ∀N_{2}: ((N_{1} + 1) = N_{2} ⇒ BS(M, (N_{1} + 1)) = BS(M, N_{2}))]

SystemQ proof of SameBS(2)(Indu):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N_{1}, N_{2}  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  M, N_{1}, N_{2}  ;
L05: Premise ≫  ∀N_{2}: (N_{1}  =  N_{2}  ⇒

BS(M, N_{1}) = BS(M, N_{2}))

;

L06: Premise ≫  (N_{1} + 1) = N_{2}  ;

L07: (+1)IsPositive(N) ≫  0 < (N_{1} + 1)  ;

L08: BSpositive ⊳ L07 ≫ BS(M, (N_{1} + 1)) = (1/2(exp)((M + ((N_{1} + 1)))) + BS(M, ((N_{1} + 1) − 1))) ;

L09: x = x + y − y ≫ N_{1} = ((N_{1} + 1) − 1) ;

L10: A4 @((N_{1} + 1) − 1) ⊳ L05 ≫ N_{1} = ((N_{1} + 1) − 1) ⇒

BS(M, N_{1}) = BS(M, ((N_{1} + 1) − 1)) ;

L11: MP ⊳ L10 ⊳ L09 ≫  {BS(M, N_{1}) = BS(M, ((N_{1} + \atop 1) − 1))  ;}
L12: eqSymmetry ⊳ L11 ≫  {BS(M, ((N_{1} + 1) − 1)) = \atop BS(M, N_{1})  ;}

L13: EqAdditionLeft ⊳ L12 ≫ (1/2(exp)((M + ((N_{1} + 1)))) + BS(M, ((N_{1} + 1) − 1))) = (1/2(exp)((M + ((N_{1} + 1)))) + BS(M, N_{1})) ;

L14: PositiveToRight(Eq) ⊳ L06 ≫ N_{1} = (N_{2} − 1)  ;

L15: A4 @(N_{2} − 1) ⊳ L05 ≫ N_{1} = (N_{2} − 1) ⇒ BS(M, N_{1}) = BS(M, (N_{2} − 1)) ;

L16: MP ⊳ L15 ⊳ L14 ≫  BS(M, N_{1}) = BS(M, (N_{2} − 1)) ;

L17: EqAdditionLeft ⊳ L16 ≫ (1/2(exp)((M + ((N_{1} + 1)))) + BS(M, N_{1})) = (1/2(exp)((M + ((N_{1} + 1)))) + BS(M, (N_{2} − 1))) ;

L18: EqAdditionLeft ⊳ L06 ≫  (M + ((N_{1} + 1))) = (M + N_{2}) ;

L19: SameExp ⊳ L18 ≫ 1/2(exp)((M + ((N_{1} + 1)))) = 1/2(exp)((M + N_{2})) ;

L20: eqAddition ⊳ L19 ≫ (1/2(exp)((M + ((N_{1} + 1)))) + BS(M, (N_{2} − 1))) = (1/2(exp)((M + N_{2})) + BS(M, (N_{2} − 1))) ;

L21: SubLessRight ⊳ L06 ⊳ L07 ≫ 0 < N_{2}  ;

L22: BSpositive ⊳ L21 ≫ BS(M, N_{2}) = (1/2(exp)((M + N_{2})) + BS(M, (N_{2} − 1))) ;

L23: eqSymmetry ⊳ L22 ≫ (1/2(exp)((M + N_{2})) + BS(M, (N_{2} −1))) = BS(M, N_{2}) ;

L24: eqTransitivity6 ⊳ L08 ⊳ L13 ⊳ L17 ⊳ L20 ⊳ L23 ≫

BS(M, (N_{1} + 1)) = BS(M, N_{2}) ;

L25: Block ≫ End ;

L05: Ded ⊳ L25 ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒

BS(M, N_{1}) = BS(M, N_{2})) ⇒ (N_{1} + 1) = N_{2} ⇒ BS(M, (N_{1} + 1)) = BS(M, N_{2}) ;

L06: Premise ≫ ∀N_{2}: (N_{1} = N_{2} ⇒

BS(M, N_{1}) = BS(M, N_{2}))

;

L07: MP ⊳ L05 ⊳ L06 ≫ (N_{1} + 1) = N_{2} ⇒ BS(M, (N_{1} + 1)) = BS(M, N_{2}) ; L26: Gen ⊳ L07 ≫

∀N_{2}: ((N_{1} + 1) = N_{2} ⇒
BS(M, (N_{1} +1)) = BS(M, N_{2})) ;
L27: Block ≫  End  ;
L28: Arbitrary ≫  M, N_{1}, N_{2}  ;

L29: Ded ⊳ L27 ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒
BS(M, N_{1}) = BS(M, N_{2})) ⇒
∀N_{2}: ((N_{1} + 1) = N_{2} ⇒
BS(M, (N_{1} +1)) = BS(M, N_{2})) □

[SystemQ lemma SameBS(2): ΠM, N_{1}, N_{2}: N_{1} = N_{2} ⊢ BS(M, N_{1}) = BS(M, N_{2})] SystemQ proof of SameBS(2):

L01: Arbitrary ≫  M, N_{1}, N_{2}  ;
L02: Premise ≫  N_{1} = N_{2}  ;
L03: SameBS(2)(Base) ≫  {∀N_{2}: (0 = N_{2} ⇒ BS(M, 0) = \atop BS(M, N_{2}))  ;}

L04: SameBS(2)(Indu) ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒
BS(M, N_{1}) = BS(M, N_{2})) ⇒
∀N_{2}: ((N_{1} + 1) = N_{2} ⇒
BS(M, (N_{1} +1)) = BS(M, N_{2})) ;

L05: Induction ⊳ L03 ⊳ L04 ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒

BS(M, N_{1}) = BS(M, N_{2}))

;

L06: A4 @ N_{2} ⊳ L05 ≫

N_{1} = N_{2} ⇒ BS(M, N_{1}) =
BS(M, N_{2}) ;
L07: MP ⊳ L06 ⊳ L02 ≫ BS(M, N_{1}) = BS(M, N_{2}) □

————–

[SystemQ lemma NegativeToLeft(Less)(1term): ΠX , Y: 0 < (X − Y) ⊢ Y < X]

SystemQ proof of NegativeToLeft(Less)(1term):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  0 < (X − Y)  ;
L03: LessAddition ⊳ L02 ≫  (0 + Y) < ((X − Y) + Y)  ;
L04: plus0Left ≫  (0 + Y) = Y  ;
L05: SubLessLeft ⊳ L04 ⊳ L03 ≫  Y < ((X − Y) + Y)  ;
L06: Three2threeTerms ≫  ((X − Y) + Y) = ((X + Y) − Y) ;
L07: x = x + y − y ≫  X = ((X + Y) − Y)  ;
L08: eqSymmetry ⊳ L07 ≫  ((X + Y) − Y) = X  ;
L09: eqTransitivity ⊳ L06 ⊳ L08 ≫ ((X − Y) + Y) = X  ;
L10: SubLessRight ⊳ L09 ⊳ L05 ≫ Y < X  □

[SystemQ lemma BS(+1): ΠM, N: BS(M, (N +1)) = (1/2(exp)(((M+N)+ 1)) + BS(M, N))]

SystemQ proof of BS(+1):

L01: Arbitrary ≫  M, N  ;
L02: (+1)IsPositive(N) ≫  0 < (N + 1)  ;
L03: BSpositive ⊳ L02 ≫  BS(M, (N + 1))  = ; (1/2(exp)((M + ((N + 1)))) + ; BS(M, ((N + 1) − 1)))  ;

L04: plusAssociativity ≫  ((M+N)+1) = (M+((N +1))) ;
L05: SameExp ⊳ L04 ≫  {1/2(exp)(((M + N) + 1)) = \atop 1/2(exp)((M + ((N + 1))))  ;}
L06: eqSymmetry ⊳ L05 ≫  {1/2(exp)((M + ((N + 1)))) = \atop 1/2(exp)(((M + N) + 1))  ;}
L07: x = x + y − y ≫  N = ((N + 1) − 1)  ;
L08: SameBS(2) ⊳ L07 ≫  {BS(M, N) = BS(M, ((N +1)− \atop 1))  ;}
L09: eqSymmetry ⊳ L08 ≫  {BS(M, ((N + 1) − 1)) = \atop BS(M, N)  ;}

L10: AddEquations ⊳ L06 ⊳ L09 ≫

(1/2(exp)((M + ((N + 1)))) +
BS(M, ((N + 1) − 1))) =
(1/2(exp)(((M + N) + 1)) +
BS(M, N)) ;
L11: eqTransitivity ⊳ L03 ⊳ L10 ≫ BS(M, (N + 1))  = ; (1/2(exp)(((M + N) + 1)) + ; BS(M, N))  □

[SystemQ lemma BSbound(Exact)(Base): ΠM: (BS((M+1), 0)+1/2(exp)(((M+ 1) + 0))) = 1/2(exp)M]

SystemQ proof of BSbound(Exact)(Base):

L01: Arbitrary ≫  M  ;
L02: BSzero(Exact) ≫  {BS((M + 1), 0)  = \atop 1/2(exp)((M + 1))  ;}
L03: Exp(+1) ≫  {1/2(exp)((M + 1)) = (1/2 ∗ \atop 1/2(exp)M)  ;}
L04: eqTransitivity ⊳ L02 ⊳ L03 ≫ {BS((M + 1), 0) = (1/2 ∗ \atop 1/2(exp)M)  ;}
L05: plus0 ≫  ((M + 1) + 0) = (M + 1)  ;
L06: SameExp ⊳ L05 ≫  {1/2(exp)(((M + 1) + 0)) = \atop 1/2(exp)((M + 1))  ;}
L07: eqTransitivity ⊳ L06 ⊳ L03 ≫ {1/2(exp)(((M+1)+0)) = (1/2∗ \atop 1/2(exp)M)  ;}

L08: AddEquations ⊳ L04 ⊳ L07 ≫

(BS((M  +  1), 0)  +
1/2(exp)(((M + 1) + 0))) =
((1/2 ∗ 1/2(exp)M) + (1/2 ∗
1/2(exp)M)) ;

L09: TwoHalves ≫

((1/2 ∗ 1/2(exp)M) + (1/2 ∗
1/2(exp)M)) = 1/2(exp)M ;

L10: eqTransitivity ⊳ L08 ⊳ L09 ≫

(BS((M  +  1), 0)  +
1/2(exp)(((M + 1) + 0))) =
1/2(exp)M □

[SystemQ lemma BSbound(Exact)(Indu): ΠM, N: (BS((M+1), N)+1/2(exp)(((M+ 1) + N))) = 1/2(exp)M ⇒ (BS((M + 1), (N + 1)) + 1/2(exp)((((M + 1) + N) + 1))) = 1/2(exp)M]

SystemQ proof of BSbound(Exact)(Indu):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N  ;

L03: Premise ≫ (BS((M + 1), N) + 1/2(exp)(((M + 1) + N))) = 1/2(exp)M ;

L04: BS(+1) ≫  BS((M + 1), (N + 1)) = ; (1/2(exp)((((M+1)+N)+1))+ ; BS((M + 1), N))  ;

L05: eqAddition ⊳ L04 ≫ (BS((M + 1), (N + 1)) + 1/2(exp)((((M + 1) + N) + 1))) = ((1/2(exp)((((M + 1) + N) + 1)) + BS((M + 1), N)) + 1/2(exp)((((M + 1) + N) + 1))) ;

L06: plusCommutativity ≫ (1/2(exp)((((M+1)+N)+1))+ BS((M + 1), N)) = (BS((M + 1), N) + 1/2(exp)((((M + 1) + N) + 1))) ;

L07: eqAddition ⊳ L06 ≫ ((1/2(exp)((((M + 1) + N) + 1)) + BS((M + 1), N)) + 1/2(exp)((((M + 1) + N) + 1))) = ((BS((M + 1), N) + 1/2(exp)((((M+1)+N)+1)))+ 1/2(exp)((((M + 1) + N) + 1))) ;

L08: Exp(+1) ≫  {1/2(exp)((((M+1)+N)+1)) = \atop (1/2∗1/2(exp)(((M+1)+N))) ;}

L09: AddEquations ⊳ L08 ⊳ L08 ≫ (1/2(exp)((((M + 1) + N) + 1)) + 1/2(exp)((((M + 1) + N) + 1))) = ((1/2 ∗ 1/2(exp)(((M + 1) + N))) + (1/2∗1/2(exp)(((M+1)+N)))) ;

L10: TwoHalves ≫ ((1/2 ∗ 1/2(exp)(((M + 1) + N))) + (1/2 ∗ 1/2(exp)(((M + 1) + N)))) = 1/2(exp)(((M + 1) + N)) ;

L11: eqTransitivity ⊳ L09 ⊳ L10 ≫ (1/2(exp)((((M + 1) + N) + 1))+1/2(exp)((((M+1)+N)+ 1))) = 1/2(exp)(((M+1)+N)) ;

L12: Three2twoTerms ⊳ L11 ≫ ((BS((M + 1), N) + 1/2(exp)((((M + 1) + N) + 1))) + 1/2(exp)((((M + 1) + N) + 1))) = (BS((M + 1), N) + 1/2(exp)(((M + 1) + N))) ;

L13: eqTransitivity5 ⊳ L05 ⊳ L07 ⊳

L12 ⊳ L03 ≫ (BS((M + 1), (N + 1)) + 1/2(exp)((((M + 1) + N) + 1))) = 1/2(exp)M ;

L14: Block ≫  End  ;
L15: Arbitrary ≫  M, N  ;

L16: Ded ⊳ L14 ≫ (BS((M + 1), N) +

1/2(exp)(((M + 1) + N))) = 1/2(exp)M ⇒ (BS((M + 1), (N + 1)) + 1/2(exp)((((M + 1) + N) + 1))) = 1/2(exp)M □

[SystemQ lemma BSbound(Exact): ΠM, N: (BS((M+1), N)+1/2(exp)(((M+ 1) + N))) = 1/2(exp)M]

SystemQ proof of BSbound(Exact):

L01: Arbitrary ≫ M, N ;

L02: BSbound(Exact)(Base) ≫

(BS((M  +  1), 0)  +

1/2(exp)(((M + 1) + 0))) = 1/2(exp)M ;

L03: BSbound(Exact)(Indu) ≫ (BS((M + 1), N) + 1/2(exp)(((M + 1) + N))) = 1/2(exp)M ⇒ (BS((M + 1), (N + 1)) + 1/2(exp)((((M + 1) + N) + 1))) = 1/2(exp)M ;

L04: Induction ⊳ L02 ⊳ L03 ≫ (BS((M + 1), N) + 1/2(exp)(((M + 1) + N))) = 1/2(exp)M □

[SystemQ lemma BSbound: ΠM, N: BS((M + 1), N) < 1/2(exp)M] SystemQ proof of BSbound:

L01: Arbitrary ≫ M, N ;

L02: BSbound(Exact) ≫ (BS((M + 1), N) + 1/2(exp)(((M + 1) + N))) = 1/2(exp)M ;

L03: plusCommutativity ≫ (1/2(exp)(((M + 1) + N)) + BS((M + 1), N)) = (BS((M + 1), N) + 1/2(exp)(((M + 1) + N))) ;

L04: eqTransitivity ⊳ L03 ⊳ L02 ≫ (1/2(exp)(((M + 1) + N)) + BS((M + 1), N)) = 1/2(exp)M ;

L05: PositiveToRight(Eq) ⊳ L04 ≫ 1/2(exp)(((M + 1) + N)) = (1/2(exp)M − BS((M + 1), N)) ;

L06: 0 < 1/2 ≫ 0 < 1/2 ;
L07: PositiveBase ⊳ L06 ≫  0 < 1/2(exp)(((M + 1) + N)) ;
L08: SubLessRight ⊳ L05 ⊳ L07 ≫ {0 < (1/2(exp)M − BS((M + \atop 1), N))  ;}

L09: NegativeToLeft(Less)(1term) ⊳

L08 ≫ BS((M + 1), N) < 1/2(exp)M □

——— [SystemQ lemma SameSeries(NumDiff): ΠFX, FY, O, P, N_{1}, N_{2}: O = P ⊢

N_{1} = N_{2} ⊢ |(FX[O] − FY[N_{1}])| = |(FX[P] − FY[N_{2}])|]

SystemQ proof of SameSeries(NumDiff):

L01: Arbitrary ≫  FX, FY, O, P, N_{1}, N_{2}  ;
L02: Premise ≫  O = P  ;

L03: Premise ≫  N_{1} = N_{2}  ;
L04: SameSeries ⊳ L02 ≫  FX[O] = FX[P]  ;
L05: SameSeries ⊳ L03 ≫  FY[N_{1}] = FY[N_{2}]  ;
L06: EqNegated ⊳ L05 ≫  (−uFY[N_{1}]) = (−uFY[N_{2}])  ;

L07: AddEquations ⊳ L04 ⊳ L06 ≫

(FX[O] − FY[N_{1}]) = (FX[P] −
FY[N_{2}]) ;

L08: SameNumerical ⊳ L07 ≫

|(FX[O]−FY[N_{1}])| = |(FX[P]−
FY[N_{2}])| □

[SystemQ lemma UStelescope(Zero)(Exact): ΠM: UStelescope(M, 0) = |(us[M]− us[(M + 1)])|]

SystemQ proof of UStelescope(Zero)(Exact):

L01: Arbitrary ≫  M  ;
L02: eqReflexivity ≫  0 = 0  ;

L03: UStelescope(Zero) ⊳ L02 ≫ UStelescope(M, 0) = |(us[M] − us[(M + 1)])| □

[SystemQ lemma SameTelescope(2)(Base): ΠM, N_{2}: ∀N_{2}: (0 = N_{2} ⇒ UStelescope(M, 0) = UStelescope(M, N_{2}))]

SystemQ proof of SameTelescope(2)(Base):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N_{2}  ;
L03: Premise ≫  0 = N_{2}  ;
L04: eqSymmetry ⊳ L03 ≫  N_{2} = 0  ;

L05: UStelescope(Zero) ⊳ L04 ≫ UStelescope(M, N_{2}) = |(us[M] − us[(M + 1)])|

;

L06: eqSymmetry ⊳ L05 ≫ |(us[M] − us[(M + 1)])| = UStelescope(M, N_{2}) ;

L07: UStelescope(Zero)(Exact) ≫ UStelescope(M, 0) = |(us[M] − us[(M + 1)])| ;

L08: eqTransitivity ⊳ L07 ⊳ L06 ≫ UStelescope(M, 0) = UStelescope(M, N_{2}) ;

L09: Block ≫  End  ;
L10: Arbitrary ≫  M, N_{2}  ;

L03: Ded ⊳ L09 ≫ 0 = N_{2} ⇒ UStelescope(M, 0) = UStelescope(M, N_{2}) ;

L11: Gen ⊳ L03 ≫ ∀N_{2}: (0  =  N_{2}  ⇒

UStelescope(M, 0) = UStelescope(M, N_{2})) □

[SystemQ lemma SameTelescope(2)(Indu): ΠM, N_{1}, N_{2}: ∀N_{2}: (N_{1} = N_{2} ⇒ UStelescope(M, N_{1}) = UStelescope(M, N_{2})) ⇒ ∀N_{2}: ((N_{1}+1) = N_{2} ⇒ UStelescope(M, (N_{1}+ 1)) = UStelescope(M, N_{2}))]

SystemQ proof of SameTelescope(2)(Indu):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N_{1}, N_{2}  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  M, N_{1}, N_{2}  ;

L05: Premise ≫  ∀N_{2}: (N_{1}  =  N_{2}  ⇒

UStelescope(M, N_{1}) = UStelescope(M, N_{2})) ;

L06: Premise ≫  (N_{1} + 1) = N_{2}  ;
L07: (+1)IsPositive(N) ≫  0 < (N_{1} + 1)  ;

L08: UStelescope(Positive) ⊳ L07 ≫ UStelescope(M, (N_{1} + 1)) = (|(us[(M + ((N_{1} + 1)))] − us[(M + (((N_{1} + 1) + 1)))])| + UStelescope(M, ((N_{1} +1)−1))) ;

L09: x = x + y − y ≫ N_{1} = ((N_{1} + 1) − 1) ;

L10: A4 @((N_{1} + 1) − 1) ⊳ L05 ≫ N_{1} = ((N_{1} + 1) − 1) ⇒

UStelescope(M, N_{1}) = UStelescope(M, ((N_{1} + 1) − 1)) ;

L11: MP ⊳ L10 ⊳ L09 ≫ UStelescope(M, N_{1}) = UStelescope(M, ((N_{1} + 1) − 1)) ;

L12: eqSymmetry ⊳ L11 ≫ UStelescope(M, ((N_{1} + 1) − 1)) = UStelescope(M, N_{1}) ;

L13: PositiveToRight(Eq) ⊳ L06 ≫ N_{1} = (N_{2} − 1)  ;

L14: A4 @(N_{2} − 1) ⊳ L05 ≫ N_{1} = (N_{2} − 1) ⇒

UStelescope(M, N_{1}) = UStelescope(M, (N_{2} − 1))

;

L15: MP ⊳ L14 ⊳ L13 ≫ UStelescope(M, N_{1}) = UStelescope(M, (N_{2} − 1))

;

L16: eqTransitivity ⊳ L12 ⊳ L15 ≫ UStelescope(M, ((N_{1} + 1) − 1)) = UStelescope(M, (N_{2} − 1)) ;

L17: EqAdditionLeft ⊳ L06 ≫  (M + ((N_{1} + 1))) = (M + N_{2}) ;
L18: eqAddition ⊳ L06 ≫  ((N_{1} + 1) + 1) = (N_{2} + 1)  ;
L19: EqAdditionLeft ⊳ L18 ≫  {(M + (((N_{1} + 1) + 1))) = (M + \atop ((N_{2} + 1)))  ;}

L20: SameSeries(NumDiff) ⊳ L17 ⊳

L19 ≫ |(us[(M+((N_{1}+1)))]−us[(M+ (((N_{1} + 1) + 1)))])| = |(us[(M + N_{2})] − us[(M + ((N_{2} + 1)))])| ;

L21: AddEquations ⊳ L20 ⊳ L16 ≫ (|(us[(M + ((N_{1} + 1)))] − us[(M + (((N_{1} + 1) + 1)))])| + UStelescope(M, ((N_{1} + 1) − 1))) = (|(us[(M + N_{2})] − us[(M + ((N_{2} + 1)))])| + UStelescope(M, (N_{2} − 1))) ;

L22: SubLessRight ⊳ L06 ⊳ L07 ≫ 0 < N_{2}  ;

L23: UStelescope(Positive) ⊳ L22 ≫ UStelescope(M, N_{2}) = (|(us[(M+N_{2})]−us[(M+((N_{2}+ 1)))])| + UStelescope(M, (N_{2} − 1))) ; L24: eqSymmetry ⊳ L23 ≫ (|(us[(M+N_{2})]−us[(M+((N_{2}+ 1)))])| + UStelescope(M, (N_{2} − 1))) = UStelescope(M, N_{2}) ;

L25: eqTransitivity4 ⊳ L08 ⊳ L21 ⊳

L24 ≫ UStelescope(M, (N_{1} + 1)) =

UStelescope(M, N_{2}) ;

L26: Block ≫ End ;

L05: Ded ⊳ L26 ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒

UStelescope(M, N_{1}) = UStelescope(M, N_{2})) ⇒ (N_{1} + 1) = N_{2} ⇒ UStelescope(M, (N_{1} + 1)) = UStelescope(M, N_{2}) ;

L06: Premise ≫ ∀N_{2}: (N_{1} = N_{2} ⇒ UStelescope(M, N_{1}) = UStelescope(M, N_{2})) ;

L07: MP ⊳ L05 ⊳ L06 ≫ (N_{1} + 1) = N_{2} ⇒

UStelescope(M, (N_{1} + 1)) = UStelescope(M, N_{2}) ;

L27: Gen ⊳ L07 ≫ ∀N_{2}: ((N_{1} + 1) = N_{2} ⇒ UStelescope(M, (N_{1} + 1)) = UStelescope(M, N_{2})) ;

L28: Block ≫  End  ;
L29: Arbitrary ≫  M, N_{1}, N_{2}  ;

L30: Ded ⊳ L28 ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒

UStelescope(M, N_{1}) = UStelescope(M, N_{2})) ⇒ ∀N_{2}: ((N_{1} + 1) = N_{2} ⇒ UStelescope(M, (N_{1} + 1)) = UStelescope(M, N_{2})) □

[SystemQ lemma SameTelescope(2): ΠM, N_{1}, N_{2}: N_{1} = N_{2} ⊢ UStelescope(M, N_{1}) = UStelescope(M, N_{2})]

SystemQ proof of SameTelescope(2):

L01: Arbitrary ≫  M, N_{1}, N_{2}  ;
L02: Premise ≫  N_{1} = N_{2}  ;

L03: SameTelescope(2)(Base) ≫

∀N_{2}: (0  =  N_{2}  ⇒

UStelescope(M, 0) = UStelescope(M, N_{2})) ;

L04: SameTelescope(2)(Indu) ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒

UStelescope(M, N_{1}) = UStelescope(M, N_{2})) ⇒ ∀N_{2}: ((N_{1} + 1) = N_{2} ⇒ UStelescope(M, (N_{1} + 1)) = UStelescope(M, N_{2})) ;

L05: Induction ⊳ L03 ⊳ L04 ≫

∀N_{2}: (N_{1}  =  N_{2}  ⇒

UStelescope(M, N_{1}) = UStelescope(M, N_{2})) ;

L06: A4 @ N_{2} ⊳ L05 ≫ N_{1}  =  N_{2}  ⇒

UStelescope(M, N_{1}) = UStelescope(M, N_{2}) ;

L07: MP ⊳ L06 ⊳ L02 ≫ UStelescope(M, N_{1}) = UStelescope(M, N_{2}) □

[SystemQ lemma TelescopeNumerical(Base): ΠM: |(us[M] − us[(M + ((0 + 1)))])| <= UStelescope(M, 0)]

SystemQ proof of TelescopeNumerical(Base):

L01: Arbitrary ≫  M  ;
L02: eqReflexivity ≫  0 = 0  ;

L03: UStelescope(Zero) ⊳ L02 ≫ UStelescope(M, 0) = |(us[M] − us[(M + 1)])| ;

L04: eqReflexivity ≫  M = M  ;
L05: plus0Left ≫  (0 + 1) = 1  ;
L06: EqAdditionLeft ⊳ L05 ≫  (M + ((0 + 1))) = (M + 1)  ;
L07: eqSymmetry ⊳ L06 ≫  (M + 1) = (M + ((0 + 1)))  ;

L08: SameSeries(NumDiff) ⊳ L04 ⊳

L07 ≫ |(us[M] − us[(M + 1)])| =

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

L09: eqTransitivity ⊳ L03 ⊳ L08 ≫ UStelescope(M, 0) = |(us[M] − us[(M + ((0 + 1)))])| ;

L10: eqSymmetry ⊳ L09 ≫ |(us[M]−us[(M+((0+1)))])| = UStelescope(M, 0) ;

L11: eqLeq ⊳ L10 ≫ |(us[M] − us[(M + ((0 + 1)))])| <= UStelescope(M, 0) □

[SystemQ lemma TelescopeNumerical(Indu): ΠM, N: |(us[M]−us[(M+((N + 1)))])| <= UStelescope(M, N) ⇒ |(us[M] − us[(M + (((N + 1) + 1)))])| <= UStelescope(M, (N + 1))]

SystemQ proof of TelescopeNumerical(Indu):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N  ;

L03: Premise ≫ |(us[M] − us[(M + ((N +

1)))])| <= UStelescope(M, N) ;

L04: (+1)IsPositive(N) ≫ 0 < (N + 1) ;

L05: UStelescope(Positive) ⊳ L04 ≫ UStelescope(M, (N + 1)) = (|(us[(M + ((N + 1)))] − us[(M + (((N + 1) + 1)))])| + UStelescope(M, ((N + 1) − 1))) ;

L06: x = x + y − y ≫  N = ((N + 1) − 1)  ;
L07: eqSymmetry ⊳ L06 ≫  ((N + 1) − 1) = N  ;

L08: SameTelescope(2) ⊳ L07 ≫ UStelescope(M, ((N +1)−1)) = UStelescope(M, N) ; L09: EqAdditionLeft ⊳ L08 ≫ (|(us[(M + ((N + 1)))] − us[(M + (((N + 1) + 1)))])| + UStelescope(M, ((N + 1) − 1))) = (|(us[(M + ((N + 1)))] − us[(M + (((N + 1) + 1)))])| + UStelescope(M, N)) ;

L10: eqTransitivity ⊳ L05 ⊳ L09 ≫ UStelescope(M, (N + 1)) = (|(us[(M + ((N + 1)))] − us[(M + (((N + 1) + 1)))])| + UStelescope(M, N)) ;

L11: eqSymmetry ⊳ L10 ≫ (|(us[(M + ((N + 1)))] − us[(M + (((N + 1) + 1)))])| + UStelescope(M, N)) = UStelescope(M, (N + 1))

;

L12: LeqAdditionLeft ⊳ L03 ≫ (|(us[(M+((N +1)))]−us[(M+ (((N + 1) + 1)))])| + |(us[M] − us[(M + ((N + 1)))])|) <= (|(us[(M + ((N + 1)))] − us[(M + (((N + 1) + 1)))])| + UStelescope(M, N)) ;

L13: subLeqRight ⊳ L11 ⊳ L12 ≫ (|(us[(M+((N +1)))]−us[(M+ (((N + 1) + 1)))])| + |(us[M] − us[(M + ((N + 1)))])|) <= UStelescope(M, (N + 1)) ;

L14: plusCommutativity ≫ (|(us[(M+((N +1)))]−us[(M+ (((N + 1) + 1)))])| + |(us[M] − us[(M + ((N + 1)))])|) = (|(us[M] − us[(M + ((N + 1)))])|+|(us[(M+((N +1)))]− us[(M + (((N + 1) + 1)))])|) ;

L15: subLeqLeft ⊳ L14 ⊳ L13 ≫ (|(us[M] − us[(M + ((N + 1)))])|+|(us[(M+((N +1)))]− us[(M + (((N + 1) + 1)))])|) <= UStelescope(M, (N + 1)) ;

L16: insertMiddleTerm(Numerical) ≫ |(us[M] − us[(M + (((N + 1) + 1)))])| <= (|(us[M] − us[(M + ((N + 1)))])| + |(us[(M + ((N + 1)))] − us[(M + (((N + 1) + 1)))])|) ;

L17: leqTransitivity ⊳ L16 ⊳ L15 ≫

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

(((N + 1) + 1)))])| <= UStelescope(M, (N + 1))

;

L18: Block ≫  End  ;

L19: Arbitrary ≫  M, N  ;

L20: Ded ⊳ L18 ≫

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

((N + 1)))])| <= UStelescope(M, N) ⇒ |(us[M] − us[(M + (((N + 1) + 1)))])| <= UStelescope(M, (N + 1)) □

[SystemQ lemma TelescopeNumerical: ΠM, N: |(us[M] − us[(M + ((N + 1)))])| <= UStelescope(M, N)]

SystemQ proof of TelescopeNumerical:

L01: Arbitrary ≫ M, N ;

L02: TelescopeNumerical(Base) ≫ |(us[M] − us[(M + ((0 + 1)))])| <= UStelescope(M, 0) ;

L03: TelescopeNumerical(Indu) ≫

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

((N + 1)))])| <= UStelescope(M, N) ⇒ |(us[M] − us[(M + (((N + 1) + 1)))])| <= UStelescope(M, (N + 1))

;

L04: Induction ⊳ L02 ⊳ L03 ≫ |(us[M] − us[(M + ((N + 1)))])| <= UStelescope(M, N) □

—————(21.10.06) [SystemQ lemma EqAdditionLeft(R): ΠFX, FY, FZ: R(FX) == R(FY) ⊢

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

SystemQ proof of EqAdditionLeft(R):

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

L03: EqAddition(R) ⊳ L02 ≫ R(FX) + +R(FZ) == R(FY) + +R(FZ) ;

L04: PlusCommutativity(R) ≫ R(FZ) + +R(FX) == R(FX) + +R(FZ) ;

L05: PlusCommutativity(R) ≫ R(FY) + +R(FZ) == R(FZ) + +R(FY) ;

L06: eqTransitivity4 ⊳ L04 ⊳ L03 ⊳

L05 ≫ R(FZ) + +R(FX) == R(FZ) +

+R(FY) □

[SystemQ lemma x = x+(y−y)(R): ΠFX, FY: R(FX) = R(FX)++(R(FY)+ +(− − R(FY)))]

SystemQ proof of x = x + (y − y)(R):

L01: Arbitrary ≫  FX, FY  ;
L02: Plus0(R) ≫  R(FX) + +00 == R(FX)  ;
L03: ==Symmetry ⊳ L02 ≫  R(FX) == R(FX) + +00  ;
L04: Negative(R) ≫  R(FY) + +(− − R(FY)) == 00 ;
L05: ==Symmetry ⊳ L04 ≫  00 == R(FY) + +(− − R(FY)) ;

L06: EqAdditionLeft(R) ⊳ L05 ≫ R(FX) + +00 == R(FX) + +(R(FY) + +(− − R(FY))) ;

L07: eqTransitivity ⊳ L03 ⊳ L06 ≫ R(FX) == R(FX)++(R(FY)+ +(− − R(FY))) □

[SystemQ lemma x = x + y − y(R): ΠFX, FY: R(FX) = R(FX) + +R(FY) + +(− − R(FY))]

SystemQ proof of x = x + y − y(R):

L01: Arbitrary ≫ FX, FY ;

L02: x = x + (y − y)(R) ≫ R(FX) == R(FX)++(R(FY)+ +(− − R(FY))) ;

L03: PlusAssociativity(R) ≫ R(FX) + +R(FY) + +(− − R(FY)) == R(FX) + +(R(FY) + +(− − R(FY))) ;

L04: ==Symmetry ⊳ L03 ≫ R(FX) + +(R(FY) + +(− − R(FY))) == R(FX) + +R(FY) + +(− − R(FY))

;

L05: eqTransitivity ⊳ L02 ⊳ L04 ≫ R(FX) == R(FX) + +R(FY) + +(− − R(FY)) □

———-(22.10.06) [SystemQ lemma Three2twoTerms(R): ΠFX, FY, FZ, FU: R(FY)++R(FZ) ==

R(FU) ⊢ R(FX) + +R(FY) + +R(FZ) == R(FX) + +R(FU)]

SystemQ proof of Three2twoTerms(R):

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

L03: EqAdditionLeft(R) ⊳ L02 ≫ R(FX) + +(R(FY) + +R(FZ)) == R(FX) + +R(FU) ;

L04: PlusAssociativity(R) ≫ R(FX)++R(FY)++R(FZ) == R(FX) + +(R(FY) + +R(FZ)) ;

L05: eqTransitivity ⊳ L04 ⊳ L03 ≫ R(FX)++R(FY)++R(FZ) == R(FX) + +R(FU) □

[SystemQ lemma PositiveToRight(Less)(R): ΠFX, FY, FZ: R(FX)++R(FY) << R(FZ) ⊢ R(FX) << R(FZ) + +(− − R(FY))]

SystemQ proof of PositiveToRight(Less)(R):

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

L03: lessAddition(R) ⊳ L02 ≫ R(FX) + +R(FY) + +(− − R(FY)) << R(FZ) + +(− − R(FY)) ;

L04: x = x + y − y(R) ≫ R(FX) == R(FX) + +R(FY) + +(− − R(FY)) ;

L05: ==Symmetry ⊳ L04 ≫ R(FX) + +R(FY) + +(− − R(FY)) == R(FX) ;

L06: SubLessLeft(R) ⊳ L05 ⊳ L03 ≫ R(FX) << R(FZ) + +(− − R(FY)) □

[SystemQ lemma Three2threeTerms(R): ΠFX, FY, FZ: R(FX) + +R(FY) + +R(FZ) == R(FX) + +R(FZ) + +R(FY)]

SystemQ proof of Three2threeTerms(R):

L01: Arbitrary ≫ FX, FY, FZ ;

L02: PlusCommutativity(R) ≫ R(FY) + +R(FZ) == R(FZ) + +R(FY) ;

L03: Three2twoTerms(R) ⊳ L02 ≫ R(FX)++R(FY)++R(FZ) == R(FX) + +(R(FZ) + +R(FY)) ;

L04: PlusAssociativity(R) ≫ R(FX)++R(FZ)++R(FY) == R(FX) + +(R(FZ) + +R(FY)) ;

L05: ==Symmetry ⊳ L04 ≫ R(FX) + +(R(FZ) + +R(FY)) == R(FX) + +R(FZ) + +R(FY) ;

L06: eqTransitivity ⊳ L03 ⊳ L05 ≫ R(FX)++R(FY)++R(FZ) == R(FX) + +R(FZ) + +R(FY) □

——–(22.10.06)

[SystemQ lemma Plus0Left(R): ΠFX: 00 + +R(FX) == R(FX)]

SystemQ proof of Plus0Left(R):

L01: Arbitrary ≫  FX  ;
L02: Plus0(R) ≫  R(FX) + +00 == R(FX)  ;
L03: PlusCommutativity(R) ≫  00 + +R(FX) == R(FX) + +00 ;
L04: eqTransitivity ⊳ L03 ⊳ L02 ≫ 00 + +R(FX) == R(FX)  □

[SystemQ lemma PositiveToRight(Eq)(R): ΠFX, FY, FZ: R(FX)++R(FY) == R(FZ) ⊢ R(FX) == R(FZ) + +(− − R(FY))]

SystemQ proof of PositiveToRight(Eq)(R):

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

L03: EqAddition(R) ⊳ L02 ≫ R(FX) + +R(FY) + +(− − R(FY)) == R(FZ) + +(− − R(FY)) ;

L04: x = x + y − y(R) ≫ R(FX) == R(FX) + +R(FY) + +(− − R(FY)) ;

L05: eqTransitivity ⊳ L04 ⊳ L03 ≫

R(FX) == R(FZ) + +(− −
R(FY)) □

[SystemQ lemma SubtractEquations(R): ΠFX, FY, FZ, FU: R(FX)++R(FZ) == R(FY) + +R(FU) ⊢ R(FZ) == R(FU) ⊢ R(FX) == R(FY)]

SystemQ proof of SubtractEquations(R):

L01: Arbitrary ≫ FX, FY, FZ, FU ;

L02: Premise ≫ R(FX) + +R(FZ) == R(FY) +

+R(FU) ;

L03: Premise ≫ R(FZ) == R(FU) ;

L04: EqAddition(R) ⊳ L02 ≫ R(FX) + +R(FZ) + +(− − R(FZ)) == R(FY)++R(FU)+ +(− − R(FZ)) ;

L05: Plus0Left(R) ≫ 00 + +R(FZ) == R(FZ) ;
L06: eqTransitivity ⊳ L05 ⊳ L03 ≫ 00 + +R(FZ) == R(FU)  ;

L07: PositiveToRight(Eq)(R) ⊳

L06 ≫ 00 == R(FU) + +(− − R(FZ)) ;

L08: ==Symmetry ⊳ L07 ≫  R(FU) + +(− − R(FZ)) == 00 ;

L09: EqAdditionLeft(R) ⊳ L08 ≫ R(FY) + +(R(FU) + +(− − R(FZ))) == R(FY) + +00 ;

L10: PlusAssociativity(R) ≫ R(FY) + +R(FU) + +(− − R(FZ)) == R(FY) + +(R(FU) + +(− − R(FZ)))

;

L11: Plus0(R) ≫ R(FY) + +00 == R(FY) ;

L12: eqTransitivity4 ⊳ L10 ⊳ L09 ⊳

L11 ≫ R(FY) + +R(FU) + +(− −

R(FZ)) == R(FY) ;

L13: x = x + y − y(R) ≫ R(FX) == R(FX) + +R(FZ) + +(− − R(FZ)) ;

L14: eqTransitivity4 ⊳ L13 ⊳ L04 ⊳

L12 ≫ R(FX) == R(FY) □

[SystemQ lemma NeqAddition(R): ΠFX, FY, FZ: R(FX) ≠ R(FY) ⊢ R(FX)+ +R(FZ) ≠ R(FY) + +R(FZ)]

SystemQ proof of NeqAddition(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY, FZ  ;
L03: Premise ≫  R(FX) ≠ R(FY)  ;

L04: Premise ≫ R(FX) + +R(FZ) == R(FY) +

+R(FZ) ;

L05: ==Reflexivity ≫ R(FZ) == R(FZ) ;

L06: SubtractEquations(R) ⊳ L04 ⊳

L05 ≫ R(FX) == R(FY) ;

L07: FromContradiction ⊳ L06 ⊳

L03 ≫ R(FX) + +R(FZ) ≠ R(FY) +

+R(FZ) ;

L08: Block ≫  End  ;
L09: Arbitrary ≫  FX, FY, FZ  ;

L10: Ded ⊳ L08 ≫

R(FX)  ≠  R(FY)  ⇒

R(FX) + +R(FZ) == R(FY) + +R(FZ) ⇒ R(FX) + +R(FZ) ≠ R(FY) + +R(FZ) ;

L11: Premise ≫ R(FX) ≠ R(FY) ;

L12: MP ⊳ L10 ⊳ L11 ≫ R(FX) + +R(FZ) == R(FY) + +R(FZ) ⇒ R(FX) + +R(FZ) ≠ R(FY) + +R(FZ) ;

L13: prop lemma imply negation ⊳

L12 ≫ R(FX) + +R(FZ) ≠ R(FY) +

+R(FZ) □

———–(22.10.06)

[SystemQ lemma PositiveToRight(Less)(1term)(R): ΠFX, FY: R(FX) << R(FY) ⊢ 00 << R(FY) + +(− − R(FX))]

SystemQ proof of PositiveToRight(Less)(1term)(R):

L01: Arbitrary ≫  FX, FY  ;

L02: Premise ≫  R(FX) << R(FY)  ;
L03: Plus0Left(R) ≫  00 + +R(FX) == R(FX)  ;
L04: ==Symmetry ⊳ L03 ≫  R(FX) == 00 + +R(FX)  ;
L05: SubLessLeft(R) ⊳ L04 ⊳ L02 ≫ 00 + +R(FX) << R(FY)  ;

L06: PositiveToRight(Less)(R) ⊳

L05 ≫ 00 << R(FY) + +(− − R(FX)) □

———–(22.10.06)

[SystemQ lemma To!! ==: ΠM, N , ϵ, FX, FY: ˙¬ (SF(FX, FY))n ⊢ R(FX)!! == R(FY)]

SystemQ proof of To!! ==:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N , ϵ, FX, FY  ;
L03: Premise ≫  R(FX) == R(FY)  ;
L04: From == ⊳L03 ≫  SF(FX, FY)  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  M, N , ϵ, FX, FY  ;

L03: Ded ⊳ L05 ≫

R(FX) == R(FY) ⇒
SF(FX, FY) ;
L07: Premise ≫  ˙¬ (SF(FX, FY))n  ;
L08: MT ⊳ L03 ⊳ L07 ≫  R(FX)!! == R(FY)  □

[SystemQ lemma SwitchTerms(x <= y − z): ΠX , Y, Z: X <= (Y − Z) ⊢ Z <= (Y − X)]

SystemQ proof of SwitchTerms(x <= y − z):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= (Y − Z)  ;
L03: negativeToLeft(Leq) ⊳ L02 ≫ (X + Z) <= Y  ;
L04: plusCommutativity ≫  (X + Z) = (Z + X)  ;
L05: subLeqLeft ⊳ L04 ⊳ L03 ≫  (Z + X) <= Y  ;
L06: PositiveToRight(Leq) ⊳ L05 ≫ Z <= (Y − X)  □

[SystemQ lemma LessNeq(F)(Helper): ΠM, N , ϵ, FX, FY: ∀M: 0 < ϵ ˙∧ (N <= M ⇒ FX[M] <= (FY[M] − ϵ)) ⇒ ˙¬ ((0 < ϵ ⇒ N <= N ⇒ |(FX[N] − FY[N])| < ϵ))n]

SystemQ proof of LessNeq(F)(Helper):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  M, N , ϵ, FX, FY  ;
L03: Premise ≫  {∀M: 0 < ϵ ˙∧ (N <= M ⇒ \atop FX[M] <= (FY[M] − ϵ))  ;}
L04: A4 @ N ⊳ L03 ≫  {0 < ϵ ˙∧ (N <= N ⇒ \atop FX[N] <= (FY[N] − ϵ))  ;}
L05: FirstConjunct ⊳ L04 ≫  0 < ϵ  ;
L06: SecondConjunct ⊳ L04 ≫  {N <= N ⇒ FX[N] <= \atop (FY[N] − ϵ)  ;}
L07: leqReflexivity ≫  N <= N  ;
L08: MP ⊳ L06 ⊳ L07 ≫  FX[N] <= (FY[N] − ϵ)  ;

L09: SwitchTerms(x <=

y − z) ⊳ L08 ≫ ϵ <= (FY[N] − FX[N]) ;

L10: x <= |x| ≫ (FY[N] − FX[N]) <=

|(FY[N] − FX[N])| ;

L11: leqTransitivity ⊳ L09 ⊳ L10 ≫ ϵ <= |(FY[N] − FX[N])|  ;

L12: NumericalDifference ≫ |(FY[N]−FX[N])| = |(FX[N]− FY[N])| ;

L13: subLeqRight ⊳ L12 ⊳ L11 ≫  ϵ <= |(FX[N] − FY[N])|  ;
L14: toNotLess ⊳ L13 ≫  ˙¬ (|(FX[N] − FY[N])| < ϵ)n  ;

L15: ToNegatedDoubleImply ⊳ L05 ⊳ L07 ⊳ L14 ≫

˙¬ ((0 < ϵ ⇒ N <= N ⇒ |(FX[N] − FY[N])| < ϵ))n ;

L16: Block ≫  End  ;
L17: Arbitrary ≫  M, N , ϵ, FX, FY  ;

L18: Ded ⊳ L16 ≫ ∀M: 0 < ϵ ˙∧ (N <= M ⇒

FX[M] <= (FY[M] − ϵ)) ⇒ ˙¬ ((0 < ϵ ⇒ N <= N ⇒ |(FX[N] − FY[N])| < ϵ))n □

[SystemQ lemma LessNeq(F): ΠM, N , ϵ, FX, FY: FX <_{f} FY ⊢ ˙¬ (SF(FX, FY))n] SystemQ proof of LessNeq(F):

L01: Arbitrary ≫  M, N , ϵ, FX, FY  ;
L02: Premise ≫  FX <_{f} FY  ;

L03: Repetition ⊳ L02 ≫ ∃(EPob): ∃n: ∀m: 0 < (EPob) ˙∧ (n <= m ⇒ FX[m] <= (FY[m] − (EPob))) ;

L04: Ded ⊳ L03 ≫  {∃ϵ: ∃N: ∀M: 0 < ϵ ˙∧ (N <= \atop M ⇒ FX[M] <= (FY[M] − ϵ)) ;}

L05: LessNeq(F)(Helper) ≫ ∀M: 0 < ϵ ˙∧ (N <= M ⇒ FX[M] <= (FY[M] − ϵ)) ⇒ ˙¬ ((0 < ϵ ⇒ N <= N ⇒ |(FX[N] − FY[N])| < ϵ))n ;

L06: TwiceExistMP ⊳ L05 ⊳ L04 ≫ {˙¬ ((0 < ϵ ⇒ N <= N ⇒ \atop |(FX[N] − FY[N])| < ϵ))n  ;}
L07: IntroExist @ N ⊳ L06 ≫  {∃M: ˙¬ ((0 < ϵ ⇒ N <= M ⇒ \atop |(FX[M] − FY[M])| < ϵ))n  ;}
L08: Gen ⊳ L07 ≫  ∀N: ∃M: ˙¬ ((0 < ϵ ⇒ N <= ; M ⇒ |(FX[M] − FY[M])| < ; ϵ))n  ;

L09: IntroExist @ ϵ ⊳ L08 ≫  ∃ϵ: ∀N: ∃M: ˙¬ ((0 < ϵ ⇒ N <= ; M ⇒ |(FX[M] − FY[M])| < ; ϵ))n  ;

L10: ToNegatedAEA ⊳ L09 ≫  ˙¬ (∀ϵ: ∃N: ∀M: (0 < ϵ ⇒ N <= ; M ⇒ |(FX[M] − FY[M])| < ; ϵ))n  ;

L11: Ded ⊳ L10 ≫ ˙¬ (∀(EPob): ∃n: ∀m: (0 < (EPob) ⇒ n <= m ⇒ |(FX[m]−FY[m])| < (EPob)))n ;

L12: Repetition ⊳ L11 ≫ ˙¬ (SF(FX, FY))n □

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

SystemQ proof of LessNeq(R):

L01: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  R(FX) << R(FY)  ;
L03: Repetition ⊳ L02 ≫  FX <_{f} FY  ;
L04: LessNeq(F) ⊳ L03 ≫  ˙¬ (SF(FX, FY))n  ;
L05: To!! == ⊳L04 ≫  R(FX)!! == R(FY)  □

[SystemQ lemma PositiveToRight(Less)(1term): ΠX , Y: X < Y ⊢ 0 < (Y − X)]

SystemQ proof of PositiveToRight(Less)(1term):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X < Y  ;
L03: plus0Left ≫  (0 + X) = X  ;
L04: eqSymmetry ⊳ L03 ≫  X = (0 + X)  ;
L05: SubLessLeft ⊳ L04 ⊳ L02 ≫  (0 + X) < Y  ;
L06: PositiveToRight(Less)⊳L05 ≫ 0 < (Y − X)  □

[SystemQ lemma ToLeq(Advanced)(R): ΠFEP, FX, FY: 00 << R(FEP) ⇒ R(FX) + +R(FEP) ≠ R(FY) ⊢ R(FY) <<== R(FX)]

SystemQ proof of ToLeq(Advanced)(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FEP, FX, FY  ;
L03: Premise ≫  R(FX) << R(FY)  ;

L04: PositiveToRight(Less)(1term)(R)⊳

L03 ≫ 00 << R(FY) + +(− − R(FX)) ; L05: PlusCommutativity(R) ≫ R(FX) + +(R(FY) + +(− − R(FX))) = R(FY) + +(− − R(FX)) + +R(FX) ;

L06: Three2threeTerms(R) ≫ R(FY) + +(− − R(FX)) + +R(FX) = R(FY) + +R(FX) + +(− − R(FX)) ;

L07: x = x + y − y(R) ≫ R(FY) = R(FY) + +R(FX) + +(− − R(FX)) ;

L08: ==Symmetry ⊳ L07 ≫ R(FY) + +R(FX) + +(− − R(FX)) == R(FY) ;

L09: eqTransitivity4 ⊳ L05 ⊳ L06 ⊳

L08 ≫ R(FX) + +(R(FY) + +(− −

R(FX))) == R(FY) ;

L10: JoinConjuncts ⊳ L04 ⊳ L09 ≫ 00 << R(FY)++(−−R(FX)) ˙∧ R(FX) + +(R(FY) + +(− − R(FX))) = R(FY) ;

L11: IntroExist @ R(FY) + +(− −

R(FX)) ⊳ L10 ≫ ∃FEP: 00 << R(FEP) ˙∧

R(FX) + +R(FEP) == R(FY) ;

L12: Block ≫  End  ;
L13: Arbitrary ≫  FEP, FX, FY  ;

L03: Ded ⊳ L12 ≫ R(FX) << R(FY) ⇒ ∃FEP: 00 << R(FEP) ˙∧ R(FX) + +R(FEP) == R(FY) ;

L04: Premise ≫ 00 << R(FEP) ⇒ R(FX) +

+R(FEP)!! == R(FY) ;

L05: ToNegatedAnd ⊳ L04 ≫ ˙¬ ((00 << R(FEP) ˙∧ R(FX) + +R(FEP) == R(FY)))n ;

L06: Gen ⊳ L05 ≫ ∀FEP: ˙¬ ((00 << R(FEP) ˙∧ R(FX) + +R(FEP) == R(FY)))n ;

L07: (A )to( E) ⊳ L06 ≫ ˙¬ (∃FEP: 00 << R(FEP) ˙∧ R(FX) + +R(FEP) == R(FY))n ;

L08: MT ⊳ L03 ⊳ L07 ≫  ˙¬ (R(FX) << R(FY))n  ;
L14: FromNotLess(R) ⊳ L08 ≫  R(FY) <<== R(FX)  □

——–(23.10.06)

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

SystemQ proof of LeqNeqLess(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY  ;
L03: Premise ≫  R(FX) <<== R(FY)  ;
L04: Premise ≫  R(FX)!! == R(FY)  ;
L05: Premise ≫  R(FY) <<== R(FX)  ;

L06: LeqAntisymmetry(R) ⊳ L03 ⊳

L05 ≫ R(FX) == R(FY) ;

L07: FromContradiction ⊳ L06 ⊳ L04 ≫

˙¬ (R(FY) <<== R(FX))n ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  FX, FY  ;

L03: Ded ⊳ L08 ≫

R(FX) <<== R(FY) ⇒
R(FX)!! == R(FY) ⇒
R(FY) <<== R(FX) ⇒
˙¬ (R(FY) <<== R(FX))n ;
L04: Premise ≫  R(FX) <<== R(FY)  ;
L05: Premise ≫  R(FX)!! == R(FY)  ;

L06: MP2 ⊳ L03 ⊳ L04 ⊳ L05 ≫

R(FY) <<== R(FX) ⇒
˙¬ (R(FY) <<== R(FX))n ;

L10: prop lemma imply negation ⊳ L06 ≫

˙¬ (R(FY) <<== R(FX))n ;
L11: ToLess(R) ⊳ L10 ≫ R(FX) << R(FY) □

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

SystemQ proof of SubLeqLeft(R):

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

L03: Premise ≫  R(FX) <<== R(FZ)  ;
L04: ==Symmetry ⊳ L02 ≫  R(FY) == R(FX)  ;
L05: lemma eqLeq(R) ⊳ L04 ≫  R(FY) <<== R(FX)  ;

L06: LeqTransitivity(R) ⊳ L05 ⊳

L03 ≫ R(FY) <<== R(FZ) □

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

SystemQ proof of LeqLessTransitivity(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY, FZ  ;
L03: Premise ≫  R(FX) <<== R(FY)  ;
L04: Premise ≫  R(FY) << R(FZ)  ;
L05: Premise ≫  R(FX) == R(FZ)  ;
L06: LessLeq(R) ⊳ L04 ≫  R(FY) <<== R(FZ)  ;
L07: LessNeq(R) ⊳ L04 ≫  R(FY)!! == R(FZ)  ;
L08: SubLeqLeft(R) ⊳ L05 ⊳ L03 ≫ R(FZ) <<== R(FY)  ;

L09: LeqAntisymmetry(R) ⊳ L06 ⊳

L08 ≫ R(FY) == R(FZ) ;

L10: FromContradiction ⊳ L09 ⊳

L07 ≫ R(FX)!! == R(FZ) ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  FX, FY, FZ  ;

L13: Ded ⊳ L11 ≫ R(FX) <<== R(FY) ⇒ R(FY) << R(FZ) ⇒ R(FX) == R(FZ) ⇒ R(FX)!! == R(FZ) ;

L14: Premise ≫  R(FX) <<== R(FY)  ;
L15: Premise ≫  R(FY) << R(FZ)  ;

L16: MP2 ⊳ L13 ⊳ L14 ⊳ L15 ≫ R(FX) == R(FZ) ⇒ R(FX)!! == R(FZ) ;

L17: prop lemma imply negation ⊳

L16 ≫ R(FX)!! == R(FZ) ;

L18: LessLeq(R) ⊳ L15 ≫ R(FY) <<== R(FZ) ;

L19: LeqTransitivity(R) ⊳ L14 ⊳

L18 ≫ R(FX) <<== R(FZ) ;

L20: LeqNeqLess(R) ⊳ L19 ⊳ L17 ≫ R(FX) << R(FZ)  □

———–(23.10.06)

[SystemQ lemma NegativeToLeft(Eq)(R): ΠFX, FY, FZ: R(FX) == R(FY)+ +(− − R(FZ)) ⊢ R(FX) + +R(FZ) == R(FY)]

SystemQ proof of NegativeToLeft(Eq)(R):

L01: Arbitrary ≫ FX, FY, FZ ;

L02: Premise ≫ R(FX) == R(FY) + +(− −

R(FZ)) ;

L03: EqAddition(R) ⊳ L02 ≫ R(FX) + +R(FZ) == R(FY) + +(− − R(FZ)) + +R(FZ) ; L04: Three2threeTerms(R) ≫ R(FY) + +(− − R(FZ)) + +R(FZ) == R(FY)++R(FZ)+ +(− − R(FZ)) ;

L05: x = x + y − y(R) ≫ R(FY) == R(FY) + +R(FZ) + +(− − R(FZ)) ;

L06: ==Symmetry ⊳ L05 ≫ R(FY) + +R(FZ) + +(− − R(FZ)) == R(FY) ;

L07: eqTransitivity4 ⊳ L03 ⊳ L04 ⊳ L06 ≫

R(FX) + +R(FZ) == R(FY) □

[SystemQ lemma NegativeToRight(Less)(R): ΠFX, FY, FZ: R(FX)++(−− R(FY)) << R(FZ) ⊢ R(FX) << R(FZ) + +R(FY)]

SystemQ proof of NegativeToRight(Less)(R):

L01: Arbitrary ≫ FX, FY, FZ ;

L02: Premise ≫ R(FX) + +(− − R(FY)) <<

R(FZ) ;

L03: lessAddition(R) ⊳ L02 ≫ R(FX) + +(− − R(FY)) + +R(FY) << R(FZ) + +R(FY) ;

L04: Three2threeTerms(R) ≫ R(FX) + +(− − R(FY)) + +R(FY) == R(FX) + +R(FY) + +(− − R(FY))

;

L05: x = x + y − y(R) ≫ R(FX) == R(FX) + +R(FY) + +(− − R(FY)) ;

L06: ==Symmetry ⊳ L05 ≫ R(FX) + +R(FY) + +(− − R(FY)) == R(FX) ;

L07: eqTransitivity ⊳ L04 ⊳ L06 ≫ R(FX) + +(− − R(FY)) + +R(FY) == R(FX) ;

L08: SubLessLeft(R) ⊳ L07 ⊳ L03 ≫ R(FX) << R(FZ) + +R(FY) □

[SystemQ lemma !! == Symmetry: ΠFX, FY: R(FX)!! == R(FY) ⊢ R(FY)!! == R(FX)]

SystemQ proof of !! == Symmetry:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY  ;
L03: Premise ≫  R(FY) == R(FX)  ;
L04: ==Symmetry ⊳ L03 ≫  R(FX) == R(FY)  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  FX, FY  ;

L07: Ded ⊳ L05 ≫ R(FY) == R(FX) ⇒ R(FX) == R(FY) ;

L08: Premise ≫  R(FX)!! == R(FY)  ;
L09: MT ⊳ L07 ⊳ L08 ≫  R(FY)!! == R(FX)  □

————-(23.10.06)

[SystemQ lemma NegativeToRight(Eq)(R): ΠFX, FY, FZ: R(FX) + +(− − R(FY)) == R(FZ) ⊢ R(FX) == R(FZ) + +R(FY)]

SystemQ proof of NegativeToRight(Eq)(R):

L01: Arbitrary ≫  FX, FY, FZ  ;

L02: Premise ≫ R(FX) + +(− − R(FY)) ==

R(FZ) ;

L03: EqAddition(R) ⊳ L02 ≫ R(FX) + +(− − R(FY)) + +R(FY) == R(FZ) + +R(FY) ;

L04: x = x + y − y(R) ≫ R(FX) == R(FX) + +R(FY) + +(− − R(FY)) ;

L05: Three2threeTerms(R) ≫ R(FX) + +R(FY) + +(− − R(FY)) == R(FX) + +(− − R(FY)) + +R(FY) ;

L06: eqTransitivity4 ⊳ L04 ⊳ L05 ⊳ L03 ≫

R(FX) == R(FZ) + +R(FY) □

[SystemQ lemma NegativeToRight(Eq)(1term)(R): ΠFX, FY: R(FX)++(−− R(FY)) == 00 ⊢ R(FX) == R(FY)]

SystemQ proof of NegativeToRight(Eq)(1term)(R):

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

L03: NegativeToRight(Eq)(R) ⊳

L02 ≫ R(FX) == 00 + +R(FY) ;

L04: Plus0Left(R) ≫ 00 + +R(FY) == R(FY) ;
L05: eqTransitivity ⊳ L03 ⊳ L04 ≫ R(FX) == R(FY)  □

[SystemQ lemma DoubleMinus(R): ΠFX: (− − (− − R(FX))) == R(FX)] SystemQ proof of DoubleMinus(R):

L01: Arbitrary ≫  FX  ;
L02: Negative(R) ≫  {(− − R(FX)) + +(− − (− − \atop R(FX))) == 00  ;}

L03: PlusCommutativity(R) ≫

(− − R(FX)) + +(− − (− −
R(FX))) == (− − (− −
R(FX))) + +(− − R(FX)) ;

L04: ==Symmetry ⊳ L03 ≫

(− − (− − R(FX))) + +(− −
R(FX)) == (− − R(FX)) +
+(− − (− − R(FX))) ;
L05: eqTransitivity ⊳ L04 ⊳ L02 ≫ {(− − (− − R(FX))) + +(− − \atop R(FX)) == 00  ;}

L06: NegativeToRight(Eq)(1term)(R)⊳

L05 ≫ (− − (− − R(FX))) == R(FX) □ [SystemQ lemma UniqueNegative(R): ΠFX, FY, FZ: R(FX) + +R(FY) ==

00 ⊢ R(FX) + +R(FZ) == 00 ⊢ R(FY) == R(FZ)]

SystemQ proof of UniqueNegative(R):

L01: Arbitrary ≫  FX, FY, FZ  ;
L02: Premise ≫  R(FX) + +R(FY) == 00  ;
L03: Premise ≫  R(FX) + +R(FZ) == 00  ;

L04: PlusCommutativity(R) ≫ R(FY) + +R(FX) == R(FX) + +R(FY) ;

L05: eqTransitivity ⊳ L04 ⊳ L02 ≫ R(FY) + +R(FX) == 00  ;

L06: PositiveToRight(Eq)(R) ⊳

L05 ≫ R(FY) == 00 + +(− − R(FX)) ;

L07: PlusCommutativity(R) ≫ R(FZ) + +R(FX) == R(FX) + +R(FZ) ;

L08: eqTransitivity ⊳ L07 ⊳ L03 ≫ R(FZ) + +R(FX) == 00  ;

L09: PositiveToRight(Eq)(R) ⊳

L08 ≫ R(FZ) == 00 + +(− − R(FX)) ;

L10: ==Symmetry ⊳ L09 ≫  00 + +(− − R(FX)) == R(FZ) ;
L11: eqTransitivity ⊳ L06 ⊳ L10 ≫ R(FY) == R(FZ)  □

[SystemQ lemma SubtractEquationsLeft(R): ΠFX, FY, FZ, FU: R(FX)++R(FZ) == R(FY) + +R(FU) ⊢ R(FX) == R(FY) ⊢ R(FZ) == R(FU)]

SystemQ proof of SubtractEquationsLeft(R):

L01: Arbitrary ≫ FX, FY, FZ, FU ;

L02: Premise ≫ R(FX) + +R(FZ) == R(FY) +

+R(FU) ;

L03: Premise ≫ R(FX) == R(FY) ;

L04: PlusCommutativity(R) ≫ R(FZ) + +R(FX) == R(FX) + +R(FZ) ;

L05: PlusCommutativity(R) ≫ R(FY) + +R(FU) == R(FU) + +R(FY) ;

L06: eqTransitivity4 ⊳ L04 ⊳ L02 ⊳

L05 ≫ R(FZ) + +R(FX) == R(FU) +

+R(FY) ;

L07: SubtractEquations(R) ⊳ L06 ⊳

L03 ≫ R(FZ) == R(FU) □

[SystemQ lemma EqNegated(R): ΠFX, FY: R(FX) == R(FY) ⊢ (−−R(FX)) == (− − R(FY))]

SystemQ proof of EqNegated(R):

L01: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  R(FX) == R(FY)  ;
L03: Negative(R) ≫  R(FX) + +(− − R(FX)) == 00 ;
L04: Negative(R) ≫  R(FY) + +(− − R(FY)) == 00 ;
L05: ==Symmetry ⊳ L04 ≫  00 == R(FY) + +(− − R(FY)) ;

L06: eqTransitivity ⊳ L03 ⊳ L05 ≫

R(FX) + +(− − R(FX)) ==
R(FY) + +(− − R(FY)) ;

L07: SubtractEquationsLeft(R) ⊳ L06 ⊳ L02 ≫

(− − R(FX)) == (− − R(FY)) □

[SystemQ lemma NeqNegated(R): ΠFX, FY: R(FX)!! == R(FY) ⊢ (− − R(FX))!! == (− − R(FY))]

SystemQ proof of NeqNegated(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY  ;
L03: Premise ≫  R(FX)!! == R(FY)  ;
L04: Premise ≫  (− − R(FX)) == (− − R(FY)) ;
L05: EqNegated(R) ⊳ L04 ≫  {(−−(−−R(FX))) == (−−(−− \atop R(FY)))  ;}
L06: DoubleMinus(R) ≫  (− − (− − R(FX))) == R(FX) ;
L07: ==Symmetry ⊳ L06 ≫  R(FX) == (− − (− − R(FX))) ;

L08: DoubleMinus(R) ≫  (− − (− − R(FY))) == R(FY) ;

L09: eqTransitivity4 ⊳ L07 ⊳ L05 ⊳

L08 ≫ R(FX) == R(FY) ;

L10: FromContradiction ⊳ L09 ⊳

L03 ≫ (− − R(FX))!! == (− − R(FY)) ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  FX, FY  ;

L13: Ded ⊳ L11 ≫ R(FX)!! == R(FY) ⇒ (− − R(FX)) == (− − R(FY)) ⇒ ˙¬ ((− − R(FX)) == (− − R(FY)))n ;

L14: Premise ≫ R(FX)!! == R(FY) ;

L15: MP ⊳ L13 ⊳ L14 ≫

(− − R(FX)) == (− −
R(FY)) ⇒ ˙¬ ((− − R(FX)) ==
(− − R(FY)))n ;

L16: prop lemma imply negation ⊳ L15 ≫

˙¬ ((− − R(FX)) == (− − R(FY)))n □

———–(23.10.06)

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

SystemQ proof of SubLeqRight(R):

L01: Arbitrary ≫  FX, FY, FZ  ;
L02: Premise ≫  R(FX) == R(FY)  ;
L03: Premise ≫  R(FZ) <<== R(FX)  ;
L04: lemma eqLeq(R) ⊳ L02 ≫  R(FX) <<== R(FY)  ;

L05: LeqTransitivity(R) ⊳ L03 ⊳

L04 ≫ R(FZ) <<== R(FY) □

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

SystemQ proof of LeqNegated(R):

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

L03: leqAddition(R) ⊳ L02 ≫

R(FX) + +(− − R(FX)) <<==
R(FY) + +(− − R(FX)) ;
L04: Negative(R) ≫  R(FX) + +(− − R(FX)) == 00 ;
L05: SubLeqLeft(R) ⊳ L04 ⊳ L03 ≫ {00 <<== R(FY) + +(− − \atop R(FX))  ;}

L06: PlusCommutativity(R) ≫ R(FY)++(−−R(FX)) == (−− R(FX)) + +R(FY) ;

L07: SubLeqRight(R)⊳L06⊳L05 ≫ {00 <<== (− − R(FX)) + \atop +R(FY)  ;}

L08: leqAddition(R) ⊳ L07 ≫ 00 + +(− − R(FY)) <<== (−−R(FX))++R(FY)++(−− R(FY)) ;

L09: Plus0Left(R) ≫  {00 + +(− − R(FY)) == (− − \atop R(FY))  ;}

L10: x = x + y − y(R) ≫

(−−R(FX)) == (−−R(FX))+
+R(FY) + +(− − R(FY)) ;

L11: ==Symmetry ⊳ L10 ≫

(−−R(FX))++R(FY)++(−−
R(FY)) == (− − R(FX)) ;

L12: SubLeqLeft(R) ⊳ L09 ⊳ L08 ≫ (− − R(FY)) <<== (− − R(FX)) + +R(FY) + +(− − R(FY)) ;

L13: SubLeqRight(R)⊳L11⊳L12 ≫ {(− − R(FY)) <<== (− − \atop R(FX))  □}

[SystemQ lemma LessNegated(R): ΠFX, FY: R(FX) << R(FY) ⊢ (−−R(FY)) << (− − R(FX))]

SystemQ proof of LessNegated(R):

L01: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  R(FX) << R(FY)  ;
L03: LessLeq(R) ⊳ L02 ≫  R(FX) <<== R(FY)  ;
L04: LeqNegated(R) ⊳ L03 ≫  {(− − R(FY)) <<== (− − \atop R(FX))  ;}
L05: LessNeq(R) ⊳ L02 ≫  R(FX)!! == R(FY)  ;
L06: NeqNegated(R) ⊳ L05 ≫  (− − R(FX))!! == (− − R(FY)) ;
L07: !! == Symmetry ⊳ L06 ≫  (− − R(FY))!! == (− − R(FX)) ;
L08: LeqNeqLess(R) ⊳ L04 ⊳ L07 ≫ (− − R(FY)) << (− − R(FX)) □

[SystemQ lemma − 0 = 0(R): (− − 00) == 00]

SystemQ proof of − 0 = 0(R):

L01: Negative(R) ≫  00 + +(− − 00) == 00  ;
L02: Plus0(R) ≫  00 + +00 == 00  ;

L03: UniqueNegative(R) ⊳ L01 ⊳

L02 ≫ (− − 00) == 00 □

[SystemQ lemma NegativeNegated(R): ΠFX: R(FX) << 00 ⊢ 00 << (− − R(FX))]

SystemQ proof of NegativeNegated(R):

L01: Arbitrary ≫  FX  ;
L02: Premise ≫  R(FX) << 00  ;
L03: LessNegated(R) ⊳ L02 ≫  (− − 00) << (− − R(FX))  ;
L04: −0 = 0(R) ≫  (− − 00) == 00  ;
L05: SubLessLeft(R) ⊳ L04 ⊳ L03 ≫ 00 << (− − R(FX))  □

[SystemQ lemma LeqTotality(R): ΠFX, FY: R(FX) <<== R(FY) ˙∨ R(FY) <<== R(FX)]

SystemQ proof of LeqTotality(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY  ;
L03: Premise ≫  ˙¬ (R(FX) <<== R(FY))n  ;
L04: ToLess(R) ⊳ L03 ≫  R(FY) << R(FX)  ;
L05: LessLeq(R) ⊳ L04 ≫  R(FY) <<== R(FX)  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  FX, FY  ;

L03: Ded ⊳ L06 ≫

˙¬ (R(FX) <<== R(FY))n ⇒
R(FY) <<== R(FX) ;

L08: Repetition ⊳ L03 ≫

R(FX) <<== R(FY) ˙∨
R(FY) <<== R(FX) □

[SystemQ lemma FromLeqGeq(R): ΠA, FX, FY: R(FX) <<== R(FY) ⇒ A ⊢ R(FY) <<== R(FX) ⇒ A ⊢ A]

SystemQ proof of FromLeqGeq(R):

L01: Arbitrary ≫  A, FX, FY  ;
L02: Premise ≫  R(FX) <<== R(FY) ⇒ A  ;
L03: Premise ≫  R(FY) <<== R(FX) ⇒ A  ;

L04: LeqTotality(R) ≫

R(FX) <<== R(FY) ˙∨
R(FY) <<== R(FX) ;

L05: FromDisjuncts ⊳ L04 ⊳ L02 ⊳

L03 ≫ A □

——–(24.10.06)

[SystemQ lemma FromLess(R): ΠFX, FY: R(FX) << R(FY) ⊢ ˙¬ (R(FY) <<== R(FX))n]

SystemQ proof of FromLess(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY  ;
L03: Premise ≫  R(FX) << R(FY)  ;
L04: Premise ≫  R(FY) <<== R(FX)  ;
L05: LessLeq(R) ⊳ L03 ≫  R(FX) <<== R(FY)  ;

L06: LeqAntisymmetry(R) ⊳ L05 ⊳

L04 ≫ R(FX) == R(FY) ;

L07: LessNeq(R) ⊳ L03 ≫ R(FX)!! == R(FY) ;

L08: FromContradiction ⊳ L06 ⊳ L07 ≫

˙¬ (R(FY) <<== R(FX))n ;
L09: Block ≫  End  ;
L10: Arbitrary ≫  FX, FY  ;

L03: Ded ⊳ L09 ≫

R(FX) << R(FY) ⇒
R(FY) <<== R(FX) ⇒
˙¬ (R(FY) <<== R(FX))n ;
L04: Premise ≫ R(FX) << R(FY) ;

L05: MP ⊳ L03 ⊳ L04 ≫

R(FY) <<== R(FX) ⇒
˙¬ (R(FY) <<== R(FX))n ;

L11: prop lemma imply negation ⊳ L05 ≫

˙¬ (R(FY) <<== R(FX))n □

[SystemQ lemma from <<==: ΠFX, FY: R(FX) <<== R(FY) ⊢ FX ≤_{f} FY]

SystemQ proof of from <<==:

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

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

L04: Repetition ⊳ L03 ≫  FX <_{f} FY ˙∨ R(FX) = R(FY) ;

L05: Block ≫  Begin  ;
L06: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  FX <_{f} FY  ;
L07: WeakenOr2 ⊳ L02 ≫  FX <_{f} FY ˙∨ SF(FX, FY)  ;
L08: Block ≫  End  ;
L09: Block ≫  Begin  ;
L10: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  R(FX) = R(FY)  ;
L03: From == ≫  SF(FX, FY)  ;
L11: WeakenOr1 ⊳ L03 ≫  FX <_{f} FY ˙∨ SF(FX, FY)  ;
L12: Block ≫  End  ;

L13: Ded ⊳ L08 ≫

FX <_{f} FY ⇒ FX <_{f} FY ˙∨
SF(FX, FY) ;

L14: Ded ⊳ L12 ≫ R(FX) = R(FY) ⇒ FX <_{f} FY ˙∨ SF(FX, FY) ;

L15: FromDisjuncts ⊳ L04 ⊳ L13 ⊳ L14 ≫

FX <_{f} FY ˙∨ SF(FX, FY) ;
L16: Repetition ⊳ L15 ≫ FX ≤_{f} FY □

[SystemQ lemma NonnegativeNumerical(F): ΠFX: 0f ≤_{f} FX ⊢ |fFX| = FX] SystemQ proof of NonnegativeNumerical(F):

L01: Arbitrary ≫  FX  ;
L02: Premise ≫  0f ≤_{f} FX  ;

L03: NumericalF ≫

(0f ≤_{f} FX ⇒ |fFX| = FX) ˙∧
( ˙¬ (0f ≤_{f} FX)n ⇒ |fFX| =
−_{f}FX) ;
L04: FirstConjunct ⊳ L03 ≫  0f ≤_{f} FX ⇒ |fFX| = FX  ;
L05: MP ⊳ L04 ⊳ L02 ≫  |fFX| = FX  □

[SystemQ lemma NonnegativeNumerical(R): ΠFX: 00 <<== R(FX) ⊢ |rR(FX)| = R(FX)]

SystemQ proof of NonnegativeNumerical(R):

L01: Arbitrary ≫  FX  ;
L02: Premise ≫  00 <<== R(FX)  ;
L03: from <<== ⊳L02 ≫  0f ≤_{f} FX  ;

L04: NonnegativeNumerical(F) ⊳

L03 ≫ |fFX| = FX ;

L05: (Adgic)SameR ⊳ L04 ≫  R(|fFX|) = R(FX)  ;
L06: Repetition ⊳ L05 ≫  |rR(FX)| = R(FX)  □

[SystemQ lemma to <<==: ΠFX, FY: FX ≤_{f} FY ⊢ R(FX) <<== R(FY)] SystemQ proof of to <<==:

L01: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  FX ≤_{f} FY  ;
L03: Repetition ⊳ L02 ≫  FX <_{f} FY ˙∨ SF(FX, FY)  ;
L04: Block ≫  Begin  ;
L05: Arbitrary ≫  FX, FY  ;
L06: Premise ≫  FX <_{f} FY  ;
L07: Repetition ⊳ L06 ≫  R(FX) << R(FY)  ;

L08: WeakenOr2 ⊳ L07 ≫ R(FX) << R(FY) ˙∨ R(FX) = R(FY) ;

L09: Block ≫  End  ;
L10: Block ≫  Begin  ;
L11: Arbitrary ≫  FX, FY  ;
L02: Premise ≫  SF(FX, FY)  ;
L03: To == ⊳L02 ≫  R(FX) = R(FY)  ;

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

L13: Block ≫ End ;

L06: Ded ⊳ L09 ≫ FX <_{f} FY ⇒ R(FX) << R(FY) ˙∨ R(FX) = R(FY) ;

L07: Ded ⊳ L13 ≫ SF(FX, FY) ⇒ R(FX) << R(FY) ˙∨ R(FX) = R(FY) ;

L14: FromDisjuncts ⊳ L03 ⊳ L06 ⊳

L07 ≫ R(FX) << R(FY) ˙∨ R(FX) =

R(FY) ;

L15: Repetition ⊳ L14 ≫ R(FX) <<== R(FY) □

[SystemQ lemma NegativeNumerical(F): ΠFX: ˙¬ (0f ≤_{f} FX)n ⊢ |fFX| = −_{f}FX]

SystemQ proof of NegativeNumerical(F):

L01: Arbitrary ≫  FX  ;
L02: Premise ≫  ˙¬ (0f ≤_{f} FX)n  ;

L03: NumericalF ≫

(0f ≤_{f} FX ⇒ |fFX| = FX) ˙∧
( ˙¬ (0f ≤_{f} FX)n ⇒ |fFX| =
−_{f}FX) ;

L04: SecondConjunct ⊳ L03 ≫

˙¬ (0f ≤_{f} FX)n ⇒ |fFX| =
−_{f}FX ;
L05: MP ⊳ L04 ⊳ L02 ≫ |fFX| = −_{f}FX □

[SystemQ lemma NegativeNumerical(R): ΠFX: R(FX) << 00 ⊢ |rR(FX)| == (− − R(FX))]

SystemQ proof of NegativeNumerical(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX  ;
L03: Premise ≫  R(FX) << 00  ;
L04: Premise ≫  0f ≤_{f} FX  ;
L05: FromLess(R) ⊳ L03 ≫  ˙¬ (00 <<== R(FX))n  ;
L06: to <<== ⊳L04 ≫  00 <<== R(FX)  ;

L07: FromContradiction ⊳ L06 ⊳

L05 ≫ ˙¬ (0f ≤_{f} FX)n ;

L08: Block ≫  End  ;
L09: Arbitrary ≫  FX  ;

L03: Ded ⊳ L08 ≫ R(FX) << 00 ⇒ 0f ≤_{f} FX ⇒ ˙¬ (0f ≤_{f} FX)n ;

L04: Premise ≫  R(FX) << 00  ;
L05: MP ⊳ L03 ⊳ L04 ≫  0f ≤_{f} FX ⇒ ˙¬ (0f ≤_{f} FX)n  ;

L06: prop lemma imply negation ⊳

L05 ≫ ˙¬ (0f ≤_{f} FX)n ;

L10: NegativeNumerical(F) ≫  |fFX| = −_{f}FX  ;
L11: (Adgic)SameR ⊳ L10 ≫  R(|fFX|) = R(−_{f}FX)  ;
L12: Repetition ⊳ L11 ≫  |rR(FX)| = (− − R(FX))  □

[SystemQ lemma 0 <= |x|(R): ΠFX: 00 <<== |rR(FX)|]

SystemQ proof of 0 <= |x|(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX  ;
L03: Premise ≫  00 <<== R(FX)  ;

L04: NonnegativeNumerical(R) ⊳ L03 ≫

|rR(FX)| == R(FX) ;
L05: ==Symmetry ⊳ L04 ≫ R(FX) == |rR(FX)| ;
L06: SubLeqRight(R)⊳L05⊳L03 ≫ 00 <<== |rR(FX)|  ;
L07: Block ≫  End  ;
L08: Block ≫  Begin  ;
L09: Arbitrary ≫  FX  ;
L10: Premise ≫  ˙¬ (00 <<== R(FX))n  ;
L11: ToLess(R) ⊳ L10 ≫  R(FX) << 00  ;
L12: NegativeNumerical(R)⊳L11 ≫ |rR(FX)| == (− − R(FX))  ;
L13: ==Symmetry ⊳ L12 ≫ (− − R(FX)) == |rR(FX)| ;
L14: NegativeNegated(R) ⊳ L11 ≫ 00 << (− − R(FX))  ;
L15: LessLeq(R) ⊳ L14 ≫ 00 <<== (− − R(FX)) ;
L16: SubLeqRight(R)⊳L13⊳L15 ≫ 00 <<== |rR(FX)|  ;
L17: Block ≫  End  ;
L18: Arbitrary ≫  FX  ;
L19: Ded ⊳ L07 ≫  {00 <<== R(FX) ⇒ 00 <<== \atop |rR(FX)|  ;}

L20: Ded ⊳ L17 ≫

˙¬ (00 <<== R(FX))n ⇒
00 <<== |rR(FX)| ;
L21: FromNegations ⊳ L19 ⊳ L20 ≫ 00 <<== |rR(FX)|  □

———–(24.10.06)

[SystemQ lemma PositiveNegated(R): ΠFX: 00 << R(FX) ⊢ (−−R(FX)) << 00]

SystemQ proof of PositiveNegated(R):

L01: Arbitrary ≫  FX  ;
L02: Premise ≫  00 << R(FX)  ;
L03: LessNegated(R) ⊳ L02 ≫  (− − R(FX)) << (− − 00)  ;
L04: −0 = 0(R) ≫  (− − 00) == 00  ;
L05: SubLessRight(R)⊳L04⊳L03 ≫ (− − R(FX)) << 00  □

[SystemQ lemma AddEquations(R): ΠFX, FY, FZ, FU: R(FX) == R(FY) ⊢ R(FZ) == R(FU) ⊢ R(FX) + +R(FZ) == R(FY) + +R(FU)]

SystemQ proof of AddEquations(R):

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

L03: Premise ≫  R(FZ) == R(FU)  ;

L04: EqAddition(R) ⊳ L02 ≫ R(FX) + +R(FZ) == R(FY) + +R(FZ) ;

L05: EqAdditionLeft(R) ⊳ L03 ≫ R(FY) + +R(FZ) == R(FY) + +R(FU) ;

L06: eqTransitivity ⊳ L04 ⊳ L05 ≫ R(FX) + +R(FZ) == R(FY) + +R(FU) □

[SystemQ lemma DistributionOut(R): ΠFX, FY, FZ: R(FX)∗∗R(FY)++R(FX)∗ ∗R(FZ) == R(FX) ∗ ∗(R(FY) + +R(FZ))]

SystemQ proof of DistributionOut(R):

L01: Arbitrary ≫ FX, FY, FZ ;

L02: Distribution(R) ≫ R(FX)∗∗(R(FY)++R(FZ)) == R(FX) ∗ ∗R(FY) + +R(FX) ∗ ∗R(FZ) ;

L03: ==Symmetry ⊳ L02 ≫ R(FX) ∗ ∗R(FY) + +R(FX) ∗ ∗R(FZ) == R(FX) ∗ ∗(R(FY) + +R(FZ)) □

[SystemQ lemma x∗0+x = x(R): ΠFX: R(FX)∗∗00++R(FX) == R(FX)] SystemQ proof of x ∗ 0 + x = x(R):

L01: Arbitrary ≫  FX  ;
L02: Times1(R) ≫  R(FX) ∗ ∗01 == R(FX)  ;
L03: ==Symmetry ⊳ L02 ≫  R(FX) == R(FX) ∗ ∗01  ;

L04: EqAdditionLeft(R) ⊳ L03 ≫ R(FX) ∗ ∗00 + +R(FX) == R(FX) ∗ ∗00 + +R(FX) ∗ ∗01 ;

L05: Distribution(R) ≫ R(FX)∗∗(00++01) == R(FX)∗ ∗00 + +R(FX) ∗ ∗01 ;

L06: ==Symmetry ⊳ L05 ≫ R(FX)∗∗00++R(FX)∗∗01 == R(FX) ∗ ∗(00 + +01) ;

L07: Plus0Left(R) ≫ 00 + +01 == 01 ;

L08: EqMultiplicationLeft(R) ⊳

L07 ≫ R(FX)∗∗(00++01) == R(FX)∗ ∗01 ;

L09: eqTransitivity5 ⊳ L04 ⊳ L06 ⊳

L08 ⊳ L02 ≫ R(FX) ∗ ∗00 + +R(FX) ==

R(FX) □

——–(24.10.06) [SystemQ lemma x ∗ 0 = 0(R)(fff): ΠFX: R(FX) ∗ ∗00 == 00] SystemQ proof of x ∗ 0 = 0(R)(fff):

L01: Arbitrary ≫ FX ;

L02: x = x + (y − y)(R) ≫ R(FX) ∗ ∗00 == R(FX) ∗ ∗00 + +(R(FX) + +(− − R(FX))) ;

L03: PlusAssociativity(R) ≫ R(FX) ∗ ∗00 + +R(FX) + +(− − R(FX)) == R(FX) ∗ ∗00 + +(R(FX) + +(− − R(FX))) ;

L04: ==Symmetry ⊳ L03 ≫ R(FX)∗∗00++(R(FX)++(−− R(FX))) == R(FX) ∗ ∗00 + +R(FX) + +(− − R(FX)) ; L05: x ∗ 0 + x = x(R) ≫ R(FX) ∗ ∗00 + +R(FX) == R(FX) ;

L06: EqAddition(R) ⊳ L05 ≫ R(FX) ∗ ∗00 + +R(FX) + +(− − R(FX)) == R(FX) + +(− − R(FX)) ;

L07: Negative(R) ≫  R(FX) + +(− − R(FX)) == 00 ;

L08: eqTransitivity5 ⊳ L02 ⊳ L04 ⊳

L06 ⊳ L07 ≫ R(FX) ∗ ∗00 == 00 □

[SystemQ lemma Times(−1)(R): ΠFX: R(FX)∗∗(−−01) == (−−R(FX))] SystemQ proof of Times(−1)(R):

L01: Arbitrary ≫  FX  ;
L02: Negative(R) ≫  01 + +(− − 01) == 00  ;
L03: PlusCommutativity(R) ≫  {(− − 01) + +01 == 01 + +(− − \atop 01)  ;}
L04: eqTransitivity ⊳ L03 ⊳ L02 ≫ (− − 01) + +01 == 00  ;

L05: EqMultiplicationLeft(R) ⊳

L04 ≫ R(FX) ∗ ∗((− − 01) + +01) == R(FX) ∗ ∗00 ;

L06: x ∗ 0 = 0(R)(fff) ≫  R(FX) ∗ ∗00 == 00  ;
L07: eqTransitivity ⊳ L05 ⊳ L06 ≫ R(FX)∗∗((−−01)++01) == 00 ;

L08: Distribution(R) ≫

R(FX) ∗ ∗((− − 01) + +01) ==
R(FX)∗∗(−−01)++R(FX)∗∗01 ;

L09: ==Symmetry ⊳ L08 ≫ R(FX) ∗ ∗(− − 01) + +R(FX) ∗ ∗01 == R(FX) ∗ ∗((− − 01) + +01) ;

L10: eqTransitivity ⊳ L09 ⊳ L07 ≫ {R(FX) ∗ ∗(− − 01) + +R(FX) ∗ \atop ∗01 == 00  ;}

L11: PositiveToRight(Eq)(R) ⊳

L10 ≫ R(FX) ∗ ∗(− − 01) == 00 + +(− − (R(FX) ∗ ∗01)) ;

L12: Plus0Left(R) ≫  {00 + +(− − (R(FX) ∗ ∗01)) == \atop (− − (R(FX) ∗ ∗01))  ;}
L13: eqTransitivity ⊳ L11 ⊳ L12 ≫ {R(FX) ∗ ∗(− − 01) == (− − \atop (R(FX) ∗ ∗01))  ;}
L14: Times1(R) ≫  R(FX) ∗ ∗01 == R(FX)  ;
L15: EqNegated(R) ⊳ L14 ≫  {(− − (R(FX) ∗ ∗01)) == (− − \atop R(FX))  ;}
L16: eqTransitivity ⊳ L13 ⊳ L15 ≫ {R(FX) ∗ ∗(− − 01) == (− − \atop R(FX))  □}

[SystemQ lemma Times(−1)Left(R): ΠFX: (− − 01) ∗ ∗R(FX) == (− − R(FX))]

SystemQ proof of Times(−1)Left(R):

L01: Arbitrary ≫  FX  ;
L02: Times(−1)(R) ≫  {R(FX) ∗ ∗(− − 01) == (− − \atop R(FX))  ;}
L03: TimesCommutativity(R) ≫  {(− − 01) ∗ ∗R(FX) == R(FX) ∗ \atop ∗(− − 01)  ;}

L04: eqTransitivity ⊳ L03 ⊳ L02 ≫ {(− − 01) ∗ ∗R(FX) == (− − \atop R(FX))  □}

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

[SystemQ lemma − x − y = −(x + y)(R): ΠFX, FY: (− − R(FX)) + +(− − R(FY)) == (− − (R(FX) + +R(FY)))]

SystemQ proof of − x − y = −(x + y)(R):

L01: Arbitrary ≫  FX, FY  ;
L02: Times(−1)Left(R) ≫  {(− − 01) ∗ ∗R(FX) == (− − \atop R(FX))  ;}
L03: Times(−1)Left(R) ≫  {(− − 01) ∗ ∗R(FY) == (− − \atop R(FY))  ;}

L04: AddEquations(R) ⊳ L02 ⊳

L03 ≫ (−−01)∗∗R(FX)++(−−01)∗

∗R(FY) == (− − R(FX)) +
+(− − R(FY)) ;

L05: ==Symmetry ⊳ L04 ≫

(− − R(FX)) + +(− −
R(FY)) == (−−01)∗∗R(FX)+
+(− − 01) ∗ ∗R(FY) ;

L06: DistributionOut(R) ≫

(− − 01) ∗ ∗R(FX) + +(− −
01) ∗ ∗R(FY) == (− − 01) ∗
∗(R(FX) + +R(FY)) ;

L07: Times(−1)Left(R) ≫ (− − 01) ∗ ∗(R(FX) + +R(FY)) == (− − (R(FX) + +R(FY))) ;

L08: eqTransitivity4 ⊳ L05 ⊳ L06 ⊳

L07 ≫ (− − R(FX)) + +(− −

R(FY)) == (− − (R(FX) +

+R(FY))) □

[SystemQ lemma LessTotality(R): ΠFX, FY: R(FX) << R(FY) ˙∨ R(FX) == R(FY) ˙∨ R(FY) << R(FX)]

SystemQ proof of LessTotality(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY  ;
L03: Premise ≫  ˙¬ (R(FX) << R(FY))n  ;
L04: Premise ≫  R(FX)!! == R(FY)  ;
L05: FromNotLess(R) ⊳ L03 ≫  R(FY) <<== R(FX)  ;
L06: !! == Symmetry ⊳ L04 ≫  R(FY)!! == R(FX)  ;
L07: LeqNeqLess(R) ⊳ L05 ⊳ L06 ≫ R(FY) << R(FX)  ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  FX, FY  ;

L10: Ded ⊳ L08 ≫

˙¬ (R(FX) << R(FY))n ⇒
R(FX)!! == R(FY) ⇒
R(FY) << R(FX) ;

L11: Repetition ⊳ L10 ≫ R(FX) << R(FY) ˙∨ R(FX) == R(FY) ˙∨ R(FY) << R(FX) □

[SystemQ lemma SameNumerical(R): ΠFX, FY: R(FX) == R(FY) ⊢ |rR(FX)| == |rR(FY)|]

SystemQ proof of SameNumerical(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX, FY  ;
L03: Premise ≫  00 <<== R(FX)  ;
L04: Premise ≫  R(FX) == R(FY)  ;

L05: NonnegativeNumerical(R) ⊳ L03 ≫

|rR(FX)| == R(FX) ;
L06: SubLeqRight(R)⊳L04⊳L03 ≫ 00 <<== R(FY)  ;

L07: NonnegativeNumerical(R) ⊳ L06 ≫

|rR(FY)| == R(FY) ;
L08: ==Symmetry ⊳ L07 ≫ R(FY) == |rR(FY)| ;

L09: eqTransitivity4 ⊳ L05 ⊳ L04 ⊳ L08 ≫

|rR(FX)| == |rR(FY)| ;

L10: Block ≫  End  ;
L11: Block ≫  Begin  ;
L12: Arbitrary ≫  FX, FY  ;
L13: Premise ≫  ˙¬ (00 <<== R(FX))n  ;
L14: Premise ≫  R(FX) == R(FY)  ;
L15: ToLess(R) ⊳ L13 ≫  R(FX) << 00  ;
L16: NegativeNumerical(R)⊳L15 ≫ |rR(FX)| == (− − R(FX))  ;
L17: SubLessLeft(R) ⊳ L14 ⊳ L15 ≫ R(FY) << 00  ;
L18: NegativeNumerical(R)⊳L17 ≫ |rR(FY)| == (− − R(FY))  ;
L19: ==Symmetry ⊳ L18 ≫ (− − R(FY)) == |rR(FY)| ;
L20: EqNegated(R) ⊳ L14 ≫  (− − R(FX)) == (− − R(FY)) ;

L21: eqTransitivity4 ⊳ L16 ⊳ L20 ⊳ L19 ≫

|rR(FX)| == |rR(FY)| ;

L22: Block ≫  End  ;
L23: Arbitrary ≫  FX, FY  ;
L24: Premise ≫  R(FX) == R(FY)  ;

L25: Ded ⊳ L10 ≫ 00 <<== R(FX) ⇒ R(FX) == R(FY) ⇒ |rR(FX)| == |rR(FY)| ;

L26: Ded ⊳ L22 ≫ ˙¬ (00 <<== R(FX))n ⇒ R(FX) == R(FY) ⇒ |rR(FX)| == |rR(FY)| ;

L27: FromNegations ⊳ L25 ⊳ L26 ≫ R(FX) == R(FY) ⇒ |rR(FX)| == |rR(FY)| ;

L28: MP ⊳ L27 ⊳ L24 ≫ |rR(FX)| == |rR(FY)| □

[SystemQ lemma MinusNegated(R): ΠFX, FY: (−−(R(FX)++(−−R(FY)))) == R(FY) + +(− − R(FX))]

SystemQ proof of MinusNegated(R):

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

L03: EqAddition(R) ⊳ L02 ≫ (− − (− − R(FY))) + +(− − R(FX)) == R(FY) + +(− − R(FX)) ;

L04: ==Symmetry ⊳ L03 ≫

R(FY)++(−−R(FX)) == (−−
(− − R(FY))) + +(− − R(FX)) ;

L05: −x − y = −(x + y)(R) ≫ (− − (− − R(FY))) + +(− − R(FX)) == (−−((−−R(FY))+ +R(FX))) ;

L06: PlusCommutativity(R) ≫

(− − R(FY)) + +R(FX) ==
R(FX) + +(− − R(FY)) ;

L07: EqNegated(R) ⊳ L06 ≫

(− − ((− − R(FY)) +
+R(FX))) == (− − (R(FX) +
+(− − R(FY)))) ;

L08: eqTransitivity4 ⊳ L04 ⊳ L05 ⊳

L07 ≫ R(FY)++(−−R(FX)) == (−−

(R(FX) + +(− − R(FY)))) ;

L09: ==Symmetry ⊳ L08 ≫

(− − (R(FX) + +(− −
R(FY)))) == R(FY) + +(− −
R(FX)) □

———–(24.10.06)

[SystemQ lemma PositiveNumerical(R): ΠFX: 00 << R(FX) ⊢ |rR(FX)| == R(FX)]

SystemQ proof of PositiveNumerical(R):

L01: Arbitrary ≫  FX  ;
L02: Premise ≫  00 << R(FX)  ;
L03: LessLeq(R) ⊳ L02 ≫  00 <<== R(FX)  ;

L04: NonnegativeNumerical(R) ⊳ L03 ≫

|rR(FX)| == R(FX) □

[SystemQ lemma SignNumerical(+)(R): ΠFX: 00 << R(FX) ⊢ |rR(FX)| == |r(− − R(FX))|]

SystemQ proof of SignNumerical(+)(R):

L01: Arbitrary ≫  FX  ;
L02: Premise ≫  00 << R(FX)  ;
L03: PositiveNumerical(R) ⊳ L02 ≫ |rR(FX)| == R(FX)  ;
L04: PositiveNegated(R) ⊳ L02 ≫ (− − R(FX)) << 00 ;
L05: NegativeNumerical(R)⊳L04 ≫ {|r(− − R(FX))| == (− − (− − \atop R(FX)))  ;}
L06: DoubleMinus(R) ≫  (− − (− − R(FX))) == R(FX) ;
L07: eqTransitivity ⊳ L05 ⊳ L06 ≫ |r(− − R(FX))| == R(FX)  ;
L08: ==Symmetry ⊳ L07 ≫ R(FX) == |r(− − R(FX))| ;
L09: eqTransitivity ⊳ L03 ⊳ L08 ≫ |rR(FX)| == |r(− − R(FX))| □

[SystemQ lemma SignNumerical(R): ΠFX: |rR(FX)| == |r(− − R(FX))|] SystemQ proof of SignNumerical(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX  ;
L03: Premise ≫  R(FX) << 00  ;

L04: NegativeNegated(R) ⊳ L03 ≫ 00 << (− − R(FX))  ;

L05: SignNumerical(+)(R) ⊳ L04 ≫

|r(− − R(FX))| == |r(− − (− −
R(FX)))| ;
L06: DoubleMinus(R) ≫  (− − (− − R(FX))) == R(FX) ;

L07: SameNumerical(R) ⊳ L06 ≫

|r(− − (− − R(FX)))| ==
|rR(FX)| ;
L08: eqTransitivity ⊳ L05 ⊳ L07 ≫ |r(− − R(FX))| == |rR(FX)|  ;
L09: ==Symmetry ⊳ L08 ≫  |rR(FX)| == |r(− − R(FX))|  ;
L10: Block ≫  End  ;
L11: Block ≫  Begin  ;
L12: Arbitrary ≫  FX  ;
L03: Premise ≫  R(FX) == 00  ;
L04: EqNegated(R) ⊳ L03 ≫  (− − R(FX)) == (− − 00)  ;
L05: −0 = 0(R) ≫  (− − 00) == 00  ;
L06: ==Symmetry ⊳ L03 ≫  00 == R(FX)  ;

L07: eqTransitivity4 ⊳ L04 ⊳ L05 ⊳

L06 ≫ (− − R(FX)) == R(FX) ;

L08: ==Symmetry ⊳ L07 ≫  R(FX) == (− − R(FX))  ;
L13: SameNumerical(R) ⊳ L08 ≫  |rR(FX)| == |r(− − R(FX))|  ;
L14: Block ≫  End  ;
L15: Block ≫  Begin  ;
L16: Arbitrary ≫  FX  ;
L03: Premise ≫  00 << R(FX)  ;
L17: SignNumerical(+)(R) ⊳ L03 ≫ |rR(FX)| == |r(− − R(FX))|  ;
L18: Block ≫  End  ;
L19: Arbitrary ≫  FX  ;

L20: Ded ⊳ L10 ≫

R(FX) << 00 ⇒ |rR(FX)| ==
|r(− − R(FX))| ;

L21: Ded ⊳ L14 ≫

R(FX) == 00 ⇒ |rR(FX)| ==
|r(− − R(FX))| ;

L22: Ded ⊳ L18 ≫

00 << R(FX) ⇒ |rR(FX)| ==
|r(− − R(FX))| ;

L23: LessTotality(R) ≫

R(FX) << 00 ˙∨ R(FX) ==
00 ˙∨ 00 << R(FX) ;

L24: From3Disjuncts ⊳ L23 ⊳ L20 ⊳ L21 ⊳ L22 ≫

|rR(FX)| == |r(− − R(FX))| □

[SystemQ lemma NumericalDifference(R): ΠFX, FY: |rR(FX)++(−−R(FY))| == |rR(FY) + +(− − R(FX))|]

SystemQ proof of NumericalDifference(R):

L01: Arbitrary ≫ FX, FY ;

L02: SignNumerical(R) ≫

|rR(FX) + +(− − R(FY))| ==
|r(−−(R(FX)++(−−R(FY))))| ;

L03: MinusNegated(R) ≫ (− − (R(FX) + +(− − R(FY)))) == R(FY) + +(− − R(FX)) ; L04: SameNumerical(R) ⊳ L03 ≫

|r(− − (R(FX) + +(− −
R(FY))))| == |rR(FY) +
+(− − R(FX))| ;

L05: eqTransitivity ⊳ L02 ⊳ L04 ≫

|rR(FX) + +(− − R(FY))| ==
|rR(FY) + +(− − R(FX))| □

——–(25.10.06)

[SystemQ lemma x <= |x|(R): ΠFX: R(FX) <<== |rR(FX)|] SystemQ proof of x <= |x|(R):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  FX  ;
L03: Premise ≫  00 <<== R(FX)  ;
L04: NonnegativeNumerical(R) ≫  |rR(FX)| == R(FX)  ;
L05: ==Symmetry ⊳ L04 ≫  R(FX) == |rR(FX)|  ;
L06: lemma eqLeq(R) ⊳ L05 ≫  R(FX) <<== |rR(FX)|  ;
L07: Block ≫  End  ;
L08: Block ≫  Begin  ;
L09: Arbitrary ≫  FX  ;
L03: Premise ≫  R(FX) <<== 00  ;
L04: 0 <= |x|(R) ≫  00 <<== |rR(FX)|  ;

L10: LeqTransitivity(R) ⊳ L03 ⊳ L04 ≫

R(FX) <<== |rR(FX)| ;
L11: Block ≫  End  ;
L12: Arbitrary ≫  FX  ;

L03: Ded ⊳ L07 ≫ 00 <<== R(FX) ⇒ R(FX) <<== |rR(FX)|

;

L04: Ded ⊳ L11 ≫ R(FX) <<== 00 ⇒ R(FX) <<== |rR(FX)|

;

L13: FromLeqGeq(R)⊳L03⊳L04 ≫ R(FX) <<== |rR(FX)|  □

a

venter—-

Priority table Preassociative [sup2], [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}(∗)], [kvanti], [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)], [sup], [ToNegatedAnd(1)], [UniqueNegative], [DoubleMinus], [MinusNegated], [eqReflexivity], [eqSymmetry], [eqTransitivity], [eqTransitivity4], [eqTransitivity5], [eqTransitivity6], [AddEquations], [SubtractEquations], [SubtractEquationsLeft], [MultiplyEquations], [EqNegated], [PositiveToRight(Eq)], [PositiveToLeft(Eq)(1term)], [NegativeToLeft(Eq)], [NonreciprocalToRight(Eq)(1term)], [PlusAssociativity(4terms)], [LessNeq], [NeqSymmetry], [NeqNegated], [SubNeqRight], [SubNeqLeft], [NegativeToRight(Neq)(1term)], [NeqAddition], [NeqMultiplication], [NonzeroProduct(2)], [UStelescope(+1)], [TelescopeBound(Base)], [TelescopeBound(Indu)], [TelescopeBound], [IntervalSize(Base)], [IntervalSize(Indu)], [IntervalSize], [XS < US], [lemma USdecreasing(+1)], [CloseUS], [CloseUS(n + 1)], [AllNegated(Imply)], [ExistNegated(Imply)], [IntroExist(Helper)], [IntroExist], [ExistMP], [ExistMP2], [TwiceExistMP], [TwiceExistMP2], [EAE − MP], [AddAll], [AddExist(Helper1)], [AddExist(Helper2)], [AddExist], [AddExist(SimpleAnt)], [AddExist(Simple)], [AddEAE], [AEA − negated], [EEA − negated], [Induction], [leqAntisymmetry], [leqTransitivity], [leqAddition], [leqMultiplication], [Reciprocal], [Equality], [eqLeq], [eqAddition], [eqMultiplication], [LeqMultiplicationLeft], [LeqLessEq], [LessLeq], [FromLeqGeq], [subLeqRight], [subLeqLeft], [Leq + 1], [PositiveToRight(Leq)], [PositiveToRight(Leq)(1term)], [lemma negativeToRight(Leq)], [PositiveToLeft(Leq)], [negativeToLeft(Leq)], [negativeToLeft(Leq)(1term)], [LeqAdditionLeft], [leqSubtraction], [leqSubtractionLeft], [thirdGeq], [LeqNegated], [AddEquations(Leq)], [MultiplyEquations(Leq)], [ThirdGeqSeries], [LeqNeqLess], [FromLess], [ToLess], [fromNotLess], [toNotLess], [NegativeLessPositive], [leqLessTransitivity], [LessLeqTransitivity], [LessTransitivity], [LessTotality], [SubLessRight], [SubLessLeft], [SwitchTerms(x < y − z)], [SwitchTerms(x − y < z)], [LessAddition], [LessAdditionLeft], [LessMultiplication], [LessMultiplicationLeft], [LessDivision], [PositiveToRight(Less)], [PositiveToLeft(Less)], [NegativeToLeft(Less)], [NegativeToRight(Less)], [AddEquations(Less)], [AddEquations(LeqLess)], [reciprocalToLeft(Less)], [LessNegated], [PositiveNonzero], [PositiveNegated], [NonpositiveNegated], [NegativeNegated], [NonnegativeNegated], [PositiveHalved], [PositiveInverted], [NonnegativeNumerical], [NegativeNumerical], [PositiveNumerical], [lemma nonpositiveNumerical], [|0| = 0], [0 <= |x|], [x <= |x|], [FromPositiveNumerical], [SameNumerical], [SignNumerical(+)], [SignNumerical], [ToNumericalLess], [FromNumericalGreater], [NumericalDifference], [NumericalDifferenceLess(Helper)], [NumericalDifferenceLess], [SplitNumericalSumHelper], [splitNumericalSum(++)], [splitNumericalSum(−−)], [splitNumericalSum(+ − small)], [splitNumericalSum(+ − big)], [splitNumericalSum(+−)], [splitNumericalSum(−+)], [splitNumericalSum], [SplitNumericalProduct(++)], [SplitNumericalProduct(+−)], [SplitNumericalProduct], [insertMiddleTerm(Numerical)], [insertTwoMiddleTerms(Numerical)], [Three2twoTerms], [Three2threeTerms], [Three2twoFactors], [Three2threeFactors], [Times(−1)], [Times(−1)Left], [MaxLeq(1)], [MaxLeq(2)], [LessThanMax], [x + y = zBackwards], [x ∗ y = zBackwards], [x = x + (y − y)], [x = x + y − y], [x = x ∗ y ∗ (1/y)], [insertMiddleTerm(Sum)], [insertTwoMiddleTerms(Sum)], [insertMiddleTerm(Difference)], [x ∗ 0 + x = x], [x ∗ 0 = 0], [NonnegativeFactors], [NonzeroFactors], [PositiveFactors], [PlusTimesMinus], [MinusTimesMinus], [(−1) ∗ (−1) + (−1) ∗ 1 = 0], [(−1) ∗ (−1) = 1], [0 < 1Helper], [0 < 1], [0 < 2], [0 < 3], [0 < 1/2], [0 < 1/3], [TwoWholes], [ThreeWholes], [TwoHalves], [ThreeThirds], [−x − y = −(x + y)], [−x ∗ y = −(x ∗ y)], [−0 = 0], [SFsymmetry], [SFtransitivity], [f2R(Plus)], [f2R(Times)], [<< TransitivityHelper(Q)], [<< Transitivity], [<<== Reflexivity], [<<== AntisymmetryHelper(Q)], [FromNot < f(Weak)(Helper)], [FromNot < f(Weak)], [FromNot < f(Strong)(Helper2)], [FromNot < f(Strong)(Helper)], [FromNot < f(Strong)], [fromNotSameF(Strongest)(Helper2)], [fromNotSameF(Strongest)(Helper)], [fromNotSameF(Strongest)], [ToLess(F)(Helper)], [ToLess(F)], [FromNot <<], [ToLess(R)], [FromNotSameF(Weak)(Helper)], [FromNotSameF(Weak)], [FromNotLess(F)], [== Addition], [== AdditionLeft], [Fpart − Bounded(Base)], [Fpart − Bounded(InduHelper)], [Fpart − Bounded(Indu)], [Fpart − Bounded], [F − Bounded(Helper)], [F − Bounded], [SameFmultiplication(Helper)], [SameFmultiplication], [EqMultiplication(R)], [EqMultiplicationLeft(R)], [x ∗ 0 = 0(F)], [x ∗ 0 = 0(R)], [LessMultiplication(F)(Helper2)], [LessMultiplication(F)(Helper)], [LessMultiplication(F)], [LessMultiplication(R)], [LeqMultiplication(R)], [PlusAssociativity(F)], [Plus0(F)], [PlusCommutativity(F)], [TimesAssociativity(F)], [Times1f], [Cauchy(2)(Helper)], [Cauchy(2)], [ReciprocalFnonzero], [(Eventually = f)2sameF(Helper)], [(Eventually = f)2sameF], [FromNotSameF(Strong)(Helper2)], [FromNotSameF(Strong)(Helper)], [FromNotSameF(Strong)], [SameFreciprocal(Helper)], [SameFreciprocal], [From!! ==], [Reciprocal(R)], [TimesCommutativity(F)], [Distribution(F)], [FromMax(1)], [FromMax(2)], [ToNegatedAnd], [DistributionOut], [DistributionOutLeft], [DistributionLeft], [FromNotLess(R)], [CartProdIsRelation], [FromSubset], [SubsetIsRelation], [ToSeries], [FromSeries], [SeriesSubsetCP], [ValueType], [RemoveOr], [FromSingleton], [InPair(1)], [InPair(2)], [SameMember(2)], [ToBinaryUnion(1)], [ToBinaryUnion(2)], [FromOrderedPair(TwoLevels)], [ToCartProd(Helper)], [ToCartProd], [NonreciprocalToRight(Eq)], [NonreciprocalToLeft(Eq)(1term)], [SameReciprocal], [CPseparationIsRelation], [OrderedPairEquality], [ReciprocalIsFunction], [ReciprocalIsTotal], [ReciprocalIsRationalSeries], [CrsIsRelation], [CrsIsFunction], [CrsIsTotal], [CrsIsSeries], [CrsLookup], [0f], [1f], [ToSingleton], [FromSameSingleton], [SingletonmembersEqual], [UnequalsNotInSingleton], [NonsingletonmembersUnequal], [FromOrderedPair], [FromOrderedPair(1)], [FromOrderedPair(2)], [FromCartProd], [FromCartProd(1)], [FromCartProd(2)], [sameOrderedPair], [InSeriesHelper], [InSeries], [To = f(Subset)(Helper)], [To = f(Subset)], [To = f], [productIsFunction], [productIsTotal], [ProductIsRationalSeries], [TimesF], [−x + (1/2)x = −(1/2)x], [PositiveTripled], [PositiveDividedBy3], [|x − x| = 0], [1 < 2], [1/3 < 2/3], [(1/3)x + (1/3)x = (2/3)x], [(2/3)x + (1/3)x = x], [−x + (2/3)x = −(1/3)x], [−(1/3)x − (1/3)x = −(2/3)x], [−x + (1/3)x = −(2/3)x], [PreserveLessGreater], [ClosetolessIsLess], [SubLessLeft(F)], [SubLessLeft(R)], [ClosetogreaterIsGreater], [SubLessRight(F)], [SubLessRight(R)], [plus0Left], [times1Left], [EqAdditionLeft], [EqMultiplicationLeft], [PlusF(Sym)], [TimesF(Sym)], [SameSeries(Gen)], [EqualsSameF], [LeqReflexivity(R)], [LeqTotality(R)], [PositiveToLeft(Eq)], [ExpZero(Exact)], [SameExp(Base)], [SameExp(Indu)], [SameExp], [(1/2)(x + y) − x = (1/2)(y − x)], [y − (1/2)(x + y) = (1/2)(y − x)], [BSzero(Exact)], [SameBS(2)(Base)], [SameBS(2)(Indu)], [SameBS(2)], [NegativeToLeft(Less)(1term)], [BS(+1)], [BSbound(Exact)(Base)], [BSbound(Exact)(Indu)], [BSbound(Exact)], [BSbound], [UStelescope(Zero)(Exact)], [SameTelescope(2)(Base)], [SameTelescope(2)(Indu)], [SameTelescope(2)], [Exp(+1)], [PositiveBase(Base)], [PositiveBase(Indu)], [PositiveBase], [TelescopeNumerical(Base)], [TelescopeNumerical(Indu)], [TelescopeNumerical], [(+1)IsPositive(N)], [DistributionOut(Minus)], [PositiveToRight(Eq)(1term)], [SameSeries(NumDiff)], [ToNegatedDoubleImply], [AddNegatedAll], [(A)to( E )(Imply)], [(E)to( A )(Imply)], [(E )to( A)(Imply)], [ToNegatedAEA], [Three2threeTerms(R)], [LessNeq(F)(Helper)], [LessNeq(F)], [LessNeq(R)], [x = x + (y − y)(R)], [x = x + y − y(R)], [SubtractEquations(R)], [NeqAddition(R)], [PositiveToRight(Less)(R)], [PositiveToRight(Less)(1term)(R)], [LeqNeqLess(R)], [SubLeqLeft(R)], [ToLeq(Advanced)(R)], [LeqLessTransitivity(R)], [NegativeToLeft(Eq)(R)], [NegativeToRight(Less)(R)], [!! == Symmetry], [SwitchTerms(x <= y − z)], [Plus0Left(R)], [PositiveToRight(Eq)(R)], [EqAdditionLeft(R)], [Three2twoTerms(R)], [To!! ==], [PositiveToRight(Less)(1term)], [(A )to( E)], [NegativeToRight(Eq)(R)], [NegativeToRight(Eq)(1term)(R)], [DoubleMinus(R)], [UniqueNegative(R)], [SubtractEquationsLeft(R)], [EqNegated(R)], [NeqNegated(R)], [−0 = 0(R)], [NegativeNegated(R)], [FromLeqGeq(R)], [0 <= |x|(R)], [PositiveNegated(R)], [AddEquations(R)], [Times(−1)(R)], [Times(−1)Left(R)], [−x − y = −(x + y)(R)], [LessTotality(R)], [SameNumerical(R)], [MinusNegated(R)], [PositiveNumerical(R)], [SignNumerical(+)(R)], [NonnegativeNumerical(R)], [NegativeNumerical(R)], [LeqNegated(R)], [LessNegated(R)], [SubLeqRight(R)], [FromLess(R)], [DistributionOut(R)], [x ∗ 0 + x = x(R)], [x ∗ 0 = 0(R)(fff)], [SignNumerical(R)], [NumericalDifference(R)], [x <= |x|(R)], [USlimitIsUpperBound(Helper)], [USlimitIsUpperBound], [(−1) ∗ (−1) + (−1) ∗ 1 = 0(R)], [(−1) ∗ (−1) = 1(R)], [0 < 1Helper(R)], [0 < 1(R)], [ExpZero(Exact)(R)], [PositiveBase(R)(Base)], [Three2twoFactors(R)], [x = x ∗ y ∗ (1/y)(R)], [NeqMultiplication(R)], [LessTransitivity(R)], [0 < 2(R)], [SameExp(R)(Base)], [SameExp(R)(Indu)], [SameExp(R)], [SubNeqLeft(R)], [SubNeqRight(R)], [NonzeroFactors(R)], [NonnegativeFactors(R)], [PositiveFactors(R)], [LessDivision(R)], [0 < 1/2(R)], [PositiveToRight(Eq)(1term)(R)], [Exp(+1)(R)], [PositiveBase(R)(Indu)], [PositiveBase(R)], [−x ∗ y = −(x ∗ y)(R)], [PositiveToLeft(Eq)(R)], [Times1Left(R)], [x + x = 2 ∗ x(R)], [(1/2)x + (1/2)x = x(R)], [DistributionOut(Minus)(R)], [(1/2)(x + y) − x = (1/2)(y − x)(R)], [IntervalSize(R)(Base)], [LessMultiplicationLeft(R)], [NegativeToLeft(Less)(R)], [NegativeToLeft(Less)(1term)(R)], [y − (1/2)(x + y) = (1/2)(y − x)(R)], [IntervalSize(R)(Indu)], [IntervalSize(R)], [XSlessUS(R)], [USdecreasing(+1)(R)], [ExpUnbounded(Base)], [ExpUnbounded(Indu)], [ExpUnbounded], [1 <= x + 1(N)], [ExpNonzero(Base)], [ExpNonzero(Indu)], [ExpNonzero], [ExpNonzero(2)], [HalfBase(Base)], [HalfBase(Indu)], [MultiplyEquations(R)], [NonreciprocalToRight(Eq)(1term)(R)], [PositiveNonzero(R)], [NonzeroProduct(2)(R)], [HalfBase], [Three2threeFactors(R)], [x ∗ y = zBackwards(R)], [PositiveInverted(R)], [ReciprocalToRight(Less)(R)], [ReciprocalToRight(Less)(1term)(R)], [NonreciprocalToLeft(Less)(R)], [1 < x ∗ y(R)], [SwitchFactors(1/x < y)(R)], [SmallHalving], [IntervalSize(anyPositive)], [USdecreasing(+n)(Base)], [USdecreasing(+n)(Indu)], [USdecreasing(+n)], [USdecreasing], [LeqAdditionLeft(R)], [ToNotLess(R)], [LimitOfUSIsLeq], [SubtractEquations(Less)(R)], [SubtractEquationsLeft(Less)(R)], [LessNegated(Negative)(R)], [FromNegatedAnd(Imply)], [RemoveDoubleNeg(Consequent)], [FromNotUpperBound], [LeqNUB], [USlimitIsLeastUpperBound(Helper)], [USlimitIsLeastUpperBound], [ExistMP3], [GreaterPositive(N)], [ysFClose(Helper)], [ysFClose], [ysFCauchy(Helper)], [ysFCauchy], [from <<==], [to <<==], [NonnegativeNumerical(F)], [NegativeNumerical(F)]; Preassociative [tester1], [tester2], [tester3], [tester4], [tester5], [tester6]; 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

([LeqTotality(R) →^{pyk} “lemma leqTotality(R)”] [PositiveToLeft(Eq) →^{pyk} “lemma positiveToLeft(Eq)”] [ExpZero(Exact) →^{pyk} “lemma expZero exact”] [SameExp(Base) →^{pyk} “lemma sameExp base”] [SameExp(Indu) →^{pyk} “lemma sameExp indu”] [SameExp →^{pyk} “lemma sameExp”] [(1/2)(x + y) − x = (1/2)(y − x) →^{pyk} “lemma (1/2)(x+y)-x=(1/2)(y-x)”] [y − (1/2)(x + y) = (1/2)(y − x) →^{pyk} “lemma y-(1/2)(x+y)=(1/2)(y-x)”] [BSzero(Exact) →^{pyk} “lemma base(1/2)Sum zero exact”] [SameBS(2)(Base) →^{pyk} “lemma sameBase(1/2)Sum second base”] [SameBS(2)(Indu) →^{pyk} “lemma sameBase(1/2)Sum second indu”] [SameBS(2) →^{pyk} “lemma sameBase(1/2)Sum second”] [NegativeToLeft(Less)(1term) →^{pyk} “lemma negativeToLeft(Less)(1 term)”] [BS(+1) →^{pyk} “lemma base(1/2)Sum(+1)”] [BSbound(Exact)(Base) →^{pyk} “lemma base(1/2)Sum exact bound base”] [BSbound(Exact)(Indu) →^{pyk} “lemma base(1/2)Sum exact bound indu”] [BSbound(Exact) →^{pyk} “lemma base(1/2)Sum exact bound”] [BSbound →^{pyk} “lemma base(1/2)Sum bound”] [UStelescope(Zero)(Exact) →^{pyk} “lemma UStelescope zero exact”] [SameTelescope(2)(Base) →^{pyk} “lemma sameTelescope second base”] [SameTelescope(2)(Indu) →^{pyk} “lemma sameTelescope second indu”] [SameTelescope(2) →^{pyk} “lemma sameTelescope second”] [Exp(+1) →^{pyk} “lemma exp(+1)”] [PositiveBase(Base) →^{pyk} “lemma positiveBase base”] [PositiveBase(Indu) →^{pyk} “lemma positiveBase indu”] [PositiveBase →^{pyk} “lemma positiveBase”] [TelescopeNumerical(Base) →^{pyk} “lemma telescopeNumerical base”] [TelescopeNumerical(Indu) →^{pyk} “lemma telescopeNumerical indu”] [TelescopeNumerical →^{pyk} “lemma telescopeNumerical”] [(+1)IsPositive(N) →^{pyk} “lemma +1IsPositive(N)”] [DistributionOut(Minus) →^{pyk} “lemma distributionOut(Minus)”] [PositiveToRight(Eq)(1term) →^{pyk} “lemma positiveToRight(Eq)(1 term)”] [SameSeries(NumDiff) →^{pyk} “lemma sameSeries(NumDiff)”] [ToNegatedDoubleImply →^{pyk} “prop lemma to negated double imply”] [AddNegatedAll →^{pyk} “pred lemma addNegatedAll”] [(A)to( E )(Imply) →^{pyk} “pred lemma (A)to(˜ E˜ )(Imply)”] [(E)to( A )(Imply) →^{pyk} “pred lemma (E)to(˜ A˜ )(Imply)”] [(E )to( A)(Imply) →^{pyk} “pred lemma (E˜ )to(˜ A)(Imply)”] [ToNegatedAEA →^{pyk} “pred lemma toNegatedAEA”] [Three2threeTerms(R) →^{pyk} “lemma three2threeTerms(R)”] [LessNeq(F)(Helper) →^{pyk} “lemma lessNeq(F) helper”] [LessNeq(F) →^{pyk} “lemma lessNeq(F)”] [LessNeq(R) →^{pyk} “lemma lessNeq(R)”] [x = x + (y − y)(R) →^{pyk} “lemma x=x+(y-y)(R)”] [x = x + y − y(R) →^{pyk} “lemma x=x+y-y(R)”] [SubtractEquations(R) →^{pyk} “lemma subtractEquations(R)”] [NeqAddition(R) →^{pyk} “lemma neqAddition(R)”] [PositiveToRight(Less)(R) →^{pyk} “lemma positiveToRight(Less)(R)”] [PositiveToRight(Less)(1term)(R) →^{pyk} “lemma positiveToRight(Less)(1 term)(R)”] [LeqNeqLess(R) →^{pyk} “lemma leqNeqLess(R)”] [SubLeqLeft(R) →^{pyk} “lemma subLeqLeft(R)”] [ToLeq(Advanced)(R) →^{pyk} “lemma toLeq(Advanced)(R)”] [LeqLessTransitivity(R) →^{pyk} “lemma leqLessTransitivity(R)”] [NegativeToLeft(Eq)(R) →^{pyk} “lemma negativeToLeft(Eq)(R)”] [NegativeToRight(Less)(R) →^{pyk} “lemma negativeToRight(Less)(R)”] [!! == Symmetry →^{pyk} “lemma !!==Symmetry”] [SwitchTerms(x <= y − z) →^{pyk} “lemma switchTerms(x<=y-z)”] [Plus0Left(R) →^{pyk} “lemma plus0Left(R)”] [PositiveToRight(Eq)(R) →^{pyk} “lemma positiveToRight(Eq)(R)”] [EqAdditionLeft(R) →^{pyk} “lemma eqAdditionLeft(R)”] [Three2twoTerms(R) →^{pyk} “lemma three2twoTerms(R)”] [To!! == →^{pyk} “lemma to!!==”] [PositiveToRight(Less)(1term) →^{pyk} “lemma positiveToRight(Less)(1 term)”] [(A )to( E) →^{pyk} “pred lemma (A˜ )to(˜ E)”] [NegativeToRight(Eq)(R) →^{pyk} “lemma negativeToRight(Eq)(R)”] [NegativeToRight(Eq)(1term)(R) →^{pyk} “lemma negativeToRight(Eq)(1 term)(R)”] [DoubleMinus(R) →^{pyk} “lemma doubleMinus(R)”] [UniqueNegative(R) →^{pyk} “lemma uniqueNegative(R)”] [SubtractEquationsLeft(R) →^{pyk} “lemma subtractEquationsLeft(R)”] [EqNegated(R) →^{pyk} “lemma eqNegated(R)”] [NeqNegated(R) →^{pyk} “lemma neqNegated(R)”] [−0 = 0(R) →^{pyk} “lemma -0=0(R)”] [NegativeNegated(R) →^{pyk} “lemma negativeNegated(R)”] [FromLeqGeq(R) →^{pyk} “lemma from leqGeq(R)”] [0 <= |x|(R) →^{pyk} “lemma 0<=|x|(R)”] [PositiveNegated(R) →^{pyk} “lemma positiveNegated(R)”] [AddEquations(R) →^{pyk} “lemma addEquations(R)”] [Times(−1)(R) →^{pyk} “lemma times(-1)(R)”] [Times(−1)Left(R) →^{pyk} “lemma times(-1)Left(R)”] [−x − y = −(x + y)(R) →^{pyk} “lemma -x-y=-(x+y)(R)”] [LessTotality(R) →^{pyk} “lemma lessTotality(R)”] [SameNumerical(R) →^{pyk} “lemma sameNumerical(R)”] [MinusNegated(R) →^{pyk} “lemma minusNegated(R)”] [PositiveNumerical(R) →^{pyk} “lemma positiveNumerical(R)”] [SignNumerical(+)(R) →^{pyk} “lemma signNumerical(+)(R)”] [NonnegativeNumerical(R) →^{pyk} “lemma nonnegativeNumerical(R)”] [NegativeNumerical(R) →^{pyk} “lemma negativeNumerical(R)”] [LeqNegated(R) →^{pyk} “lemma leqNegated(R)”] [LessNegated(R) →^{pyk} “lemma lessNegated(R)”] [SubLeqRight(R) →^{pyk} “lemma subLeqRight(R)”] [FromLess(R) →^{pyk} “lemma fromLess(R)”] [DistributionOut(R) →^{pyk} “lemma distributionOut(R)”] [x ∗ 0 + x = x(R) →^{pyk} “lemma x∗0+x=x(R)”] [x ∗ 0 = 0(R)(fff) →^{pyk} “lemma x∗0=0(R)fff”] [SignNumerical(R) →^{pyk} “lemma signNumerical(R)”] [NumericalDifference(R) →^{pyk} “lemma numericalDifference(R)”] [x <= |x|(R) →^{pyk} “lemma x<=|x|(R)”] [USlimitIsUpperBound(Helper) →^{pyk} “lemma USlimitIsUpperBound helper”] [USlimitIsUpperBound →^{pyk} “lemma USlimitIsUpperBound”] [(−1) ∗ (−1) + (−1) ∗ 1 = 0(R) →^{pyk} “lemma (-1)∗(-1)+(-1)∗1=0(R)”] [(−1) ∗ (−1) = 1(R) →^{pyk} “lemma (-1)∗(-1)=1(R)”] [0 < 1Helper(R) →^{pyk} “lemma 0<1Helper(R)”] [0 < 1(R) →^{pyk} “lemma 0<1(R)”] [ExpZero(Exact)(R) →^{pyk} “lemma expZero exact(R)”] [PositiveBase(R)(Base) →^{pyk} “lemma positiveBase(R) base”] [Three2twoFactors(R) →^{pyk} “lemma three2twoFactors(R)”] [x = x ∗ y ∗ (1/y)(R) →^{pyk} “lemma x=x∗y∗(1/y)(R)”] [NeqMultiplication(R) →^{pyk} “lemma neqMultiplication(R)”] [LessTransitivity(R) →^{pyk} “lemma lessTransitivity(R)”] [0 < 2(R) →^{pyk} “lemma 0<2(R)”] [SameExp(R)(Base) →^{pyk} “lemma sameExp(R) base”] [SameExp(R)(Indu) →^{pyk} “lemma sameExp(R) indu”] [SameExp(R) →^{pyk} “lemma sameExp(R)”] [SubNeqLeft(R) →^{pyk} “lemma subNeqLeft(R)”] [SubNeqRight(R) →^{pyk} “lemma subNeqRight(R)”] [NonzeroFactors(R) →^{pyk} “lemma nonzeroFactors(R)”] [NonnegativeFactors(R) →^{pyk} “lemma nonnegativeFactors(R)”] [PositiveFactors(R) →^{pyk} “lemma positiveFactors(R)”] [LessDivision(R) →^{pyk} “lemma lessDivision(R)”] [0 < 1/2(R) →^{pyk} “lemma 0<1/2(R)”] [PositiveToRight(Eq)(1term)(R) →^{pyk} “lemma positiveToRight(Eq)(1 term)(R)”] [Exp(+1)(R) →^{pyk} “lemma exp(+1)(R)”] [PositiveBase(R)(Indu) →^{pyk} “lemma positiveBase(R) indu”] [PositiveBase(R) →^{pyk} “lemma positiveBase(R)”] [−x ∗ y = −(x ∗ y)(R) →^{pyk} “lemma -x∗y=-(x∗y)(R)”] [PositiveToLeft(Eq)(R) →^{pyk} “lemma positiveToLeft(Eq)(R)”] [Times1Left(R) →^{pyk} “lemma times1Left(R)”] [x + x = 2 ∗ x(R) →^{pyk} “lemma x+x=2∗x(R)”] [(1/2)x + (1/2)x = x(R) →^{pyk} “lemma (1/2)x+(1/2)x=x(R)”] [DistributionOut(Minus)(R) →^{pyk} “lemma distributionOut(Minus)(R)”] [(1/2)(x + y) − x = (1/2)(y − x)(R) →^{pyk} “lemma (1/2)(x+y)-x=(1/2)(y-x)(R)”] [IntervalSize(R)(Base) →^{pyk} “lemma intervalSize(R) base”] [LessMultiplicationLeft(R) →^{pyk} “lemma lessMultiplicationLeft(R)”] [NegativeToLeft(Less)(R) →^{pyk} “lemma negativeToLeft(Less)(R)”] [NegativeToLeft(Less)(1term)(R) →^{pyk} “lemma negativeToLeft(Less)(1 term)(R)”] [y − (1/2)(x + y) = (1/2)(y − x)(R) →^{pyk} “lemma y-(1/2)(x+y)=(1/2)(y-x)(R)”] [IntervalSize(R)(Indu) →^{pyk} “lemma intervalSize(R) indu”] [IntervalSize(R) →^{pyk} “lemma intervalSize(R)”] [XSlessUS(R) →^{pyk} “lemma XSlessUS(R)”] [USdecreasing(+1)(R) →^{pyk} “lemma USdecreasing(+1)(R)”] [ExpUnbounded(Base) →^{pyk} “lemma expUnbounded base”] [ExpUnbounded(Indu) →^{pyk} “lemma expUnbounded indu”] [ExpUnbounded →^{pyk} “lemma expUnbounded”] [1 <= x + 1(N) →^{pyk} “lemma 1<=x+1(N)”] [ExpNonzero(Base) →^{pyk} “lemma expNonzero base”] [ExpNonzero(Indu) →^{pyk} “lemma expNonzero indu”] [ExpNonzero →^{pyk} “lemma expNonzero”] [ExpNonzero(2) →^{pyk} “lemma expNonzero(2)”] [HalfBase(Base) →^{pyk} “lemma halfBase base”] [HalfBase(Indu) →^{pyk} “lemma halfBase indu”] [MultiplyEquations(R) →^{pyk} “lemma multiplyEquations(R)”] [NonreciprocalToRight(Eq)(1term)(R) →^{pyk} “lemma nonreciprocalToRight(Eq)(1 term)(R)”] [PositiveNonzero(R) →^{pyk} “lemma positiveNonzero(R)”] [NonzeroProduct(2)(R) →^{pyk} “lemma nonzeroProduct(2)(R)”] [HalfBase →^{pyk} “lemma halfBase”] [Three2threeFactors(R) →^{pyk} “lemma three2threeFactors(R)”] [x ∗ y = zBackwards(R) →^{pyk} “lemma x∗y=zBackwards(R)”] [PositiveInverted(R) →^{pyk} “lemma positiveInverted(R)”] [ReciprocalToRight(Less)(R) →^{pyk} “lemma reciprocalToRight(Less)(R)”] [ReciprocalToRight(Less)(1term)(R) →^{pyk} “lemma reciprocalToRight(Less)(1 term)(R)”] [NonreciprocalToLeft(Less)(R) →^{pyk} “lemma nonreciprocalToLeft(Less)(R)”] [1 < x ∗ y(R) →^{pyk} “lemma 1<x∗y(R)”] [SwitchFactors(1/x < y)(R) →^{pyk} “lemma switchFactors(1/x<y)(R)”] [SmallHalving →^{pyk} “lemma smallHalving”] [IntervalSize(anyPositive) →^{pyk} “lemma intervalSize(anyPositive)”] [USdecreasing(+n)(Base) →^{pyk} “lemma USdecreasing(+n) base”] [USdecreasing(+n)(Indu) →^{pyk} “lemma USdecreasing(+n) indu”] [USdecreasing(+n) →^{pyk} “lemma USdecreasing(+n)”] [USdecreasing →^{pyk} “lemma USdecreasing”] [LeqAdditionLeft(R) →^{pyk} “lemma leqAdditionLeft(R)”] [ToNotLess(R) →^{pyk} “lemma toNotLess(R)”] [LimitOfUSIsLeq →^{pyk} “lemma limitOfUSIsLeq”] [SubtractEquations(Less)(R) →^{pyk} “lemma subtractEquations(Less)(R)”] [SubtractEquationsLeft(Less)(R) →^{pyk} “lemma subtractEquationsLeft(Less)(R)”] [LessNegated(Negative)(R) →^{pyk} “lemma lessNegated(Negative)(R)”] [FromNegatedAnd(Imply) →^{pyk} “prop lemma from negated and (imply)”] [RemoveDoubleNeg(Consequent) →^{pyk} “prop lemma remove double neg (consequent)”] [FromNotUpperBound →^{pyk} “lemma fromNotUpperBound”] [LeqNUB →^{pyk} “lemma leqNUB”] [USlimitIsLeastUpperBound(Helper) →^{pyk} “lemma USlimitIsLeastUpperBound helper”] [USlimitIsLeastUpperBound →^{pyk} “lemma USlimitIsLeastUpperBound”] [ExistMP3 →^{pyk} “pred lemma exist mp3”] [GreaterPositive(N) →^{pyk} “lemma greaterPositive(N)”] [ysFClose(Helper) →^{pyk} “lemma ysFClose helper”] [ysFClose →^{pyk} “lemma ysFClose”] [ysFCauchy(Helper) →^{pyk} “lemma ysFCauchy helper”] [ysFCauchy →^{pyk} “lemma ysFCauchy”] [from <<== →^{pyk} “lemma from<<==”] [to <<== →^{pyk} “lemma to<<==”] [NonnegativeNumerical(F) →^{pyk} “lemma nonnegativeNumerical(F)”] [NegativeNumerical(F) →^{pyk} “lemma negativeNumerical(F)”] [tester1 →^{pyk} “tester1”] [tester2 →^{pyk} “tester2”] [tester3 →^{pyk} “tester3”] [tester4 →^{pyk} “tester4”] [tester5 →^{pyk} “tester5”] [tester6 →^{pyk} “tester6”] [sup2 →^{pyk} “sup2”] )^{p} [sup2 =^{tex} “sup2”] [LeqTotality(R) =^{tex} “LeqTotality(R)”] [PositiveToLeft(Eq) =^{tex} “PositiveToLeft(Eq)”] [ExpZero(Exact) =^{tex} “ExpZero(Exact) ”] [(+1)IsPositive(N) =^{tex} “(+1)IsPositive(N)”] [SameExp(Base) =^{tex} “SameExp(Base)”] [SameExp(Indu) =^{tex} “SameExp(Indu)”] [SameExp =^{tex} “SameExp”] [Exp(+1) =^{tex} “Exp(+1)”] [DistributionOut(Minus) =^{tex} “DistributionOut(Minus)”] [(1/2)(x + y) − x = (1/2)(y − x) =^{tex} “(1/2)(x+y)-x=(1/2)(y-x)”] [y − (1/2)(x + y) = (1/2)(y − x) =^{tex} “y-(1/2)(x+y)=(1/2)(y-x)”] [PositiveBase(Base) =^{tex} “PositiveBase(Base)”] [PositiveBase(Indu) =^{tex} “PositiveBase(Indu)”] [PositiveBase =^{tex} “PositiveBase”] [PositiveToRight(Eq)(1term) =^{tex} “PositiveToRight(Eq)(1 term)”] [BSzero(Exact) =^{tex} “BSzero(Exact)”] [SameBS(2)(Base) =^{tex} “SameBS(2)(Base)”] [SameBS(2)(Indu) =^{tex} “SameBS(2)(Indu)”] [SameBS(2) =^{tex} “SameBS(2)”] [NegativeToLeft(Less)(1term) =^{tex} “NegativeToLeft(Less)(1 term)”]

[BS(+1) =^{tex} “BS(+1)”]

[BSbound(Exact)(Base) =^{tex} “BSbound(Exact)(Base)”] [BSbound(Exact)(Indu) =^{tex} “BSbound(Exact)(Indu)”] [BSbound(Exact) =^{tex} “BSbound(Exact)”] [BSbound =^{tex} “BSbound”] [SameSeries(NumDiff) =^{tex} “SameSeries(NumDiff)”] [UStelescope(Zero)(Exact) =^{tex} “UStelescope(Zero)(Exact)”] [SameTelescope(2)(Base) =^{tex} “SameTelescope(2)(Base)”] [SameTelescope(2)(Indu) =^{tex} “SameTelescope(2)(Indu)”] [SameTelescope(2) =^{tex} “SameTelescope(2)”] [TelescopeNumerical(Base) =^{tex} “TelescopeNumerical(Base)”] [TelescopeNumerical(Indu) =^{tex} “TelescopeNumerical(Indu)”] [TelescopeNumerical =^{tex} “TelescopeNumerical”] [ToNegatedDoubleImply =^{tex} “ToNegatedDoubleImply”] [EqAdditionLeft(R) =^{tex} “EqAdditionLeft(R)”] [x = x + (y − y)(R) =^{tex} “x=x+(y-y)(R)”] [x = x + y − y(R) =^{tex} “x=x+y-y(R)”] [Three2twoTerms(R) =^{tex} “Three2twoTerms(R)”] [PositiveToRight(Less)(R) =^{tex} “PositiveToRight(Less)(R)”] [Three2threeTerms(R) =^{tex} “Three2threeTerms(R)”] [Plus0Left(R) =^{tex} “Plus0Left(R)”] [PositiveToRight(Eq)(R) =^{tex} “PositiveToRight(Eq)(R)”] [SubtractEquations(R) =^{tex} “SubtractEquations(R)”] [NeqAddition(R) =^{tex} “NeqAddition(R)”] [PositiveToRight(Less)(R) =^{tex} “PositiveToRight(Less)(R)”] [PositiveToRight(Less)(1term)(R) =^{tex} “PositiveToRight(Less)(1 term)(R)”]

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

[SwitchTerms(x <= y − z) =^{tex} “SwitchTerms(x<=y-z)”] [(A)to( E )(Imply) =^{tex} “(A)to(˜ E˜ )(Imply)”] [(E)to( A )(Imply) =^{tex} “(E)to(˜ A˜ )(Imply)”] [(E )to( A)(Imply) =^{tex} “(E˜ )to(˜ A)(Imply)”] [AddNegatedAll =^{tex} “AddNegatedAll”] [ToNegatedAEA =^{tex} “ToNegatedAEA ”] [LessNeq(F)(Helper) =^{tex} “LessNeq(F)(Helper)”] [LessNeq(F) =^{tex} “LessNeq(F)”] [LessNeq(R) =^{tex} “LessNeq(R)”] [PositiveToRight(Less)(1term) =^{tex} “PositiveToRight(Less)(1 term)”] [(A )to( E) =^{tex} “(A˜ )to(˜ E)”] [ToLeq(Advanced)(R) =^{tex} “ToLeq(Advanced)(R)”] [LeqNeqLess(R) =^{tex} “LeqNeqLess(R)”] [SubLeqLeft(R) =^{tex} “SubLeqLeft(R)”] [LeqLessTransitivity(R) =^{tex} “LeqLessTransitivity(R)”] [NegativeToLeft(Eq)(R) =^{tex} “NegativeToLeft(Eq)(R)”] [NegativeToRight(Less)(R) =^{tex} “NegativeToRight(Less)(R)”] [!! == Symmetry =^{tex} “!!==Symmetry”] [NegativeToRight(Eq)(R) =^{tex} “NegativeToRight(Eq)(R)”] [NegativeToRight(Eq)(1term)(R) =^{tex} “NegativeToRight(Eq)(1 term)(R)”] [DoubleMinus(R) =^{tex} “DoubleMinus(R)”] [UniqueNegative(R) =^{tex} “UniqueNegative(R)”] [SubtractEquationsLeft(R) =^{tex} “SubtractEquationsLeft(R)”] [EqNegated(R) =^{tex} “EqNegated(R)”] [NeqNegated(R) =^{tex} “NeqNegated(R)”] [SubLeqRight(R) =^{tex} “SubLeqRight(R)”] [LeqNegated(R) =^{tex} “LeqNegated(R)”] [LessNegated(R) =^{tex} “LessNegated(R)”]

[−0 = 0(R) =^{tex} “-0=0(R)”]

[NegativeNegated(R) =^{tex} “NegativeNegated(R)”] [FromLeqGeq(R) =^{tex} “FromLeqGeq(R)”] [FromLess(R) =^{tex} “FromLess(R)”] [NonnegativeNumerical(R) =^{tex} “NonnegativeNumerical(R)”] [NegativeNumerical(R) =^{tex} “NegativeNumerical(R)”]

[0 <= |x|(R) =^{tex} “0<=|x|(R)”]

[PositiveNegated(R) =^{tex} “PositiveNegated(R)”] [AddEquations(R) =^{tex} “AddEquations(R)”] [DistributionOut(R) =^{tex} “DistributionOut(R)”] [x ∗ 0 + x = x(R) =^{tex} “x∗0+x=x(R)”] [x ∗ 0 = 0(R)(fff) =^{tex} “x∗0=0(R)(fff)”] [Times(−1)(R) =^{tex} “Times(-1)(R)”] [Times(−1)Left(R) =^{tex} “Times(-1)Left(R)”] [−x − y = −(x + y)(R) =^{tex} “-x-y=-(x+y)(R)”] [LessTotality(R) =^{tex} “LessTotality(R)”] [SameNumerical(R) =^{tex} “SameNumerical(R)”] [MinusNegated(R) =^{tex} “MinusNegated(R)”] [PositiveNumerical(R) =^{tex} “PositiveNumerical(R)”] [SignNumerical(+)(R) =^{tex} “SignNumerical(+)(R)”] [SignNumerical(R) =^{tex} “SignNumerical(R)”] [NumericalDifference(R) =^{tex} “NumericalDifference(R)”] [x <= |x|(R) =^{tex} “x<=|x|(R)”] [USlimitIsUpperBound(Helper) =^{tex} “USlimitIsUpperBound(Helper)”] [USlimitIsUpperBound =^{tex} “USlimitIsUpperBound”]

[(−1) ∗ (−1) + (−1) ∗ 1 = 0(R) =^{tex} “(-1)∗(-1)+(-1)∗1=0(R)”]

[(−1) ∗ (−1) = 1(R) =^{tex} “(-1)∗(-1)=1(R)”]

[0 < 1Helper(R) =^{tex} “0<1Helper(R)”]

[0 < 1(R) =^{tex} “0<1(R)”]

[ExpZero(Exact)(R) =^{tex} “ExpZero(Exact)(R)”] [PositiveBase(R)(Base) =^{tex} “PositiveBase(R)(Base)”] [Three2twoFactors(R) =^{tex} “Three2twoFactors(R)”] [x = x ∗ y ∗ (1/y)(R) =^{tex} “x=x∗y∗(1/y)(R)”] [NeqMultiplication(R) =^{tex} “NeqMultiplication(R)”] [LessTransitivity(R) =^{tex} “LessTransitivity(R)”]

[0 < 2(R) =^{tex} “0<2(R)”]

[SameExp(R)(Base) =^{tex} “SameExp(R)(Base)”] [SameExp(R)(Indu) =^{tex} “SameExp(R)(Indu)”] [SameExp(R) =^{tex} “SameExp(R)”] [SubNeqLeft(R) =^{tex} “SubNeqLeft(R)”] [SubNeqRight(R) =^{tex} “SubNeqRight(R)”] [NonzeroFactors(R) =^{tex} “NonzeroFactors(R)”] [NonnegativeFactors(R) =^{tex} “NonnegativeFactors(R)”] [PositiveFactors(R) =^{tex} “PositiveFactors(R)”] [LessDivision(R) =^{tex} “LessDivision(R)”]

[0 < 1/2(R) =^{tex} “0<1/2(R)”]

[PositiveToRight(Eq)(1term)(R) =^{tex} “PositiveToRight(Eq)(1 term)(R)”] [Exp(+1)(R) =^{tex} “Exp(+1)(R)”] [PositiveBase(R)(Indu) =^{tex} “PositiveBase(R)(Indu)”] [PositiveBase(R) =^{tex} “PositiveBase(R)”] [−x ∗ y = −(x ∗ y)(R) =^{tex} “-x∗y=-(x∗y)(R)”] [PositiveToLeft(Eq)(R) =^{tex} “PositiveToLeft(Eq)(R)”] [Times1Left(R) =^{tex} “Times1Left(R)”] [x + x = 2 ∗ x(R) =^{tex} “x+x=2∗x(R)”] [(1/2)x + (1/2)x = x(R) =^{tex} “(1/2)x+(1/2)x=x(R)”] [DistributionOut(Minus)(R) =^{tex} “DistributionOut(Minus)(R)”] [(1/2)(x + y) − x = (1/2)(y − x)(R) =^{tex} “(1/2)(x+y)-x=(1/2)(y-x)(R)”] [IntervalSize(R)(Base) =^{tex} “IntervalSize(R)(Base)”] [LessMultiplicationLeft(R) =^{tex} “LessMultiplicationLeft(R)”] [NegativeToLeft(Less)(R) =^{tex} “NegativeToLeft(Less)(R)”] [NegativeToLeft(Less)(1term)(R) =^{tex} “NegativeToLeft(Less)(1 term)(R)”] [y − (1/2)(x + y) = (1/2)(y − x)(R) =^{tex} “y-(1/2)(x+y)=(1/2)(y-x)(R)”] [IntervalSize(R)(Indu) =^{tex} “IntervalSize(R)(Indu)”] [IntervalSize(R) =^{tex} “IntervalSize(R)”] [XSlessUS(R) =^{tex} “XSlessUS(R)”] [USdecreasing(+1)(R) =^{tex} “USdecreasing(+1)(R)”]

[1 <= x + 1(N) =^{tex} “1<=x+1(N)”]

[ExpUnbounded(Base) =^{tex} “ExpUnbounded(Base)”] [ExpUnbounded(Indu) =^{tex} “ExpUnbounded(Indu)”] [ExpUnbounded =^{tex} “ExpUnbounded”] [NonzeroProduct(2)(R) =^{tex} “NonzeroProduct(2)(R)”] [PositiveNonzero(R) =^{tex} “PositiveNonzero(R)”] [NonreciprocalToRight(Eq)(1term)(R) =^{tex} “NonreciprocalToRight(Eq)(1 term)(R)”] [ExpNonzero(Base) =^{tex} “ExpNonzero(Base)”] [ExpNonzero(Indu) =^{tex} “ExpNonzero(Indu)”] [ExpNonzero =^{tex} “ExpNonzero”] [MultiplyEquations(R) =^{tex} “MultiplyEquations(R)”] [ExpNonzero(2) =^{tex} “ExpNonzero(2)”] [HalfBase(Base) =^{tex} “HalfBase(Base)”] [HalfBase(Indu) =^{tex} “HalfBase(Indu)”] [HalfBase =^{tex} “HalfBase”] [Three2threeFactors(R) =^{tex} “Three2threeFactors(R)”] [x ∗ y = zBackwards(R) =^{tex} “x∗y=zBackwards(R)”] [PositiveInverted(R) =^{tex} “PositiveInverted(R)”] [ReciprocalToRight(Less)(R) =^{tex} “ReciprocalToRight(Less)(R)”] [ReciprocalToRight(Less)(1term)(R) =^{tex} “ReciprocalToRight(Less)(1 term)(R)”] [NonreciprocalToLeft(Less)(R) =^{tex} “NonreciprocalToLeft(Less)(R)”] [1 < x ∗ y(R) =^{tex} “1<x∗y(R)”] [SwitchFactors(1/x < y)(R) =^{tex} “SwitchFactors(1/x<y)(R)”] [SmallHalving =^{tex} “SmallHalving”] [IntervalSize(anyPositive) =^{tex} “IntervalSize(anyPositive)”] [USdecreasing(+n)(Base) =^{tex} “USdecreasing(+n)(Base)”] [USdecreasing(+n)(Indu) =^{tex} “USdecreasing(+n)(Indu)”] [USdecreasing(+n) =^{tex} “USdecreasing(+n)”] [USdecreasing =^{tex} “USdecreasing”] [LeqAdditionLeft(R) =^{tex} “LeqAdditionLeft(R)”] [ToNotLess(R) =^{tex} “ToNotLess(R)”] [LimitOfUSIsLeq =^{tex} “LimitOfUSIsLeq”] [SubtractEquations(Less)(R) =^{tex} “SubtractEquations(Less)(R)”] [SubtractEquationsLeft(Less)(R) =^{tex} “SubtractEquationsLeft(Less)(R)”] [LessNegated(Negative)(R) =^{tex} “LessNegated(Negative)(R)”] [FromNegatedAnd(Imply) =^{tex} “FromNegatedAnd(Imply)”] [RemoveDoubleNeg(Consequent) =^{tex} “RemoveDoubleNeg(Consequent)”] [FromNotUpperBound =^{tex} “FromNotUpperBound”] [LeqNUB =^{tex} “LeqNUB”] [USlimitIsLeastUpperBound(Helper) =^{tex} “USlimitIsLeastUpperBound(Helper)”] [USlimitIsLeastUpperBound =^{tex} “USlimitIsLeastUpperBound”] [ExistMP3 =^{tex} “ExistMP3”] [GreaterPositive(N) =^{tex} “GreaterPositive(N)”] [ysFClose(Helper) =^{tex} “ysFClose(Helper)”] [ysFClose =^{tex} “ysFClose”] [ysFCauchy(Helper) =^{tex} “ysFCauchy(Helper)”] [ysFCauchy =^{tex} “ysFCauchy”] [from <<== =^{tex} “from<<==”] [NonnegativeNumerical(F) =^{tex} “NonnegativeNumerical(F)”]

[to <<== =^{tex} “to<<==”]

[NegativeNumerical(F) =^{tex} “NegativeNumerical(F)”]