J

K

1J

1K

C1

Q

\overline Q

gatx = (1, 0)
gaty = (0, -2)
A = (2.5, 5)
a = Segment(A, A + gatx)
b = Segment(A, A + gaty)
c = Segment(A + gatx, A + gatx + gaty)
d = Segment(A + gaty, A + gatx + gaty)
f = Segment(A - 0.5 * gatx + 0.5 * gaty, A + 0.5 * gaty)
k_3 = Segment(A - 0.5 * gatx + 0.85 * gaty, A + 0.85 * gaty)
e = Segment(A - 0.5 * gatx + 0.15 * gaty, A + 0.15 * gaty)
h = Segment(A + gatx + 0.25 * gaty, A + 0.25 * gaty + 1.5 * gatx)
i = Segment(A + 1.2 * gatx + 0.75 * gaty, A + 0.75 * gaty + 1.5 * gatx)
k_1 = Circle(A + 1.1 * gatx + 0.75 * gaty, 0.1)
j_1 = Segment(A + 0.45 * gaty, A + 0.5 * gaty + 0.3 * gatx)
l = Segment(A + 0.55 * gaty, A + 0.5 * gaty + 0.3 * gatx)
j = true
k = true
clock = 2 (slider from 0 to 100, step 1)
jkq1: Mod[clock, 4.0] < 2.0 ∧ j ∧ k ∨ j ∧ (¬k)
njkq1: ¬jkq1

Tool: UND
Input: gatx, gaty, E
Output: l_1, m_1, p_1, n_1, q_1, r_1, s_1

l_1 = Segment(E, E + gatx)
m_1 = Segment(E, E + gaty)
n_1 = Segment(E + gatx, E + gatx + gaty)
p_1 = Segment(E + gaty, E + gatx + gaty)
q_1 = Segment(E - 0.5 * gatx + 0.25 * gaty, E + 0.25 * gaty)
r_1 = Segment(E - 0.5 * gatx + 0.75 * gaty, E + 0.75 * gaty)
s_1 = Segment(E + gatx + 0.5 * gaty, E + 1.5 * gatx + 0.5 * gaty)

Tool: jk
Input: A, gatx, gaty
Output: k, a, b, c, d, e, f, g, h, i, j, l

a = Segment(A, A + gatx)
b = Segment(A, A + gaty)
c = Segment(A + gatx, A + gatx + gaty)
d = Segment(A + gaty, A + gatx + gaty)
f = Segment(A - 0.5 * gatx + 0.5 * gaty, A + 0.5 * gaty)
g = Segment(A - 0.5 * gatx + 0.85 * gaty, A + 0.85 * gaty)
e = Segment(A - 0.5 * gatx + 0.15 * gaty, A + 0.15 * gaty)
h = Segment(A + gatx + 0.25 * gaty, A + 0.25 * gaty + 1.5 * gatx)
i = Segment(A + 1.2 * gatx + 0.75 * gaty, A + 0.75 * gaty + 1.5 * gatx)
k = Circle(A + 1.1 * gatx + 0.75 * gaty, 0.1)
j = Segment(A + 0.45 * gaty, A + 0.5 * gaty + 0.3 * gatx)
l = Segment(A + 0.55 * gaty, A + 0.5 * gaty + 0.3 * gatx)