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