:: On an algorithmic algebra over simple-named complex-valued nominative data
:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Received June 29, 2018
:: Copyright (c) 2018-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NOMIN_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1,
MARGREL1, XBOOLEAN, TARSKI, ZFMISC_1, NOMIN_2, PARTPR_1, FUNCOP_1, NAT_1,
FINSEQ_1, FINSET_1, PARTPR_2, XXREAL_0, ARYTM_3, CARD_1, NUMBERS,
FINSEQ_2, CARD_3, ORDERS_5, SETFAM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, MARGREL1, RELAT_1,
RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, BINOP_1,
SETFAM_1, XXREAL_0, NAT_1, CARD_1, NUMBERS, CARD_3, FINSEQ_1, FINSEQ_2,
NOMIN_1, PARTPR_1, PARTPR_2;
constructors ENUMSET1, RELSET_1, SETFAM_1, NOMIN_1, PARTPR_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, RELSET_1, NOMIN_1,
PARTPR_1, FINSEQ_1, PARTPR_2, ORDINAL1, XREAL_0, FINSEQ_2, FINSET_1,
FINSEQ_3, JORDAN23;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin :: Preliminaries
reserve a,b,c,v,v1,x,y for object;
reserve V,A for set;
reserve d for TypeSCNominativeData of V,A;
theorem :: NOMIN_2:1
{a,b,c} c= A iff a in A & b in A & c in A;
registration
let a,b,c,d,e,f be object;
cluster {[a,b],[c,d],[e,f]} -> Relation-like;
end;
theorem :: NOMIN_2:2
for a,b,c,d,e,f being object holds dom {[a,b],[c,d],[e,f]} = {a,c,e};
theorem :: NOMIN_2:3
for a,b,c,d,e,f being object holds rng {[a,b],[c,d],[e,f]} = {b,d,f};
registration
let V;
cluster one-to-one V-valued for FinSequence;
end;
theorem :: NOMIN_2:4
dom <*a,b,c*> = {1,2,3};
registration
let V,A;
cluster NDSS(V,A) -> non with_non-empty_elements;
cluster ND(V,A) -> non with_non-empty_elements;
end;
theorem :: NOMIN_2:5
v in V implies {[v,d]} is NonatomicND of V,A;
theorem :: NOMIN_2:6
for D being finite Function st dom D c= V & rng D c= ND(V,A) holds
D is NonatomicND of V,A;
theorem :: NOMIN_2:7
for d1,d2 being TypeSCNominativeData of V,A holds
d2 c= global_overlapping(V,A,d1,d2);
theorem :: NOMIN_2:8
for d being NonatomicND of V,A holds d is TypeSCNominativeData of V,A;
theorem :: NOMIN_2:9
for d1,d2 being NonatomicND of V,A holds
global_overlapping(V,A,d1,d2) is NonatomicND of V,A;
registration
let V,A;
let d1,d2 be NonatomicND of V,A;
cluster global_overlapping(V,A,d1,d2) -> Function-like Relation-like;
end;
registration
let V,A,v;
let d1,d2 be NonatomicND of V,A;
cluster local_overlapping(V,A,d1,d2,v) -> Function-like Relation-like;
end;
registration
let V,A,v;
let d1 be NonatomicND of V,A;
let d2 be TypeSCNominativeData of V,A;
cluster local_overlapping(V,A,d1,d2,v) -> Function-like Relation-like;
end;
theorem :: NOMIN_2:10
v in V implies
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;
theorem :: NOMIN_2:11
v in V & v <> v1 implies
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;
theorem :: NOMIN_2:12
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;
theorem :: NOMIN_2:13
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;
theorem :: NOMIN_2:14
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;
definition
let V,A;
mode SCPartialNominativePredicate of V,A is PartialPredicate of ND(V,A);
end;
reserve p,q,r for SCPartialNominativePredicate of V,A;
theorem :: NOMIN_2:15
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};
theorem :: NOMIN_2:16
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};
theorem :: NOMIN_2:17
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};
definition
let V,A,v;
func SCexists(V,A,v) -> Function of Pr(ND(V,A)),Pr(ND(V,A)) means
:: 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);
end;
definition
let V,A,v,p;
func SC_exists(p,v) -> SCPartialNominativePredicate of V,A equals
:: NOMIN_2:def 2
SCexists(V,A,v).p;
end;
theorem :: NOMIN_2:18
x in dom SC_exists(p,v) implies
(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);
theorem :: NOMIN_2:19
SC_exists(PP_BottomPred(ND(V,A)),v) = PP_BottomPred(ND(V,A));
::$N Distributivity law
theorem :: NOMIN_2:20
SC_exists(PP_or(p,q),v) = PP_or(SC_exists(p,v),SC_exists(q,v));
begin :: On an algorithmic algebra over simple-named complex-valued nominative data
reserve n for Nat;
reserve X for Function;
definition
let F be Function-yielding Function;
let d be object;
pred d in_doms F means
:: NOMIN_2:def 3
for x being object st x in dom F holds d in dom(F.x);
end;
definition
let g be Function-yielding Function;
let X be Function;
let d be object;
func NDdataSeq(g,X,d) -> Function means
:: NOMIN_2:def 4
dom it = dom X &
for x st x in dom X holds it.x = [X.x,g.x.d];
end;
registration
let g be Function-yielding Function;
let X be finite Function;
let d be object;
cluster NDdataSeq(g,X,d) -> finite;
end;
registration
let g be Function-yielding Function;
let X be FinSequence;
let d be object;
cluster NDdataSeq(g,X,d) -> FinSequence-like;
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);
end;
theorem :: NOMIN_2:21
for f being Function, a,d being object holds
NDentry(<*f*>,<*a*>,d) = {[a,f.d]};
theorem :: NOMIN_2:22
for f,g being Function, a,b,d being object holds
NDentry(<*f,g*>,<*a,b*>,d) = {[a,f.d],[b,g.d]};
theorem :: NOMIN_2:23
for f,g,h being Function, a,b,c,d being object holds
NDentry(<*f,g,h*>,<*a,b,c*>,d) = {[a,f.d],[b,g.d],[c,h.d]};
registration
let g be Function-yielding Function;
let X be Function;
let d be object;
cluster NDentry(g,X,d) -> Relation-like;
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;
end;
registration
let g be Function-yielding Function;
let X be finite Function;
let d be object;
cluster NDentry(g,X,d) -> finite;
end;
theorem :: NOMIN_2:24
for g being Function-yielding Function, X being Function, d being object
holds dom NDentry(g,X,d) = rng X;
definition
let V,A;
mode SCBinominativeFunction of V,A is PartFunc of ND(V,A),ND(V,A);
end;
reserve f,g,h for SCBinominativeFunction of V,A;
theorem :: NOMIN_2:25
rng NDdataSeq(<*f*>,<*v*>,d) = v.-->f.d;
theorem :: NOMIN_2:26
a in V & d in dom f implies NDentry(<*f*>,<*a*>,d) = naming(V,A,a,f.d);
theorem :: NOMIN_2:27
a in V & d in dom f implies
NDentry(<*f*>,<*a*>,d) is NonatomicND of V,A;
theorem :: NOMIN_2:28
{a,b} c= V & a <> b & d in dom f & d in dom g implies
NDentry(<*f,g*>,<*a,b*>,d) is NonatomicND of V,A;
theorem :: NOMIN_2:29
{a,b,c} c= V & a,b,c are_mutually_distinct &
d in dom f & d in dom g & d in dom h implies
NDentry(<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A;
definition
let V,A;
let f be FinSequence;
attr f is (V,A)-FPrg-yielding means
:: NOMIN_2:def 6
for n st 1 <= n <= len f holds f.n is SCBinominativeFunction of V,A;
end;
registration
let V,A,f;
cluster <*f*> -> (V,A)-FPrg-yielding;
end;
registration
let V,A,f,g;
cluster <*f,g*> -> (V,A)-FPrg-yielding;
end;
registration
let V,A,f,g,h;
cluster <*f,g,h*> -> (V,A)-FPrg-yielding;
end;
registration
let V,A,n;
cluster (V,A)-FPrg-yielding n-element for FinSequence;
end;
registration
let V,A,x;
let g be (V,A)-FPrg-yielding FinSequence;
cluster g.x -> Function-like Relation-like;
end;
registration
let V,A;
cluster (V,A)-FPrg-yielding -> Function-yielding for FinSequence;
end;
theorem :: NOMIN_2:30
for g being (V,A)-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);
theorem :: NOMIN_2:31
for g being (V,A)-FPrg-yielding FinSequence
for X being one-to-one V-valued FinSequence st
dom g = dom X & d in_doms g
holds NDentry(g,X,d) is NonatomicND of V,A;
::$N Assignment composition
definition
let V,A,v;
func SCassignment(V,A,v) -> Function of FPrg(ND(V,A)),FPrg(ND(V,A)) means
:: NOMIN_2:def 7
for f being SCBinominativeFunction of V,A holds
dom(it.f) = dom f &
for d being TypeSCNominativeData of V,A holds
d in dom(it.f) implies it.f.d = local_overlapping(V,A,d,f.d,v);
end;
::$N Assignment composition
definition
let V,A,v,f;
func SC_assignment(f,v) -> SCBinominativeFunction of V,A equals
:: NOMIN_2:def 8
SCassignment(V,A,v).f;
end;
registration
let V,A,f,v;
let d be NonatomicND of V,A;
cluster (SC_assignment(f,v)).d -> Function-like Relation-like;
end;
theorem :: NOMIN_2:32
for d being NonatomicND of V,A holds
v in V & not d in A & not naming(V,A,v,f.d) in A & d in dom f implies
dom (SC_assignment(f,v).d) = dom d \/ {v};
::$N The composition of superposition into a predicate
definition
let V,A;
let g be (V,A)-FPrg-yielding FinSequence such that
product g <> {};
let X be Function;
func SCPsuperpos(g,X) -> Function of [:Pr(ND(V,A)),product g:],Pr(ND(V,A))
means
:: 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));
end;
::$N The composition of superposition into a predicate
definition
let V,A,p;
let g be (V,A)-FPrg-yielding FinSequence such that
product g <> {};
let X be Function;
let x be Element of product g;
func SC_Psuperpos(p,x,X) -> SCPartialNominativePredicate of V,A equals
:: NOMIN_2:def 10
SCPsuperpos(g,X).(p,x);
end;
theorem :: NOMIN_2:33
for g being (V,A)-FPrg-yielding FinSequence st product g <> {}
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));
::$N The composition of superposition into a predicate (one function)
definition
let V,A,v;
func SCPsuperpos(V,A,v) ->
Function of [:Pr(ND(V,A)),FPrg(ND(V,A)):],Pr(ND(V,A))
means
:: 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);
end;
::$N The composition of superposition into a predicate (one function)
definition
let V,A,v,p,f;
func SC_Psuperpos(p,f,v) -> SCPartialNominativePredicate of V,A equals
:: NOMIN_2:def 12
SCPsuperpos(V,A,v).(p,f);
end;
theorem :: NOMIN_2:34
d in dom(SC_Psuperpos(p,f,v)) implies
SC_Psuperpos(p,f,v).d = p.local_overlapping(V,A,d,f.d,v) & d in dom f;
theorem :: NOMIN_2:35
for x being Element of product <*f*> st
v in V & product <*f*> <> {} holds
SC_Psuperpos(p,f,v) = SC_Psuperpos(p,x,<*v*>);
::$N The composition of superposition into a function
definition
let V,A;
let g be (V,A)-FPrg-yielding FinSequence such that
product g <> {};
let X be Function;
func SCFsuperpos(g,X) ->
Function of [:FPrg(ND(V,A)),product g:],FPrg(ND(V,A))
means
:: 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));
end;
::$N The composition of superposition into a function
definition
let V,A,f;
let g be (V,A)-FPrg-yielding FinSequence such that
product g <> {};
let X be Function;
let x be Element of product g;
func SC_Fsuperpos(f,x,X) -> SCBinominativeFunction of V,A equals
:: NOMIN_2:def 14
SCFsuperpos(g,X).(f,x);
end;
theorem :: NOMIN_2:36
for g being (V,A)-FPrg-yielding FinSequence st product g <> {}
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));
::$N The composition of superposition into a function (one function)
definition
let V,A,v;
func SCFsuperpos(V,A,v) ->
Function of [:FPrg(ND(V,A)),FPrg(ND(V,A)):],FPrg(ND(V,A))
means
:: 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);
end;
::$N The composition of superposition into a function (one function)
definition
let V,A,v,f,g;
func SC_Fsuperpos(f,g,v) -> SCBinominativeFunction of V,A equals
:: NOMIN_2:def 16
SCFsuperpos(V,A,v).(f,g);
end;
theorem :: NOMIN_2:37
d in dom(SC_Fsuperpos(f,g,v)) implies
SC_Fsuperpos(f,g,v).d = f.local_overlapping(V,A,d,g.d,v) & d in dom g;
theorem :: NOMIN_2:38
for x being Element of product <*g*> st
v in V & product <*g*> <> {} holds
SC_Fsuperpos(f,g,v) = SC_Fsuperpos(f,x,<*v*>);
::$N Name checking predicate
definition
let V,A,v;
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);
end;