? ; dans la trace qui suit, les entrées de l’utilisateur sont données en rouge

? ; d'abord démontrons l’associativité de append, ou append est définie comme :
? ; (de app (x y)(if (null x) y (cons (car x) (app (cdr x) y))))
?
? (theo (app X (app Y Z)) = (app (app X Y) Z))
** 0 prove (app X (app Y Z)) = (app (app X Y) Z)
** reduit a (app X (app Y Z)) = (app (app X Y) Z)
command ?
(induct list X)
** base
** 1 prove (app nil (app Y Z)) = (app (app nil Y) Z)
** reduit a (app Y Z) = (app Y Z)
** 1 proved
** step
** 1 prove (app (cons g001 X) (app Y Z)) = (app (app (cons g001 X) Y) Z)
** reduit a (cons g001 (app X (app Y Z))) = (cons g001 (app (app X Y) Z))
** 2 prove (cons g001 (app X (app Y Z))) = (cons g001 (app (app X Y) Z))
** reduit a (cons g001 (app X (app Y Z))) = (cons g001 (app (app X Y) Z))
command ?
(indhyp 1 <-)
** 3 prove (cons g001 (app X (app Y Z))) = (cons g001 (app X (app Y Z)))
** reduit a (cons g001 (app X (app Y Z))) = (cons g001 (app X (app Y Z)))
** 3 proved
** 2 proved
** 1 proved
** 0 proved

? ; ensuite avec la fonction reverse (rev) définie comme :
? ; (de rev (x) (if (null x) nil (app (rev (cdr x)) (cons (car x) nil))))
? ; démontrons que :
? (theo (app (rev A) (rev B)) = (rev (app B A)))
** 0 prove (app (rev A) (rev B)) = (rev (app B A))
** reduit a (app (rev A) (rev B)) = (rev (app B A))
command ?
(induct list B)
** base
** 1 prove (app (rev A) (rev nil)) = (rev (app nil A))
** reduit a (app (rev A) nil) = (rev A)
** 2 prove (app (rev A) nil) = (rev A)
** reduit a (app (rev A) nil) = (rev A)
command ?
(gen C (rev A))
** 3 prove (app C nil) = C
** reduit a (app C nil) = C
command ?
(induct list C)
** base
** 4 prove (app nil nil) = nil
** reduit a nil = nil
** 4 proved
** step
** 4 prove (app (cons g002 C) nil) = (cons g002 C)
** reduit a (cons g002 (app C nil)) = (cons g002 C)
** 5 prove (cons g002 (app C nil)) = (cons g002 C)
** reduit a (cons g002 (app C nil)) = (cons g002 C)
command ?
(indhyp 1 ->)
** 6 prove (cons g002 C) = (cons g002 C)
** reduit a (cons g002 C) = (cons g002 C)
** 6 proved
** 5 proved
** 4 proved
** 3 proved
** 2 proved
** 1 proved
** step
** 1 prove (app (rev A) (rev (cons g003 B))) = (rev (app (cons g003 B) A))
** reduit a (app (rev A) (app (rev B) (cons g003 nil))) = (app (rev (app B A)) (cons g003 nil))
** 2 prove (app (rev A) (app (rev B) (cons g003 nil))) = (app (rev (app B A)) (cons g003 nil))
** reduit a (app (rev A) (app (rev B) (cons g003 nil))) = (app (rev (app B A)) (cons g003 nil))
command ?
(indhyp 1 <-)
** 3 prove (app (rev A) (app (rev B) (cons g003 nil))) = (app (app (rev A) (rev B)) (cons g003 nil))
** reduit a (app (rev A) (app (rev B) (cons g003 nil))) = (app (app (rev A) (rev B)) (cons g003 nil))
command ?
(gen X (rev A) Y (rev B) Z (cons g003 nil))
** 4 prove (app X (app Y Z)) = (app (app X Y) Z)
** reduit a (app X (app Y Z)) = (app (app X Y) Z) ;;; c'est le théorème sur l'associativité de append juste démontré!!
command ?
(induct list X)
** base
** 5 prove (app nil (app Y Z)) = (app (app nil Y) Z)
** reduit a (app Y Z) = (app Y Z)
** 5 proved
** step
** 5 prove (app (cons g004 X) (app Y Z)) = (app (app (cons g004 X) Y) Z)
** reduit a (cons g004 (app X (app Y Z))) = (cons g004 (app (app X Y) Z))
** 6 prove (cons g004 (app X (app Y Z))) = (cons g004 (app (app X Y) Z))
** reduit a (cons g004 (app X (app Y Z))) = (cons g004 (app (app X Y) Z))
command ?
(indhyp 1 <-)
** 7 prove (cons g004 (app X (app Y Z))) = (cons g004 (app X (app Y Z)))
** reduit a (cons g004 (app X (app Y Z))) = (cons g004 (app X (app Y Z)))
** 7 proved
** 6 proved
** 5 proved
** 4 proved
** 3 proved
** 2 proved
** 1 proved
** 0 proved


? ; finalement, avec l'addition définie comme :
? ; (de p (x y) (if (zerop x) y (1+ (p (1- x) y))))
? ; démontrons la commutativité de l'addition
? (theo (p x y) = (p y x))
** 0 prove (p x y) = (p y x)
** reduit a (p x y) = (p y x)
command ?
(induct num x)
** base
** 1 prove (p 0 y) = (p y 0)
** reduit a y = (p y 0)
** 2 prove y = (p y 0)
** reduit a y = (p y 0)
command ?
(induct num y)
** base
** 3 prove 0 = (p 0 0)
** reduit a 0 = 0
** 3 proved
** step
** 3 prove (1+ y) = (p (1+ y) 0)
** reduit a (1+ y) = (1+ (p y 0))
** 4 prove (1+ y) = (1+ (p y 0))
** reduit a (1+ y) = (1+ (p y 0))
command ?
(indhyp 1 <-)
** 5 prove (1+ y) = (1+ y)
** reduit a (1+ y) = (1+ y)
** 5 proved
** 4 proved
** 3 proved
** 2 proved
** 1 proved
** step
** 1 prove (p (1+ x) y) = (p y (1+ x))
** reduit a (1+ (p x y)) = (p y (1+ x))
** 2 prove (1+ (p x y)) = (p y (1+ x))
** reduit a (1+ (p x y)) = (p y (1+ x))
command ?
(indhyp 1 ->)
** 3 prove (1+ (p y x)) = (p y (1+ x))
** reduit a (1+ (p y x)) = (p y (1+ x))
command ?
(induct num y)
** base
** 4 prove (1+ (p 0 x)) = (p 0 (1+ x))
** reduit a (1+ x) = (1+ x)
** 4 proved
** step
** 4 prove (1+ (p (1+ y) x)) = (p (1+ y) (1+ x))
** reduit a (1+ (1+ (p y x))) = (1+ (p y (1+ x)))
** 5 prove (1+ (1+ (p y x))) = (1+ (p y (1+ x)))
** reduit a (1+ (1+ (p y x))) = (1+ (p y (1+ x)))
command ?
(indhyp 1 <-)
** 6 prove (1+ (1+ (p y x))) = (1+ (1+ (p y x)))
** reduit a (1+ (1+ (p y x))) = (1+ (1+ (p y x)))
** 6 proved
** 5 proved
** 4 proved
** 3 proved
** 2 proved
** 1 proved
** 0 proved