1. a k c are collinear (by assumption)
2. a l b are collinear (by assumption)
3. |o a| = |o b| (by assumption)
4. |o p| = |o a| (by assumption)
5. |o b| = |o p| (by calculation 3 4)
  |o b| = |o a| (by 3: |o a| = |o b|)
        = |o p| (by 4: |o p| = |o a|)
6. ∠o b p = ∠b p o (by isosceles triangle 5)
7. |o a| = |o c| (by assumption)
8. |o p| = |o c| (by calculation 4 7)
  |o p| = |o a| (by 4: |o p| = |o a|)
        = |o c| (by 7: |o a| = |o c|)
9. ∠o c p = ∠c p o (by isosceles triangle 8)
10. |o b| = |o a| (by calculation 3)
  |o b| = |o a| (by 3: |o a| = |o b|)
11. ∠a b o = ∠o a b (by isosceles triangle 10)
12. ∠a c o = ∠o a c (by isosceles triangle 7)
13. b d c are collinear (by assumption)
14. x b c are collinear (by assumption)
15. b x d c are collinear (by merge lines 13 14)
16. y b c are collinear (by assumption)
17. b x d y c are collinear (by merge lines 15 16)
18. ∠y b i = ∠d b i (by calculation 15 17)
  d(i b) + -1*d(y b) = d(i b) + -1*d(b d) (∠y b i = ∠d b i)
     1 ×    d(y b) + -1*d(b d) = 0        (17: b x d y c are collinear)
19. ∠a b i = ∠i b c (by assumption)
20. i d ⊥ b c (by assumption)
21. y t2 || a b (by assumption)
22. |i t2| = |i d| (by assumption)
23. |i y| / |i d| = |i y| / |i t2| (by calculation 22)
  |y i| / |d i| = |y i| / |i t2| (by 22: |i t2| = |i d|)
24. y t2 ⊥ t2 i (by assumption)
25. ∠y t2 i = ∠i d y (by calculation 17 20 24)
  d(i t2) + -1*d(t2 y) = d(y d) + -1*d(i d) (∠y t2 i = ∠i d y)
     1 ×    d(t2 y) + -1*d(i t2) = 1/2*pi        (24: y t2 ⊥ t2 i)
     1 ×    d(y d) + -1*d(c b) = 0        (17: b x d y c are collinear)
    -1 ×    d(i d) + -1*d(c b) = 1/2*pi        (20: i d ⊥ b c)
26. |i t2| < |i y| (by diagram check)
27. d → i → y and i → t2 → y are of same clock direction. (by diagram check)
28. ∠d y i = ∠i y t2 (by similar triangles Ssa 23 25 26 27)
29. ∠y i b = ∠b d i (by calculation 15 17 19 20 21 28)
  d(i b) + -1*d(i y) = d(i d) + -1*d(b d) (∠y i b = ∠b d i)
  -1/2 ×    d(i b) + -1*d(a b) = d(c b) + -1*d(i b)        (19: ∠a b i = ∠i b c)
   1/2 ×    d(i y) + -1*d(y d) = d(t2 y) + -1*d(i y)        (28: ∠d y i = ∠i y t2)
   1/2 ×    d(t2 y) + -1*d(a b) = 0        (21: y t2 || a b)
   1/2 ×    d(y d) + -1*d(b d) = 0        (17: b x d y c are collinear)
   1/2 ×    d(c b) + -1*d(b d) = 0        (15: b x d c are collinear)
     1 ×    d(i d) + -1*d(c b) = 1/2*pi        (20: i d ⊥ b c)
30. |b y| / |y i| = |b i| / |i d| (by similar triangles aa 18 29)
31. ∠x b i = ∠i b a (by calculation 14 19)
  d(i b) + -1*d(x b) = d(a b) + -1*d(i b) (∠x b i = ∠i b a)
    -1 ×    d(i b) + -1*d(a b) = d(c b) + -1*d(i b)        (19: ∠a b i = ∠i b c)
    -1 ×    d(c b) + -1*d(x b) = 0        (14: x b c are collinear)
32. ∠b a i = ∠i a c (by assumption)
33. x t1 || a c (by assumption)
34. |i t1| = |i d| (by assumption)
35. |i x| / |i t1| = |i x| / |i d| (by calculation 34)
  |x i| / |i t1| = |x i| / |d i| (by 34: |i t1| = |i d|)
36. x t1 ⊥ t1 i (by assumption)
37. ∠x d i = ∠i t1 x (by calculation 15 20 36)
  d(i d) + -1*d(x d) = d(t1 x) + -1*d(t1 i) (∠x d i = ∠i t1 x)
    -1 ×    d(i d) + -1*d(c b) = 1/2*pi        (20: i d ⊥ b c)
     1 ×    d(x d) + -1*d(c b) = 0        (15: b x d c are collinear)
     1 ×    d(t1 x) + -1*d(t1 i) = 1/2*pi        (36: x t1 ⊥ t1 i)
38. |i d| < |i x| (by diagram check)
39. i → t1 → x and d → i → x are of same clock direction. (by diagram check)
40. ∠t1 x i = ∠i x d (by similar triangles Ssa 35 37 38 39)
41. ∠x i b = ∠i a b (by calculation 15 19 32 33 40)
  d(i b) + -1*d(i x) = d(a b) + -1*d(i a) (∠x i b = ∠i a b)
  -1/2 ×    d(i b) + -1*d(a b) = d(c b) + -1*d(i b)        (19: ∠a b i = ∠i b c)
   1/2 ×    d(i x) + -1*d(t1 x) = d(x d) + -1*d(i x)        (40: ∠t1 x i = ∠i x d)
   1/2 ×    d(t1 x) + -1*d(c a) = 0        (33: x t1 || a c)
   1/2 ×    d(x d) + -1*d(c b) = 0        (15: b x d c are collinear)
  -1/2 ×    d(i a) + -1*d(a b) = d(c a) + -1*d(i a)        (32: ∠b a i = ∠i a c)
42. |b x| / |b i| = |b i| / |b a| (by similar triangles aa 31 41)
43. |b x| / |x i| = |b i| / |i a| (by similar triangles aa 31 41)
44. ∠x c i = ∠d c i (by calculation 14 15)
  d(c i) + -1*d(c x) = d(c i) + -1*d(c d) (∠x c i = ∠d c i)
    -1 ×    d(c d) + -1*d(c x) = 0        (15: b x d c are collinear)
45. ∠b c i = ∠i c a (by assumption)
46. ∠x i c = ∠c d i (by calculation 15 20 33 40 45)
  d(c i) + -1*d(i x) = d(i d) + -1*d(c d) (∠x i c = ∠c d i)
  -1/2 ×    d(c i) + -1*d(c b) = d(c a) + -1*d(c i)        (45: ∠b c i = ∠i c a)
   1/2 ×    d(i x) + -1*d(t1 x) = d(x d) + -1*d(i x)        (40: ∠t1 x i = ∠i x d)
   1/2 ×    d(t1 x) + -1*d(c a) = 0        (33: x t1 || a c)
   1/2 ×    d(x d) + -1*d(c b) = 0        (15: b x d c are collinear)
     1 ×    d(i d) + -1*d(c b) = 1/2*pi        (20: i d ⊥ b c)
    -1 ×    d(c d) + -1*d(c b) = 0        (15: b x d c are collinear)
47. |c x| / |x i| = |c i| / |i d| (by similar triangles aa 44 46)
48. e i b are collinear (by assumption)
49. ∠a b e = ∠i b y (by calculation 17 19 48)
  d(e b) + -1*d(a b) = d(y b) + -1*d(i b) (∠a b e = ∠i b y)
     1 ×    d(i b) + -1*d(e b) = 0        (48: e i b are collinear)
    -1 ×    d(i b) + -1*d(a b) = d(c b) + -1*d(i b)        (19: ∠a b i = ∠i b c)
    -1 ×    d(c b) + -1*d(y b) = 0        (17: b x d y c are collinear)
50. |l e| = |l b| (by assumption)
51. |l b| = |l e| (by calculation 50)
  |b l| = |e l| (by 50: |l e| = |l b|)
52. ∠l e b = ∠e b l (by isosceles triangle 51)
53. |a l| = |b l| (by assumption)
54. |l a| = |l e| (by calculation 50 53)
  |a l| = |b l| (by 53: |a l| = |b l|)
        = |e l| (by 50: |l e| = |l b|)
55. ∠l a e = ∠a e l (by isosceles triangle 54)
56. ∠a e b = ∠b i y (by calculation 2 17 19 21 28 52 55)
  d(e b) + -1*d(e a) = d(i y) + -1*d(i b) (∠a e b = ∠b i y)
  -1/2 ×    d(e b) + -1*d(e l) = d(l b) + -1*d(e b)        (52: ∠l e b = ∠e b l)
  -1/2 ×    d(l b) + -1*d(a l) = 0        (2: a l b are collinear)
   1/2 ×    d(e a) + -1*d(a l) = d(e l) + -1*d(e a)        (55: ∠l a e = ∠a e l)
   1/2 ×    d(i y) + -1*d(y d) = d(t2 y) + -1*d(i y)        (28: ∠d y i = ∠i y t2)
   1/2 ×    d(t2 y) + -1*d(a b) = 0        (21: y t2 || a b)
   1/2 ×    d(y d) + -1*d(c b) = 0        (17: b x d y c are collinear)
  -1/2 ×    d(i b) + -1*d(a b) = d(c b) + -1*d(i b)        (19: ∠a b i = ∠i b c)
57. |b a| / |a e| = |b y| / |y i| (by similar triangles aa 49 56)
58. p a i are collinear (by assumption)
59. |o b| = |o c| (by calculation 3 7)
  |o b| = |o a| (by 3: |o a| = |o b|)
        = |o c| (by 7: |o a| = |o c|)
60. ∠c b o = ∠o c b (by isosceles triangle 59)
61. |o a| = |o p| (by calculation 4)
  |o a| = |o p| (by 4: |o p| = |o a|)
62. ∠a p o = ∠o a p (by isosceles triangle 61)
63. ∠a l e = ∠i p c (by calculation 2 9 11 19 48 52 58 60 62)
  d(e l) + -1*d(a l) = d(p c) + -1*d(p i) (∠a l e = ∠i p c)
     2 ×    d(i b) + -1*d(e b) = 0        (48: e i b are collinear)
    -1 ×    d(i b) + -1*d(a b) = d(c b) + -1*d(i b)        (19: ∠a b i = ∠i b c)
   1/2 ×    d(o b) + -1*d(c b) = d(c b) + -1*d(o c)        (60: ∠c b o = ∠o c b)
  -1/2 ×    d(o b) + -1*d(a b) = d(a b) + -1*d(o a)        (11: ∠a b o = ∠o a b)
     1 ×    d(e b) + -1*d(e l) = d(l b) + -1*d(e b)        (52: ∠l e b = ∠e b l)
     1 ×    d(l b) + -1*d(a l) = 0        (2: a l b are collinear)
    -2 ×    d(a b) + -1*d(a l) = 0        (2: a l b are collinear)
   1/2 ×    d(p c) + -1*d(o c) = d(o p) + -1*d(p c)        (9: ∠o c p = ∠c p o)
    -1 ×    d(p i) + -1*d(p a) = 0        (58: p a i are collinear)
   1/2 ×    d(o p) + -1*d(p a) = d(p a) + -1*d(o a)        (62: ∠a p o = ∠o a p)
64. ∠a e l = ∠p i c (by calculation 2 19 32 45 48 52 55 58)
  d(e l) + -1*d(e a) = d(c i) + -1*d(p i) (∠a e l = ∠p i c)
   1/2 ×    d(e a) + -1*d(a l) = d(e l) + -1*d(e a)        (55: ∠l a e = ∠a e l)
    -1 ×    d(a b) + -1*d(a l) = 0        (2: a l b are collinear)
   1/2 ×    d(c i) + -1*d(c b) = d(c a) + -1*d(c i)        (45: ∠b c i = ∠i c a)
     1 ×    d(i b) + -1*d(e b) = 0        (48: e i b are collinear)
  -1/2 ×    d(i b) + -1*d(a b) = d(c b) + -1*d(i b)        (19: ∠a b i = ∠i b c)
   1/2 ×    d(e b) + -1*d(e l) = d(l b) + -1*d(e b)        (52: ∠l e b = ∠e b l)
   1/2 ×    d(l b) + -1*d(a l) = 0        (2: a l b are collinear)
     1 ×    d(i a) + -1*d(p i) = 0        (58: p a i are collinear)
  -1/2 ×    d(i a) + -1*d(a b) = d(c a) + -1*d(i a)        (32: ∠b a i = ∠i a c)
65. |l a| / |a e| = |p c| / |c i| (by similar triangles aa 63 64)
66. |a l| / |a i| = |c p| / |c x| (by calculation 30 42 43 47 57 65)
  |a l| / |i a| = |a l| * |x b| / |i x| / |i b| (by 43: |b x| / |x i| = |b i| / |i a|)
                = |a l| / |i x| * |i b| / |a b| (by 42: |b x| / |b i| = |b i| / |b a|)
                = |a l| / |i x| / |a b| * |y b| / |i y| * |i d| (by 30: |b y| / |y i| = |b i| / |i d|)
                = |a l| / |i x| * |i d| / |e a| (by 57: |b a| / |a e| = |b y| / |y i|)
                = |i x|^-1 * |i d| * |c p| / |c i| (by 65: |l a| / |a e| = |p c| / |c i|)
                = |c p| / |c x| (by 47: |c x| / |x i| = |c i| / |i d|)
67. ∠p c x = ∠i a l (by calculation 2 9 11 14 58 60 62)
  d(c x) + -1*d(p c) = d(a l) + -1*d(i a) (∠p c x = ∠i a l)
     1 ×    d(c b) + -1*d(c x) = 0        (14: x b c are collinear)
   1/2 ×    d(o b) + -1*d(c b) = d(c b) + -1*d(o c)        (60: ∠c b o = ∠o c b)
  -1/2 ×    d(o b) + -1*d(a b) = d(a b) + -1*d(o a)        (11: ∠a b o = ∠o a b)
   1/2 ×    d(p c) + -1*d(o c) = d(o p) + -1*d(p c)        (9: ∠o c p = ∠c p o)
    -1 ×    d(a b) + -1*d(a l) = 0        (2: a l b are collinear)
    -1 ×    d(i a) + -1*d(p a) = 0        (58: p a i are collinear)
   1/2 ×    d(o p) + -1*d(p a) = d(p a) + -1*d(o a)        (62: ∠a p o = ∠o a p)
68. c → p → x and i → l → a are of same clock direction. (by diagram check)
69. ∠c p x = ∠i l a (by similar triangles sas 66 67 68)
70. ∠c b p = ∠p c b (by calculation 6 9 11 12 32 58 60 62)
  d(p b) + -1*d(c b) = d(c b) + -1*d(p c) (∠c b p = ∠p c b)
  -1/2 ×    d(p b) + -1*d(o b) = d(o p) + -1*d(p b)        (6: ∠o b p = ∠b p o)
     2 ×    d(i a) + -1*d(p a) = 0        (58: p a i are collinear)
    -1 ×    d(i a) + -1*d(a b) = d(c a) + -1*d(i a)        (32: ∠b a i = ∠i a c)
   1/2 ×    d(o b) + -1*d(a b) = d(a b) + -1*d(o a)        (11: ∠a b o = ∠o a b)
   1/2 ×    d(o c) + -1*d(c a) = d(c a) + -1*d(o a)        (12: ∠a c o = ∠o a c)
    -1 ×    d(o p) + -1*d(p a) = d(p a) + -1*d(o a)        (62: ∠a p o = ∠o a p)
    -1 ×    d(o b) + -1*d(c b) = d(c b) + -1*d(o c)        (60: ∠c b o = ∠o c b)
  -1/2 ×    d(p c) + -1*d(o c) = d(o p) + -1*d(p c)        (9: ∠o c p = ∠c p o)
71. |p b| = |p c| (by isosceles triangle 70)
72. ∠y c i = ∠i c a (by calculation 17 45)
  d(c i) + -1*d(c y) = d(c a) + -1*d(c i) (∠y c i = ∠i c a)
    -1 ×    d(c i) + -1*d(c b) = d(c a) + -1*d(c i)        (45: ∠b c i = ∠i c a)
     1 ×    d(c y) + -1*d(c b) = 0        (17: b x d y c are collinear)
73. ∠y i c = ∠i a c (by calculation 17 21 28 32 45)
  d(c i) + -1*d(i y) = d(c a) + -1*d(i a) (∠y i c = ∠i a c)
  -1/2 ×    d(c i) + -1*d(c b) = d(c a) + -1*d(c i)        (45: ∠b c i = ∠i c a)
   1/2 ×    d(i y) + -1*d(y d) = d(t2 y) + -1*d(i y)        (28: ∠d y i = ∠i y t2)
   1/2 ×    d(t2 y) + -1*d(a b) = 0        (21: y t2 || a b)
   1/2 ×    d(y d) + -1*d(c b) = 0        (17: b x d y c are collinear)
  -1/2 ×    d(i a) + -1*d(a b) = d(c a) + -1*d(i a)        (32: ∠b a i = ∠i a c)
74. |c y| / |c i| = |c i| / |c a| (by similar triangles aa 72 73)
75. |c y| / |y i| = |c i| / |i a| (by similar triangles aa 72 73)
76. ∠c a b = ∠k a l (by calculation 1 2)
  d(a b) + -1*d(c a) = d(a l) + -1*d(k a) (∠c a b = ∠k a l)
    -1 ×    d(a b) + -1*d(a l) = 0        (2: a l b are collinear)
     1 ×    d(c a) + -1*d(k a) = 0        (1: a k c are collinear)
77. |a k| = |c k| (by assumption)
78. |c k| / |c o| = |a k| / |a o| (by calculation 7 77)
  |k c| / |o c| = |o c|^-1 * |k a| (by 77: |a k| = |c k|)
                = |k a| / |o a| (by 7: |o a| = |o c|)
79. |o k| / |o c| = |o k| / |o a| (by calculation 7)
  |o k| / |o c| = |o k| / |o a| (by 7: |o a| = |o c|)
80. c → k → o and o → k → a are of same clock direction. (by diagram check)
81. ∠c k o = ∠o k a (by similar triangles sss 78 79 80)
82. |b l| / |b o| = |a l| / |a o| (by calculation 3 53)
  |b l| / |b o| = |b l| / |a o| (by 3: |o a| = |o b|)
                = |a o|^-1 * |a l| (by 53: |a l| = |b l|)
83. |o l| / |o b| = |o l| / |o a| (by calculation 3)
  |o l| / |o b| = |o l| / |o a| (by 3: |o a| = |o b|)
84. b → l → o and o → l → a are of same clock direction. (by diagram check)
85. ∠b l o = ∠o l a (by similar triangles sss 82 83 84)
86. ∠a l o = ∠a k o (by calculation 1 2 81 85)
  d(o l) + -1*d(a l) = d(o k) + -1*d(k a) (∠a l o = ∠a k o)
  -1/2 ×    d(o l) + -1*d(l b) = d(a l) + -1*d(o l)        (85: ∠b l o = ∠o l a)
  -1/2 ×    d(l b) + -1*d(a l) = 0        (2: a l b are collinear)
   1/2 ×    d(o k) + -1*d(c k) = d(k a) + -1*d(o k)        (81: ∠c k o = ∠o k a)
   1/2 ×    d(c k) + -1*d(k a) = 0        (1: a k c are collinear)
87. l k a o are concyclic (by inscribed angle 86)
88. ∠l k o = ∠l a o (by inscribed angle 87)
89. ∠c b a = ∠k l a (by calculation 1 11 12 60 81 88)
  d(a b) + -1*d(c b) = d(a l) + -1*d(k l) (∠c b a = ∠k l a)
  -1/2 ×    d(o b) + -1*d(c b) = d(c b) + -1*d(o c)        (60: ∠c b o = ∠o c b)
   1/2 ×    d(o b) + -1*d(a b) = d(a b) + -1*d(o a)        (11: ∠a b o = ∠o a b)
   1/2 ×    d(o c) + -1*d(c a) = d(c a) + -1*d(o a)        (12: ∠a c o = ∠o a c)
     1 ×    d(c a) + -1*d(k a) = 0        (1: a k c are collinear)
     1 ×    d(o k) + -1*d(k l) = d(o a) + -1*d(a l)        (88: ∠l k o = ∠l a o)
  -1/2 ×    d(o k) + -1*d(c k) = d(k a) + -1*d(o k)        (81: ∠c k o = ∠o k a)
  -1/2 ×    d(c k) + -1*d(k a) = 0        (1: a k c are collinear)
90. |a c| / |a b| = |a k| / |a l| (by similar triangles aa 76 89)
91. |a k| / |a i| = |b p| / |b y| (by calculation 57 65 71 74 75 90)
  |k a| / |i a| = |k a| / |i a| * |p b| / |p c| (by 71: |p b| = |p c|)
                = |k a| / |i a| * |p b| / |a l| * |e a| / |c i| (by 65: |l a| / |a e| = |p c| / |c i|)
                = |i a|^-1 * |p b| * |e a| / |c i| * |c a| / |a b| (by 90: |a c| / |a b| = |a k| / |a l|)
                = |i a|^-1 * |p b| * |e a| * |c i| / |a b| / |c y| (by 74: |c y| / |c i| = |c i| / |c a|)
                = |p b| * |e a| / |a b| / |i y| (by 75: |c y| / |y i| = |c i| / |i a|)
                = |p b| / |y b| (by 57: |b a| / |a e| = |b y| / |y i|)
92. ∠p b y = ∠i a k (by calculation 1 6 12 17 58 60 62)
  d(y b) + -1*d(p b) = d(k a) + -1*d(i a) (∠p b y = ∠i a k)
     1 ×    d(c b) + -1*d(y b) = 0        (17: b x d y c are collinear)
   1/2 ×    d(o b) + -1*d(c b) = d(c b) + -1*d(o c)        (60: ∠c b o = ∠o c b)
  -1/2 ×    d(o c) + -1*d(c a) = d(c a) + -1*d(o a)        (12: ∠a c o = ∠o a c)
   1/2 ×    d(p b) + -1*d(o b) = d(o p) + -1*d(p b)        (6: ∠o b p = ∠b p o)
    -1 ×    d(c a) + -1*d(k a) = 0        (1: a k c are collinear)
    -1 ×    d(i a) + -1*d(p a) = 0        (58: p a i are collinear)
   1/2 ×    d(o p) + -1*d(p a) = d(p a) + -1*d(o a)        (62: ∠a p o = ∠o a p)
93. b → p → y and i → k → a are of same clock direction. (by diagram check)
94. ∠b p y = ∠i k a (by similar triangles sas 91 92 93)
95.  d(i l) - d(i k) + d(p x) - d(p y)  + 180 = 0 (by calculation 1 2 6 9 11 12 69 94)
  d(i l) + -1*d(k i) + d(p x) + -1*d(p y) = 0 ( d(i l) - d(i k) + d(p x) - d(p y)  + 180 = 0)
    -1 ×    d(p x) + -1*d(p c) = d(a l) + -1*d(i l)        (69: ∠c p x = ∠i l a)
  -1/2 ×    d(p c) + -1*d(o c) = d(o p) + -1*d(p c)        (9: ∠o c p = ∠c p o)
     1 ×    d(a b) + -1*d(a l) = 0        (2: a l b are collinear)
   1/2 ×    d(o b) + -1*d(a b) = d(a b) + -1*d(o a)        (11: ∠a b o = ∠o a b)
     1 ×    d(p y) + -1*d(p b) = d(k a) + -1*d(k i)        (94: ∠b p y = ∠i k a)
   1/2 ×    d(p b) + -1*d(o b) = d(o p) + -1*d(p b)        (6: ∠o b p = ∠b p o)
    -1 ×    d(c a) + -1*d(k a) = 0        (1: a k c are collinear)
  -1/2 ×    d(o c) + -1*d(c a) = d(c a) + -1*d(o a)        (12: ∠a c o = ∠o a c)