The transformation context
The condition to read
The assertions already known to hold there
The variables the filtered operation certainly binds, which is what the substitution folds
sameTerm(?x, ?x) against; leaving it empty only means fewer residuals fold
the conjunction and the residual, or undefined when the condition is contradictory, which
makes the filter empty
Splits a filter condition into the assertions it carries and what is left of it, folding in the assertions
knownto already hold there (Θ).The leftovers have the strong assertions substituted into them, per (FReord):
σ_R(A) == σ_{simplify(R[theta])}(σ_θ(A)). That can turn a leftover into an assertion of its own -sameTerm(?y, ?x)becomessameTerm(?y, c)- so this repeats until the substitution stops changing. Merging intoknownis also what makes the pass idempotent: re-running it re-derives the same conjunction and absorbs it rather than stacking a second copy.