Programming Notes – Programming Solutions Part 2
Theorem 1: given k£n, ("i|k£i£n:P[i] {r} R[i]) Þ (Çi|k£i£n:P[i]) {r} (Çi|k£i£n:R[i])
(Given k£n, prove LHS Þ RHS using induction)
Case n=k
("i|k£i£k:P[i] {r} R[i])
º(Arithmetic, one point
rule)
P[k] {r} R[k]
º(one point rule)
(Çi|k£i£k:P[i]) {r} (Ç|k£i£k:R[i])
End of Proof Case n=k
Case n=m,m+1
(Given true for
n=m, prove true for n=m+1)
("i|k£i£m+1:P[i] {r} R[i])
º(Split off term)
("i|k£i£m:P[i] {r} R[i]) Ù P[m+1] {r} R[m+1]
º(Given)
(Çi|k£i£m:P[i]) {r} (Çi|k£i£m:R[i]) Ù P[m+1] {r} R[m+1]
((Çi|k£i£m:P[i])ÇP[m+1]) {r} (Çi|k£i£m:R[i])ÇR[m+1])
º(Split off terms)
(Çi|k£i£m+1:P[i]) {r} (Çi|k£i£m+1:R[i])
End of Proof Case n=m,m+1
End of Proof
Theorem 2: ("i|k£i£n:P[i] {r} R[i]) Þ (Èi|k£i£n:P[i]) {r} (Èi|k£i£n:R[i])
(Prove LHS Þ RHS using induction)
Case n<k
("i|k£i£n:P[i] {r} R[i])
º(Arithmetic)
("i|false:P[i] {r} R[i])
º(empty range)
true
Æ {r} Æ
º(Empty Range)
(Èi|false:P[i]) {r} (È|false:R[i])
º(n<k, arithmetic)
(Èi|k£i£n:P[i]) {r} (È|k£i£n:R[i])
End of Proof Case n=k
Case n=m,m+1
(Given true for
n=m, prove true for n=m+1)
("i|k£i£m+1:P[i] {r} R[i])
º(Split off term)
("i|k£i£m:P[i] {r} R[i]) Ù P[m+1] {r} R[m+1]
º(Given)
(Èi|k£i£m:P[i]) {r} (Èi|k£i£m:R[i]) Ù P[m+1] {r} R[m+1]
((Èi|k£i£m:P[i])ÈP[m+1]) {r} (Èi|k£i£m:R[i])ÈR[m+1])
º(Split off terms)
(Èi|k£i£m+1:P[i]) {r} (Èi|k£i£m+1:R[i])
End of Proof Case n=m,m+1
End of Proof
Theorem 3: given k£n, ("i|k£i£n:P {r} R[i]) º P {r} (Çi|k£i£n:R[i])
(Given k£n, prove LHS º RHS using induction)
Case n=k
("i|k£i£k:P {r} R[i])
º(Arithmetic, one point
rule)
P {r} R[k]
º(one point rule)
P {r} (Ç|k£i£k:R[i])
End of Proof Case n=k
Case n=m,m+1
(Given true for n=m,
prove true for n=m+1)
("i|k£i£m+1:P {r} R[i])
º(Split off term)
("i|k£i£m:P {r} R[i]) Ù P {r} R[m+1]
º(Given)
P {r} (Çi|k£i£m:R[i]) Ù P {r} R[m+1]
P {r} (Çi|k£i£m:R[i])ÇR[m+1])
º(Split off terms)
P {r} (Çi|k£i£m+1:R[i])
End of Proof Case n=m,m+1
End of Proof
Theorem 4: ("i|k£i£n:P[i] {r} R) º (Èi|k£i£n:P[i]) {r} R
(Prove LHS Þ RHS using induction)
Case n<k
("i|k£i£n:P[i] {r} R)
º(n<k, arithmetic)
("i|false:P[i] {r} R)
º(empty range)
true
Æ {r} R
º(Empty Range)
(Èi|false:P[i]) {r} R
º(n<k, arithmetic)
(Èi|k£i£n:P[i]) {r} R
End of Proof Case n=k
Case n=m,m+1
(Given true for n=m,
prove true for n=m+1)
("i|k£i£m+1:P[i] {r} R)
º(Split off term)
("i|k£i£m:P[i] {r} R) Ù P[m+1] {r} R
º(Given)
(Èi|k£i£m:P[i]) {r} R Ù P[m+1] {r} R
((Èi|k£i£m:P[i])ÈP[m+1]) {r} R
º(Split off term)
(Èi|k£i£m+1:P[i]) {r} R
End of Proof Case n=m,m+1
End of Proof
References:
Dijkstra, Edsgar, 1976, A Discipline of
Programming, Englewood Cliffs, NJ: Prentice-Hall
Fejer,
Peter and Simovici, Dan A., 1991, Mathematical Foundations of Computer
Science, New York, NY: Springer-Verlag
Gries, David, 1981, The
Science of Programming, New York, NY: Springer-Verlag
Gries, David and Schneider,
Fred B., 1993, A Logical Approach to Discrete Math, New York, NY:
Springer-Verlag