Universal Rule Match, OpenNARS

Premises:
(tim --> cat).
((&&,($1 --> cat),($1 --> [orange])) ==>  ($1 <-> garfield)).

Rule:
(S --> M), ((&&,($1 --> M),A_1..n) ==> B), substitute($1,S) |- ((&&,A_1..n) ==> B)

Match Process:
P:={}, Q:={}

MATCH Step1:
Unify (S --> M) with (tim --> cat) under P
=> P={S -> tim, M -> cat}

MATCH Step2:
Unify ((&&,($1 --> M),A_1..n) ==> B) with ((&&,($1 --> cat),($1 --> [orange])) ==>  ($1 <-> garfield)) under P
=> P={S -> tim, M -> cat, A_1 -> ($1 --> [orange]), B -> ($1 <-> garfield)}

MATCH Step3:
Satisfy substitute($1,S) by applying the subsitutions in M to substitute($1,S) leading to substitute($1,tim),
this described substitution is now added to the substitution set Q:
=> Q={$1 -> S}

"Construction of Conclusion" Step4:
The match process is finished, and was satisfyable, now lets build the conclusion
by applying at first the substitutions in P to the conclusion ((&&,A_1..n) ==> B) specified by the rule
leading to:
(($1 --> [orange]) ==> ($1 <-> garfield))

now finally we apply Q to this result and get:
((tim --> [orange]) ==> (tim <-> garfield))