Wohlfundierte monotone Algebren (II)

• Satz: SN(→_R) $\iff$ ∃ wfmA, die mit R kompatibel ist.

• Beweis (SN(→_R)⇐...): indirekt:

  falls x₀→_Rx₁→_Rx₂→_R... unendlich,

  dann [x₀]_A > [x₁]_A > [x₂]_A > ... unendlich,

  Widerspruch zu SN( > ).

• Beweis (SN(→_R)⇒...) zu konstruieren ist die wfmA:
  • Universum: Term(Σ), Interpretation: Symbol durch sich
  • u > v : ⇔f (u) > f (v) mit f (t) : = max{k | ∃t' : t→_R^kt'}, ist erlaubt (max. über endliche Menge) wegen SN(→_R).
• Das hilft aber nicht bei der Suche nach kompatibler wfmA
• Q: warum ist dieses f keine wfmA ($\mathbb {N}$, > ,[⋅])?

  A: es ist im allgemeinen keine Algebra (kein fold)