let i, n be Nat; :: thesis: 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); :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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, Def7;
A5: o2 is_strongly_connected_in Bags (n -' (i + 1)) by A2, Def7;
set BO = BlockOrder i,n,o1,o2;

now

now

let x, y be set ; :: thesis: ( x in Bags n & y in Bags n & not [x,y] in BlockOrder i,n,o1,o2 implies [b₂,b₁] in BlockOrder i,n,o1,o2 )
assume that
A6: x in Bags n and
A7: y in Bags n ; :: thesis: ( not [x,y] in BlockOrder i,n,o1,o2 implies [b₂,b₁] 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 ; :: thesis: [b₂,b₁] 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, Def12;

suppose A13: 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q ; :: thesis: [b₂,b₁] in BlockOrder i,n,o1,o2

now

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, Def12;

suppose 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q ; :: thesis: [y,x] in BlockOrder i,n,o1,o2

hence [y,x] in BlockOrder i,n,o1,o2 by A13; :: thesis: verum

end;

suppose not [((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ; :: thesis: [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, RELAT_2:def 7;
hence [y,x] in BlockOrder i,n,o1,o2 by A13, Def12; :: thesis: verum

end;

end;

end;

hence [y,x] in BlockOrder i,n,o1,o2 ; :: thesis: verum

end;

suppose not [(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ; :: thesis: [b₂,b₁] in BlockOrder i,n,o1,o2

then A14: [(0 ,(i + 1) -cut q),(0 ,(i + 1) -cut p)] in o1 by A4, A8, A9, RELAT_2:def 7;

now

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, Def12;

suppose 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q ; :: thesis: [y,x] in BlockOrder i,n,o1,o2

hence [y,x] in BlockOrder i,n,o1,o2 by A14, Def12; :: thesis: verum

end;

suppose not [((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ; :: thesis: [y,x] in BlockOrder i,n,o1,o2

then A15: [((i + 1),n -cut q),((i + 1),n -cut p)] in o2 by A5, A10, A11, RELAT_2:def 7;

now

per cases ( 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q or 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q ) ;

suppose 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q ; :: thesis: [y,x] in BlockOrder i,n,o1,o2

hence [y,x] in BlockOrder i,n,o1,o2 by A15, Def12; :: thesis: verum

end;

suppose 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q ; :: thesis: [y,x] in BlockOrder i,n,o1,o2

hence [y,x] in BlockOrder i,n,o1,o2 by A14, Def12; :: thesis: verum

end;

end;

end;

hence [y,x] in BlockOrder i,n,o1,o2 ; :: thesis: verum

end;

end;

end;

hence [y,x] in BlockOrder i,n,o1,o2 ; :: thesis: verum

end;

end;

end;

hence BlockOrder i,n,o1,o2 is_strongly_connected_in Bags n by RELAT_2:def 7; :: thesis: 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
[(b₆ + b₈),(b₇ + b₈)] in BlockOrder i,n,o1,o2 ) )
let a be bag of n; :: thesis: ( [(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
[(b₅ + b₇),(b₆ + b₇)] 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

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 ; :: thesis: [(EmptyBag n),a] in BlockOrder i,n,o1,o2

0 ,(i + 1) -cut (EmptyBag n) = EmptyBag ((i + 1) -' 0 ) by Th17;
then [(0 ,(i + 1) -cut (EmptyBag n)),(0 ,(i + 1) -cut a)] in o1 by A1, A3, Def7;
hence [(EmptyBag n),a] in BlockOrder i,n,o1,o2 by A16, Def12; :: thesis: verum

end;

suppose A17: 0 ,(i + 1) -cut (EmptyBag n) = 0 ,(i + 1) -cut a ; :: thesis: [(EmptyBag n),a] in BlockOrder i,n,o1,o2

(i + 1),n -cut (EmptyBag n) = EmptyBag (n -' (i + 1)) by Th17;
then [((i + 1),n -cut (EmptyBag n)),((i + 1),n -cut a)] in o2 by A2, Def7;
hence [(EmptyBag n),a] in BlockOrder i,n,o1,o2 by A17, Def12; :: thesis: verum

end;

end;

end;

hence [(EmptyBag n),a] in BlockOrder i,n,o1,o2 ; :: thesis: for a, b, c being bag of n st [a,b] in BlockOrder i,n,o1,o2 holds
[(b₅ + b₇),(b₆ + b₇)] in BlockOrder i,n,o1,o2
let a, b, c be bag of n; :: thesis: ( [a,b] in BlockOrder i,n,o1,o2 implies [(b₂ + b₄),(b₃ + b₄)] in BlockOrder i,n,o1,o2 )
assume A18: [a,b] in BlockOrder i,n,o1,o2 ; :: thesis: [(b₂ + b₄),(b₃ + b₄)] 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, Def12;

suppose A19: ( 0 ,(i + 1) -cut a <> 0 ,(i + 1) -cut b & [(0 ,(i + 1) -cut a),(0 ,(i + 1) -cut b)] in o1 ) ; :: thesis: [(b₂ + b₄),(b₃ + b₄)] 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, Def7;
then [(0 ,(i + 1) -cut (a + c)),((0 ,(i + 1) -cut b) + (0 ,(i + 1) -cut c))] in o1 by Th18;
then A20: [(0 ,(i + 1) -cut (a + c)),(0 ,(i + 1) -cut (b + c))] in o1 by Th18;

now

assume A21: (0 ,(i + 1) -cut a) + (0 ,(i + 1) -cut c) = (0 ,(i + 1) -cut b) + (0 ,(i + 1) -cut c) ; :: thesis: 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; :: thesis: verum

end;

then 0 ,(i + 1) -cut (a + c) <> (0 ,(i + 1) -cut b) + (0 ,(i + 1) -cut c) by Th18;
then 0 ,(i + 1) -cut (a + c) <> 0 ,(i + 1) -cut (b + c) by Th18;
hence [(a + c),(b + c)] in BlockOrder i,n,o1,o2 by A20, Def12; :: thesis: 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 ) ; :: thesis: [(b₂ + b₄),(b₃ + b₄)] 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, Def7;
then [((i + 1),n -cut (a + c)),(((i + 1),n -cut b) + ((i + 1),n -cut c))] in o2 by Th18;
then A23: [((i + 1),n -cut (a + c)),((i + 1),n -cut (b + c))] in o2 by Th18;
0 ,(i + 1) -cut (a + c) = (0 ,(i + 1) -cut b) + (0 ,(i + 1) -cut c) by A22, Th18;
then 0 ,(i + 1) -cut (a + c) = 0 ,(i + 1) -cut (b + c) by Th18;
hence [(a + c),(b + c)] in BlockOrder i,n,o1,o2 by A23, Def12; :: thesis: verum

end;

end;

end;

hence BlockOrder i,n,o1,o2 is admissible by Def7; :: thesis: verum