:: MCART_6 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: MCART_6:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in Y holds
Y1 misses X ) )
proof end;

theorem :: MCART_6:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE, YF being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in YF & YF in Y holds
Y1 misses X ) )
proof end;

definition
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ;
func [x1,x2,x3,x4,x5,x6,x7,x8,x9] -> set equals :: MCART_6:def 1
[[x1,x2,x3,x4,x5,x6,x7,x8],x9];
coherence
[[x1,x2,x3,x4,x5,x6,x7,x8],x9] is set ;
end;

:: deftheorem defines [ MCART_6:def 1 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6,x7,x8],x9];

theorem Th3: :: MCART_6:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[[[[[[[x1,x2],x3],x4],x5],x6],x7],x8],x9]
proof end;

theorem :: MCART_6:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MCART_6:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6,x7],x8,x9]
proof end;

theorem :: MCART_6:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6],x7,x8,x9]
proof end;

theorem :: MCART_6:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5],x6,x7,x8,x9]
proof end;

theorem :: MCART_6:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4],x5,x6,x7,x8,x9]
proof end;

theorem :: MCART_6:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3],x4,x5,x6,x7,x8,x9]
proof end;

theorem Th10: :: MCART_6:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2],x3,x4,x5,x6,x7,x8,x9]
proof end;

theorem Th11: :: MCART_6:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9, y1, y2, y3, y4, y5, y6, y7, y8, y9 being set st [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [y1,y2,y3,y4,y5,y6,y7,y8,y9] holds
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 & x8 = y8 & x9 = y9 )
proof end;

definition
let X1, X2, X3, X4, X5, X6, X7, X8, X9 be set ;
func [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] -> set equals :: MCART_6:def 2
[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];
coherence
[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] is set ;
end;

:: deftheorem defines [: MCART_6:def 2 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];

theorem Th12: :: MCART_6:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:]
proof end;

theorem :: MCART_6:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MCART_6:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8,X9:]
proof end;

theorem :: MCART_6:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6:],X7,X8,X9:]
proof end;

theorem :: MCART_6:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5:],X6,X7,X8,X9:]
proof end;

theorem :: MCART_6:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4:],X5,X6,X7,X8,X9:]
proof end;

theorem :: MCART_6:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8,X9:]
proof end;

theorem Th19: :: MCART_6:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8,X9:]
proof end;

theorem Th20: :: MCART_6:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} ) iff [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {} )
proof end;

theorem Th21: :: MCART_6:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 & X9 = Y9 )
proof end;

theorem :: MCART_6:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {} & [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 & X9 = Y9 )
proof end;

theorem :: MCART_6:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st [:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:] holds
X = Y
proof end;

theorem Th24: :: MCART_6:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 ex xx7 being Element of X7 ex xx8 being Element of X8 ex xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9]
proof end;

definition
let X1, X2, X3, X4, X5, X6, X7, X8, X9 be set ;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} ) ;
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
func x `1 -> Element of X1 means :Def3: :: MCART_6:def 3
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x1
proof end;
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> Element of X2 means :Def4: :: MCART_6:def 4
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x2
proof end;
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> Element of X3 means :Def5: :: MCART_6:def 5
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x3
proof end;
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x3 ) holds
b1 = b2
proof end;
func x `4 -> Element of X4 means :Def6: :: MCART_6:def 6
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x4
proof end;
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x4 ) holds
b1 = b2
proof end;
func x `5 -> Element of X5 means :Def7: :: MCART_6:def 7
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x5
proof end;
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x5 ) holds
b1 = b2
proof end;
func x `6 -> Element of X6 means :Def8: :: MCART_6:def 8
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x6;
existence
ex b1 being Element of X6 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x6
proof end;
uniqueness
for b1, b2 being Element of X6 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x6 ) holds
b1 = b2
proof end;
func x `7 -> Element of X7 means :Def9: :: MCART_6:def 9
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x7;
existence
ex b1 being Element of X7 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x7
proof end;
uniqueness
for b1, b2 being Element of X7 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x7 ) holds
b1 = b2
proof end;
func x `8 -> Element of X8 means :Def10: :: MCART_6:def 10
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x8;
existence
ex b1 being Element of X8 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x8
proof end;
uniqueness
for b1, b2 being Element of X8 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x8 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x8 ) holds
b1 = b2
proof end;
func x `9 -> Element of X9 means :Def11: :: MCART_6:def 11
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x9;
existence
ex b1 being Element of X9 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x9
proof end;
uniqueness
for b1, b2 being Element of X9 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x9 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x9 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines `1 MCART_6:def 3 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X1 holds
( b11 = x `1 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x1 );

:: deftheorem Def4 defines `2 MCART_6:def 4 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X2 holds
( b11 = x `2 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x2 );

:: deftheorem Def5 defines `3 MCART_6:def 5 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X3 holds
( b11 = x `3 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x3 );

:: deftheorem Def6 defines `4 MCART_6:def 6 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X4 holds
( b11 = x `4 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x4 );

:: deftheorem Def7 defines `5 MCART_6:def 7 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X5 holds
( b11 = x `5 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x5 );

:: deftheorem Def8 defines `6 MCART_6:def 8 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X6 holds
( b11 = x `6 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x6 );

:: deftheorem Def9 defines `7 MCART_6:def 9 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X7 holds
( b11 = x `7 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x7 );

:: deftheorem Def10 defines `8 MCART_6:def 10 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X8 holds
( b11 = x `8 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x8 );

:: deftheorem Def11 defines `9 MCART_6:def 11 :
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for b11 being Element of X9 holds
( b11 = x `9 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x9 );

theorem :: MCART_6:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 & x `9 = x9 ) by Def3, Def4, Def5, Def6, Def7, Def8, Def9, Def10, Def11;

theorem Th26: :: MCART_6:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 ),(x `6 ),(x `7 ),(x `8 ),(x `9 )]
proof end;

theorem Th27: :: MCART_6:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
( x `1 = (((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 & x `2 = (((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `2 & x `3 = ((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `2 & x `4 = (((((x `1 ) `1 ) `1 ) `1 ) `1 ) `2 & x `5 = ((((x `1 ) `1 ) `1 ) `1 ) `2 & x `6 = (((x `1 ) `1 ) `1 ) `2 & x `7 = ((x `1 ) `1 ) `2 & x `8 = (x `1 ) `2 & x `9 = x `2 )
proof end;

theorem :: MCART_6:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds
( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 & X8 meets Y8 & X9 meets Y9 )
proof end;

theorem :: MCART_6:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8},{x9}:] = {[x1,x2,x3,x4,x5,x6,x7,x8,x9]}
proof end;

theorem :: MCART_6:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 & x `9 = x9 ) by Def3, Def4, Def5, Def6, Def7, Def8, Def9, Def10, Def11;

theorem :: MCART_6:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y1 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y1 = xx1 ) holds
y1 = x `1
proof end;

theorem :: MCART_6:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y2 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y2 = xx2 ) holds
y2 = x `2
proof end;

theorem :: MCART_6:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y3 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y3 = xx3 ) holds
y3 = x `3
proof end;

theorem :: MCART_6:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y4 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y4 = xx4 ) holds
y4 = x `4
proof end;

theorem :: MCART_6:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y5 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y5 = xx5 ) holds
y5 = x `5
proof end;

theorem :: MCART_6:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y6 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y6 = xx6 ) holds
y6 = x `6
proof end;

theorem :: MCART_6:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y7 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y7 = xx7 ) holds
y7 = x `7
proof end;

theorem :: MCART_6:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y8 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y8 = xx8 ) holds
y8 = x `8
proof end;

theorem :: MCART_6:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, y9 being set
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4
for xx5 being Element of X5
for xx6 being Element of X6
for xx7 being Element of X7
for xx8 being Element of X8
for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y9 = xx9 ) holds
y9 = x `9
proof end;

theorem :: MCART_6:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st y in [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
ex x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9 & y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] )
proof end;

theorem :: MCART_6:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds
( [x1,x2,x3,x4,x5,x6,x7,x8,x9] in [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9 ) )
proof end;

theorem :: MCART_6:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st ( for y being set holds
( y in Z iff ex x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & x9 in X9 & y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] ) ) ) holds
Z = [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
proof end;

theorem Th43: :: MCART_6:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} & Y6 <> {} & Y7 <> {} & Y8 <> {} & Y9 <> {} holds
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] st x = y holds
( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 & x `9 = y `9 )
proof end;

theorem :: MCART_6:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4
for A5 being Subset of X5
for A6 being Subset of X6
for A7 being Subset of X7
for A8 being Subset of X8
for A9 being Subset of X9
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 & x `9 in A9 )
proof end;

theorem Th45: :: MCART_6:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, Y1, X2, Y2, X3, Y3, X4, Y4, X5, Y5, X6, Y6, X7, Y7, X8, Y8, X9, Y9 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7 & X8 c= Y8 & X9 c= Y9 holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
proof end;

theorem :: MCART_6:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4
for A5 being Subset of X5
for A6 being Subset of X6
for A7 being Subset of X7
for A8 being Subset of X8
for A9 being Subset of X9 holds [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] by Th45;