:: 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-2021 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, ORDINAL1, 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 be NonatomicND of V,A; let d2 be object; 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 for d1 being NonatomicND of V,A, z being Element of V holds V is non empty & v in dom d1 & d = denaming(V,A,v).d1 implies local_overlapping(V,A,d1,d,z).z = d1.v; theorem :: NOMIN_2:12 v in V & v <> v1 implies for d1 being NonatomicND of V,A for d2 being TypeSCNominativeData of V,A st v1 in dom d1 & not d1 in A & not naming(V,A,v,d2) in A holds local_overlapping(V,A,d1,d2,v).v1 = d1.v1; theorem :: NOMIN_2:13 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:14 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:15 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:16 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:17 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:18 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:19 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:20 SC_exists(PP_BottomPred(ND(V,A)),v) = PP_BottomPred(ND(V,A)); ::$N Distributivity law theorem :: NOMIN_2:21 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:22 for f being Function, a,d being object holds NDentry(<*f*>,<*a*>,d) = {[a,f.d]}; theorem :: NOMIN_2:23 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:24 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:25 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:26 rng NDdataSeq(<*f*>,<*v*>,d) = v.-->f.d; theorem :: NOMIN_2:27 a in V & d in dom f implies NDentry(<*f*>,<*a*>,d) = naming(V,A,a,f.d); theorem :: NOMIN_2:28 a in V & d in dom f implies NDentry(<*f*>,<*a*>,d) is NonatomicND of V,A; theorem :: NOMIN_2:29 {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:30 {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:31 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:32 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:33 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:34 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:35 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:36 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:37 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:38 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:39 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;