:: General theory and tools for proving algorithms in nominative data systems :: by Adrian Jaszczak :: :: Received October 25, 2020 :: Copyright (c) 2020-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, NUMBERS, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1, NAT_1, ARYTM_3, PARTFUN1, XBOOLEAN, TARSKI, NOMIN_3, NOMIN_4, XCMPLX_0, NOMIN_2, PARTPR_1, PARTPR_2, CARD_1, CAT_6, NOMIN_7, XXREAL_0, ARYTM_1, NOMIN_8, MARGREL1, FUNCOP_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MARGREL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCOP_1, CARD_1, FINSEQ_1, XXREAL_0, XCMPLX_0, NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5, NOMIN_6, NOMIN_7; constructors RELSET_1, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5, NOMIN_6, NOMIN_7; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, RELSET_1, INT_1, NOMIN_1, MARGREL1, NOMIN_2, NAT_1, XXREAL_0, XREAL_0, CARD_1, FINSEQ_1, PARTFUN1, NOMIN_7, PARTPR_2; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin registration let D be non empty set; cluster non empty D-valued for FinSequence; end; registration let D be non empty set, n be Nat; cluster D-valued n-element for FinSequence; end; reserve D for non empty set; reserve f1,f2,f3,f4,f5,f6,f7,f8,f9,f10 for BinominativeFunction of D; reserve p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11 for PartialPredicate of D; reserve q1,q2,q3,q4,q5,q6,q7,q8,q9,q10 for total PartialPredicate of D; reserve n,m,N for Nat; reserve fD for PFuncs(D,D)-valued FinSequence; reserve fB for PFuncs(D,BOOLEAN)-valued FinSequence; reserve V,A for set; reserve val for Function; reserve loc for V-valued Function; reserve d1 for NonatomicND of V,A; reserve p for SCPartialNominativePredicate of V,A; reserve d,v for object; reserve size for non zero Nat; reserve inp,pos for FinSequence; reserve prg for non empty FPrg(ND(V,A))-valued FinSequence; definition let D,f1,f2,f3,f4,f5,f6,f7; func PP_composition(f1,f2,f3,f4,f5,f6,f7) -> BinominativeFunction of D equals :: NOMIN_8:def 1 PP_composition(PP_composition(f1,f2,f3,f4,f5,f6),f7); end; ::$N Unconditional composition rule for 7 programs theorem :: NOMIN_8:1 <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*p7,f7,p8*> is SFHT of D & <*PP_inversion(p2),f2,p3*> is SFHT of D & <*PP_inversion(p3),f3,p4*> is SFHT of D & <*PP_inversion(p4),f4,p5*> is SFHT of D & <*PP_inversion(p5),f5,p6*> is SFHT of D & <*PP_inversion(p6),f6,p7*> is SFHT of D & <*PP_inversion(p7),f7,p8*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7),p8*> is SFHT of D; definition let D,f1,f2,f3,f4,f5,f6,f7,f8; func PP_composition(f1,f2,f3,f4,f5,f6,f7,f8) -> BinominativeFunction of D equals :: NOMIN_8:def 2 PP_composition(PP_composition(f1,f2,f3,f4,f5,f6,f7),f8); end; ::$N Unconditional composition rule for 8 programs theorem :: NOMIN_8:2 <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*p7,f7,p8*> is SFHT of D & <*p8,f8,p9*> is SFHT of D & <*PP_inversion(p2),f2,p3*> is SFHT of D & <*PP_inversion(p3),f3,p4*> is SFHT of D & <*PP_inversion(p4),f4,p5*> is SFHT of D & <*PP_inversion(p5),f5,p6*> is SFHT of D & <*PP_inversion(p6),f6,p7*> is SFHT of D & <*PP_inversion(p7),f7,p8*> is SFHT of D & <*PP_inversion(p8),f8,p9*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8),p9*> is SFHT of D; definition let D,f1,f2,f3,f4,f5,f6,f7,f8,f9; func PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9) -> BinominativeFunction of D equals :: NOMIN_8:def 3 PP_composition(PP_composition(f1,f2,f3,f4,f5,f6,f7,f8),f9); end; ::$N Unconditional composition rule for 9 programs theorem :: NOMIN_8:3 <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*p7,f7,p8*> is SFHT of D & <*p8,f8,p9*> is SFHT of D & <*p9,f9,p10*> is SFHT of D & <*PP_inversion(p2),f2,p3*> is SFHT of D & <*PP_inversion(p3),f3,p4*> is SFHT of D & <*PP_inversion(p4),f4,p5*> is SFHT of D & <*PP_inversion(p5),f5,p6*> is SFHT of D & <*PP_inversion(p6),f6,p7*> is SFHT of D & <*PP_inversion(p7),f7,p8*> is SFHT of D & <*PP_inversion(p8),f8,p9*> is SFHT of D & <*PP_inversion(p9),f9,p10*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9),p10*> is SFHT of D; definition let D,f1,f2,f3,f4,f5,f6,f7,f8,f9,f10; func PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10) -> BinominativeFunction of D equals :: NOMIN_8:def 4 PP_composition(PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9),f10); end; ::$N Unconditional composition rule for 10 programs theorem :: NOMIN_8:4 <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*p7,f7,p8*> is SFHT of D & <*p8,f8,p9*> is SFHT of D & <*p9,f9,p10*> is SFHT of D & <*p10,f10,p11*> is SFHT of D & <*PP_inversion(p2),f2,p3*> is SFHT of D & <*PP_inversion(p3),f3,p4*> is SFHT of D & <*PP_inversion(p4),f4,p5*> is SFHT of D & <*PP_inversion(p5),f5,p6*> is SFHT of D & <*PP_inversion(p6),f6,p7*> is SFHT of D & <*PP_inversion(p7),f7,p8*> is SFHT of D & <*PP_inversion(p8),f8,p9*> is SFHT of D & <*PP_inversion(p9),f9,p10*> is SFHT of D & <*PP_inversion(p10),f10,p11*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10),p11*> is SFHT of D; theorem :: NOMIN_8:5 <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2),p2*> is SFHT of D; theorem :: NOMIN_8:6 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3),p2*> is SFHT of D; theorem :: NOMIN_8:7 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4),p2*> is SFHT of D; theorem :: NOMIN_8:8 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5),p2*> is SFHT of D; theorem :: NOMIN_8:9 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6),p2*> is SFHT of D; theorem :: NOMIN_8:10 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7),p2*> is SFHT of D; theorem :: NOMIN_8:11 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8),p2*> is SFHT of D; theorem :: NOMIN_8:12 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,q8*> is SFHT of D & <*q8,f9,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9),p2*> is SFHT of D; theorem :: NOMIN_8:13 <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,q8*> is SFHT of D & <*q8,f9,q9*> is SFHT of D & <*q9,f10,p2*> is SFHT of D implies <*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10),p2*> is SFHT of D; definition let D,fD such that 0 < len fD; func PP_compositionSeq(fD) -> FinSequence of PFuncs(D,D) means :: NOMIN_8:def 5 len it = len fD & it.1 = fD.1 & for n being Nat st 1 <= n < len fD holds it.(n+1) = PP_composition(it.n,fD.(n+1)); end; definition let D,fD; func PP_composition(fD) -> BinominativeFunction of D equals :: NOMIN_8:def 6 PP_compositionSeq(fD).len PP_compositionSeq(fD); end; definition let D,fD,fB; pred fD,fB are_composable means :: NOMIN_8:def 7 1 <= len fD & len fB = len fD + 1 & (for n st 1 <= n <= len fD holds <*fB.n,fD.n,fB.(n+1)*> is SFHT of D) & (for n st 2 <= n <= len fD holds <*PP_inversion(fB.n),fD.n,fB.(n+1)*> is SFHT of D); end; ::$N Composition rule for sequences of programs theorem :: NOMIN_8:14 fD,fB are_composable implies <*fB.1,PP_composition(fD),fB.(len fB)*> is SFHT of D; definition let V,A; let val be FinSequence; func denamingSeq(V,A,val) -> FinSequence of PFuncs(ND(V,A),ND(V,A)) means :: NOMIN_8:def 8 len it = len val & for n being Nat st 1 <= n <= len it holds it.n = denaming(V,A,val.n); end; definition let V,A,loc; let val be FinSequence such that len val > 0; let p be SCPartialNominativePredicate of V,A; func SC_Psuperpos_Seq(loc,val,p) -> FinSequence of PFuncs(ND(V,A),BOOLEAN) means :: NOMIN_8:def 9 len it = len val & it.1 = SC_Psuperpos(p,denaming(V,A,val.len val),loc/.len val) & for n being Nat st 1 <= n < len it holds it.(n+1) = SC_Psuperpos(it.n,denaming(V,A,val.(len val-n)),loc/.(len val-n)); end; theorem :: NOMIN_8:15 for size being non zero Nat for val being size-element FinSequence holds loc,val,size are_correct_wrt d1 & 1 <= n & n <= len LocalOverlapSeq(A,loc,val,d1,size) & 1 <= m & m <= len LocalOverlapSeq(A,loc,val,d1,size) implies LocalOverlapSeq(A,loc,val,d1,size).n in dom denaming(V,A,val.m); definition let V,A,inp,d; let val be FinSequence; pred inp is_valid_input V,A,val,d means :: NOMIN_8:def 10 ex d1 being NonatomicND of V,A st d = d1 & val is_valid_wrt d1 & for n being Nat st 1 <= n <= len inp holds d1.(val.n) = inp.n; end; definition let V,A,inp; let val be FinSequence; func valid_input(V,A,val,inp) -> SCPartialNominativePredicate of V,A means :: NOMIN_8:def 11 dom it = ND(V,A) & for d being object st d in dom it holds (inp is_valid_input V,A,val,d implies it.d = TRUE) & (not inp is_valid_input V,A,val,d implies it.d = FALSE); end; registration let V,A,inp; let val be FinSequence; cluster valid_input(V,A,val,inp) -> total; end; definition let V,A,d; let Z,res be FinSequence; pred res is_valid_output V,A,Z,d means :: NOMIN_8:def 12 ex d1 being NonatomicND of V,A st d = d1 & Z is_valid_wrt d1 & for n being Nat st 1 <= n <= len Z holds d1.(Z.n) = res.n; end; definition let V,A; let Z,res be object; func valid_output(V,A,Z,res) -> SCPartialNominativePredicate of V,A means :: NOMIN_8:def 13 dom it = {d where d is TypeSCNominativeData of V,A: d in dom denaming(V,A,Z)} & for d being object st d in dom it holds (<*res*> is_valid_output V,A,<*Z*>,d implies it.d = TRUE) & (not <*res*> is_valid_output V,A,<*Z*>,d implies it.d = FALSE); end; theorem :: NOMIN_8:16 for val being size-element FinSequence holds loc,val,size are_correct_wrt d1 & d = LocalOverlapSeq(A,loc,val,d1,size).(size-1) & 2 <= n+1 < size & local_overlapping(V,A,d,denaming(V,A,val.len val).d,loc/.len val) in dom p implies local_overlapping(V,A,LocalOverlapSeq(A,loc,val,d1,size).(size-n-1), denaming(V,A,val.(len val-n)). (LocalOverlapSeq(A,loc,val,d1,size).(size-n-1)), loc/.(len val-n)) in dom(SC_Psuperpos_Seq(loc,val,p).n); theorem :: NOMIN_8:17 for val being size-element FinSequence holds loc,val,size are_correct_wrt d1 & d = LocalOverlapSeq(A,loc,val,d1,size).(size-1) & local_overlapping(V,A,d,denaming(V,A,val.len val).d,loc/.len val) in dom p implies for m,n being Nat st 1 <= m < size & 1 <= n < size holds SC_Psuperpos_Seq(loc,val,p).m.(LocalOverlapSeq(A,loc,val,d1,size).(size-m)) = SC_Psuperpos_Seq(loc,val,p).n.(LocalOverlapSeq(A,loc,val,d1,size).(size-n)); theorem :: NOMIN_8:18 for val being size-element FinSequence for dx,dy being object for NN being Nat st NN = size-2 holds loc,val,size are_correct_wrt d1 & dx = LocalOverlapSeq(A,loc,val,d1,size).(size-1) & local_overlapping(V,A,dx,denaming(V,A,val.len val).dx,loc/.len val) in dom p & dy = local_overlapping(V,A,LocalOverlapSeq(A,loc,val,d1,size).NN, denaming(V,A,val.(NN+1)).(LocalOverlapSeq(A,loc,val,d1,size).NN), loc/.(NN+1)) & local_overlapping(V,A,dy,denaming(V,A,val.len val).dy,loc/.len val) in dom p implies SC_Psuperpos_Seq(loc,val,p).1.(LocalOverlapSeq(A,loc,val,d1,size).(size-1)) = p.(LocalOverlapSeq(A,loc,val,d1,size).size); theorem :: NOMIN_8:19 for val being size-element FinSequence for p being SCPartialNominativePredicate of V,A holds 3 <= size & loc,val,size are_correct_wrt d1 & local_overlapping(V,A,LocalOverlapSeq(A,loc,val,d1,size).(size-1), denaming(V,A,val.len val).(LocalOverlapSeq(A,loc,val,d1,size).(size-1)), loc/.len val) in dom p & local_overlapping(V,A,d1,denaming(V,A,val.1).d1,loc/.1) in dom(SC_Psuperpos_Seq(loc,val,p).(size-1)) implies (SC_Psuperpos_Seq(loc,val,p).len SC_Psuperpos_Seq(loc,val,p)).d1 = SC_Psuperpos(SC_Psuperpos_Seq(loc,val,p).(size-2),denaming(V,A,val.2), loc/.2).(LocalOverlapSeq(A,loc,val,d1,size).1); definition let V,A,loc,d1,pos; let prg be FPrg(ND(V,A))-valued FinSequence such that len prg > 0; func PrgLocalOverlapSeq(A,loc,d1,prg,pos) -> FinSequence of ND(V,A) means :: NOMIN_8:def 14 len it = len prg & it.1 = local_overlapping(V,A,d1,(prg.1).d1,loc/.(pos.1)) & for n being Nat st 1 <= n < len it holds it.(n+1) = local_overlapping(V,A,it.n,prg.(n+1).(it.n),loc/.(pos.(n+1))); end; registration let V,A,loc,d1,prg,pos; cluster PrgLocalOverlapSeq(A,loc,d1,prg,pos) -> (V,A)-NonatomicND-yielding; end; registration let V,A,loc,d1,prg,pos,n; cluster PrgLocalOverlapSeq(A,loc,d1,prg,pos).n -> Function-like Relation-like; end; definition let V,A,loc,d1,prg,pos; pred prg_doms_of loc,d1,prg,pos means :: NOMIN_8:def 15 for n being Nat st 1 <= n < len prg holds PrgLocalOverlapSeq(A,loc,d1,prg,pos).n in dom(prg.(n+1)); end; theorem :: NOMIN_8:20 1 <= n <= len prg & PrgLocalOverlapSeq(A,loc,d1,prg,pos).m in dom(prg.n) implies prg.n.(PrgLocalOverlapSeq(A,loc,d1,prg,pos).m) is TypeSCNominativeData of V,A; theorem :: NOMIN_8:21 V is non empty & A is_without_nonatomicND_wrt V implies for n being Nat st 1 <= n & n < len prg & PrgLocalOverlapSeq(A,loc,d1,prg,pos).n in dom(prg.(n+1)) holds dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).(n+1)) = { loc/.(pos.(n+1)) } \/ dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).n); theorem :: NOMIN_8:22 V is non empty & A is_without_nonatomicND_wrt V implies for n being Nat st 1 <= n & n < len prg & PrgLocalOverlapSeq(A,loc,d1,prg,pos).n in dom(prg.(n+1)) holds dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).n) c= dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).(n+1)); theorem :: NOMIN_8:23 V is non empty & A is_without_nonatomicND_wrt V & dom PrgLocalOverlapSeq(A,loc,d1,prg,pos) c= dom prg & d1 in dom(prg.1) & prg_doms_of loc,d1,prg,pos implies for n being Nat st 1 <= n <= len prg holds dom(d1) c= dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).n); theorem :: NOMIN_8:24 V is non empty & A is_without_nonatomicND_wrt V & prg_doms_of loc,d1,prg,pos implies for m,n being Nat st 1 <= n <= m <= len prg holds dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).n) c= dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).m); theorem :: NOMIN_8:25 V is non empty & A is_without_nonatomicND_wrt V & dom PrgLocalOverlapSeq(A,loc,d1,prg,pos) c= dom prg & d1 in dom(prg.1) & prg_doms_of loc,d1,prg,pos implies for m,n being Nat st 1 <= n <= m <= len prg holds loc/.(pos.n) in dom(PrgLocalOverlapSeq(A,loc,d1,prg,pos).m);