fac 0 = 1 (1) fac n = n * fac (n-1) (2) Provar que para todo n fac n > 0 Indução sobre n Caso base n = 0 fac 0 > 0 Passo da indução n = x fac x > 0, onde x > 0 (3) assumindo fac (x-1) > 0 (4) Provando o caso base fac 0 = 1 (por 1) e 1 > 0 (pela aritmética) Provando o passo da indução fac x = x * fac (x-1) (por 2) fac (x-1) > 0 (por 4) x > 0 (por 3) logo x * fac (x-1) > 0 (pela aritmética) PROVADO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% power2 0 = 1 (1) power2 r = 2 * power2 (r-1) (2) Provar que para todo n power2 (n+1) = 2 * power2 n indução sobre n Caso base n = 0 power2 1 = 2 * power2 0 Passo da indução n = x power2 (x+1) = 2 * power2 x assumindo n = x-1 power2 x = 2 * power2 (x-1) (3) Provando o caso base power2 1 = 2 * power2 0 (por 1) (prova direta) Provando o passo da indução power2 (x+1) = 2 * power2 ((x+1)-1) (por 1) = 2 * power2 x (pela aritmética) Prova sem usar suposição do passo da indução PROVADO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sumList [] = 0 (1) sumList (a:as) = a + sumList as (2) double [] = [] (3) double (a:as) = 2*a: double as (4) Provar que para toda lista x sumList (double x) = 2 * sumList x Indução sobre x Caso base x = [] sumList (double []) = 2 * sumList [] Passo da indução x = (y:ys) sumList (double (y:ys)) = 2 * sumList (y:ys) assumindo x = ys sumList (double yx) = 2 * sumList ys (5) Provando o caso base sumList (double []) = sumList [] (por 3) = 0 (por 1) 2 * sumList [] = 2 * 0 (por 1) = 0 (pela aritmética) Provando o passo da indução sumList (double (y:ys)) = sumList (2*y: double ys) (por 4) = 2*y + sumList (double ys) (por 2) = 2*y + 2* sumList ys (por 5) = 2 * (y + sumList ys) (pela aritmética) = 2 * sumList (y:ys) (por 2) PROVADO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% [] ++ y = y (1) (x:xs) ++ y = x:(xs++y) (2) Provar que para todas as lista finitas x, y e z x ++ (y ++ z) = (x ++ y) ++ z Indução sobre x, uma vez que a própria definição de ++ leva em conta apenas a lista do lado esquerdo, a recursão é a esquerda. Caso base x = [] [] ++ (y ++ z) = ([] ++ y) ++ z Passo da indução x = (a:as) (a:as) ++ (y ++ z) = ((a:as) ++ y) ++ z assumindo x = as as ++ (y ++ z) = (as ++ y) ++ z (3) Provando o caso base [] ++ (y ++ z) = (y ++ z) (por 1) = y ++ z ([] ++ y) ++ z = (y) ++ z (por 1) = y ++ z Provando o passo da indução (a:as) ++ (y ++ z) = a:(as ++ (y ++ z)) (por 2) = a:((as ++ y) ++ z) (por 3) = (a:(as ++ y)) ++ z) (por 2) (as ++ y) = xs = ((a:as) ++ y) ++ z) (por 2) (as ++ y) = xs ++ y PROVADO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% member [] b = False (1) member (a:as) b = (a==b) || member as b (2) Provar que para todas as listas finitas x e y member (x++y) c = member x c || member y c Indução sobre x (a recursão tambem é a esquerda na definição de member) Caso base x = [] member ([]++y) c = member [] c || member y c Passo da indução x = (d:ds) member ((d:ds)++y) c = member (d:ds) c || member y c assumindo x = ds member (ds++y) c = member ds c || member y c (3) Provando o caso base member ([]++y) c = member y c (por ++ 1) member [] c || member y c = False || member y c (por 1) = member y c (pela lógica booleana) Provando o passo da indução member ((d:ds)++y) c = member (d:(ds++y)) c (por ++ 2) = (d==c) || member (ds++y) c (por 2) = (d==c) || member ds c || member y c (por 3) = member (d:ds) c || member y c (por 2) ((d==c) || member ds c) = member (d:ds) c PROVADO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% numBorrowed [] per = 0 (1) numBorrowed (a:as) per | (fst a) == per = 1 + numBorrowed as per (2) | otherwise = numBorrowed as per (3) books [] per = 0 (4) books (a:as) per | (fst a) == per = b:books as per (5) | otherwise = books as per (6) Provar que para todos os banco de dados db finitos e todas as pessoas per numBorrowed db per = length (books db per) indução sobre db (é quem sofre a recursão) Caso base db = [] numBorrowed [] per = length (books [] per) Passo da indução db = (a:as) numBorrowed (a:as) per = length (books (a:as) per) assumindo x = as numBorrowed as per = length (books as per) (7) Provando o caso base numBorrowed [] per = 0 (por 1) length (books [] per) = length [] (por 4) = 0 (por length) Provando o passo da indução LADO ESQUERDO numBorrowed (a:as) per se (fst a) == per = 1 + numBorrowed as per (por 2) = 1 + length (books as per) (por 7) senão = numBorrowed as per (por 3) = length (books as per) (por 7) LADO DIREITO length (books (a:as) per) se (fst a) == per = length (b:books as per) (por 5) = 1 + length (books as per) (por length) senão = length (books as per) (por 6) PROVADO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% borrowed [] bk = False (1) borrowed (a:as) bk | (snd a) == bk = True (2) | otherwise = borrowed as bk (3) borrowers [] bk = [] (4) borrowers (a:as) bk | (snd a) == bk = (fst a):borrowers as bk (5) | otherwise = borrowers as bk (6) Provar que para todos os banco de dados db finitos e todas os livros bk borrowed db bk = (borrowers db bk \= []) Indução sobre db Caso base db = [] borrowed [] bk = (borrowers [] bk \= []) Passo da indução db = (a:as) borrowed (a:as) bk = (borrowers (a:as) bk \= []) assumindo x = as borrowed as bk = (borrowers as bk \= []) (7) Provando o caso base borrowed [] bk = False (por 1) borrowers [] bk \= [] = [] \= [] (por 4) = False (por \=) Provando o passo da indução LADO ESQUERDO borrowed (a:as) bk se (snd a) == bk = True (por 2) senão = borrowed as bk (por 3) = borrowers as bk \= [] (por 7) LADO DIREITO borrowers (a:as) bk \= [] se (snd a) == bk = (fst a):borrowers as bk \= [] (por 5) = True (por listas) senão = borrowers as bk \= [] (por 6) PROVADO