let i, n be Nat; for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1)) st o1 is admissible & o2 is admissible holds
BlockOrder (i,n,o1,o2) is admissible
let o1 be TermOrder of (i + 1); for o2 being TermOrder of (n -' (i + 1)) st o1 is admissible & o2 is admissible holds
BlockOrder (i,n,o1,o2) is admissible
let o2 be TermOrder of (n -' (i + 1)); ( o1 is admissible & o2 is admissible implies BlockOrder (i,n,o1,o2) is admissible )
assume that
A1:
o1 is admissible
and
A2:
o2 is admissible
; BlockOrder (i,n,o1,o2) is admissible
A3:
i + 1 = (i + 1) -' 0
by NAT_D:40;
then A4:
o1 is_strongly_connected_in Bags ((i + 1) -' 0)
by A1;
A5:
o2 is_strongly_connected_in Bags (n -' (i + 1))
by A2;
set BO = BlockOrder (i,n,o1,o2);
now ( BlockOrder (i,n,o1,o2) is_strongly_connected_in Bags n & ( for a being bag of n holds
( [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) & ( for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(a + c),(b + c)] in BlockOrder (i,n,o1,o2) ) ) ) )now for x, y being object st x in Bags n & y in Bags n & not [x,y] in BlockOrder (i,n,o1,o2) holds
[y,x] in BlockOrder (i,n,o1,o2)let x,
y be
object ;
( x in Bags n & y in Bags n & not [x,y] in BlockOrder (i,n,o1,o2) implies [b2,b1] in BlockOrder (i,n,o1,o2) )assume that A6:
x in Bags n
and A7:
y in Bags n
;
( not [x,y] in BlockOrder (i,n,o1,o2) implies [b2,b1] in BlockOrder (i,n,o1,o2) )reconsider p =
x,
q =
y as
bag of
n by A6, A7;
set CUTP1 = (
0,
(i + 1))
-cut p;
set CUTP2 = (
(i + 1),
n)
-cut p;
set CUTQ1 = (
0,
(i + 1))
-cut q;
set CUTQ2 = (
(i + 1),
n)
-cut q;
A8:
(
0,
(i + 1))
-cut p in Bags ((i + 1) -' 0)
by PRE_POLY:def 12;
A9:
(
0,
(i + 1))
-cut q in Bags ((i + 1) -' 0)
by PRE_POLY:def 12;
A10:
(
(i + 1),
n)
-cut p in Bags (n -' (i + 1))
by PRE_POLY:def 12;
A11:
(
(i + 1),
n)
-cut q in Bags (n -' (i + 1))
by PRE_POLY:def 12;
assume A12:
not
[x,y] in BlockOrder (
i,
n,
o1,
o2)
;
[b2,b1] in BlockOrder (i,n,o1,o2)per cases
( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q or not [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 )
by A12, Def10;
suppose A13:
(
0,
(i + 1))
-cut p = (
0,
(i + 1))
-cut q
;
[b2,b1] in BlockOrder (i,n,o1,o2)now [y,x] in BlockOrder (i,n,o1,o2)per cases
( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q or not [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 )
by A12, Def10;
suppose
not
[(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2
;
[y,x] in BlockOrder (i,n,o1,o2)then
[(((i + 1),n) -cut q),(((i + 1),n) -cut p)] in o2
by A5, A10, A11;
hence
[y,x] in BlockOrder (
i,
n,
o1,
o2)
by A13, Def10;
verum end; end; end; hence
[y,x] in BlockOrder (
i,
n,
o1,
o2)
;
verum end; end; end; hence
BlockOrder (
i,
n,
o1,
o2)
is_strongly_connected_in Bags n
;
for a being bag of n holds
( [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) & ( for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(b6 + b8),(b7 + b8)] in BlockOrder (i,n,o1,o2) ) )let a be
bag of
n;
( [(EmptyBag n),a] in BlockOrder (i,n,o1,o2) & ( for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(b5 + b7),(b6 + b7)] in BlockOrder (i,n,o1,o2) ) )set CUTE1 = (
0,
(i + 1))
-cut (EmptyBag n);
set CUTA1 = (
0,
(i + 1))
-cut a;
set CUTE2 = (
(i + 1),
n)
-cut (EmptyBag n);
set CUTA2 = (
(i + 1),
n)
-cut a;
now [(EmptyBag n),a] in BlockOrder (i,n,o1,o2)per cases
( (0,(i + 1)) -cut (EmptyBag n) <> (0,(i + 1)) -cut a or (0,(i + 1)) -cut (EmptyBag n) = (0,(i + 1)) -cut a )
;
suppose A16:
(
0,
(i + 1))
-cut (EmptyBag n) <> (
0,
(i + 1))
-cut a
;
[(EmptyBag n),a] in BlockOrder (i,n,o1,o2)
(
0,
(i + 1))
-cut (EmptyBag n) = EmptyBag ((i + 1) -' 0)
by Th15;
then
[((0,(i + 1)) -cut (EmptyBag n)),((0,(i + 1)) -cut a)] in o1
by A1, A3;
hence
[(EmptyBag n),a] in BlockOrder (
i,
n,
o1,
o2)
by A16, Def10;
verum end; end; end; hence
[(EmptyBag n),a] in BlockOrder (
i,
n,
o1,
o2)
;
for a, b, c being bag of n st [a,b] in BlockOrder (i,n,o1,o2) holds
[(b5 + b7),(b6 + b7)] in BlockOrder (i,n,o1,o2)let a,
b,
c be
bag of
n;
( [a,b] in BlockOrder (i,n,o1,o2) implies [(b2 + b4),(b3 + b4)] in BlockOrder (i,n,o1,o2) )assume A18:
[a,b] in BlockOrder (
i,
n,
o1,
o2)
;
[(b2 + b4),(b3 + b4)] in BlockOrder (i,n,o1,o2)set CUTA1 = (
0,
(i + 1))
-cut a;
set CUTA2 = (
(i + 1),
n)
-cut a;
set CUTB1 = (
0,
(i + 1))
-cut b;
set CUTB2 = (
(i + 1),
n)
-cut b;
set CUTC1 = (
0,
(i + 1))
-cut c;
set CUTC2 = (
(i + 1),
n)
-cut c;
set CUTAC1 = (
0,
(i + 1))
-cut (a + c);
set CUTBC1 = (
0,
(i + 1))
-cut (b + c);
set CUTAC2 = (
(i + 1),
n)
-cut (a + c);
set CUTBC2 = (
(i + 1),
n)
-cut (b + c);
per cases
( ( (0,(i + 1)) -cut a <> (0,(i + 1)) -cut b & [((0,(i + 1)) -cut a),((0,(i + 1)) -cut b)] in o1 ) or ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & [(((i + 1),n) -cut a),(((i + 1),n) -cut b)] in o2 ) )
by A18, Def10;
suppose A19:
( (
0,
(i + 1))
-cut a <> (
0,
(i + 1))
-cut b &
[((0,(i + 1)) -cut a),((0,(i + 1)) -cut b)] in o1 )
;
[(b2 + b4),(b3 + b4)] in BlockOrder (i,n,o1,o2)then
[(((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c)),(((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c))] in o1
by A1, A3;
then
[((0,(i + 1)) -cut (a + c)),(((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c))] in o1
by Th16;
then A20:
[((0,(i + 1)) -cut (a + c)),((0,(i + 1)) -cut (b + c))] in o1
by Th16;
now not ((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c) = ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c)assume A21:
((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c) = ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c)
;
contradiction
(((0,(i + 1)) -cut a) + ((0,(i + 1)) -cut c)) -' ((0,(i + 1)) -cut c) = (
0,
(i + 1))
-cut a
by PRE_POLY:48;
hence
contradiction
by A19, A21, PRE_POLY:48;
verum end; then
(
0,
(i + 1))
-cut (a + c) <> ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c)
by Th16;
then
(
0,
(i + 1))
-cut (a + c) <> (
0,
(i + 1))
-cut (b + c)
by Th16;
hence
[(a + c),(b + c)] in BlockOrder (
i,
n,
o1,
o2)
by A20, Def10;
verum end; suppose A22:
( (
0,
(i + 1))
-cut a = (
0,
(i + 1))
-cut b &
[(((i + 1),n) -cut a),(((i + 1),n) -cut b)] in o2 )
;
[(b2 + b4),(b3 + b4)] in BlockOrder (i,n,o1,o2)then
[((((i + 1),n) -cut a) + (((i + 1),n) -cut c)),((((i + 1),n) -cut b) + (((i + 1),n) -cut c))] in o2
by A2;
then
[(((i + 1),n) -cut (a + c)),((((i + 1),n) -cut b) + (((i + 1),n) -cut c))] in o2
by Th16;
then A23:
[(((i + 1),n) -cut (a + c)),(((i + 1),n) -cut (b + c))] in o2
by Th16;
(
0,
(i + 1))
-cut (a + c) = ((0,(i + 1)) -cut b) + ((0,(i + 1)) -cut c)
by A22, Th16;
then
(
0,
(i + 1))
-cut (a + c) = (
0,
(i + 1))
-cut (b + c)
by Th16;
hence
[(a + c),(b + c)] in BlockOrder (
i,
n,
o1,
o2)
by A23, Def10;
verum end; end; end;
hence
BlockOrder (i,n,o1,o2) is admissible
; verum