The reason I studied the thinning theorem again is because I need a slightly generalised variation. The following seems to be what I need. The general idea and the term “pruning” emerged from discussion with Sharon Curtis. The term “lax preorder” is invented by myself. I am not good at naming, and welcome suggestions for better names.

The notation below are mostly taken from the book Algebra of Programming. Not many people, even among functional programmers, are familiar with these notations involving relational intersection, division, etc. One starts to appreciate their benefits once he/she gets used to using their calculation rules. Most of the time when I was doing the proof, I was merely manipulating the symbols. I could not have managed the complexity if I had to fall back to the semantics and think about what they “mean” all the time.

A relation *lax preorder* if it is

**reflexive**in the sense that∋ ⊆ Q , and**transitive**in the sense that(Q/∋) . Q ⊆ Q .

A relation

Given a lax preorder, we define:

$prune\; Q\; =\; \in \backslash \in \; \cap \; Q/\ni $

The definition induces the universal property:

$X\; \subseteq \; prune\; Q\; .\; \Lambda S\equiv \; \in \; .\; X\; \subseteq \; S\; \bigwedge \; X\; .\; S\u02d8\subseteq \; Q$

Any preorder

**Theorem**: if

$fold\; (prune\; Q\; .\; \Lambda (S\; .\; F\in ))\; \subseteq \; prune\; Q\; .\; \Lambda (fold\; S)$

**Proof**. Since

$prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; \subseteq \; prune\; Q\; .\; \Lambda (S\; .\; F\in )$

By the universal property of

$\in \; .\; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; \subseteq \; S\; .\; F\in \; \bigwedge $

prune Q . Λ(S . F∈) . F(prune Q) . (S . F∈)˘ ⊆ Q

The first inclusion is proved by:

$\in \; .\; prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)$

⊆{ since prune Q ⊆ ∈\∈ }

∈ . ∈\∈ . Λ(S . F∈) . F(thin Q)

⊆{ division }

∈ . Λ(S . F∈) . F(thin Q)

={ power transpose }

S . F∈ . F(thin Q)

⊆{ since prune Q ⊆ ∈\∈ }

S . F∈ . F(∈\∈)

⊆{ division }

S . F∈

And the second by:

$prune\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(prune\; Q)\; .\; (S\; .\; F\in )\u02d8$

⊆{ since prune Q ⊆ Q/∋, converse }

prune Q . Λ(S . F∈) . F(Q/∋) . F∋ . S˘

⊆{ division }

prune Q . Λ(S . F∈) . FQ . S˘

⊆{ monotonicity: FQ . S˘⊆ Λ(S . F∈)˘. Q }

prune Q . Λ(S . F∈) . Λ(S . F∈)˘. Q

⊆{ since Λ(S . F∈)˘is a function, that is, f . f˘⊆ id }

prune Q . Q

⊆{ since thin Q ⊆ Q/∋, division }

Q/∋ . Q

⊆{ since Q transitive }

Q

**Endproof.**

The proof above uses transitivity of

$foldr\; (prune\; Q\; .\; \Lambda (S\; .\; (id\; \times \; \in )))\; \{e\}\; \subseteq \; prune\; Q\; .\; \Lambda (foldr\; S\; e)$

if