1) Prove that `(∀cs | cs is finite) putCharList cs = map putChar cs`

where

putCharList [] = [] putCharList (c:cs) = putChar c : putCharList cs map f [] = [] map f (x:xs) = f x : map f xs |

Base case:

putCharList [] => [] => map putChar [] |

Inductive Step:

assume that `purCharList cs = map putChar cs`

then

putCharList (c:cs) => putChar c : putCharList cs => putChar c : map putChar cs => map putChar (c:cs) |

QED.

2) Prove that `(∀xs | xs is finite) listProd xs = fold (*) 1 xs`

where

listProd [] = 1 listProd (x:xs) = x * listProd xs fold op init [] = init fold op init (x:xs) = x `op` fold op init xs |

Base case:

listProd [] => 1 => fold (*) 1 [] |

Inductive Step:

assume that `listProd xs = fold (*) 1 xs`

then

listProd (x:xs) => x * listProd xs => x * fold (*) 1 xs => fold (*) 1 (x:xs) |

QED.