===Unify-Direct-1===

Ersetzen Sie in dem Paar von Termen
    (t1, t2) = ( f (f (Y, undefined), f (f (Z, f (a, undefined)),
undefined))
               , f (f (f (X, a), X), undefined)
               )
die Zeichen undefined so durch Terme, daß
    sigma = listToFM
                [ ( X , f (Z, f (a, a)) ) , ( Y , f (f (Z, f (a, a)), a) )
]
ein allgemeinster Unifikator von t1 und t2 ist.

==Bei Eingabe der Lösung:==

( f (f (Y, X), f (f (Z, f (a, a)), a))
, f (f (f (X, a), X), Y)
)

==bekomme ich die Meldung:==

gelesen: ( f (f (Y, X), f (f (Z, f (a, a)), a))
         , f (f (f (X, a), X), Y)
         )

partiell korrekt?

paßt der Term f (f (Y, X), f (f (Z, f (a, a)), a))
zum Muster f (f (Y, undefined), f (f (Z, f (a, undefined)), undefined))
?

Nein: Y /= Y

==============================================================================

===Unify-Quiz-2===

Ersetzen Sie in dem Paar von Termen
    (t1, t2) = ( f (undefined, f (undefined, f (Z, f (f (Z, Y), f
(undefined, Y)))))
               , f (undefined, undefined)
               )
die Zeichen undefined so durch Terme, daß
    sigma = listToFM
                [ ( X
                  , f (f (a, f (f (a, f (a, Y)), Y)), f (f (f (a, f (f (a,
f (a, Y)), Y)), Y), f (f (a, f (f (a, f (a, Y)), Y)), Y)))
                  )
                , ( Z , f (a, f (f (a, f (a, Y)), Y)) )
                ]
ein allgemeinster Unifikator von t1 und t2 ist.

==Bei Eingabe der Lösung:==

( f (B, f (A, f (Z, f (f (Z, Y), f (Z, Y)))))
, f (B, f (A, X))
)

==bekomme ich die Ausgabe:==

gelesen: ( f (B, f (A, f (Z, f (f (Z, Y), f (Z, Y)))))
         , f (B, f (A, X))
         )

partiell korrekt?

paßt der Term f (B, f (A, f (Z, f (f (Z, Y), f (Z, Y)))))
zum Muster f (undefined, f (undefined, f (Z, f (f (Z, Y), f (undefined,
Y)))))
?

Nein: Z /= Z