:: Simple-named complex-valued nominative data -- definition and basic operations
:: by Ievgen Ivanov , Mykola Nikitchenko , Andrii Kryvolap and Artur Korni{\l}owicz
::
:: Received August 30, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th1: :: NOMIN_1:1

for x being object
for n being Nat
for f being FinSequence st n in dom f holds
(<*x*> ^ f) . (n + 1) = f . n

proof end;

theorem Th2: :: NOMIN_1:2

for n being Nat
for f being Function st dom f = NAT holds
f | (Seg n) is FinSequence

proof end;

theorem Th3: :: NOMIN_1:3

for f, g being FinSequence holds
( dom f c= dom g or dom g c= dom f )

proof end;

registration

let f, g be FinSequence;

cluster f +* g -> FinSequence-like ;

coherence
f +* g is FinSequence-like

proof end;

end;

registration

let f1, f2 be Function;

cluster f2 \/ (f1 | ((dom f1) \ (dom f2))) -> Function-like ;

coherence
f2 \/ (f1 | ((dom f1) \ (dom f2))) is Function-like

proof end;

end;

definition

let f, g be Function;
let x, y be object ;

pred f,x =~ g,y means :: NOMIN_1:def 1
( ( x in dom f implies y in dom g ) & ( y in dom g implies x in dom f ) & ( x in dom f implies f . x = g . y ) );

end;

:: deftheorem defines =~ NOMIN_1:def 1 :
for f, g being Function
for x, y being object holds
( f,x =~ g,y iff ( ( x in dom f implies y in dom g ) & ( y in dom g implies x in dom f ) & ( x in dom f implies f . x = g . y ) ) );

definition

let V, A be set ;
mode NominativeSet of V,A is PartFunc of V,A;

end;

registration

let V, A be set ;

cluster Relation-like V -defined A -valued Function-like finite for Element of bool [:V,A:];

existence
ex b₁ being NominativeSet of V,A st b₁ is finite

proof end;

end;

definition

let V, A be set ;
mode TypeSSNominativeData of V,A is finite NominativeSet of V,A;

end;

definition

let V, A be set ;

func NDSS (V,A) -> set equals :: NOMIN_1:def 2
{ d where d is TypeSSNominativeData of V,A : verum } ;

coherence
{ d where d is TypeSSNominativeData of V,A : verum } is set ;

end;

:: deftheorem defines NDSS NOMIN_1:def 2 :
for V, A being set holds NDSS (V,A) = { d where d is TypeSSNominativeData of V,A : verum } ;

registration

let V, A be set ;

cluster NDSS (V,A) -> non empty ;

coherence
not NDSS (V,A) is empty

proof end;

end;

theorem Th4: :: NOMIN_1:4

for x being object
for V, A being set st x in NDSS (V,A) holds
x is TypeSSNominativeData of V,A

proof end;

theorem :: NOMIN_1:5

for V, A being set holds NDSS (V,A) c= PFuncs (V,A)

proof end;

theorem Th6: :: NOMIN_1:6

for V, A being set holds {} in NDSS (V,A)

proof end;

theorem Th7: :: NOMIN_1:7

for V, A, B being set st A c= B holds
NDSS (V,A) c= NDSS (V,B)

proof end;

theorem Th8: :: NOMIN_1:8

for V, A being set
for f, g being finite Function st f tolerates g & f in NDSS (V,A) & g in NDSS (V,A) holds
f \/ g in NDSS (V,A)

proof end;

definition

let V, A be set ;

func FNDSC (V,A) -> Function means :Def3: :: NOMIN_1:def 3
( dom it = NAT & it . 0 = A & ( for n being Nat holds it . (n + 1) = NDSS (V,(A \/ (it . n))) ) );

existence
ex b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = A & ( for n being Nat holds b₁ . (n + 1) = NDSS (V,(A \/ (b₁ . n))) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & b₁ . 0 = A & ( for n being Nat holds b₁ . (n + 1) = NDSS (V,(A \/ (b₁ . n))) ) & dom b₂ = NAT & b₂ . 0 = A & ( for n being Nat holds b₂ . (n + 1) = NDSS (V,(A \/ (b₂ . n))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines FNDSC NOMIN_1:def 3 :
for V, A being set
for b₃ being Function holds
( b₃ = FNDSC (V,A) iff ( dom b₃ = NAT & b₃ . 0 = A & ( for n being Nat holds b₃ . (n + 1) = NDSS (V,(A \/ (b₃ . n))) ) ) );

theorem Th9: :: NOMIN_1:9

for V, A being set holds (FNDSC (V,A)) . 1 = NDSS (V,A)

proof end;

theorem Th10: :: NOMIN_1:10

for V, A being set holds (FNDSC (V,A)) . 2 = NDSS (V,(A \/ (NDSS (V,A))))

proof end;

theorem Th11: :: NOMIN_1:11

for V, A being set holds A c= Union (FNDSC (V,A))

proof end;

theorem :: NOMIN_1:12

for V, A being set
for n being Nat st 1 <= n holds
{} in (FNDSC (V,A)) . n

proof end;

registration

let V, A be set ;
let n be Nat;

cluster (FNDSC (V,A)) | (Seg n) -> FinSequence-like ;

coherence
(FNDSC (V,A)) | (Seg n) is FinSequence-like

proof end;

end;

theorem Th13: :: NOMIN_1:13

for V, A being set
for m, n being Nat st m <> 0 & m <= n holds
(FNDSC (V,A)) . m c= (FNDSC (V,A)) . n

proof end;

definition

let V, A be set ;
let S be FinSequence;

pred S IsNDRankSeq V,A means :: NOMIN_1:def 4
( S . 1 = NDSS (V,A) & ( for n being Nat st n in dom S & n + 1 in dom S holds
S . (n + 1) = NDSS (V,(A \/ (S . n))) ) );

end;

:: deftheorem defines IsNDRankSeq NOMIN_1:def 4 :
for V, A being set
for S being FinSequence holds
( S IsNDRankSeq V,A iff ( S . 1 = NDSS (V,A) & ( for n being Nat st n in dom S & n + 1 in dom S holds
S . (n + 1) = NDSS (V,(A \/ (S . n))) ) ) );

theorem :: NOMIN_1:14

for V, A being set
for S being FinSequence st S IsNDRankSeq V,A holds
S <> {} ;

theorem Th15: :: NOMIN_1:15

for V, A being set
for S, S1 being FinSequence st S IsNDRankSeq V,A & S1 c= S & S1 <> {} holds
S1 IsNDRankSeq V,A

proof end;

theorem Th16: :: NOMIN_1:16

for V, A being set
for n being Nat
for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds
S | n IsNDRankSeq V,A

proof end;

theorem Th17: :: NOMIN_1:17

for V, A being set
for S being FinSequence st S IsNDRankSeq V,A holds
S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A

proof end;

theorem Th18: :: NOMIN_1:18

for V, A being set
for n being Nat st 1 <= n holds
(FNDSC (V,A)) | (Seg n) IsNDRankSeq V,A

proof end;

theorem Th19: :: NOMIN_1:19

for V, A being set
for n being Nat
for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds
S . n = (FNDSC (V,A)) . n

proof end;

theorem Th20: :: NOMIN_1:20

for V, A being set
for S being FinSequence st S IsNDRankSeq V,A holds
S = (FNDSC (V,A)) | (dom S)

proof end;

theorem Th21: :: NOMIN_1:21

for V, A being set
for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A holds
S1 tolerates S2

proof end;

theorem Th22: :: NOMIN_1:22

for V, A being set
for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 c= S2 holds
S2 c= S1

proof end;

theorem Th23: :: NOMIN_1:23

for V, A being set
for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 +* S2 = S1 holds
S1 +* S2 = S2

proof end;

theorem :: NOMIN_1:24

for V, A being set
for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A holds
S1 +* S2 IsNDRankSeq V,A by Th23;

theorem Th25: :: NOMIN_1:25

for V, A being set
for m, n being Nat
for S being FinSequence st S IsNDRankSeq V,A & m <= n & n in dom S holds
S . m c= S . n

proof end;

theorem Th26: :: NOMIN_1:26

for V, A being set
for F being FinSequence st F IsNDRankSeq V,A holds
ex S being FinSequence st
( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

proof end;

Lm1: for V, A being set
for f being Function st ex S being FinSequence st
( S IsNDRankSeq V,A & f in Union S ) holds
f in Union (FNDSC (V,A))

proof end;

theorem Th27: :: NOMIN_1:27

for V, A being set holds <*(NDSS (V,A))*> IsNDRankSeq V,A

proof end;

theorem Th28: :: NOMIN_1:28

for V, A being set holds <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*> IsNDRankSeq V,A

proof end;

theorem :: NOMIN_1:29

for V, A being set holds <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A))))),(NDSS (V,(A \/ (NDSS (V,(A \/ (NDSS (V,A))))))))*> IsNDRankSeq V,A

proof end;

definition

let V, A be set ;

mode NonatomicND of V,A -> Function means :Def5: :: NOMIN_1:def 5
ex S being FinSequence st
( S IsNDRankSeq V,A & it in Union S );

existence
ex b₁ being Function ex S being FinSequence st
( S IsNDRankSeq V,A & b₁ in Union S )

proof end;

sethood
ex b₁ being set st
for b₂ being Function st ex S being FinSequence st
( S IsNDRankSeq V,A & b₂ in Union S ) holds
b₂ in b₁

proof end;

end;

:: deftheorem Def5 defines NonatomicND NOMIN_1:def 5 :
for V, A being set
for b₃ being Function holds
( b₃ is NonatomicND of V,A iff ex S being FinSequence st
( S IsNDRankSeq V,A & b₃ in Union S ) );

theorem Th30: :: NOMIN_1:30

for V, A being set holds {} is NonatomicND of V,A

proof end;

theorem Th31: :: NOMIN_1:31

for V, A being set
for D being NonatomicND of V,A holds D in Union (FNDSC (V,A))

proof end;

theorem Th32: :: NOMIN_1:32

for V, A being set
for D being NonatomicND of V,A
for d being set st d c= D holds
d is NonatomicND of V,A

proof end;

theorem Th33: :: NOMIN_1:33

for V, A being set
for D being NonatomicND of V,A ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

proof end;

registration

let V, A be set ;

cluster -> finite for NonatomicND of V,A;

coherence
for b₁ being NonatomicND of V,A holds b₁ is finite

proof end;

end;

theorem Th34: :: NOMIN_1:34

for V, A being set
for m being Nat
for S being FinSequence
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m holds
D1 \/ D2 in S . m

proof end;

theorem Th35: :: NOMIN_1:35

for V, A being set
for S1, S2 being FinSequence
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S2 IsNDRankSeq V,A & S1 c= S2 & D1 in Union S1 & D2 in Union S2 holds
D1 \/ D2 in Union S2

proof end;

theorem Th36: :: NOMIN_1:36

for V, A being set
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds
D1 \/ D2 is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:37

for V, A being set
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds
D1 +* D2 is NonatomicND of V,A

proof end;

definition

let V, A be set ;

mode TypeSCNominativeData of V,A -> set means :Def6: :: NOMIN_1:def 6
( it in A or it is NonatomicND of V,A );

existence
ex b₁ being set st
( b₁ in A or b₁ is NonatomicND of V,A )

proof end;

sethood
ex b₁ being set st
for b₂ being set st ( b₂ in A or b₂ is NonatomicND of V,A ) holds
b₂ in b₁

proof end;

end;

:: deftheorem Def6 defines TypeSCNominativeData NOMIN_1:def 6 :
for V, A, b₃ being set holds
( b₃ is TypeSCNominativeData of V,A iff ( b₃ in A or b₃ is NonatomicND of V,A ) );

registration

let V, A be set ;

cluster Relation-like Function-like for TypeSCNominativeData of V,A;

existence
ex b₁ being TypeSCNominativeData of V,A st
( b₁ is Function-like & b₁ is Relation-like )

proof end;

end;

definition

let V, A be set ;
:: original: NonatomicND
redefine mode NonatomicND of V,A -> Relation-like Function-like TypeSCNominativeData of V,A;
coherence
for b₁ being NonatomicND of V,A holds b₁ is Relation-like Function-like TypeSCNominativeData of V,A by Def6;

end;

definition

let V, A be set ;

func ND (V,A) -> set equals :: NOMIN_1:def 7
{ D where D is TypeSCNominativeData of V,A : verum } ;

coherence
{ D where D is TypeSCNominativeData of V,A : verum } is set ;

end;

:: deftheorem defines ND NOMIN_1:def 7 :
for V, A being set holds ND (V,A) = { D where D is TypeSCNominativeData of V,A : verum } ;

registration

let V, A be set ;

cluster ND (V,A) -> non empty ;

coherence
not ND (V,A) is empty

proof end;

end;

theorem :: NOMIN_1:38

for V, A being set holds {} in ND (V,A)

proof end;

theorem Th39: :: NOMIN_1:39

for x being object
for V, A being set st x in ND (V,A) holds
x is TypeSCNominativeData of V,A

proof end;

theorem :: NOMIN_1:40

for V, A being set holds ND (V,A) = Union (FNDSC (V,A))

proof end;

theorem Th41: :: NOMIN_1:41

for V, A being set
for D being NonatomicND of V,A holds D in ND (V,A)

proof end;

theorem Th42: :: NOMIN_1:42

for V, A being set
for D being NonatomicND of V,A st not D in A holds
D in (ND (V,A)) \ A

proof end;

theorem Th43: :: NOMIN_1:43

for x being object
for V, A being set st x in (ND (V,A)) \ A holds
x is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:44

for V, A being set
for D being TypeSCNominativeData of V,A holds D in Union (FNDSC (V,A))

proof end;

:: [v->a]

definition

let v, a be object ;

func ND_ex_1 (v,a) -> set equals :: NOMIN_1:def 8
v .--> a;

coherence
v .--> a is set ;

end;

:: deftheorem defines ND_ex_1 NOMIN_1:def 8 :
for v, a being object holds ND_ex_1 (v,a) = v .--> a;

registration

let v, a be object ;

cluster ND_ex_1 (v,a) -> Relation-like Function-like ;

coherence
( ND_ex_1 (v,a) is Function-like & ND_ex_1 (v,a) is Relation-like ) ;

end;

theorem Th45: :: NOMIN_1:45

for a, v being object
for V, A being set st v in V & a in A holds
ND_ex_1 (v,a) in NDSS (V,A)

proof end;

theorem Th46: :: NOMIN_1:46

for a, v being object
for V, A being set st v in V & a in A holds
ND_ex_1 (v,a) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;
let v be Element of V;
let a be Element of A;
:: original: ND_ex_1
redefine func ND_ex_1 (v,a) -> NonatomicND of V,A;
coherence
ND_ex_1 (v,a) is NonatomicND of V,A by Th46;

end;

theorem :: NOMIN_1:47

for a, v being object
for V, A being set st v in V & a in A holds
ND_ex_1 (v,a) is TypeSCNominativeData of V,A by Th46;

:: [v->[v1->a]]

definition

let v, v1, a1 be object ;

func ND_ex_2 (v,v1,a1) -> set equals :: NOMIN_1:def 9
v .--> (v1 .--> a1);

coherence
v .--> (v1 .--> a1) is set ;

end;

:: deftheorem defines ND_ex_2 NOMIN_1:def 9 :
for v, v1, a1 being object holds ND_ex_2 (v,v1,a1) = v .--> (v1 .--> a1);

registration

let v, v1, a1 be object ;

cluster ND_ex_2 (v,v1,a1) -> Relation-like Function-like ;

coherence
( ND_ex_2 (v,v1,a1) is Function-like & ND_ex_2 (v,v1,a1) is Relation-like ) ;

end;

theorem Th48: :: NOMIN_1:48

for a1, v, v1 being object
for V, A being set st {v,v1} c= V & a1 in A holds
ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))

proof end;

theorem Th49: :: NOMIN_1:49

for a1, v, v1 being object
for V, A being set st {v,v1} c= V & a1 in A holds
ND_ex_2 (v,v1,a1) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;
let v, v1 be Element of V;
let a be Element of A;
:: original: ND_ex_2
redefine func ND_ex_2 (v,v1,a) -> NonatomicND of V,A;
coherence
ND_ex_2 (v,v1,a) is NonatomicND of V,A

proof end;

end;

theorem :: NOMIN_1:50

for a1, v, v1 being object
for V, A being set st {v,v1} c= V & a1 in A holds
ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A by Th49;

:: [v->a,v1->a1]

definition

let v, v1, a, a1 be object ;

func ND_ex_3 (v,v1,a,a1) -> set equals :: NOMIN_1:def 10
(v,v1) --> (a,a1);

coherence
(v,v1) --> (a,a1) is set ;

end;

:: deftheorem defines ND_ex_3 NOMIN_1:def 10 :
for v, v1, a, a1 being object holds ND_ex_3 (v,v1,a,a1) = (v,v1) --> (a,a1);

registration

let v, v1, a, a1 be object ;

cluster ND_ex_3 (v,v1,a,a1) -> Relation-like Function-like ;

coherence
( ND_ex_3 (v,v1,a,a1) is Function-like & ND_ex_3 (v,v1,a,a1) is Relation-like ) ;

end;

theorem Th51: :: NOMIN_1:51

for a, a1, v, v1 being object
for V, A being set st {v,v1} c= V & {a,a1} c= A holds
ND_ex_3 (v,v1,a,a1) in NDSS (V,A)

proof end;

theorem Th52: :: NOMIN_1:52

for a, a1, v, v1 being object
for V, A being set st {v,v1} c= V & {a,a1} c= A holds
ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;
let v, v1 be Element of V;
let a, a1 be Element of A;
:: original: ND_ex_3
redefine func ND_ex_3 (v,v1,a,a1) -> NonatomicND of V,A;
coherence
ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A

proof end;

end;

theorem :: NOMIN_1:53

for a, a1, v, v1 being object
for V, A being set st {v,v1} c= V & {a,a1} c= A holds
ND_ex_3 (v,v1,a,a1) is TypeSCNominativeData of V,A by Th52;

:: [v->a,v1->[v2->a1]]

definition

let v, v1, v2, a, a1 be object ;

func ND_ex_4 (v,v1,v2,a,a1) -> set equals :: NOMIN_1:def 11
(v,v1) --> (a,(v2 .--> a1));

coherence
(v,v1) --> (a,(v2 .--> a1)) is set ;

end;

:: deftheorem defines ND_ex_4 NOMIN_1:def 11 :
for v, v1, v2, a, a1 being object holds ND_ex_4 (v,v1,v2,a,a1) = (v,v1) --> (a,(v2 .--> a1));

registration

let v, v1, v2, a, a1 be object ;

cluster ND_ex_4 (v,v1,v2,a,a1) -> Relation-like Function-like ;

coherence
( ND_ex_4 (v,v1,v2,a,a1) is Function-like & ND_ex_4 (v,v1,v2,a,a1) is Relation-like ) ;

end;

theorem Th54: :: NOMIN_1:54

for a, a1, v, v1, v2 being object
for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds
ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))

proof end;

theorem Th55: :: NOMIN_1:55

for a, a1, v, v1, v2 being object
for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds
ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A

proof end;

definition

let V, A be non empty set ;
let v, v1, v2 be Element of V;
let a, a1 be Element of A;
:: original: ND_ex_4
redefine func ND_ex_4 (v,v1,v2,a,a1) -> NonatomicND of V,A;
coherence
ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A

proof end;

end;

theorem :: NOMIN_1:56

for a, a1, v, v1, v2 being object
for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds
ND_ex_4 (v,v1,v2,a,a1) is TypeSCNominativeData of V,A by Th55;

theorem :: NOMIN_1:57

for x being object holds <*x*> is NonatomicND of {1},{x}

proof end;

definition

let V, A be set ;
let v be object ;
let D be NonatomicND of V,A;
assume A1: v in dom D ;

func denaming (v,D) -> TypeSCNominativeData of V,A equals :Def12: :: NOMIN_1:def 12
D . v;

coherence
D . v is TypeSCNominativeData of V,A

proof end;

end;

:: deftheorem Def12 defines denaming NOMIN_1:def 12 :
for V, A being set
for v being object
for D being NonatomicND of V,A st v in dom D holds
denaming (v,D) = D . v;

definition

let V, A be set ;
let v, D be object ;
assume A1: D is TypeSCNominativeData of V,A ;
assume A2: v in V ;

func naming (V,A,v,D) -> NonatomicND of V,A equals :Def13: :: NOMIN_1:def 13
v .--> D;

coherence
v .--> D is NonatomicND of V,A

proof end;

end;

:: deftheorem Def13 defines naming NOMIN_1:def 13 :
for V, A being set
for v, D being object st D is TypeSCNominativeData of V,A & v in V holds
naming (V,A,v,D) = v .--> D;

definition

let V, A be set ;
let a be object ;
let f be V -valued FinSequence;
assume A1: len f > 0 ;

func namingSeq (V,A,f,a) -> FinSequence means :Def14: :: NOMIN_1:def 14
( len it = len f & it . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len it holds
it . (n + 1) = naming (V,A,(f . ((len f) - n)),(it . n)) ) );

existence
ex b₁ being FinSequence st
( len b₁ = len f & b₁ . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b₁ holds
b₁ . (n + 1) = naming (V,A,(f . ((len f) - n)),(b₁ . n)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st len b₁ = len f & b₁ . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b₁ holds
b₁ . (n + 1) = naming (V,A,(f . ((len f) - n)),(b₁ . n)) ) & len b₂ = len f & b₂ . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b₂ holds
b₂ . (n + 1) = naming (V,A,(f . ((len f) - n)),(b₂ . n)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines namingSeq NOMIN_1:def 14 :
for V, A being set
for a being object
for f being b₁ -valued FinSequence st len f > 0 holds
for b₅ being FinSequence holds
( b₅ = namingSeq (V,A,f,a) iff ( len b₅ = len f & b₅ . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b₅ holds
b₅ . (n + 1) = naming (V,A,(f . ((len f) - n)),(b₅ . n)) ) ) );

theorem Th58: :: NOMIN_1:58

for a being object
for V, A being set
for n being Nat
for f being b₂ -valued FinSequence st 1 <= n & n <= len f holds
(namingSeq (V,A,f,a)) . n is NonatomicND of V,A

proof end;

definition

let V, A be set ;
let f be V -valued FinSequence;
let a be object ;

func naming (V,A,f,a) -> set equals :: NOMIN_1:def 15
(namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a)));

coherence
(namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a))) is set ;

end;

:: deftheorem defines naming NOMIN_1:def 15 :
for V, A being set
for f being b₁ -valued FinSequence
for a being object holds naming (V,A,f,a) = (namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a)));

theorem :: NOMIN_1:59

for a being object
for V, A being set
for f being b₂ -valued FinSequence st len f > 0 holds
naming (V,A,f,a) is NonatomicND of V,A

proof end;

theorem :: NOMIN_1:60

for a being object
for A being set
for V being non empty set
for v being Element of V holds naming (V,A,<*v*>,a) = naming (V,A,v,a)

proof end;

theorem :: NOMIN_1:61

for a being object
for A being set
for V being non empty set
for v1, v2 being Element of V st a is TypeSCNominativeData of V,A holds
naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)

proof end;

theorem :: NOMIN_1:62

for v being object
for V, A being set
for D being TypeSCNominativeData of V,A st v in V holds
denaming (v,(naming (V,A,v,D))) = D

proof end;

theorem :: NOMIN_1:63

for v being object
for V, A being set
for D being NonatomicND of V,A st v in dom D holds
naming (V,A,v,(denaming (v,D))) = v .--> (D . v)

proof end;

definition

let V, A be set ;
let d1, d2 be object ;
assume that
A1: d1 is TypeSCNominativeData of V,A and
A2: d2 is TypeSCNominativeData of V,A ;

func global_overlapping (V,A,d1,d2) -> TypeSCNominativeData of V,A means :Def16: :: NOMIN_1:def 16
ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & it = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) if ( not d1 in A & not d2 in A )
otherwise it = d2;

existence
( ( not d1 in A & not d2 in A implies ex b₁ being TypeSCNominativeData of V,A ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₁ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) & ( ( d1 in A or d2 in A ) implies ex b₁ being TypeSCNominativeData of V,A st b₁ = d2 ) )

proof end;

uniqueness
for b₁, b₂ being TypeSCNominativeData of V,A holds
( ( not d1 in A & not d2 in A & ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₁ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) & ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₂ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) implies b₁ = b₂ ) & ( ( d1 in A or d2 in A ) & b₁ = d2 & b₂ = d2 implies b₁ = b₂ ) ) ;
consistency
for b₁ being TypeSCNominativeData of V,A holds verum ;

end;

:: deftheorem Def16 defines global_overlapping NOMIN_1:def 16 :
for V, A being set
for d1, d2 being object st d1 is TypeSCNominativeData of V,A & d2 is TypeSCNominativeData of V,A holds
for b₅ being TypeSCNominativeData of V,A holds
( ( not d1 in A & not d2 in A implies ( b₅ = global_overlapping (V,A,d1,d2) iff ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₅ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) ) & ( ( d1 in A or d2 in A ) implies ( b₅ = global_overlapping (V,A,d1,d2) iff b₅ = d2 ) ) );

definition

let V, A be set ;
let d1, d2, v be object ;

func local_overlapping (V,A,d1,d2,v) -> TypeSCNominativeData of V,A equals :: NOMIN_1:def 17
global_overlapping (V,A,d1,(naming (V,A,v,d2)));

coherence
global_overlapping (V,A,d1,(naming (V,A,v,d2))) is TypeSCNominativeData of V,A ;

end;

:: deftheorem defines local_overlapping NOMIN_1:def 17 :
for V, A being set
for d1, d2, v being object holds local_overlapping (V,A,d1,d2,v) = global_overlapping (V,A,d1,(naming (V,A,v,d2)));

theorem Th64: :: NOMIN_1:64

for V, A being set
for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A holds
global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))

proof end;

theorem Th65: :: NOMIN_1:65

for V, A being set
for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A & dom D1 c= dom D2 holds
global_overlapping (V,A,D1,D2) = D2

proof end;

theorem :: NOMIN_1:66

for V, A being set
for D being NonatomicND of V,A holds global_overlapping (V,A,D,D) = D

proof end;

theorem :: NOMIN_1:67

for a1, a2, v being object
for V, A being set st v in V & not v .--> a1 in A & not v .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds
global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2

proof end;

theorem Th68: :: NOMIN_1:68

for a1, a2, v1, v2 being object
for V, A being set st {v1,v2} c= V & v1 <> v2 & not v1 .--> a1 in A & not v2 .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds
global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) = (v2,v1) --> (a2,a1)

proof end;

theorem :: NOMIN_1:69

for a1, a2, v, v1, v2 being object
for V, A being set st {v,v1,v2} c= V & v <> v1 & a2 in A & not v1 .--> a1 in A & not v .--> (v2 .--> a2) in A & a1 is TypeSCNominativeData of V,A holds
local_overlapping (V,A,(v1 .--> a1),(v2 .--> a2),v) = (v,v1) --> ((v2 .--> a2),a1)

proof end;

definition

let V, A be set ;
let v be object ;
set Dom = { d where d is NonatomicND of V,A : v in dom d } ;

func denaming (V,A,v) -> PartFunc of (ND (V,A)),(ND (V,A)) means :: NOMIN_1:def 18
( dom it = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom it holds
it . D = denaming (v,D) ) );

existence
ex b₁ being PartFunc of (ND (V,A)),(ND (V,A)) st
( dom b₁ = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b₁ holds
b₁ . D = denaming (v,D) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of (ND (V,A)),(ND (V,A)) st dom b₁ = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b₁ holds
b₁ . D = denaming (v,D) ) & dom b₂ = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b₂ holds
b₂ . D = denaming (v,D) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines denaming NOMIN_1:def 18 :
for V, A being set
for v being object
for b₄ being PartFunc of (ND (V,A)),(ND (V,A)) holds
( b₄ = denaming (V,A,v) iff ( dom b₄ = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b₄ holds
b₄ . D = denaming (v,D) ) ) );

definition

let V, A be set ;
let v be object ;

func naming (V,A,v) -> Function of (ND (V,A)),(ND (V,A)) means :: NOMIN_1:def 19
for D being TypeSCNominativeData of V,A holds it . D = naming (V,A,v,D);

existence
ex b₁ being Function of (ND (V,A)),(ND (V,A)) st
for D being TypeSCNominativeData of V,A holds b₁ . D = naming (V,A,v,D)

proof end;

uniqueness
for b₁, b₂ being Function of (ND (V,A)),(ND (V,A)) st ( for D being TypeSCNominativeData of V,A holds b₁ . D = naming (V,A,v,D) ) & ( for D being TypeSCNominativeData of V,A holds b₂ . D = naming (V,A,v,D) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines naming NOMIN_1:def 19 :
for V, A being set
for v being object
for b₄ being Function of (ND (V,A)),(ND (V,A)) holds
( b₄ = naming (V,A,v) iff for D being TypeSCNominativeData of V,A holds b₄ . D = naming (V,A,v,D) );

definition

let V, A be set ;
let v be object ;

func local_overlapping (V,A,v) -> PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) means :: NOMIN_1:def 20
( dom it = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A
for d2 being object st not d1 in A & d2 in ND (V,A) holds
it . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) );

existence
ex b₁ being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) st
( dom b₁ = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A
for d2 being object st not d1 in A & d2 in ND (V,A) holds
b₁ . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) st dom b₁ = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A
for d2 being object st not d1 in A & d2 in ND (V,A) holds
b₁ . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) & dom b₂ = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A
for d2 being object st not d1 in A & d2 in ND (V,A) holds
b₂ . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines local_overlapping NOMIN_1:def 20 :
for V, A being set
for v being object
for b₄ being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) holds
( b₄ = local_overlapping (V,A,v) iff ( dom b₄ = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A
for d2 being object st not d1 in A & d2 in ND (V,A) holds
b₄ . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) ) );