THEOREM

*******

The composition of functions is associative, i.e. (f3 o (f2 o f1)(x) = ((f3 o f2) o f1)(x)

Notation:

f21(x) = (f2 o f1)(x)

f32(x) = (f3 o 2)(x)

f321(x) = (f3 o (f2 o f1))(x)

f321’(x) = ((f3 o (f2 o f1))(x)

We prove that f321(x) = f321’(x).

This machine verified, formal proof with written with the aid of the author's DC Proof 2.0 freeware available http://www.dcproof.com

PREVIOUS RESULT

***************

Define: Composition of functions (see proof here)

1 ALL(a):ALL(b):ALL(c):ALL(f1):ALL(f2):[Set(a) & Set(b) & Set(c)

& ALL(d):[d e a => f1(d) e b]

& ALL(d):[d e b => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e a => f2f1(d) e c]

& ALL(d):[d e a => f2f1(d)=f2(f1(d))]]]

Axiom

PROOF

*****

Suppose we have sets w, x, y and z and functions

f1: w --> x

f2: x --> y

f3: y --> z

2 Set(w) & Set(x) & Set(y) & Set(z)

& ALL(e):[e e w => f1(e) e x]

& ALL(e):[e e x => f2(e) e y]

& ALL(e):[e e y => f3(e) e z]

Premise

We have sets w, x, y and z

3 Set(w)

Split, 2

4 Set(x)

Split, 2

5 Set(y)

Split, 2

6 Set(z)

Split, 2

f1: w --> x

7 ALL(e):[e e w => f1(e) e x]

Split, 2

f2: x --> y

8 ALL(e):[e e x => f2(e) e y]

Split, 2

f3: y --> z

9 ALL(e):[e e y => f3(e) e z]

Split, 2

Apply definition of composition for functions f1 and f2

10 ALL(b):ALL(c):ALL(f1):ALL(f2):[Set(w) & Set(b) & Set(c)

& ALL(d):[d e w => f1(d) e b]

& ALL(d):[d e b => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e c]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 1

11 ALL(c):ALL(f1):ALL(f2):[Set(w) & Set(x) & Set(c)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e c]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 10

12 ALL(f1):ALL(f2):[Set(w) & Set(x) & Set(y)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f2(d) e y]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e y]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 11

13 ALL(f2):[Set(w) & Set(x) & Set(y)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f2(d) e y]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e y]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 12

14 Set(w) & Set(x) & Set(y)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f2(d) e y]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e y]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]

U Spec, 13

15 Set(w) & Set(x)

Join, 3, 4

16 Set(w) & Set(x) & Set(y)

Join, 15, 5

17 Set(w) & Set(x) & Set(y)

& ALL(e):[e e w => f1(e) e x]

Join, 16, 7

18 Set(w) & Set(x) & Set(y)

& ALL(e):[e e w => f1(e) e x]

& ALL(e):[e e x => f2(e) e y]

Join, 17, 8

19 EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e y]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]

Detach, 14, 18

20 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

E Spec, 19

Define: f21 (The composition f2 o f1: w --> y)

21 ALL(d):[d e w => f21(d) e y]

Split, 20

22 ALL(d):[d e w => f21(d)=f2(f1(d))]

Split, 20

Apply definition of composition for functions f3 and (f2 o f1)

23 ALL(b):ALL(c):ALL(f1):ALL(f2):[Set(w) & Set(b) & Set(c)

& ALL(d):[d e w => f1(d) e b]

& ALL(d):[d e b => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e c]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 1

24 ALL(c):ALL(f1):ALL(f2):[Set(w) & Set(y) & Set(c)

& ALL(d):[d e w => f1(d) e y]

& ALL(d):[d e y => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e c]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 23

25 ALL(f1):ALL(f2):[Set(w) & Set(y) & Set(z)

& ALL(d):[d e w => f1(d) e y]

& ALL(d):[d e y => f2(d) e z]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 24

26 ALL(f2):[Set(w) & Set(y) & Set(z)

& ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e y => f2(d) e z]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f2(f21(d))]]]

U Spec, 25

27 Set(w) & Set(y) & Set(z)

& ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e y => f3(d) e z]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f3(f21(d))]]

U Spec, 26

28 Set(w) & Set(y)

Join, 3, 5

29 Set(w) & Set(y) & Set(z)

Join, 28, 6

30 Set(w) & Set(y) & Set(z)

& ALL(d):[d e w => f21(d) e y]

Join, 29, 21

31 Set(w) & Set(y) & Set(z)

& ALL(d):[d e w => f21(d) e y]

& ALL(e):[e e y => f3(e) e z]

Join, 30, 9

32 EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f3(f21(d))]]

Detach, 27, 31

33 ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

E Spec, 32

Define: f321 (The composition f3 o (f2 o f1): w --> z)

34 ALL(d):[d e w => f321(d) e z]

Split, 33

35 ALL(d):[d e w => f321(d)=f3(f21(d))]

Split, 33

Apply definition of composition for functions f2 and f3

36 ALL(b):ALL(c):ALL(f1):ALL(f2):[Set(x) & Set(b) & Set(c)

& ALL(d):[d e x => f1(d) e b]

& ALL(d):[d e b => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e x => f2f1(d) e c]

& ALL(d):[d e x => f2f1(d)=f2(f1(d))]]]

U Spec, 1

37 ALL(c):ALL(f1):ALL(f2):[Set(x) & Set(y) & Set(c)

& ALL(d):[d e x => f1(d) e y]

& ALL(d):[d e y => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e x => f2f1(d) e c]

& ALL(d):[d e x => f2f1(d)=f2(f1(d))]]]

U Spec, 36

38 ALL(f1):ALL(f2):[Set(x) & Set(y) & Set(z)

& ALL(d):[d e x => f1(d) e y]

& ALL(d):[d e y => f2(d) e z]

=> EXIST(f2f1):[ALL(d):[d e x => f2f1(d) e z]

& ALL(d):[d e x => f2f1(d)=f2(f1(d))]]]

U Spec, 37

39 ALL(f):ALL(g):[Set(x) & Set(y) & Set(z)

& ALL(d):[d e x => f(d) e y]

& ALL(d):[d e y => g(d) e z]

=> EXIST(f2f1):[ALL(d):[d e x => f2f1(d) e z]

& ALL(d):[d e x => f2f1(d)=g(f(d))]]]

Rename, 38

40 ALL(g):[Set(x) & Set(y) & Set(z)

& ALL(d):[d e x => f2(d) e y]

& ALL(d):[d e y => g(d) e z]

=> EXIST(f2f1):[ALL(d):[d e x => f2f1(d) e z]

& ALL(d):[d e x => f2f1(d)=g(f2(d))]]]

U Spec, 39

41 Set(x) & Set(y) & Set(z)

& ALL(d):[d e x => f2(d) e y]

& ALL(d):[d e y => f3(d) e z]

=> EXIST(f2f1):[ALL(d):[d e x => f2f1(d) e z]

& ALL(d):[d e x => f2f1(d)=f3(f2(d))]]

U Spec, 40

42 Set(x) & Set(y)

Join, 4, 5

43 Set(x) & Set(y) & Set(z)

Join, 42, 6

44 Set(x) & Set(y) & Set(z)

& ALL(e):[e e x => f2(e) e y]

Join, 43, 8

45 Set(x) & Set(y) & Set(z)

& ALL(e):[e e x => f2(e) e y]

& ALL(e):[e e y => f3(e) e z]

Join, 44, 9

46 EXIST(f2f1):[ALL(d):[d e x => f2f1(d) e z]

& ALL(d):[d e x => f2f1(d)=f3(f2(d))]]

Detach, 41, 45

47 ALL(d):[d e x => f32(d) e z]

& ALL(d):[d e x => f32(d)=f3(f2(d))]

E Spec, 46

Define: f32 (Composition f3 o f2: x --> z)

48 ALL(d):[d e x => f32(d) e z]

Split, 47

49 ALL(d):[d e x => f32(d)=f3(f2(d))]

Split, 47

Apply definition of composition function f1 and (f3 o f2)

50 ALL(b):ALL(c):ALL(f1):ALL(f2):[Set(w) & Set(b) & Set(c)

& ALL(d):[d e w => f1(d) e b]

& ALL(d):[d e b => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e c]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 1

51 ALL(c):ALL(f1):ALL(f2):[Set(w) & Set(x) & Set(c)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f2(d) e c]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e c]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 50

52 ALL(f1):ALL(f2):[Set(w) & Set(x) & Set(z)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f2(d) e z]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 51

53 ALL(f2):[Set(w) & Set(x) & Set(z)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f2(d) e z]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f2(f1(d))]]]

U Spec, 52

54 Set(w) & Set(x) & Set(z)

& ALL(d):[d e w => f1(d) e x]

& ALL(d):[d e x => f32(d) e z]

=> EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f32(f1(d))]]

U Spec, 53

55 Set(w) & Set(x)

Join, 3, 4

56 Set(w) & Set(x) & Set(z)

Join, 55, 6

57 Set(w) & Set(x) & Set(z)

& ALL(e):[e e w => f1(e) e x]

Join, 56, 7

58 Set(w) & Set(x) & Set(z)

& ALL(e):[e e w => f1(e) e x]

& ALL(d):[d e x => f32(d) e z]

Join, 57, 48

59 EXIST(f2f1):[ALL(d):[d e w => f2f1(d) e z]

& ALL(d):[d e w => f2f1(d)=f32(f1(d))]]

Detach, 54, 58

60 ALL(d):[d e w => f321'(d) e z]

& ALL(d):[d e w => f321'(d)=f32(f1(d))]

E Spec, 59

Define: f321' (The composition (f3 o f2) o f1: w --> z)

61 ALL(d):[d e w => f321'(d) e z]

Split, 60

62 ALL(d):[d e w => f321'(d)=f32(f1(d))]

Split, 60

Prove: ALL(e):[e e w => f321(e)=f321'(e)]

Suppose...

63 p e w

Premise

64 p e w => f321(p)=f3(f21(p))

U Spec, 35

65 f321(p)=f3(f21(p))

Detach, 64, 63

66 p e w => f21(p)=f2(f1(p))

U Spec, 22

67 f21(p)=f2(f1(p))

Detach, 66, 63

As Required:

68 f321(p)=f3(f2(f1(p)))

Substitute, 67, 65

69 p e w => f321'(p)=f32(f1(p))

U Spec, 62

70 f321'(p)=f32(f1(p))

Detach, 69, 63

71 f1(p) e x => f32(f1(p))=f3(f2(f1(p)))

U Spec, 49

72 p e w => f1(p) e x

U Spec, 7

73 f1(p) e x

Detach, 72, 63

74 f32(f1(p))=f3(f2(f1(p)))

Detach, 71, 73

75 f321'(p)=f3(f2(f1(p)))

Substitute, 74, 70

76 f321(p)=f321'(p)

Substitute, 75, 68

As Required:

77 ALL(e):[e e w => f321(e)=f321'(e)]

4 Conclusion, 63

Joining results...

78 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

Join, 20, 34

79 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

Join, 78, 35

80 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

& ALL(d):[d e x => f32(d) e z]

Join, 79, 48

81 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

& ALL(d):[d e x => f32(d) e z]

& ALL(d):[d e x => f32(d)=f3(f2(d))]

Join, 80, 49

82 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

& ALL(d):[d e x => f32(d) e z]

& ALL(d):[d e x => f32(d)=f3(f2(d))]

& ALL(d):[d e w => f321'(d) e z]

Join, 81, 61

83 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

& ALL(d):[d e x => f32(d) e z]

& ALL(d):[d e x => f32(d)=f3(f2(d))]

& ALL(d):[d e w => f321'(d) e z]

& ALL(d):[d e w => f321'(d)=f32(f1(d))]

Join, 82, 62

84 ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

& ALL(d):[d e x => f32(d) e z]

& ALL(d):[d e x => f32(d)=f3(f2(d))]

& ALL(d):[d e w => f321'(d) e z]

& ALL(d):[d e w => f321'(d)=f32(f1(d))]

& ALL(e):[e e w => f321(e)=f321'(e)]

Join, 83, 77

As Required:

85 ALL(w):ALL(x):ALL(y):ALL(z):ALL(f1):ALL(f2):ALL(f3):[Set(w) & Set(x) & Set(y) & Set(z)

& ALL(e):[e e w => f1(e) e x]

& ALL(e):[e e x => f2(e) e y]

& ALL(e):[e e y => f3(e) e z]

=> EXIST(f21):EXIST(f321):EXIST(f32):EXIST(f321'):[ALL(d):[d e w => f21(d) e y]

& ALL(d):[d e w => f21(d)=f2(f1(d))]

& ALL(d):[d e w => f321(d) e z]

& ALL(d):[d e w => f321(d)=f3(f21(d))]

& ALL(d):[d e x => f32(d) e z]

& ALL(d):[d e x => f32(d)=f3(f2(d))]

& ALL(d):[d e w => f321'(d) e z]

& ALL(d):[d e w => f321'(d)=f32(f1(d))]

& ALL(e):[e e w => f321(e)=f321'(e)]]]

4 Conclusion, 2