twee-2.5: tests/sudoku4.p

fof('associativity of ∘', axiom,
    ![F,G,H]: F ∘ (G ∘ H) = (F ∘ G) ∘ H).

fof('∘ identity', axiom,
    ![F]: id ∘ F = F).

fof('∘ identity', axiom,
    ![F]: F ∘ id = F).

fof('map functor', axiom,
    ![F, G]: map(F) ∘ map(G) = map(F ∘ G)).

fof('map functor', axiom,
    map(id) = id).

fof('defn pruneBy', axiom,
    ![F]: pruneBy(F) = F ∘ (map(pruneRow) ∘ F)).

fof('defn expand', axiom,
    expand = product ∘ map(product)).

fof('expand after boxs', axiom,
    expand ∘ boxs = map(boxs) ∘ expand).

fof('filter with boxs', axiom,
    ![P, F]: filter (P ∘ boxs) = map(boxs) ∘ (filter(P) ∘ map(boxs))).

fof('boxs involution', axiom,
    boxs ∘ boxs = id).

fof('filter after product', axiom,
    ![P]: filter(all(P)) ∘ product = product ∘ map(filter(P))).

fof('law of pruneRow', axiom,
    filter(nodups) ∘ (product ∘ pruneRow) = filter(nodups) ∘ product).

fof('map/filter', axiom,
    ![P, F]: filter(P) ∘ map(F) = map(F) ∘ filter(P ∘ F)).

fof('product/map', axiom,
    ![F]: product ∘ map(F) = map(map(F)) ∘ product).

fof('conjecture', conjecture,
    filter(all(nodups) ∘ boxs) ∘ (expand ∘ pruneBy(boxs)) =
    filter(all(nodups) ∘ boxs) ∘ expand).