:: On an algorithmic algebra over simple-named complex-valued nominative data
:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Copyright (c) 2018-2019 Association of Mizar Users

theorem Th1: :: NOMIN_2:1
for a, b, c being object
for A being set holds
( {a,b,c} c= A iff ( a in A & b in A & c in A ) )
proof end;

registration
let a, b, c, d, e, f be object ;
cluster {[a,b],[c,d],[e,f]} -> Relation-like ;
coherence
{[a,b],[c,d],[e,f]} is Relation-like
proof end;
end;

theorem Th2: :: NOMIN_2:2
for a, b, c, d, e, f being object holds dom {[a,b],[c,d],[e,f]} = {a,c,e}
proof end;

theorem Th3: :: NOMIN_2:3
for a, b, c, d, e, f being object holds rng {[a,b],[c,d],[e,f]} = {b,d,f}
proof end;

registration
let V be set ;
existence
ex b1 being FinSequence st
( b1 is one-to-one & b1 is V -valued )
proof end;
end;

theorem Th4: :: NOMIN_2:4
for a, b, c being object holds dom <*a,b,c*> = {1,2,3}
proof end;

registration
let V, A be set ;
cluster NDSS (V,A) -> non with_non-empty_elements ;
coherence
not NDSS (V,A) is with_non-empty_elements
by NOMIN_1:6;
cluster ND (V,A) -> non with_non-empty_elements ;
coherence
not ND (V,A) is with_non-empty_elements
by NOMIN_1:38;
end;

theorem Th5: :: NOMIN_2:5
for v being object
for V, A being set
for d being TypeSCNominativeData of V,A st v in V holds
{[v,d]} is NonatomicND of V,A
proof end;

theorem Th6: :: NOMIN_2:6
for V, A being set
for D being finite Function st dom D c= V & rng D c= ND (V,A) holds
D is NonatomicND of V,A
proof end;

theorem :: NOMIN_2:7
for V, A being set
for d1, d2 being TypeSCNominativeData of V,A holds d2 c= global_overlapping (V,A,d1,d2)
proof end;

theorem :: NOMIN_2:8
for V, A being set
for d being NonatomicND of V,A holds d is TypeSCNominativeData of V,A ;

theorem Th9: :: NOMIN_2:9
for V, A being set
for d1, d2 being NonatomicND of V,A holds global_overlapping (V,A,d1,d2) is NonatomicND of V,A
proof end;

registration
let V, A be set ;
let d1, d2 be NonatomicND of V,A;
cluster global_overlapping (V,A,d1,d2) -> Relation-like Function-like ;
coherence
( global_overlapping (V,A,d1,d2) is Function-like & global_overlapping (V,A,d1,d2) is Relation-like )
by Th9;
end;

registration
let V, A be set ;
let v be object ;
let d1, d2 be NonatomicND of V,A;
cluster local_overlapping (V,A,d1,d2,v) -> Relation-like Function-like ;
coherence
( local_overlapping (V,A,d1,d2,v) is Function-like & local_overlapping (V,A,d1,d2,v) is Relation-like )
;
end;

registration
let V, A be set ;
let v be object ;
let d1 be NonatomicND of V,A;
let d2 be TypeSCNominativeData of V,A;
cluster local_overlapping (V,A,d1,d2,v) -> Relation-like Function-like ;
coherence
( local_overlapping (V,A,d1,d2,v) is Function-like & local_overlapping (V,A,d1,d2,v) is Relation-like )
;
end;

theorem :: NOMIN_2:10
for v being object
for V, A being set st v in V holds
for d1, d2 being TypeSCNominativeData of V,A
for L being Function st L = local_overlapping (V,A,d1,d2,v) holds
L . v = d2
proof end;

theorem :: NOMIN_2:11
for v, v1 being object
for V, A being set st v in V & v <> v1 holds
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A
for L being Function st L = local_overlapping (V,A,d1,d2,v) & v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
L . v1 = d1 . v1
proof end;

theorem Th12: :: NOMIN_2:12
for v being object
for V, A being set
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v in V & not v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
proof end;

theorem Th13: :: NOMIN_2:13
for v being object
for V, A being set
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v in V & v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = dom d1
proof end;

theorem Th14: :: NOMIN_2:14
for v being object
for V, A being set
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v in V & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
proof end;

definition
let V, A be set ;
mode SCPartialNominativePredicate of V,A is PartialPredicate of (ND (V,A));
end;

theorem Th15: :: NOMIN_2:15
for V, A being set
for p, q being SCPartialNominativePredicate of V,A holds dom (PP_or (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) }
proof end;

theorem :: NOMIN_2:16
for V, A being set
for p, q being SCPartialNominativePredicate of V,A holds dom (PP_and (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }
proof end;

theorem :: NOMIN_2:17
for V, A being set
for p, q being SCPartialNominativePredicate of V,A holds dom (PP_imp (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
proof end;

definition
let V, A be set ;
let v be object ;
defpred S1[ object , Function] means ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,$1,d1,v) in dom$2 & $2 . (local_overlapping (V,A,$1,d1,v)) = TRUE );
defpred S2[ object , Function] means for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,$1,d1,v) in dom$2 & $2 . (local_overlapping (V,A,$1,d1,v)) = FALSE );
deffunc H1( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( S1[d,$1] or S2[d,$1] ) } ;
func SCexists (V,A,v) -> Function of (Pr (ND (V,A))),(Pr (ND (V,A))) means :Def1: :: NOMIN_2:def 1
for p being SCPartialNominativePredicate of V,A holds
( dom (it . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) )
}
& ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (it . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (it . p) . d = FALSE ) ) ) );
existence
ex b1 being Function of (Pr (ND (V,A))),(Pr (ND (V,A))) st
for p being SCPartialNominativePredicate of V,A holds
( dom (b1 . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) )
}
& ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b1 . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b1 . p) . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being Function of (Pr (ND (V,A))),(Pr (ND (V,A))) st ( for p being SCPartialNominativePredicate of V,A holds
( dom (b1 . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) )
}
& ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b1 . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b1 . p) . d = FALSE ) ) ) ) ) & ( for p being SCPartialNominativePredicate of V,A holds
( dom (b2 . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) )
}
& ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b2 . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b2 . p) . d = FALSE ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines SCexists NOMIN_2:def 1 :
for V, A being set
for v being object
for b4 being Function of (Pr (ND (V,A))),(Pr (ND (V,A))) holds
( b4 = SCexists (V,A,v) iff for p being SCPartialNominativePredicate of V,A holds
( dom (b4 . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) )
}
& ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (b4 . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (b4 . p) . d = FALSE ) ) ) ) );

definition
let V, A be set ;
let v be object ;
let p be SCPartialNominativePredicate of V,A;
func SC_exists (p,v) -> SCPartialNominativePredicate of V,A equals :: NOMIN_2:def 2
(SCexists (V,A,v)) . p;
coherence
(SCexists (V,A,v)) . p is SCPartialNominativePredicate of V,A
proof end;
end;

:: deftheorem defines SC_exists NOMIN_2:def 2 :
for V, A being set
for v being object
for p being SCPartialNominativePredicate of V,A holds SC_exists (p,v) = (SCexists (V,A,v)) . p;

theorem Th18: :: NOMIN_2:18
for v, x being object
for V, A being set
for p being SCPartialNominativePredicate of V,A holds
( not x in dom (SC_exists (p,v)) or ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )
proof end;

theorem :: NOMIN_2:19
for v being object
for V, A being set holds SC_exists ((PP_BottomPred (ND (V,A))),v) = PP_BottomPred (ND (V,A))
proof end;

:: Distributivity law
theorem :: NOMIN_2:20
for v being object
for V, A being set
for p, q being SCPartialNominativePredicate of V,A holds SC_exists ((PP_or (p,q)),v) = PP_or ((SC_exists (p,v)),(SC_exists (q,v)))
proof end;

definition
let F be Function-yielding Function;
let d be object ;
pred d in_doms F means :Def3: :: NOMIN_2:def 3
for x being object st x in dom F holds
d in dom (F . x);
end;

:: deftheorem Def3 defines in_doms NOMIN_2:def 3 :
for F being Function-yielding Function
for d being object holds
( d in_doms F iff for x being object st x in dom F holds
d in dom (F . x) );

definition
let g be Function-yielding Function;
let X be Function;
let d be object ;
func NDdataSeq (g,X,d) -> Function means :Def4: :: NOMIN_2:def 4
( dom it = dom X & ( for x being object st x in dom X holds
it . x = [(X . x),((g . x) . d)] ) );
existence
ex b1 being Function st
( dom b1 = dom X & ( for x being object st x in dom X holds
b1 . x = [(X . x),((g . x) . d)] ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom X & ( for x being object st x in dom X holds
b1 . x = [(X . x),((g . x) . d)] ) & dom b2 = dom X & ( for x being object st x in dom X holds
b2 . x = [(X . x),((g . x) . d)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines NDdataSeq NOMIN_2:def 4 :
for g being Function-yielding Function
for X being Function
for d being object
for b4 being Function holds
( b4 = NDdataSeq (g,X,d) iff ( dom b4 = dom X & ( for x being object st x in dom X holds
b4 . x = [(X . x),((g . x) . d)] ) ) );

registration
let g be Function-yielding Function;
let X be finite Function;
let d be object ;
cluster NDdataSeq (g,X,d) -> finite ;
coherence
NDdataSeq (g,X,d) is finite
proof end;
end;

registration
let g be Function-yielding Function;
let X be FinSequence;
let d be object ;
cluster NDdataSeq (g,X,d) -> FinSequence-like ;
coherence
NDdataSeq (g,X,d) is FinSequence-like
proof end;
end;

definition
let g be Function-yielding Function;
let X be Function;
let d be object ;
func NDentry (g,X,d) -> set equals :: NOMIN_2:def 5
rng (NDdataSeq (g,X,d));
coherence
rng (NDdataSeq (g,X,d)) is set
;
end;

:: deftheorem defines NDentry NOMIN_2:def 5 :
for g being Function-yielding Function
for X being Function
for d being object holds NDentry (g,X,d) = rng (NDdataSeq (g,X,d));

theorem :: NOMIN_2:21
for f being Function
for a, d being object holds NDentry (<*f*>,<*a*>,d) = {[a,(f . d)]}
proof end;

theorem Th22: :: NOMIN_2:22
for f, g being Function
for a, b, d being object holds NDentry (<*f,g*>,<*a,b*>,d) = {[a,(f . d)],[b,(g . d)]}
proof end;

theorem Th23: :: NOMIN_2:23
for f, g, h being Function
for a, b, c, d being object holds NDentry (<*f,g,h*>,<*a,b,c*>,d) = {[a,(f . d)],[b,(g . d)],[c,(h . d)]}
proof end;

registration
let g be Function-yielding Function;
let X be Function;
let d be object ;
cluster NDentry (g,X,d) -> Relation-like ;
coherence
NDentry (g,X,d) is Relation-like
proof end;
end;

registration
let g be Function-yielding Function;
let X be one-to-one Function;
let d be object ;
cluster NDentry (g,X,d) -> Function-like ;
coherence
NDentry (g,X,d) is Function-like
proof end;
end;

registration
let g be Function-yielding Function;
let X be finite Function;
let d be object ;
cluster NDentry (g,X,d) -> finite ;
coherence
NDentry (g,X,d) is finite
;
end;

theorem Th24: :: NOMIN_2:24
for g being Function-yielding Function
for X being Function
for d being object holds dom (NDentry (g,X,d)) = rng X
proof end;

definition
let V, A be set ;
mode SCBinominativeFunction of V,A is PartFunc of (ND (V,A)),(ND (V,A));
end;

theorem Th25: :: NOMIN_2:25
for v being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)
proof end;

theorem Th26: :: NOMIN_2:26
for a being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))
proof end;

theorem :: NOMIN_2:27
for a being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A
proof end;

theorem :: NOMIN_2:28
for a, b being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f, g being SCBinominativeFunction of V,A st {a,b} c= V & a <> b & d in dom f & d in dom g holds
NDentry (<*f,g*>,<*a,b*>,d) is NonatomicND of V,A
proof end;

theorem :: NOMIN_2:29
for a, b, c being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f, g, h being SCBinominativeFunction of V,A st {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h holds
NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A
proof end;

definition
let V, A be set ;
let f be FinSequence;
attr f is V,A -FPrg-yielding means :Def6: :: NOMIN_2:def 6
for n being Nat st 1 <= n & n <= len f holds
f . n is SCBinominativeFunction of V,A;
end;

:: deftheorem Def6 defines -FPrg-yielding NOMIN_2:def 6 :
for V, A being set
for f being FinSequence holds
( f is V,A -FPrg-yielding iff for n being Nat st 1 <= n & n <= len f holds
f . n is SCBinominativeFunction of V,A );

registration
let V, A be set ;
let f be SCBinominativeFunction of V,A;
cluster <*f*> -> V,A -FPrg-yielding ;
coherence
<*f*> is V,A -FPrg-yielding
proof end;
end;

registration
let V, A be set ;
let f, g be SCBinominativeFunction of V,A;
cluster <*f,g*> -> V,A -FPrg-yielding ;
coherence
<*f,g*> is V,A -FPrg-yielding
proof end;
end;

registration
let V, A be set ;
let f, g, h be SCBinominativeFunction of V,A;
cluster <*f,g,h*> -> V,A -FPrg-yielding ;
coherence
<*f,g,h*> is V,A -FPrg-yielding
proof end;
end;

registration
let V, A be set ;
let n be Nat;
existence
ex b1 being FinSequence st
( b1 is V,A -FPrg-yielding & b1 is n -element )
proof end;
end;

registration
let V, A be set ;
let x be object ;
let g be V,A -FPrg-yielding FinSequence;
coherence
( g . x is Function-like & g . x is Relation-like )
proof end;
end;

registration
let V, A be set ;
coherence
for b1 being FinSequence st b1 is V,A -FPrg-yielding holds
b1 is Function-yielding
;
end;

theorem Th30: :: NOMIN_2:30
for V, A being set
for d being TypeSCNominativeData of V,A
for g being b1,b2 -FPrg-yielding FinSequence
for X being one-to-one FinSequence st dom g = dom X & d in_doms g holds
rng (NDentry (g,X,d)) c= ND (V,A)
proof end;

theorem :: NOMIN_2:31
for V, A being set
for d being TypeSCNominativeData of V,A
for g being b1,b2 -FPrg-yielding FinSequence
for X being b1 -valued one-to-one FinSequence st dom g = dom X & d in_doms g holds
NDentry (g,X,d) is NonatomicND of V,A
proof end;

:: Assignment composition
definition
let V, A be set ;
let v be object ;
func SCassignment (V,A,v) -> Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) means :Def7: :: NOMIN_2:def 7
for f being SCBinominativeFunction of V,A holds
( dom (it . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (it . f) holds
(it . f) . d = local_overlapping (V,A,d,(f . d),v) ) );
existence
ex b1 being Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) st
for f being SCBinominativeFunction of V,A holds
( dom (b1 . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b1 . f) holds
(b1 . f) . d = local_overlapping (V,A,d,(f . d),v) ) )
proof end;
uniqueness
for b1, b2 being Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) st ( for f being SCBinominativeFunction of V,A holds
( dom (b1 . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b1 . f) holds
(b1 . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) ) & ( for f being SCBinominativeFunction of V,A holds
( dom (b2 . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b2 . f) holds
(b2 . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines SCassignment NOMIN_2:def 7 :
for V, A being set
for v being object
for b4 being Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) holds
( b4 = SCassignment (V,A,v) iff for f being SCBinominativeFunction of V,A holds
( dom (b4 . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b4 . f) holds
(b4 . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) );

:: Assignment composition
definition
let V, A be set ;
let v be object ;
let f be SCBinominativeFunction of V,A;
func SC_assignment (f,v) -> SCBinominativeFunction of V,A equals :: NOMIN_2:def 8
(SCassignment (V,A,v)) . f;
coherence
(SCassignment (V,A,v)) . f is SCBinominativeFunction of V,A
proof end;
end;

:: deftheorem defines SC_assignment NOMIN_2:def 8 :
for V, A being set
for v being object
for f being SCBinominativeFunction of V,A holds SC_assignment (f,v) = (SCassignment (V,A,v)) . f;

registration
let V, A be set ;
let f be SCBinominativeFunction of V,A;
let v be object ;
let d be NonatomicND of V,A;
cluster (SC_assignment (f,v)) . d -> Relation-like Function-like ;
coherence
( (SC_assignment (f,v)) . d is Function-like & (SC_assignment (f,v)) . d is Relation-like )
proof end;
end;

theorem :: NOMIN_2:32
for v being object
for V, A being set
for f being SCBinominativeFunction of V,A
for d being NonatomicND of V,A st v in V & not d in A & not naming (V,A,v,(f . d)) in A & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}
proof end;

:: The composition of superposition into a predicate
definition
let V, A be set ;
let g be V,A -FPrg-yielding FinSequence;
assume A1: product g <> {} ;
let X be Function;
defpred S1[ object ] means $1 in_doms g; deffunc H1( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom$1 & S1[d] ) } ;
func SCPsuperpos (g,X) -> Function of [:(Pr (ND (V,A))),():],(Pr (ND (V,A))) means :Def9: :: NOMIN_2:def 9
for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (it . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
it . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) );
existence
ex b1 being Function of [:(Pr (ND (V,A))),():],(Pr (ND (V,A))) st
for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (b1 . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
b1 . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) )
proof end;
uniqueness
for b1, b2 being Function of [:(Pr (ND (V,A))),():],(Pr (ND (V,A))) st ( for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (b1 . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
b1 . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) & ( for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (b2 . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
b2 . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines SCPsuperpos NOMIN_2:def 9 :
for V, A being set
for g being b1,b2 -FPrg-yielding FinSequence st product g <> {} holds
for X being Function
for b5 being Function of [:(Pr (ND (V,A))),():],(Pr (ND (V,A))) holds
( b5 = SCPsuperpos (g,X) iff for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (b5 . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
b5 . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) );

:: The composition of superposition into a predicate
definition
let V, A be set ;
let p be SCPartialNominativePredicate of V,A;
let g be V,A -FPrg-yielding FinSequence;
assume A1: product g <> {} ;
let X be Function;
let x be Element of product g;
func SC_Psuperpos (p,x,X) -> SCPartialNominativePredicate of V,A equals :Def10: :: NOMIN_2:def 10
(SCPsuperpos (g,X)) . (p,x);
coherence
(SCPsuperpos (g,X)) . (p,x) is SCPartialNominativePredicate of V,A
proof end;
end;

:: deftheorem Def10 defines SC_Psuperpos NOMIN_2:def 10 :
for V, A being set
for p being SCPartialNominativePredicate of V,A
for g being b1,b2 -FPrg-yielding FinSequence st product g <> {} holds
for X being Function
for x being Element of product g holds SC_Psuperpos (p,x,X) = (SCPsuperpos (g,X)) . (p,x);

theorem Th33: :: NOMIN_2:33
for V, A being set
for d being TypeSCNominativeData of V,A
for p being SCPartialNominativePredicate of V,A
for X being Function
for g being b1,b2 -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
proof end;

:: The composition of superposition into a predicate (one function)
definition
let V, A be set ;
let v be object ;
deffunc H1( Function, Function) -> set = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,($2 . d),v) in dom$1 & d in dom $2 ) } ; func SCPsuperpos (V,A,v) -> Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) means :Def11: :: NOMIN_2:def 11 for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A holds ( dom (it . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds it . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ); existence ex b1 being Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) st for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A holds ( dom (b1 . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds b1 . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) proof end; uniqueness for b1, b2 being Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) st ( for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A holds ( dom (b1 . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds b1 . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ) & ( for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A holds ( dom (b2 . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds b2 . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def11 defines SCPsuperpos NOMIN_2:def 11 : for V, A being set for v being object for b4 being Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) holds ( b4 = SCPsuperpos (V,A,v) iff for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A holds ( dom (b4 . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds b4 . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ); :: The composition of superposition into a predicate (one function) definition let V, A be set ; let v be object ; let p be SCPartialNominativePredicate of V,A; let f be SCBinominativeFunction of V,A; func SC_Psuperpos (p,f,v) -> SCPartialNominativePredicate of V,A equals :: NOMIN_2:def 12 (SCPsuperpos (V,A,v)) . (p,f); coherence (SCPsuperpos (V,A,v)) . (p,f) is SCPartialNominativePredicate of V,A proof end; end; :: deftheorem defines SC_Psuperpos NOMIN_2:def 12 : for V, A being set for v being object for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A holds SC_Psuperpos (p,f,v) = (SCPsuperpos (V,A,v)) . (p,f); theorem Th34: :: NOMIN_2:34 for v being object for V, A being set for d being TypeSCNominativeData of V,A for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds ( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f ) proof end; theorem :: NOMIN_2:35 for v being object for V, A being set for p being SCPartialNominativePredicate of V,A for f being SCBinominativeFunction of V,A for x being Element of product <*f*> st v in V & product <*f*> <> {} holds SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>) proof end; :: The composition of superposition into a function definition let V, A be set ; let g be V,A -FPrg-yielding FinSequence; assume A1: product g <> {} ; let X be Function; defpred S1[ object ] means$1 in_doms g;
deffunc H1( Function) -> set = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom $1 & S1[d] ) } ; func SCFsuperpos (g,X) -> Function of [:(FPrg (ND (V,A))),():],(FPrg (ND (V,A))) means :Def13: :: NOMIN_2:def 13 for f being SCBinominativeFunction of V,A for x being Element of product g holds ( dom (it . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds it . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ); existence ex b1 being Function of [:(FPrg (ND (V,A))),():],(FPrg (ND (V,A))) st for f being SCBinominativeFunction of V,A for x being Element of product g holds ( dom (b1 . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds b1 . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) proof end; uniqueness for b1, b2 being Function of [:(FPrg (ND (V,A))),():],(FPrg (ND (V,A))) st ( for f being SCBinominativeFunction of V,A for x being Element of product g holds ( dom (b1 . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds b1 . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) & ( for f being SCBinominativeFunction of V,A for x being Element of product g holds ( dom (b2 . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds b2 . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def13 defines SCFsuperpos NOMIN_2:def 13 : for V, A being set for g being b1,b2 -FPrg-yielding FinSequence st product g <> {} holds for X being Function for b5 being Function of [:(FPrg (ND (V,A))),():],(FPrg (ND (V,A))) holds ( b5 = SCFsuperpos (g,X) iff for f being SCBinominativeFunction of V,A for x being Element of product g holds ( dom (b5 . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds b5 . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ); :: The composition of superposition into a function definition let V, A be set ; let f be SCBinominativeFunction of V,A; let g be V,A -FPrg-yielding FinSequence; assume A1: product g <> {} ; let X be Function; let x be Element of product g; func SC_Fsuperpos (f,x,X) -> SCBinominativeFunction of V,A equals :Def14: :: NOMIN_2:def 14 (SCFsuperpos (g,X)) . (f,x); coherence (SCFsuperpos (g,X)) . (f,x) is SCBinominativeFunction of V,A proof end; end; :: deftheorem Def14 defines SC_Fsuperpos NOMIN_2:def 14 : for V, A being set for f being SCBinominativeFunction of V,A for g being b1,b2 -FPrg-yielding FinSequence st product g <> {} holds for X being Function for x being Element of product g holds SC_Fsuperpos (f,x,X) = (SCFsuperpos (g,X)) . (f,x); theorem Th36: :: NOMIN_2:36 for V, A being set for d being TypeSCNominativeData of V,A for X being Function for f being SCBinominativeFunction of V,A for g being b1,b2 -FPrg-yielding FinSequence st product g <> {} holds for x being Element of product g st d in dom (SC_Fsuperpos (f,x,X)) holds ( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) proof end; :: The composition of superposition into a function (one function) definition let V, A be set ; let v be object ; deffunc H1( Function, Function) -> set = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,($2 . d),v) in dom $1 & d in dom$2 ) } ;
func SCFsuperpos (V,A,v) -> Function of [:(FPrg (ND (V,A))),(FPrg (ND (V,A))):],(FPrg (ND (V,A))) means :Def15: :: NOMIN_2:def 15
for f, g being SCBinominativeFunction of V,A holds
( dom (it . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds
it . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) );
existence
ex b1 being Function of [:(FPrg (ND (V,A))),(FPrg (ND (V,A))):],(FPrg (ND (V,A))) st
for f, g being SCBinominativeFunction of V,A holds
( dom (b1 . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds
b1 . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) )
proof end;
uniqueness
for b1, b2 being Function of [:(FPrg (ND (V,A))),(FPrg (ND (V,A))):],(FPrg (ND (V,A))) st ( for f, g being SCBinominativeFunction of V,A holds
( dom (b1 . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds
b1 . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) ) ) & ( for f, g being SCBinominativeFunction of V,A holds
( dom (b2 . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds
b2 . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines SCFsuperpos NOMIN_2:def 15 :
for V, A being set
for v being object
for b4 being Function of [:(FPrg (ND (V,A))),(FPrg (ND (V,A))):],(FPrg (ND (V,A))) holds
( b4 = SCFsuperpos (V,A,v) iff for f, g being SCBinominativeFunction of V,A holds
( dom (b4 . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds
b4 . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) ) );

:: The composition of superposition into a function (one function)
definition
let V, A be set ;
let v be object ;
let f, g be SCBinominativeFunction of V,A;
func SC_Fsuperpos (f,g,v) -> SCBinominativeFunction of V,A equals :: NOMIN_2:def 16
(SCFsuperpos (V,A,v)) . (f,g);
coherence
(SCFsuperpos (V,A,v)) . (f,g) is SCBinominativeFunction of V,A
proof end;
end;

:: deftheorem defines SC_Fsuperpos NOMIN_2:def 16 :
for V, A being set
for v being object
for f, g being SCBinominativeFunction of V,A holds SC_Fsuperpos (f,g,v) = (SCFsuperpos (V,A,v)) . (f,g);

theorem Th37: :: NOMIN_2:37
for v being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f, g being SCBinominativeFunction of V,A st d in dom (SC_Fsuperpos (f,g,v)) holds
( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g )
proof end;

theorem :: NOMIN_2:38
for v being object
for V, A being set
for f, g being SCBinominativeFunction of V,A
for x being Element of product <*g*> st v in V & product <*g*> <> {} holds
SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>)
proof end;

:: Name checking predicate
definition
let V, A be set ;
let v be object ;
defpred S1[ object ] means ex d being NonatomicND of V,A st
( d = \$1 & denaming (v,d) in (ND (V,A)) \ A );
func SC_name_check (V,A,v) -> SCPartialNominativePredicate of V,A means :: NOMIN_2:def 17
( dom it = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom it holds
( ( denaming (v,d) in dom it implies it . d = TRUE ) & ( not denaming (v,d) in dom it implies it . d = FALSE ) ) ) );
existence
ex b1 being SCPartialNominativePredicate of V,A st
( dom b1 = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b1 holds
( ( denaming (v,d) in dom b1 implies b1 . d = TRUE ) & ( not denaming (v,d) in dom b1 implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b1 holds
( ( denaming (v,d) in dom b1 implies b1 . d = TRUE ) & ( not denaming (v,d) in dom b1 implies b1 . d = FALSE ) ) ) & dom b2 = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b2 holds
( ( denaming (v,d) in dom b2 implies b2 . d = TRUE ) & ( not denaming (v,d) in dom b2 implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SC_name_check NOMIN_2:def 17 :
for V, A being set
for v being object
for b4 being SCPartialNominativePredicate of V,A holds
( b4 = SC_name_check (V,A,v) iff ( dom b4 = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b4 holds
( ( denaming (v,d) in dom b4 implies b4 . d = TRUE ) & ( not denaming (v,d) in dom b4 implies b4 . d = FALSE ) ) ) ) );