:: Simple-named complex-valued nominative data -- definition and basic operations
:: by Ievgen Ivanov , Mykola Nikitchenko , Andrii Kryvolap and Artur Korni{\l}owicz
::
:: Copyright (c) 2017-2019 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;
coherence
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 ;
existence
ex b1 being NominativeSet of V,A st b1 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 b1 being Function st
( dom b1 = NAT & b1 . 0 = A & ( for n being Nat holds b1 . (n + 1) = NDSS (V,(A \/ (b1 . n))) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = A & ( for n being Nat holds b1 . (n + 1) = NDSS (V,(A \/ (b1 . n))) ) & dom b2 = NAT & b2 . 0 = A & ( for n being Nat holds b2 . (n + 1) = NDSS (V,(A \/ (b2 . n))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines FNDSC NOMIN_1:def 3 :
for V, A being set
for b3 being Function holds
( b3 = FNDSC (V,A) iff ( dom b3 = NAT & b3 . 0 = A & ( for n being Nat holds b3 . (n + 1) = NDSS (V,(A \/ (b3 . 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 b1 being Function ex S being FinSequence st
( S IsNDRankSeq V,A & b1 in Union S )
proof end;
sethood
ex b1 being set st
for b2 being Function st ex S being FinSequence st
( S IsNDRankSeq V,A & b2 in Union S ) holds
b2 in b1
proof end;
end;

:: deftheorem Def5 defines NonatomicND NOMIN_1:def 5 :
for V, A being set
for b3 being Function holds
( b3 is NonatomicND of V,A iff ex S being FinSequence st
( S IsNDRankSeq V,A & b3 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 b1 being NonatomicND of V,A holds b1 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 b1 being set st
( b1 in A or b1 is NonatomicND of V,A )
proof end;
sethood
ex b1 being set st
for b2 being set st ( b2 in A or b2 is NonatomicND of V,A ) holds
b2 in b1
proof end;
end;

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

registration
let V, A be set ;
existence
ex b1 being TypeSCNominativeData of V,A st
( b1 is Function-like & b1 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 b1 being NonatomicND of V,A holds b1 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 ;
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 b1 being FinSequence st
( len b1 = len f & b1 . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b1 holds
b1 . (n + 1) = naming (V,A,(f . ((len f) - n)),(b1 . n)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = len f & b1 . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b1 holds
b1 . (n + 1) = naming (V,A,(f . ((len f) - n)),(b1 . n)) ) & len b2 = len f & b2 . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b2 holds
b2 . (n + 1) = naming (V,A,(f . ((len f) - n)),(b2 . n)) ) holds
b1 = b2
proof end;
end;

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

theorem Th58: :: NOMIN_1:58
for a being object
for V, A being set
for n being Nat
for f being b2 -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 b1 -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 b2 -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 b1 being TypeSCNominativeData of V,A ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b1 = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) & ( ( d1 in A or d2 in A ) implies ex b1 being TypeSCNominativeData of V,A st b1 = d2 ) )
proof end;
uniqueness
for b1, b2 being TypeSCNominativeData of V,A holds
( ( not d1 in A & not d2 in A & ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b1 = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) & ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b2 = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) implies b1 = b2 ) & ( ( d1 in A or d2 in A ) & b1 = d2 & b2 = d2 implies b1 = b2 ) )
;
consistency
for b1 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 b5 being TypeSCNominativeData of V,A holds
( ( not d1 in A & not d2 in A implies ( b5 = global_overlapping (V,A,d1,d2) iff ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b5 = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) ) & ( ( d1 in A or d2 in A ) implies ( b5 = global_overlapping (V,A,d1,d2) iff b5 = 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 st not D in 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 b1 being PartFunc of (ND (V,A)),(ND (V,A)) st
( dom b1 = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b1 holds
b1 . D = denaming (v,D) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (ND (V,A)),(ND (V,A)) st dom b1 = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b1 holds
b1 . D = denaming (v,D) ) & dom b2 = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b2 holds
b2 . D = denaming (v,D) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines denaming NOMIN_1:def 18 :
for V, A being set
for v being object
for b4 being PartFunc of (ND (V,A)),(ND (V,A)) holds
( b4 = denaming (V,A,v) iff ( dom b4 = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b4 holds
b4 . 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 b1 being Function of (ND (V,A)),(ND (V,A)) st
for D being TypeSCNominativeData of V,A holds b1 . D = naming (V,A,v,D)
proof end;
uniqueness
for b1, b2 being Function of (ND (V,A)),(ND (V,A)) st ( for D being TypeSCNominativeData of V,A holds b1 . D = naming (V,A,v,D) ) & ( for D being TypeSCNominativeData of V,A holds b2 . D = naming (V,A,v,D) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines naming NOMIN_1:def 19 :
for V, A being set
for v being object
for b4 being Function of (ND (V,A)),(ND (V,A)) holds
( b4 = naming (V,A,v) iff for D being TypeSCNominativeData of V,A holds b4 . 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 b1 being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) st
( dom b1 = [:((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
b1 . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) st dom b1 = [:((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
b1 . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) & dom b2 = [:((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
b2 . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines local_overlapping NOMIN_1:def 20 :
for V, A being set
for v being object
for b4 being PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) holds
( b4 = local_overlapping (V,A,v) iff ( dom b4 = [:((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
b4 . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) ) );