Helping Wonky Man so much doesn't feel right. A student
should do his homework on his own to learn something.
Ok, one more piece of the puzzle revealed, this theorem:
Theorem specialize to b
37 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=b =>
[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] =>
x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Rem DNeg, 36
Proved from Theorem specialize to r and Theorem swap
---------------------------- begin proof --------------------------------------------------
Theorem specialize to r
1 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=r => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Axiom
Theorem swap
2 ALL(x):ALL(b):ALL(r):ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]
=> [[x=b | x=r] & [y=b | y=r] & [z=b | z=r] => x=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r] | [y=b & z=b | y=r & z=r]]]
Axiom
3 ~ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Premise
4 ~ALL(x):ALL(r):ALL(b):ALL(y):~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Quant, 3
5 ~ALL(x):ALL(r):ALL(b):~EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Quant, 4
6 ~ALL(x):ALL(r):~EXIST(b):~~EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Quant, 5
7 ~ALL(x):~EXIST(r):~~EXIST(b):~~EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Quant, 6
8 ~~EXIST(x):~~EXIST(r):~~EXIST(b):~~EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Quant, 7
9 EXIST(x):~~EXIST(r):~~EXIST(b):~~EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Rem DNeg, 8
10 EXIST(x):EXIST(r):~~EXIST(b):~~EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Rem DNeg, 9
11 EXIST(x):EXIST(r):EXIST(b):~~EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Rem DNeg, 10
12 EXIST(x):EXIST(r):EXIST(b):EXIST(y):~~EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Rem DNeg, 11
13 EXIST(x):EXIST(r):EXIST(b):EXIST(y):EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Rem DNeg, 12
14 EXIST(r):EXIST(b):EXIST(y):EXIST(z):~[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
E Spec, 13
15 EXIST(b):EXIST(y):EXIST(z):~[x=b => [[x=u | x=b] & [y=u | y=b] & [z=u | z=b] => x=u & y=u | x=b & y=b | [x=u & z=u | x=b & z=b] | [y=u & z=u | y=b & z=b]]]
E Spec, 14
16 EXIST(y):EXIST(z):~[x=v => [[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]]
E Spec, 15
17 EXIST(z):~[x=v => [[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]]
E Spec, 16
18 ~[x=v => [[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]]
E Spec, 17
19 ~~[x=v & ~[[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]]
Imply-And, 18
20 x=v & ~[[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]
Rem DNeg, 19
21 x=v
Split, 20
22 ~[[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]
Split, 20
23 ALL(r):ALL(b):ALL(y):ALL(z):[x=r => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
U Spec, 1
24 ALL(b):ALL(y):ALL(z):[x=v => [[x=v | x=b] & [y=v | y=b] & [z=v | z=b] => x=v & y=v | x=b & y=b | [x=v & z=v | x=b & z=b] | [y=v & z=v | y=b & z=b]]]
U Spec, 23
25 ALL(y):ALL(z):[x=v => [[x=v | x=u] & [y=v | y=u] & [z=v | z=u] => x=v & y=v | x=u & y=u | [x=v & z=v | x=u & z=u] | [y=v & z=v | y=u & z=u]]]
U Spec, 24
26 ALL(z):[x=v => [[x=v | x=u] & [y=v | y=u] & [z=v | z=u] => x=v & y=v | x=u & y=u | [x=v & z=v | x=u & z=u] | [y=v & z=v | y=u & z=u]]]
U Spec, 25
27 x=v => [[x=v | x=u] & [y=v | y=u] & [z=v | z=u] => x=v & y=v | x=u & y=u | [x=v & z=v | x=u & z=u] | [y=v & z=v | y=u & z=u]]
U Spec, 26
28 [x=v | x=u] & [y=v | y=u] & [z=v | z=u] => x=v & y=v | x=u & y=u | [x=v & z=v | x=u & z=u] | [y=v & z=v | y=u & z=u]
Detach, 27, 21
29 ALL(b):ALL(r):ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]
=> [[x=b | x=r] & [y=b | y=r] & [z=b | z=r] => x=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r] | [y=b & z=b | y=r & z=r]]]
U Spec, 2
30 ALL(r):ALL(y):ALL(z):[[x=r | x=u] & [y=r | y=u] & [z=r | z=u] => x=r & y=r | x=u & y=u | [x=r & z=r | x=u & z=u] | [y=r & z=r | y=u & z=u]
=> [[x=u | x=r] & [y=u | y=r] & [z=u | z=r] => x=u & y=u | x=r & y=r | [x=u & z=u | x=r & z=r] | [y=u & z=u | y=r & z=r]]]
U Spec, 29
31 ALL(y):ALL(z):[[x=v | x=u] & [y=v | y=u] & [z=v | z=u] => x=v & y=v | x=u & y=u | [x=v & z=v | x=u & z=u] | [y=v & z=v | y=u & z=u]
=> [[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]]
U Spec, 30
32 ALL(z):[[x=v | x=u] & [y=v | y=u] & [z=v | z=u] => x=v & y=v | x=u & y=u | [x=v & z=v | x=u & z=u] | [y=v & z=v | y=u & z=u]
=> [[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]]
U Spec, 31
33 [x=v | x=u] & [y=v | y=u] & [z=v | z=u] => x=v & y=v | x=u & y=u | [x=v & z=v | x=u & z=u] | [y=v & z=v | y=u & z=u]
=> [[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]
U Spec, 32
34 [x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]
Detach, 33, 28
35 ~[[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]
& [[x=u | x=v] & [y=u | y=v] & [z=u | z=v] => x=u & y=u | x=v & y=v | [x=u & z=u | x=v & z=v] | [y=u & z=u | y=v & z=v]]
Join, 22, 34
36 ~~ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Conclusion, 3
37 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=b => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Rem DNeg, 36
---------------------------- end proof --------------------------------------------------