# Formal Foundations of Computer Science 1 (Errata) Wolfgang Schreiner
1. A.3/290, last line of Definition 141 (14.10.1999, Werner Danelczyk-Landerl)

Replace

forall x0, ..., xn-1, y: f(x0, ..., xn-1) = y <=> (<x0, ..., xn-1> in A /\  y = T).
by
forall x0, ..., xn-1: <x0, ..., xn-1> in A => f(x0, ..., xn-1) = T.
2. 2.2/12, last line of Proposition 1 (15.10.1999, 4.1.2000, Wolfgang Schreiner)

Drop

(usually x is free in A).
3. 2.3.4/39, last line of Proposition 15 (15.10.1999, Wolfgang Schreiner)

(usually x is free in A).
4. 7.1/229, Proposition 114 (15.10.1999, Wolfgang Schreiner)

Replace

 forall S, R: R is equivalence class on R => x in [x]R.
by
 forall S, R: R is equivalence relation on S => forall x in S: x in [x]R.
5. 4.1/101, Proposition 38 (2.11.1999, Wolfgang Schreiner)

Replace

 for every formula F: (F(0) /\  forall x in N: F(x) => F(x+1)) => forall x in N: F(x).

by

 forall F: (F(0) /\  forall x in N: F(x) => F(x+1)) => forall x in N: F(x).
where the quantified variable F denotes a unary relation.
6. 4.1/107, Definition 41 (2.11.1999, Wolfgang Schreiner)

Replace

A number greater than 1 is  prime (prim) if its only divisors are are 1 and itself:

by

A number greater than 1 is  prime (prim) if its only divisors are 1 and itself:
7. 4.5/124, Definition 51 (2.11.1999, Wolfgang Schreiner)

Replace

 x * y := ((x0 *R y0) -R (x1 *R y1)) + ((x0 * R y1) + (x1 *R y0))i;

by

 x * y := ((x0 *R y0) -R (x1 *R y1)) + ((x0 * R y1) +R (x1 *R y0))i;
8. 4.2/112, Proof of Proposition 44 (2.11.1999, Wolfgang Schreiner)

Replace

 (x+(-y))+y = (associativity of+)

by

 (x+(-y))+y = (associativity of +)
9. 4.7.2/130,133, Definitions 56 and 57 (2.11.1999, Wolfgang Schreiner)

Replace "for some x" by "for every x".

10. 3.5/94, Definition 30 (7.11.1999, Clemens Holzmann)

Replace

s is a finite sequence over S : <=>
exists n in N: s is a sequence of length n over S.
by
s is a finite sequence over S : <=>
exists n in N: s is a sequence of length n over S.
11. 3.5/97, Example (7.11.1999, Clemens Holzmann)

Replace

A0 = 0, A1 =0, A2 = 3; A3=1; A4=2.

by

A0 = 0, A1 =0, A2 = 3; A3=1; A4=1.
12. 4.1/104, erster Satz (9.11.1999, Student)

Replace

x <= a /\  x < b

by

a <= x /\  x < b
13. 4.7.2/130 (16.11.1999, Bernhard Aichinger)

Replace

is used to denote (sum0 <= i <= a T).

by

is used to denote (suma <= i <= b T).
14. 4.7.2/133 (16.11.1999, Wolfgang Schreiner)

Replace

 (prodx, F T) = T[x <- y] + (prodx, F /\  x != y T)).

by

 (prodx, F T) = T[x <- y] * (prodx, F /\  x != y T)).
15. 4.7.3/136 (16.11.1999, Wolfgang Schreiner)

Replace

(n k) = (prodn-k+1 <= i <= n i)/(prod1 <= i <= n i).

by

(n k) = (prodn-k+1 <= i <= n i)/(prod1 <= i <= k i).
16. 4.7.5/141, Definition 64 (16.11.1999, Wolfgang Schreiner)

Replace

 [ ]: Poly x R -> R p[a] := (sum0 <= i <= deg(p) pi*ai).

by

 [ ]: Poly x R -> R p[a] := (sum0 <= i <= deg(p) pi *R ai).
17. 4.7.5/141, Proposition 63 (16.11.1999, Wolfgang Schreiner)

Replace

 cPoly[a] = cPoly, x[a] = aPoly, (p+q)[a] = p[a] + q[a], (p*q)[a] = p[a] * q[a].

by

 cPoly[a] = c, x[a] = a, (p+q)[a] = p[a] +R q[a], (p*q)[a] = p[a] *R q[a].
18. 4.7.5/142, Example (16.11.1999, Wolfgang Schreiner)

Replace

 (x+1) = 2+1 (= 3Poly) (x*x) = 2*2 (= 4Poly) (x*x+2*x+1) = 3*3+2*3+1 (= 16Poly)

by

 (x+1) = 2+1 = 3 (x*x) = 2*2 = 4 (x*x+2*x+1) = 3*3+2*3+1 = 16
19. 3.3/82, after Definition 27 (16.11.1999, Student)

Replace

a in A /\  c in C

by

a in domain(R) /\  c in range(S)
20. 6.2/178, Proposition 76 (18.11.1999, Wolfgang Schreiner)

Replace

Proposition

by

Definition
21. 5.1/146, Definition 66 (23.11.1999, Martin Reichör)

Replace

is the  base formula in which f does not occur and where every application of f in the  recursion formula

by

is the  base formula in which p does not occur and where every application of p in the  recursion formula
22. 6.2/183, Proposition 82 (24.11.1999, Werner Danielczyk-Landerl)

Replace

The number of permutations of length n is 2n:
forall n in N: |{f: f is permutation of length n}| = 2n.

by

The number of permutations of length n is n!:
forall n in N: |{f: f is permutation of length n}| = n!.
23. 6.2/183, Proof of Proposition 82 (24.11.1999, Werner Danielczyk-Landerl)

Replace

Assume |{f: f is permutation of length n}| = 2n.

by

Assume |{f: f is permutation of length n}| = n!.
24. 6.3/188 (24.11.1999, Werner Danielczyk-Landerl)

Replace

Thus we can define a "polar" variant of C
C' := R x [0,2pi[
assuming that angles are uniquely expressed in "radians" (i.e., pi = 180 o ).

by

Thus we can define a "polar" variant of C
C' := (R> 0 x [0,2pi[) union {<0,3 pi /2>}
where we assume that angles are uniquely expressed in "radians" (i.e., pi = 180 o ) and assign to the zero point the unique (but arbitrary) angle 3 pi /2 (see the definition of "polar" given below).
25. 6.2/180, Proposition 80 (24.11.1999, Werner Danielczyk-Landerl))

Replace

Every set is smaller than the set of all functions into it:
 forall A, B: B is smaller than A -> B.

by

Every set is smaller than the set of all functions from an infinite domain into it:
 forall A, B: A is infinite => B is smaller than A -> B.
26. 5.2/148 (23.11.1999, Wolfgang Schreiner)

Replace

(4) n+1 < 2n+1 <= 2n+2n = 2*2n = 2n+1

by

(4) n+1 < 2n+1 <= 2n+2n = 2*2n = 2n+1
27. 5.4/160 (23.11.1999, Wolfgang Schreiner)

Replace

for some constructors "empty" and "tree".

by

for some constructors "empty" and "node".
28. 5.4/161 (23.11.1999, Wolfgang Schreiner)

Replace

An element of "Formula" is "forall(X, and(T, or(T, F)))" (assuming X in "Variable").

by

An element of "Formula" is "forall(X, and(T, and(T, T)))" (assuming X in "Variable").
29. 5.4/162 (23.11.1999, Wolfgang Schreiner)

Replace

 value: Term -> N value(0) := 0N value(1) := 1N value(-x) := -Nvalue(x) value(x+y) := value(x)+Nvalue(y) value(x*y) := value(x)*Nvalue(y)

by

 value: Term -> Z value(0) := 0Z value(1) := 1Z value(-x) := -Zvalue(x) value(x+y) := value(x)+Zvalue(y) value(x*y) := value(x)*Zvalue(y)
30. B.5.2/324, Proposition 155 (Werner Danielczyk-Landerl, 24.11.1999)

Replace

 (exists x: A) /\  (exists x: B) (exists x: A /\  B)

by

 (exists x: A /\  B) (exists x: A) /\  (exists x: B)
31. 6.4/198, Example (Clemens Holzmann, 24.11.1999)

Change the example to

Let s := [(-1)i*1/i]i. We show that s converges to 0. Take arbitrary epsilon > 0. We have to find some n in N such that
forall i >= n: |(-1)i*1/i - 0| < epsilon
which can be simplified to
forall i >= n: 1/i < epsilon .
Take n := such n in N: 1/ epsilon < n. Because epsilon > 0, we know 1/ epsilon in R>0. Because N is unbounded (i.e., forall r in R: exists n in N: r < n), we know 1/ epsilon < n and thus n > 0.

Take arbitrary i >= n. We then know i > 0 and

1/i <= 1/n < 1/1/ epsilon = epsilon .
32. 6.1/167, Definition 71 (Wolfgang Schreiner, 24.11.1999)

Replace

f is  surjective (surjektiv) (also called  onto) if it

by

f is  surjective (surjektiv) (also called  onto) if
33. 6.4/192, Definition 80 (Wolfgang Schreiner, 26.11.1999)

Replace

f is  monotonically decreasing (monoton wachsend)

by

f is  monotonically decreasing (monoton fallend)

Replace

f is  strictly monotonically decreasing (streng monoton wachsend)

by

f is  strictly monotonically decreasing (streng monoton fallend)
34. 6.4/194, Definition 81 (Wolfgang Schreiner, 26.11.1999)

Replace

f has a lower bound (untere Schranke) L, if every element of f is lower than or equal L:
L is lower bound of f : <=> f: N -> R /\  forall i in N: fi <= L.

by

f has a lower bound (untere Schranke) L, if every element of f is greater than or equal L:
L is lower bound of f : <=> f: N -> R /\  forall i in N: fi >= L.
35. 6.5/205, Definition 87 (Wolfgang Schreiner, 26.11.1999)

Replace

(f+g)(x) := f(x) - g(x);

by

(f-g)(x) := f(x) - g(x);
36. 6.5/207 (Wolfgang Schreiner, 26.11.1999)

Replace

if we shift it up one unit, it lies completely above the floor function

by

if we shift it up one unit, it lies completely above the ceiling function
37. B.4/316, first paragraph (Student, 30.11.1999)

Replace

If we have to show G0 <=> G1 <=> G2, i.e., (G0 <=> G1) /\  (G1 <=> G0),

by

If we have to show G0 <=> G1 <=> G2, i.e., (G0 <=> G1) /\  (G1 <=> G2),
38. B.4/317, after Proposition 145 (Wolfgang Schreiner, 30.11.1999)

Replace

 K G0 /\  G1
~~>
 K union {~G0 \/ ~G1} F(alse)
~~>
 K union ~G0 F(alse)
 K union ~G1 F(alse)

by

 K G0 /\  G1
~~>
 K union {~G0 \/ ~G1} F(alse)
~~>
 K union {~G0} F(alse)
 K union {~G1} F(alse)
39. B.4/317, Proposition 146 (Wolfgang Schreiner, 30.11.1999)

Replace

 K G0 \/ G1
~~>
 K union ~G0 G1

by

 K G0 \/ G1
~~>
 K union {~G0} G1
40. B.4/318, Proposition 148 (Wolfgang Schreiner, 30.11.1999)

Replace

For proving the goal F[x <- G(a0, ..., an-1)] where f is a function explicitly defined as
G(x0, ..., xn-1) := T,
it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]] (for some terms T, a0, ..., an-1):
 K union {forall x0, ..., xn-1: G(x0, ..., xn-1) = T} G[x <- G(a0, ..., an-1)]
~~>
 K union {forall x0, ..., xn-1: G(x0, ..., xn-1) = T} G[x <- T[x0 <- a0, ..., xn-1 <- an-1]]

by

For proving the goal G[x <- F(a0, ..., an-1)] where F is a function explicitly defined as
F(x0, ..., xn-1) := T,
it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]] (for some terms T, a0, ..., an-1):
 K union {forall x0, ..., xn-1: F(x0, ..., xn-1) = T} G[x <- F(a0, ..., an-1)]
~~>
 K union {forall x0, ..., xn-1: F(x0, ..., xn-1) = T} G[x <- T[x0 <- a0, ..., xn-1 <- an-1]]

After the definition: replace

We have to prove F[x <- G(a0, ..., an-1)]. By definition of G, it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]].

by

We have to prove G[x <- F(a0, ..., an-1)]. By definition of F, it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]].
41. B.5/321, Proposition 152 (Wolfgang Schreiner, 30.11.1999)

Replace

 K G
~~>
 K union F G
(F holds in every domain in which K holds).

by

 K G
~~>
 K union {F} G
(F holds in every domain in which K holds).
42. 6.2/176, Proposition 75 (Wolfgang Schreiner, 7.12.1999)

Replace

If A is of size n, then A has 2n subsets:
 forall A, n in N: |A| = n => |{S in P(S): T}| = 2n.

by

If A is of size n, then A has 2n subsets:
 forall A, n in N: |A| = n => |P(A)| = 2n.
43. 6.2/182, Example (Wolfgang Schreiner, 7.12.1999)

Replace

 t is sorted with respect to <= : <=> forall 0 <= i < length(t): ti <= ti+1.

by

 t is sorted with respect to <= : <=> forall 0 <= i < length(t)-1: ti <= ti+1.
44. 6.3/186 (Wolfgang Schreiner, 7.12.1999)

Replace

 (x + y)[a] = x(a) +R y(a) (x - y)[a] = x(a) -R y(a) (-x)[a] = -Rx(a) (x * y)[a] = x(a) *R y(a)

by

 (x + y)[a] = x[a] +R y[a] (x - y)[a] = x[a] -R y[a] (-x)[a] = -Rx[a] (x * y)[a] = x[a] *R y[a]
45. 6.3/189 (Wolfgang Schreiner, 7.12.1999)

Replace

 cartesian: C ->iso(*C, *C') C' polar: C' ->iso(*C', *C) C

by

 polar: C ->iso(*C, *C') C' cartesian: C' ->iso(*C', *C) C
46. 6.3/191, Picture (Wolfgang Schreiner, 7.12.1999)

Replace the picture by 47. B.3/312 (Gerhard Nussbaum, 6.12.1999)

Replace

Again, since we don't know the truth of G for sure, we generally we have two possibilities:

by

Again, since we don't know the truth of G for sure, we generally have two possibilities:
48. 6.4/195, Example (Wolfgang Schreiner, 14.12.1999)

Replace

[i3]i has no upper bound and no lower bound.

by

[i3*(-1)i]i has no upper bound and no lower bound.
49. 6.5/207, Picture (Wolfgang Schreiner, 14.12.1999)

Replace picture by 50. 4.2/112, After Proof (Michael Petz, 15.12.1999)

Replace

Thus our definition of Z meets one of the two requirements stated at the begin of this section.

by

Thus our definition of Z meets one of the two requirements stated at the beginning of this section.

Also on page 117, after proof: replace

Our definition of Q meets one of the two requirements stated at the begin of this section.

by

Our definition of Q meets one of the two requirements stated at the beginning of this section.

Also on page 121, after example: replace

Then we have the following result which implies that the problem stated at the begin of this section can be solved.

by

Then we have the following result which implies that the problem stated at the beginning of this section can be solved.

Also on page 124, after Definition 152: replace

This imaginary constant is the "missing value" that solves the equation stated at the begin of this section.

by

This imaginary constant is the "missing value" that solves the equation stated at the beginning of this section.
51. 6.2/183, Example (Clemens Holzmann, 19.12.1999)

Replace

Then
p o q = [1,2,0,4,3],
e.g., (p o q)(2) = q(p(2)) = q(4) = 0. We also have
 p-1 = [2,0,1,4,3]
e.g., p-1(2) = 1 because p(1)=2, and thus
 p o p-1 = p-1 o p = [0,1,2,3,4].

by

Then
r := p o q = [1,2,0,4,3],
e.g., r(2) = (p o q)(2) = q(p(2)) = q(4) = 0. We also have
 r-1 = [2,0,1,4,3]
e.g., r-1(2) = 1 because r(1)=2, and thus
 r o r-1 = r-1 o r = [0,1,2,3,4].
52. 7.1.1/226, Example (Wolfgang Schreiner, 4.1.2000)

Replace

Let r(x, y) : <=> x0+y0 = x1+y1. Then r is an equivalence relation on R x R.

by

Let r(x, y) : <=> x0+y1 = x1+y0. Then r is an equivalence relation on R x R.
53. 5.2/153, Proof (Wolfgang Schreiner, 4.1.2000)

Replace

Take k:=ka+kb and f(i):=if i < ka then fa(i) else fb(i).

by

Take k:=ka+kb and f(i):=if i < ka then fa(i) else fb(i-ka).
54. 7.1/245, Proposition 124 (Wolfgang Schreiner, 11.1.2000)

Replace

 i(0Z') = 0Z, i(x+Z'y) = x+Zy, i(-Z' x) = -Z x, i(x-Z'y) = x-Zy, i(x*Z'y) = i(x)*Zi(y), x <= Z' y <=> i(x) <= Z i(y).

by

 i(0Z') = 0Z, i(x+Z'y) = i(x)+Zi(y), i(-Z' x) = -Z i(x), i(x-Z'y) = i(x)-Zi(y), i(x*Z'y) = i(x)*Zi(y), x <= Z' y <=> i(x) <= Z i(y).
55. 7.1/245, Proof (Wolfgang Schreiner, 11.1.2000)

Replace the proof by

Take arbitrary x in Z' and y in Z'. We prove
 i(x+Z'y) = i(x)+Zi(y).
We know
 i(x+Z'y) = i(I(x0 +N y0, x1 +N y1)).
Case x0 +N y0 >= x1 +N y1:
We have
 i(I(x0 +N y0, x1 +N y1)) = i(<(x0 +N y0) - (x1 +N y1)>) = [<(x0 +N y0) - (x1 +N y1)>] = (definition  ~ Z) [] = (congruence properties) [x] +Z [y] = i(x) +Z i(y).
Case x0 +N y0 < x1 +N y1:
Proceeds analogously.
56. 7.1/248, Proposition 126 (Wolfgang Schreiner, 11.1.2000)

Replace

 i(0Q') = 0Q, i(x+Q'y) = x+Qy, i(-Q' x) = -Q x, i(x-Q'y) = x-Qy, i(x*Q'y) = x*Qy, i(x-1) = x-1, i(x/Q'y) = x/Qy, x <= Q' y <=> i(x) <= Q i(y).

by

 i(0Q') = 0Q, i(x+Q'y) = i(x)+Qi(y), i(-Q' x) = -Q i(x), i(x-Q'y) = i(x)-Qi(y), i(x*Q'y) = i(x)*Qi(y), i(x-1) = i(x)-1, i(x/Q'y) = i(x)/Qi(y), x <= Q' y <=> i(x) <= Q i(y).
57. 7.1/234, Example (Wolfgang Schreiner, 11.1.2000)

Replace

 B := {x in N: x is odd /\  x is not prime}.

by

 C := {x in N: x is odd /\  x is not prime}.
58. 7.1/230, Example (Wolfgang Schreiner, 12.1.2000)

Replace

Let r subset R x R such that r(x, y) <=> x0+x1 = y0+y1.

by

Let r subset (R x R) x (R x R) such that r(x, y) <=> x0+x1 = y0+y1.
59. 7.2/253, Definition 116 (Wolfgang Schreiner, 13.1.2000)

Replace definition by

A binary relation on S is a  quasi order (Quasi-Ordnung), if it is irreflexive and transitive:
 R is quasi order on S : <=> R subset S x S /\ R is irreflexive on S /\ R is transitive on S.
60. 7.2/261, Before Picture (Wolfgang Schreiner, 13.1.2000)

Replace

Please note that an lower (respectively upper bound) of a set S need not be an element of S:

by

Please note that a lower (respectively upper) bound of a set S need not be an element of S:
61. 7.3/270, Definition 128 (Wolfgang Schreiner, 14.1.2000)

Replace

A path from x to y has initial node x and terminal node y : <=>

by

A path from x to y has initial node x and terminal node y:
62. 7.3/272, Example (Wolfgang Schreiner, 14.1.2000)

Replace

 reflexiveN5(E) = {<0, 0>, <1, 1>, <2, 2>, <3, 3>, <4, 4>}.

by

 reflexiveN5(E) = E union {<0, 0>, <1, 1>, <2, 2>, <3, 3>, <4, 4>}.
63. 7.3/273, Proposition 132 (Wolfgang Schreiner, 14.1.2000)

Replace

 forall S, R: R subset S x S => reflexiveS(R) = R union (S x S).

by

 forall S, R: R subset S x S => reflexiveS(R) = R union {: x in S}.
64. 7.3/260, Definition 120 (Wolfgang Ziegler, 18.1.2000)

Replace

If x is an element of S such that no element of S is smaller than S, then x is called a  minimal element (minimales Element) of S.
...
Correspondingly, if x is an element of S such that no element of S is greater than S, then x is called a  maximal element (maximales Element) of S.

by

If x is an element of S such that no element of S is smaller than x, then x is called a  minimal element (minimales Element) of S.
...
Correspondingly, if x is an element of S such that no element of S is greater than x, then x is called a  maximal element (maximales Element) of S.
65. 7.3/263, Definition 123 (18.1.2000, Student)

Replace

A  directed graph (gerichteter Graph) is a pair <V, E> of a set V of  vertices (Knoten) or  nodes and a set of E of  edges (Kanten) or  arcs where E is a binary relation on S:

by

A  directed graph (gerichteter Graph) is a pair <V, E> of a set V of  vertices (Knoten) or  nodes and a set of E of  edges (Kanten) or  arcs where E is a binary relation on V:
66. 7.3/263, after Definition 123 (18.1.2000, Wolfgang Schreiner)

Replace

by

67. 7.2/255, Example (18.1.2000, Wolfgang Schreiner)

Replace

w := such u in W_n-1: forall i in N_n-1: u_i = w_i+1

by

w := such u: exists n in N: w in W_n /\  u in W_n-1 /\  forall i in N_n-1: u_i = w_i+1

Replace

w <= _n u : <=> n = 0 \/ w_0 < u_0 \/ (w_0 = u_0 /\  w <= _n-1 u)

by

w <= _n u : <=> n = 0 \/ w_0 < u_0 \/ (w_0 = u_0 /\  w <= _n-1 u)
68. 7.3/270, Definition 128 (25.1.2000, Wolfgang Schreiner)

Replace

 length(p) := such n in N: p: Nn+1 -> V.

by

 length(p) := such n in N: exists V: p: Nn+1 -> V.
69. 7.3/271, Definition 128 (25.1.2000, Wolfgang Schreiner)

Replace

 p is elementary : <=> forall i in Nn, j in Nn: pi = pj => i = j where n = length(p).

by

 p is elementary : <=> forall i in Nn, j in Nn: pi = pj => i = j where n = 1+length(p).
70. 7.1/248, Proposition 126 (25.1.2000, Wolfgang Ziegler)

Replace

Let Q' denote the old construction of the integers and Q denote the new one.

by

Let Q' denote the old construction of the rationals and Q denote the new one.
71. 7.3/266, Example (25.1.2000, Wolfgang Schreiner)

Drop the

```  return C;
```
72. 7.3/274, before Trees (25.1.2000, Wolfgang Schreiner)

Replace

(see the example on page 105)

by

(see the example on page 265)
73. 7.3/273, after Proposition 133 (26.1.2000, Wolfgang Schreiner)

Replace

In other words, the transitive closure of R is the union of all members of the sequence

by

In other words, we can compute the transitive closure of R by the sequence
74. B/308, end of second paragraph (31.1.2000, Wolfgang Ziegler)

Replace

if we are given some knowledge, we must able to check it (i.e., its proof).

by

if we are given some knowledge, we must be able to check it (i.e., its proof).
75. B/309, second paragraph (31.1.2000, Wolfgang Ziegler)

Replace

the skeleton provided by the proof rules help us
the skeleton provided by the proof rules helps us
76. B.5/321, before Proposition 152 (31.1.2000, Wolfgang Ziegler)

Replace

and the proof that the square root of 2 is not rational on page 4.4

by

and the proof that the square root of 2 is not rational on page 118
77. B.5/321, Proposition 152 (31.1.200, Wolfgang Ziegler)

Replace

if F holds in every domain in which (some of) the formulas in K holds.

by

if F holds in every domain in which (some of) the formulas in K hold.

Maintainer: Wolfgang Schreiner
Last Modification: January 31, 2000

[Up] [RISC-Linz] [University] [Search]