Function compose_substitutions 

pub fn compose_substitutions(s1: Substitution, s2: Substitution) -> Substitution

Compose two substitutions: apply s2 after s1.

The resulting substitution applies s1 first, then s2. This is the standard composition operation for Most General Unifiers.

Semantics

For any term t: apply(compose(s1, s2), t) = apply(s2, apply(s1, t))

Arguments

• s1 - The first substitution (applied first)
• s2 - The second substitution (applied second)

Returns

A combined substitution equivalent to applying s1 then s2.

Example

use logicaffeine_proof::{ProofTerm, unify::{Substitution, compose_substitutions}};

let mut s1 = Substitution::new();
s1.insert("x".into(), ProofTerm::Variable("y".into()));

let mut s2 = Substitution::new();
s2.insert("y".into(), ProofTerm::Constant("a".into()));

let composed = compose_substitutions(s1, s2);
// x ↦ a (via y), y ↦ a