let N: int = 16;

namespace std::array(N);
    let len = [];

namespace Main(N);
    let<T> make_array: int, (int -> T) -> T[] = |n, f| if n == 0 { [] } else { make_array(n - 1, f) + [f(n - 1)] };
    let nth_clock: int -> (int -> int) = |k| |i| if i % std::array::len(clocks) == k { 1 } else { 0 };
    let clocks: col[4] = make_array(4, nth_clock);
    let wit: col[4];

    make_array(4, |k| wit[k] = clocks[k]);

    // The constraint above is already sufficient.
    // These are here to check that the correct witnesses and the correct clocks are
    // referenced above.
    wit[0] * wit[1] = 0;
    wit[0] * wit[2] = 0;
    wit[0] * wit[3] = 0;
    wit[1] * wit[2] = 0;
    wit[1] * wit[3] = 0;
    wit[2] * wit[3] = 0;
    wit[0] + wit[1] + wit[2] + wit[3] = 1;

    // intermediate poly array
    let inter: inter[4] = make_array(4, |i| wit[i] + 10);

    make_array(4, |k| inter[k] = clocks[k] + 10);
