reconsider x = t1 as Element of the generators of G . a by A1;
the assignments of A . [t1,t2] = x := (t2,A) ;
hence the assignments of A . [t1,t2] is absolutely-terminating Algorithm of A ; :: thesis: verum