Chair For Logic And Verification

Beweis (cprf):

Hintergrundtheorie (cthy):

• T7.1: filter p . filter p .=. filter p
• T6.2: sum2 xs ys = sum xs + sum ys
• T6.1: sum (xs ++ ys) = sum xs + sum ys
• T5.2.2: reverse (reverse xs) .=. xs
• H7.1: foldl f a .=. foldr f a
• H6.2: countGt xs ys <= length xs + length ys
• H6.1: addAbsLt xs y = itAddAbsLt xs y
• H5.2:
• H5.1

Die Beweise werden mit dem Tool Cyp getestet