:: MCART_2 semantic presentation

Lemma1: for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
for b₃ being Element of [:b₁,b₂:] ex b₄ being Element of b₁ex b₅ being Element of b₂ st b₃ = [b₄,b₅]

proof end;

Lemma2: for b₁, b₂, b₃ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} holds
for b₄ being Element of [:b₁,b₂,b₃:] ex b₅ being Element of b₁ex b₆ being Element of b₂ex b₇ being Element of b₃ st b₄ = [b₅,b₆,b₇]

proof end;

Lemma3: for b₁, b₂, b₃, b₄ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} holds
for b₅ being Element of [:b₁,b₂,b₃,b₄:] ex b₆ being Element of b₁ex b₇ being Element of b₂ex b₈ being Element of b₃ex b₉ being Element of b₄ st b₅ = [b₆,b₇,b₈,b₉]

proof end;

theorem Th1: :: MCART_2:1

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈ being set st b₃ in b₄ & b₄ in b₅ & b₅ in b₆ & b₆ in b₇ & b₇ in b₈ & b₈ in b₂ holds
b₃ misses b₁ ) )

proof end;

theorem Th2: :: MCART_2:2

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being set st b₃ in b₄ & b₄ in b₅ & b₅ in b₆ & b₆ in b₇ & b₇ in b₈ & b₈ in b₉ & b₉ in b₂ holds
b₃ misses b₁ ) )

proof end;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func [c₁,c₂,c₃,c₄,c₅] -> set equals :: MCART_2:def 1
[[a₁,a₂,a₃,a₄],a₅];
correctness ;

end;

:: deftheorem Def1 defines [ MCART_2:def 1 :

theorem Th3: :: MCART_2:3

for b₁, b₂, b₃, b₄, b₅ being set holds [b₁,b₂,b₃,b₄,b₅] = [[[[b₁,b₂],b₃],b₄],b₅]

proof end;

theorem Th4: :: MCART_2:4

canceled;

theorem Th5: :: MCART_2:5

for b₁, b₂, b₃, b₄, b₅ being set holds [b₁,b₂,b₃,b₄,b₅] = [[b₁,b₂,b₃],b₄,b₅]

proof end;

theorem Th6: :: MCART_2:6

for b₁, b₂, b₃, b₄, b₅ being set holds [b₁,b₂,b₃,b₄,b₅] = [[b₁,b₂],b₃,b₄,b₅]

proof end;

theorem Th7: :: MCART_2:7

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set st [b₁,b₂,b₃,b₄,b₅] = [b₆,b₇,b₈,b₉,b₁₀] holds
( b₁ = b₆ & b₂ = b₇ & b₃ = b₈ & b₄ = b₉ & b₅ = b₁₀ )

proof end;

theorem Th8: :: MCART_2:8

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇ being set holds
( ( not b₃ in b₁ & not b₄ in b₁ ) or not b₂ = [b₃,b₄,b₅,b₆,b₇] ) ) )

proof end;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func [:c₁,c₂,c₃,c₄,c₅:] -> set equals :: MCART_2:def 2
[:[:a₁,a₂,a₃,a₄:],a₅:];
correctness ;

end;

:: deftheorem Def2 defines [: MCART_2:def 2 :

theorem Th9: :: MCART_2:9

for b₁, b₂, b₃, b₄, b₅ being set holds [:b₁,b₂,b₃,b₄,b₅:] = [:[:[:[:b₁,b₂:],b₃:],b₄:],b₅:]

proof end;

theorem Th10: :: MCART_2:10

canceled;

theorem Th11: :: MCART_2:11

for b₁, b₂, b₃, b₄, b₅ being set holds [:b₁,b₂,b₃,b₄,b₅:] = [:[:b₁,b₂,b₃:],b₄,b₅:]

proof end;

theorem Th12: :: MCART_2:12

for b₁, b₂, b₃, b₄, b₅ being set holds [:b₁,b₂,b₃,b₄,b₅:] = [:[:b₁,b₂:],b₃,b₄,b₅:]

proof end;

theorem Th13: :: MCART_2:13

for b₁, b₂, b₃, b₄, b₅ being set holds
( ( b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} ) iff [:b₁,b₂,b₃,b₄,b₅:] <> {} )

proof end;

theorem Th14: :: MCART_2:14

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & [:b₁,b₂,b₃,b₄,b₅:] = [:b₆,b₇,b₈,b₉,b₁₀:] holds
( b₁ = b₆ & b₂ = b₇ & b₃ = b₈ & b₄ = b₉ & b₅ = b₁₀ )

proof end;

theorem Th15: :: MCART_2:15

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set st [:b₁,b₂,b₃,b₄,b₅:] <> {} & [:b₁,b₂,b₃,b₄,b₅:] = [:b₆,b₇,b₈,b₉,b₁₀:] holds
( b₁ = b₆ & b₂ = b₇ & b₃ = b₈ & b₄ = b₉ & b₅ = b₁₀ )

proof end;

theorem Th16: :: MCART_2:16

for b₁, b₂ being set st [:b₁,b₁,b₁,b₁,b₁:] = [:b₂,b₂,b₂,b₂,b₂:] holds
b₁ = b₂

proof end;

theorem Th17: :: MCART_2:17

for b₁, b₂, b₃, b₄, b₅ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} holds
for b₆ being Element of [:b₁,b₂,b₃,b₄,b₅:] ex b₇ being Element of b₁ex b₈ being Element of b₂ex b₉ being Element of b₃ex b₁₀ being Element of b₄ex b₁₁ being Element of b₅ st b₆ = [b₇,b₈,b₉,b₁₀,b₁₁]

proof end;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
assume E14: ( c₁ <> {} & c₂ <> {} & c₃ <> {} & c₄ <> {} & c₅ <> {} ) ;
let c₆ be Element of [:c₁,c₂,c₃,c₄,c₅:];
func c₆ `1 -> Element of a₁ means :Def3: :: MCART_2:def 3
for b₁, b₂, b₃, b₄, b₅ being set st a₆ = [b₁,b₂,b₃,b₄,b₅] holds
a₇ = b₁;
existence

proof end;

proof end;

func c₆ `2 -> Element of a₂ means :Def4: :: MCART_2:def 4
for b₁, b₂, b₃, b₄, b₅ being set st a₆ = [b₁,b₂,b₃,b₄,b₅] holds
a₇ = b₂;
existence

proof end;

proof end;

func c₆ `3 -> Element of a₃ means :Def5: :: MCART_2:def 5
for b₁, b₂, b₃, b₄, b₅ being set st a₆ = [b₁,b₂,b₃,b₄,b₅] holds
a₇ = b₃;
existence

proof end;

proof end;

func c₆ `4 -> Element of a₄ means :Def6: :: MCART_2:def 6
for b₁, b₂, b₃, b₄, b₅ being set st a₆ = [b₁,b₂,b₃,b₄,b₅] holds
a₇ = b₄;
existence

proof end;

proof end;

func c₆ `5 -> Element of a₅ means :Def7: :: MCART_2:def 7
for b₁, b₂, b₃, b₄, b₅ being set st a₆ = [b₁,b₂,b₃,b₄,b₅] holds
a₇ = b₅;
existence

proof end;

proof end;

end;

:: deftheorem Def3 defines `1 MCART_2:def 3 :

:: deftheorem Def4 defines `2 MCART_2:def 4 :

:: deftheorem Def5 defines `3 MCART_2:def 5 :

:: deftheorem Def6 defines `4 MCART_2:def 6 :

:: deftheorem Def7 defines `5 MCART_2:def 7 :

theorem Th18: :: MCART_2:18

for b₁, b₂, b₃, b₄, b₅ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} holds
for b₆ being Element of [:b₁,b₂,b₃,b₄,b₅:]
for b₇, b₈, b₉, b₁₀, b₁₁ being set st b₆ = [b₇,b₈,b₉,b₁₀,b₁₁] holds
( b₆ `1 = b₇ & b₆ `2 = b₈ & b₆ `3 = b₉ & b₆ `4 = b₁₀ & b₆ `5 = b₁₁ ) by Def3, Def4, Def5, Def6, Def7;

theorem Th19: :: MCART_2:19

for b₁, b₂, b₃, b₄, b₅ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} holds
for b₆ being Element of [:b₁,b₂,b₃,b₄,b₅:] holds b₆ = [(b₆ `1 ),(b₆ `2 ),(b₆ `3 ),(b₆ `4 ),(b₆ `5 )]

proof end;

theorem Th20: :: MCART_2:20

for b₁, b₂, b₃, b₄, b₅ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} holds
for b₆ being Element of [:b₁,b₂,b₃,b₄,b₅:] holds
( b₆ `1 = (((b₆ `1 ) `1 ) `1 ) `1 & b₆ `2 = (((b₆ `1 ) `1 ) `1 ) `2 & b₆ `3 = ((b₆ `1 ) `1 ) `2 & b₆ `4 = (b₆ `1 ) `2 & b₆ `5 = b₆ `2 )

proof end;

theorem Th21: :: MCART_2:21

for b₁, b₂, b₃, b₄, b₅ being set st ( b₁ c= [:b₁,b₂,b₃,b₄,b₅:] or b₁ c= [:b₂,b₃,b₄,b₅,b₁:] or b₁ c= [:b₃,b₄,b₅,b₁,b₂:] or b₁ c= [:b₄,b₅,b₁,b₂,b₃:] or b₁ c= [:b₅,b₁,b₂,b₃,b₄:] ) holds
b₁ = {}

proof end;

theorem Th22: :: MCART_2:22

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set st [:b₁,b₂,b₃,b₄,b₅:] meets [:b₆,b₇,b₈,b₉,b₁₀:] holds
( b₁ meets b₆ & b₂ meets b₇ & b₃ meets b₈ & b₄ meets b₉ & b₅ meets b₁₀ )

proof end;

theorem Th23: :: MCART_2:23

for b₁, b₂, b₃, b₄, b₅ being set holds [:{b₁},{b₂},{b₃},{b₄},{b₅}:] = {[b₁,b₂,b₃,b₄,b₅]}

proof end;

theorem Th24: :: MCART_2:24

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Element of [:b₁,b₂,b₃,b₄,b₅:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} holds
for b₇, b₈, b₉, b₁₀, b₁₁ being set st b₆ = [b₇,b₈,b₉,b₁₀,b₁₁] holds
( b₆ `1 = b₇ & b₆ `2 = b₈ & b₆ `3 = b₉ & b₆ `4 = b₁₀ & b₆ `5 = b₁₁ ) by Def3, Def4, Def5, Def6, Def7;

theorem Th25: :: MCART_2:25

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & ( for b₈ being Element of b₁
for b₉ being Element of b₂
for b₁₀ being Element of b₃
for b₁₁ being Element of b₄
for b₁₂ being Element of b₅ st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂] holds
b₆ = b₈ ) holds
b₆ = b₇ `1

proof end;

theorem Th26: :: MCART_2:26

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & ( for b₈ being Element of b₁
for b₉ being Element of b₂
for b₁₀ being Element of b₃
for b₁₁ being Element of b₄
for b₁₂ being Element of b₅ st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂] holds
b₆ = b₉ ) holds
b₆ = b₇ `2

proof end;

theorem Th27: :: MCART_2:27

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & ( for b₈ being Element of b₁
for b₉ being Element of b₂
for b₁₀ being Element of b₃
for b₁₁ being Element of b₄
for b₁₂ being Element of b₅ st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂] holds
b₆ = b₁₀ ) holds
b₆ = b₇ `3

proof end;

theorem Th28: :: MCART_2:28

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & ( for b₈ being Element of b₁
for b₉ being Element of b₂
for b₁₀ being Element of b₃
for b₁₁ being Element of b₄
for b₁₂ being Element of b₅ st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂] holds
b₆ = b₁₁ ) holds
b₆ = b₇ `4

proof end;

theorem Th29: :: MCART_2:29

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & ( for b₈ being Element of b₁
for b₉ being Element of b₂
for b₁₀ being Element of b₃
for b₁₁ being Element of b₄
for b₁₂ being Element of b₅ st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂] holds
b₆ = b₁₂ ) holds
b₆ = b₇ `5

proof end;

theorem Th30: :: MCART_2:30

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ in [:b₂,b₃,b₄,b₅,b₆:] holds
ex b₇, b₈, b₉, b₁₀, b₁₁ being set st
( b₇ in b₂ & b₈ in b₃ & b₉ in b₄ & b₁₀ in b₅ & b₁₁ in b₆ & b₁ = [b₇,b₈,b₉,b₁₀,b₁₁] )

proof end;

theorem Th31: :: MCART_2:31

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set holds
( [b₁,b₂,b₃,b₄,b₅] in [:b₆,b₇,b₈,b₉,b₁₀:] iff ( b₁ in b₆ & b₂ in b₇ & b₃ in b₈ & b₄ in b₉ & b₅ in b₁₀ ) )

proof end;

theorem Th32: :: MCART_2:32

for b₁, b₂, b₃, b₄, b₅, b₆ being set st ( for b₇ being set holds
( b₇ in b₁ iff ex b₈, b₉, b₁₀, b₁₁, b₁₂ being set st
( b₈ in b₂ & b₉ in b₃ & b₁₀ in b₄ & b₁₁ in b₅ & b₁₂ in b₆ & b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂] ) ) ) holds
b₁ = [:b₂,b₃,b₄,b₅,b₆:]

proof end;

theorem Th33: :: MCART_2:33

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & b₉ <> {} & b₁₀ <> {} holds
for b₁₁ being Element of [:b₁,b₂,b₃,b₄,b₅:]
for b₁₂ being Element of [:b₆,b₇,b₈,b₉,b₁₀:] st b₁₁ = b₁₂ holds
( b₁₁ `1 = b₁₂ `1 & b₁₁ `2 = b₁₂ `2 & b₁₁ `3 = b₁₂ `3 & b₁₁ `4 = b₁₂ `4 & b₁₁ `5 = b₁₂ `5 )

proof end;

theorem Th34: :: MCART_2:34

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Subset of b₁
for b₇ being Subset of b₂
for b₈ being Subset of b₃
for b₉ being Subset of b₄
for b₁₀ being Subset of b₅
for b₁₁ being Element of [:b₁,b₂,b₃,b₄,b₅:] st b₁₁ in [:b₆,b₇,b₈,b₉,b₁₀:] holds
( b₁₁ `1 in b₆ & b₁₁ `2 in b₇ & b₁₁ `3 in b₈ & b₁₁ `4 in b₉ & b₁₁ `5 in b₁₀ )

proof end;

theorem Th35: :: MCART_2:35

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set st b₁ c= b₂ & b₃ c= b₄ & b₅ c= b₆ & b₇ c= b₈ & b₉ c= b₁₀ holds
[:b₁,b₃,b₅,b₇,b₉:] c= [:b₂,b₄,b₆,b₈,b₁₀:]

proof end;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
let c₆ be Subset of c₁;
let c₇ be Subset of c₂;
let c₈ be Subset of c₃;
let c₉ be Subset of c₄;
let c₁₀ be Subset of c₅;
redefine func [: as [:c₆,c₇,c₈,c₉,c₁₀:] -> Subset of [:a₁,a₂,a₃,a₄,a₅:];
coherence by Th35;

end;

theorem Th36: :: MCART_2:36

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
for b₃ being Element of [:b₁,b₂:] ex b₄ being Element of b₁ex b₅ being Element of b₂ st b₃ = [b₄,b₅] by Lemma1;

theorem Th37: :: MCART_2:37

for b₁, b₂, b₃ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} holds
for b₄ being Element of [:b₁,b₂,b₃:] ex b₅ being Element of b₁ex b₆ being Element of b₂ex b₇ being Element of b₃ st b₄ = [b₅,b₆,b₇] by Lemma2;

theorem Th38: :: MCART_2:38

for b₁, b₂, b₃, b₄ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} holds
for b₅ being Element of [:b₁,b₂,b₃,b₄:] ex b₆ being Element of b₁ex b₇ being Element of b₂ex b₈ being Element of b₃ex b₉ being Element of b₄ st b₅ = [b₆,b₇,b₈,b₉] by Lemma3;