Start=formaler Beweis

MDLUL/formaler Beweis

Ziel=Prädikatenkalkül/Ableitbar/Definition