:: General theory and tools for proving algorithms in nominative data systems
:: by Adrian Jaszczak
::
:: Received October 25, 2020
:: Copyright (c) 2020-2026 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;
definitions TARSKI, RELAT_1, NOMIN_7;
equalities NOMIN_1, PARTPR_2, NOMIN_2, NOMIN_5, NOMIN_6, NOMIN_7, FINSEQ_1;
expansions TARSKI, PARTFUN1, NOMIN_7;
theorems XBOOLE_0, NOMIN_1, NOMIN_2, NOMIN_3, NOMIN_4, FUNCT_1, PARTFUN1,
TARSKI, XBOOLE_1, INT_1, XREAL_1, XXREAL_0, FINSEQ_3, NAT_1, FINSEQ_1,
RELAT_1, NOMIN_7, CARD_1;
schemes PARTPR_2, RECDEF_1, NAT_1, FINSEQ_1;
begin
registration
let D be non empty set;
cluster non empty D-valued for FinSequence;
existence
proof
take <*the Element of D*>;
thus thesis;
end;
end;
registration
let D be non empty set, n be Nat;
cluster D-valued n-element for FinSequence;
existence
proof
set p = Seg n --> the Element of D;
dom p = Seg n;
then reconsider p as FinSequence by FINSEQ_1:def 2;
take p;
thus rng p c= D by RELAT_1:def 19;
Seg len p = dom p by FINSEQ_1:def 3;
hence thesis by CARD_1:def 7,FINSEQ_1:6;
end;
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
PP_composition(PP_composition(f1,f2,f3,f4,f5,f6),f7);
coherence;
end;
::$N Unconditional composition rule for 7 programs
theorem Th1:
<*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
proof
assume that
A1: <*p1,f1,p2*> is SFHT of D and
A2: <*p2,f2,p3*> is SFHT of D and
A3: <*p3,f3,p4*> is SFHT of D and
A4: <*p4,f4,p5*> is SFHT of D and
A5: <*p5,f5,p6*> is SFHT of D and
A6: <*p6,f6,p7*> is SFHT of D and
A7: <*p7,f7,p8*> is SFHT of D and
A8: <*PP_inversion(p2),f2,p3*> is SFHT of D and
A9: <*PP_inversion(p3),f3,p4*> is SFHT of D and
A10: <*PP_inversion(p4),f4,p5*> is SFHT of D and
A11: <*PP_inversion(p5),f5,p6*> is SFHT of D and
A12: <*PP_inversion(p6),f6,p7*> is SFHT of D and
A13: <*PP_inversion(p7),f7,p8*> is SFHT of D;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6),p7*>
is SFHT of D by A1,A2,A3,A4,A5,A6,A8,A9,A10,A11,A12,NOMIN_7:3;
hence thesis by A7,A13,NOMIN_3:25;
end;
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
PP_composition(PP_composition(f1,f2,f3,f4,f5,f6,f7),f8);
coherence;
end;
::$N Unconditional composition rule for 8 programs
theorem Th2:
<*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
proof
assume that
A1: <*p1,f1,p2*> is SFHT of D and
A2: <*p2,f2,p3*> is SFHT of D and
A3: <*p3,f3,p4*> is SFHT of D and
A4: <*p4,f4,p5*> is SFHT of D and
A5: <*p5,f5,p6*> is SFHT of D and
A6: <*p6,f6,p7*> is SFHT of D and
A7: <*p7,f7,p8*> is SFHT of D and
A8: <*p8,f8,p9*> is SFHT of D and
A9: <*PP_inversion(p2),f2,p3*> is SFHT of D and
A10: <*PP_inversion(p3),f3,p4*> is SFHT of D and
A11: <*PP_inversion(p4),f4,p5*> is SFHT of D and
A12: <*PP_inversion(p5),f5,p6*> is SFHT of D and
A13: <*PP_inversion(p6),f6,p7*> is SFHT of D and
A14: <*PP_inversion(p7),f7,p8*> is SFHT of D and
A15: <*PP_inversion(p8),f8,p9*> is SFHT of D;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7),p8*>
is SFHT of D by A1,A2,A3,A4,A5,A6,A7,A9,A10,A11,A12,A13,A14,Th1;
hence thesis by A8,A15,NOMIN_3:25;
end;
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
PP_composition(PP_composition(f1,f2,f3,f4,f5,f6,f7,f8),f9);
coherence;
end;
::$N Unconditional composition rule for 9 programs
theorem Th3:
<*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
proof
assume that
A1: <*p1,f1,p2*> is SFHT of D and
A2: <*p2,f2,p3*> is SFHT of D and
A3: <*p3,f3,p4*> is SFHT of D and
A4: <*p4,f4,p5*> is SFHT of D and
A5: <*p5,f5,p6*> is SFHT of D and
A6: <*p6,f6,p7*> is SFHT of D and
A7: <*p7,f7,p8*> is SFHT of D and
A8: <*p8,f8,p9*> is SFHT of D and
A9: <*p9,f9,p10*> is SFHT of D and
A10: <*PP_inversion(p2),f2,p3*> is SFHT of D and
A11: <*PP_inversion(p3),f3,p4*> is SFHT of D and
A12: <*PP_inversion(p4),f4,p5*> is SFHT of D and
A13: <*PP_inversion(p5),f5,p6*> is SFHT of D and
A14: <*PP_inversion(p6),f6,p7*> is SFHT of D and
A15: <*PP_inversion(p7),f7,p8*> is SFHT of D and
A16: <*PP_inversion(p8),f8,p9*> is SFHT of D and
A17: <*PP_inversion(p9),f9,p10*> is SFHT of D;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8),p9*>
is SFHT of D by A1,A2,A3,A4,A5,A6,A7,A10,A11,A12,A13,A14,A15,A8,A16,Th2;
hence thesis by A9,A17,NOMIN_3:25;
end;
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
PP_composition(PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9),f10);
coherence;
end;
::$N Unconditional composition rule for 10 programs
theorem
<*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
proof
assume that
A1: <*p1,f1,p2*> is SFHT of D and
A2: <*p2,f2,p3*> is SFHT of D and
A3: <*p3,f3,p4*> is SFHT of D and
A4: <*p4,f4,p5*> is SFHT of D and
A5: <*p5,f5,p6*> is SFHT of D and
A6: <*p6,f6,p7*> is SFHT of D and
A7: <*p7,f7,p8*> is SFHT of D and
A8: <*p8,f8,p9*> is SFHT of D and
A9: <*p9,f9,p10*> is SFHT of D and
A10: <*p10,f10,p11*> is SFHT of D and
A11: <*PP_inversion(p2),f2,p3*> is SFHT of D and
A12: <*PP_inversion(p3),f3,p4*> is SFHT of D and
A13: <*PP_inversion(p4),f4,p5*> is SFHT of D and
A14: <*PP_inversion(p5),f5,p6*> is SFHT of D and
A15: <*PP_inversion(p6),f6,p7*> is SFHT of D and
A16: <*PP_inversion(p7),f7,p8*> is SFHT of D and
A17: <*PP_inversion(p8),f8,p9*> is SFHT of D and
A18: <*PP_inversion(p9),f9,p10*> is SFHT of D and
A19: <*PP_inversion(p10),f10,p11*> is SFHT of D;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9),p10*> is SFHT of D
by A1,A2,A3,A4,A5,A6,A7,A11,A12,A13,A14,A15,A16,A8,A17,A9,A18,Th3;
hence thesis by A10,A19,NOMIN_3:25;
end;
theorem Th5:
<*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
proof
<*PP_inversion(q1),f2,p2*> is SFHT of D by NOMIN_3:19;
hence thesis by NOMIN_3:25;
end;
theorem Th6:
<*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
proof
assume that
A1: <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D and
A2: <*q2,f3,p2*> is SFHT of D;
A3: <*PP_inversion(q2),f3,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2),q2*> is SFHT of D by A1,Th5;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th7:
<*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
proof
assume that
A1: <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D &
<*q2,f3,q3*> is SFHT of D and
A2: <*q3,f4,p2*> is SFHT of D;
A3: <*PP_inversion(q3),f4,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2,f3),q3*> is SFHT of D by A1,Th6;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th8:
<*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
proof
assume that
A1: <*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 and
A2: <*q4,f5,p2*> is SFHT of D;
A3: <*PP_inversion(q4),f5,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2,f3,f4),q4*> is SFHT of D by A1,Th7;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th9:
<*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
proof
assume that
A1: <*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 and
A2: <*q5,f6,p2*> is SFHT of D;
A3: <*PP_inversion(q5),f6,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2,f3,f4,f5),q5*> is SFHT of D by A1,Th8;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th10:
<*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
proof
assume that
A1: <*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 and
A2: <*q6,f7,p2*> is SFHT of D;
A3: <*PP_inversion(q6),f7,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6),q6*> is SFHT of D by A1,Th9;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th11:
<*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
proof
assume that
A1: <*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 and
A2: <*q7,f8,p2*> is SFHT of D;
A3: <*PP_inversion(q7),f8,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7),q7*> is SFHT of D by A1,Th10;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th12:
<*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
proof
assume that
A1: <*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 and
A2: <*q8,f9,p2*> is SFHT of D;
A3: <*PP_inversion(q8),f9,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8),q8*> is SFHT of D by A1,Th11;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem
<*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
proof
assume that
A1: <*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 and
A2: <*q9,f10,p2*> is SFHT of D;
A3: <*PP_inversion(q9),f10,p2*> is SFHT of D by NOMIN_3:19;
<*p1,PP_composition(f1,f2,f3,f4,f5,f6,f7,f8,f9),q9*> is SFHT of D
by A1,Th12;
hence thesis by A2,A3,NOMIN_3:25;
end;
definition
let D,fD such that
A1: 0 < len fD;
reconsider X = fD.1 as Element of PFuncs(D,D) by PARTFUN1:45;
defpred P[Nat,object,object] means
ex g being PartFunc of D,D st g = $2 & $3 = PP_composition(g,fD.($1+1));
func PP_compositionSeq(fD) -> FinSequence of PFuncs(D,D) means :Def5:
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));
existence
proof
A2: for n st 1 <= n & n < len fD
for x being Element of PFuncs(D,D)
ex y being Element of PFuncs(D,D) st P[n,x,y]
proof
let n;
assume 1 <= n & n < len fD;
let x be Element of PFuncs(D,D);
reconsider g = x as PartFunc of D,D by PARTFUN1:46;
reconsider y = PP_composition(g,fD.(n+1)) as Element of PFuncs(D,D)
by PARTFUN1:45;
take y;
thus thesis;
end;
consider F being FinSequence of PFuncs(D,D) such that
A3: len F = len fD and
A4: (F.1 = X or len fD = 0) and
A5: for n st 1 <= n & n < len fD holds P[n,F.n,F.(n+1)]
from RECDEF_1:sch 4(A2);
take F;
thus len F = len fD by A3;
thus F.1 = fD.1 by A1,A4;
let n be Nat;
assume 1 <= n < len fD;
then P[n,F.n,F.(n+1)] by A5;
hence thesis;
end;
uniqueness
proof
let F1,F2 being FinSequence of PFuncs(D,D) such that
A6: len F1 = len fD and
A7: F1.1 = fD.1 and
A8: for n being Nat st 1 <= n < len fD holds
F1.(n+1) = PP_composition(F1.n,fD.(n+1)) and
A9: len F2 = len fD and
A10: F2.1 = fD.1 and
A11: for n being Nat st 1 <= n < len fD holds
F2.(n+1) = PP_composition(F2.n,fD.(n+1));
A12: for n st 1 <= n & n < len fD
for x,y1,y2 being Element of PFuncs(D,D) st P[n,x,y1] & P[n,x,y2]
holds y1 = y2;
A13: len F1 = len fD & (F1.1 = X or len fD = 0) &
for n st 1 <= n & n < len fD holds P[n,F1.n,F1.(n+1)]
proof
thus len F1 = len fD by A6;
thus (F1.1 = X or len fD = 0) by A7;
let n;
assume 1 <= n & n < len fD;
then F1.(n+1) =
PP_composition(F1.n,fD.(n+1)) by A8;
hence P[n,F1.n,F1.(n+1)];
end;
A14: len F2 = len fD & (F2.1 = X or len fD = 0) &
for n st 1 <= n & n < len fD holds P[n,F2.n,F2.(n+1)]
proof
thus len F2 = len fD by A9;
thus (F2.1 = X or len fD = 0) by A10;
let n;
assume 1 <= n & n < len fD;
then F2.(n+1) =
PP_composition(F2.n,fD.(n+1)) by A11;
hence P[n,F2.n,F2.(n+1)];
end;
thus F1 = F2 from RECDEF_1:sch 8(A12,A13,A14);
end;
end;
definition
let D,fD;
func PP_composition(fD) -> BinominativeFunction of D equals
PP_compositionSeq(fD).len PP_compositionSeq(fD);
coherence;
end;
definition
let D,fD,fB;
pred fD,fB are_composable means
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
fD,fB are_composable implies
<*fB.1,PP_composition(fD),fB.(len fB)*> is SFHT of D
proof
assume that
A1: 1 <= len fD and
A2: len fB = len fD + 1 and
A3: for n st 1 <= n <= len fD holds <*fB.n,fD.n,fB.(n+1)*> is SFHT of D and
A4: for n st 2 <= n <= len fD holds <*PP_inversion(fB.n),fD.n,fB.(n+1)*>
is SFHT of D;
set G = PP_compositionSeq(fD);
defpred P[Nat] means
1 <= $1 <= len fD implies <*fB.1,G.$1,fB.($1+1)*> is SFHT of D;
A5: P[0];
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume that
A7: P[k] and
A8: 1 <= k+1 and
A9: k+1 <= len fD;
per cases;
suppose
A10: k = 0;
G.1 = fD.1 by A1,Def5;
hence <*fB.1,G.(k+1),fB.(k+1+1)*> is SFHT of D by A1,A3,A10;
end;
suppose k > 0;
then
A11: 0+1 <= k by NAT_1:13;
A12: k < len fD by A9,NAT_1:13;
A13: k <= k+1 by NAT_1:11;
A14: <*fB.(k+1),fD.(k+1),fB.(k+1+1)*> is SFHT of D by A3,A8,A9;
<*PP_inversion(fB.(k+1)),fD.(k+1),fB.(k+1+1)*> is SFHT of D
by A4,A9,A11,XREAL_1:6;
then <*fB.1,PP_composition(G.k,fD.(k+1)),PP_or(fB.(k+1+1),fB.(k+1+1))*>
is SFHT of D by A7,A9,A11,A13,A14,XXREAL_0:2,NOMIN_3:24;
hence thesis by A11,A12,Def5;
end;
end;
A15: for k being Nat holds P[k] from NAT_1:sch 2(A5,A6);
len G = len fD by A1,Def5;
hence thesis by A1,A2,A15;
end;
definition
let V,A;
let val be FinSequence;
set size = len val;
set D = PFuncs(ND(V,A),ND(V,A));
defpred P[Nat,object] means $2 = denaming(V,A,val.$1);
func denamingSeq(V,A,val) -> FinSequence of PFuncs(ND(V,A),ND(V,A)) means
len it = len val &
for n being Nat st 1 <= n <= len it holds it.n = denaming(V,A,val.n);
existence
proof
A1: for n being Nat st n in Seg size ex x being Element of D st P[n,x]
proof
let n be Nat;
assume n in Seg size;
reconsider x = denaming(V,A,val.n) as Element of D by PARTFUN1:45;
take x;
thus thesis;
end;
consider p being FinSequence of D such that
A2: dom p = Seg size and
A3: for n being Nat st n in Seg size holds P[n,p.n] from FINSEQ_1:sch 5(A1);
take p;
thus len p = size by A2,FINSEQ_1:def 3;
thus thesis by A2,A3,FINSEQ_3:25;
end;
uniqueness
proof
let F1,F2 being FinSequence of D such that
A4: len F1 = size and
A5: for n being Nat st 1 <= n <= len F1 holds F1.n = denaming(V,A,val.n) and
A6: len F2 = size and
A7: for n being Nat st 1 <= n <= len F2 holds F2.n = denaming(V,A,val.n);
for n st 1 <= n <= size holds F1.n = F2.n
proof
let n be Nat;
assume
A8: 1 <= n <= size;
hence F1.n = denaming(V,A,val.n) by A4,A5
.= F2.n by A6,A7,A8;
end;
hence thesis by A4,A6,FINSEQ_1:def 18;
end;
end;
definition
let V,A,loc;
let val be FinSequence such that
A1: len val > 0;
let p be SCPartialNominativePredicate of V,A;
set D = PFuncs(ND(V,A),BOOLEAN);
set size = len val;
set X = SC_Psuperpos(p,denaming(V,A,val.len val),loc/.len val);
defpred P[Nat,object,object] means
ex f being SCPartialNominativePredicate of V,A st f = $2 &
$3 = SC_Psuperpos(f,denaming(V,A,val.(len val-$1)),loc/.(len val-$1));
func SC_Psuperpos_Seq(loc,val,p) -> FinSequence of PFuncs(ND(V,A),BOOLEAN)
means :Def9:
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));
existence
proof
A2: for n being Nat st 1 <= n & n < size
for x being Element of D
ex y being Element of D st P[n,x,y]
proof
let n be Nat;
assume 1 <= n & n < size;
let x be Element of D;
reconsider f = x as SCPartialNominativePredicate of V,A by PARTFUN1:47;
set y = SC_Psuperpos(f,denaming(V,A,val.(len val-n)),loc/.(len val-n));
reconsider y as Element of D by PARTFUN1:45;
take y;
thus P[n,x,y];
end;
reconsider X as Element of D by PARTFUN1:45;
consider F being FinSequence of D such that
A3: len F = size & (F.1 = X or size = 0) and
A4: for n st 1 <= n & n < size holds P[n,F.n,F.(n+1)]
from RECDEF_1:sch 4(A2);
take F;
thus len F = len val &
F.1 = SC_Psuperpos(p,denaming(V,A,val.len val),loc/.len val) by A1,A3;
let n be Nat;
assume 1 <= n < len F;
then P[n,F.n,F.(n+1)] by A3,A4;
hence thesis;
end;
uniqueness
proof
let F1,F2 being FinSequence of D such that
A5: len F1 = size and
A6: F1.1 = X and
A7: for n being Nat st 1 <= n < len F1 holds F1.(n+1) =
SC_Psuperpos(F1.n,denaming(V,A,val.(len val-n)),loc/.(len val-n)) and
A8: len F2 = size and
A9: F2.1 = X and
A10: for n being Nat st 1 <= n < len F2 holds F2.(n+1) =
SC_Psuperpos(F2.n,denaming(V,A,val.(len val-n)),loc/.(len val-n));
reconsider X as Element of D by PARTFUN1:45;
A11: for n st 1 <= n & n < size
for x,y1,y2 being Element of D st
P[n,x,y1] & P[n,x,y2] holds y1 = y2;
A12: len F1 = size & (F1.1 = X or size = 0) &
for n st 1 <= n & n < size holds P[n,F1.n,F1.(n+1)]
proof
thus len F1 = size by A5;
thus F1.1 = X or size = 0 by A6;
let n;
assume 1 <= n & n < size;
then F1.(n+1) =
SC_Psuperpos(F1.n,denaming(V,A,val.(len val-n)),loc/.(len val-n))
by A5,A7;
hence P[n,F1.n,F1.(n+1)];
end;
A13: len F2 = size & (F2.1 = X or size = 0) &
for n st 1 <= n & n < size holds P[n,F2.n,F2.(n+1)]
proof
thus len F2 = size by A8;
thus F2.1 = X or size = 0 by A9;
let n;
assume 1 <= n & n < size;
then F2.(n+1) =
SC_Psuperpos(F2.n,denaming(V,A,val.(len val-n)),loc/.(len val-n))
by A8,A10;
hence P[n,F2.n,F2.(n+1)];
end;
thus F1 = F2 from RECDEF_1:sch 8(A11,A12,A13);
end;
end;
theorem Th15:
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)
proof
let size be non zero Nat;
let val be size-element FinSequence;
set F = LocalOverlapSeq(A,loc,val,d1,size);
set v = val.m;
assume that
A1: loc,val,size are_correct_wrt d1 and
A2: 1 <= n & n <= len F;
A3: len F = size by NOMIN_7:def 4;
A4: dom denaming(V,A,v) = {d where d is NonatomicND of V,A: v in dom d}
by NOMIN_1:def 18;
A5: F.n is NonatomicND of V,A by A2,NOMIN_7:def 6;
assume 1 <= m <= len F;
then v in dom(F.n) by A1,A2,A3,NOMIN_7:10;
hence thesis by A4,A5;
end;
definition
let V,A,inp,d;
let val be FinSequence;
pred inp is_valid_input V,A,val,d means
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;
defpred P[object] means inp is_valid_input V,A,val,$1;
func valid_input(V,A,val,inp) -> SCPartialNominativePredicate of V,A
means :Def11:
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);
existence
proof
A1: ND(V,A) c= ND(V,A);
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))
from PARTPR_2:sch 1(A1);
take p;
thus thesis by A2;
end;
uniqueness
proof
for p,q being SCPartialNominativePredicate of V,A st
(dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))) &
(dom q = ND(V,A) & (for d being object st d in dom q holds
(P[d] implies q.d = TRUE) & (not P[d] implies q.d = FALSE)))
holds p = q from PARTPR_2:sch 2;
hence thesis;
end;
end;
registration
let V,A,inp;
let val be FinSequence;
cluster valid_input(V,A,val,inp) -> total;
coherence by Def11;
end;
definition
let V,A,d;
let Z,res be FinSequence;
pred res is_valid_output V,A,Z,d means
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;
set D = {d where d is TypeSCNominativeData of V,A: d in dom denaming(V,A,Z)};
defpred P[object] means <*res*> is_valid_output V,A,<*Z*>,$1;
func valid_output(V,A,Z,res) -> SCPartialNominativePredicate of V,A
means
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);
existence
proof
A1: D c= ND(V,A)
proof
let v;
assume v in D;
then ex d being TypeSCNominativeData of V,A st v = d &
d in dom denaming(V,A,Z);
hence thesis;
end;
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = D & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))
from PARTPR_2:sch 1(A1);
take p;
thus thesis by A2;
end;
uniqueness
proof
for p,q being SCPartialNominativePredicate of V,A st
(dom p = D & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))) &
(dom q = D & (for d being object st d in dom q holds
(P[d] implies q.d = TRUE) & (not P[d] implies q.d = FALSE)))
holds p = q from PARTPR_2:sch 2;
hence thesis;
end;
end;
theorem Th16:
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)
proof
let val be size-element FinSequence;
set D = denaming(V,A,val.len val);
set S = SC_Psuperpos_Seq(loc,val,p);
set L = LocalOverlapSeq(A,loc,val,d1,size);
deffunc F(Nat) = local_overlapping(V,A,L.(size-$1-1),
denaming(V,A,val.(len val-$1)).(L.(size-$1-1)),loc/.(len val-$1));
assume that
A1: loc,val,size are_correct_wrt d1 and
A2: d = LocalOverlapSeq(A,loc,val,d1,size).(size-1) and
A3: 2 <= n+1 and
A4: n+1 < size and
A5: local_overlapping(V,A,d,D.d,loc/.len val) in dom p;
A6: len val = size by CARD_1:def 7;
A7: len L = size by NOMIN_7:def 4;
A8: len S = len val by Def9;
defpred P[Nat] means 2 <= $1+1 < size implies F($1) in dom(S.$1);
A9: P[0];
A10: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A11: P[k] and
2 <= k+1+1 and
A12: k+1+1 < size;
A13: 2 <= k+2 by NAT_1:11;
then
A14: 2 < size by A12,XXREAL_0:2;
per cases;
suppose
A15: k = 0;
S.1 = SC_Psuperpos(p,D,loc/.len val) by Def9;
then
A16: dom(S.1) = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,D.d,loc/.len val) in dom p & d in dom D}
by NOMIN_2:def 11;
A17: dom D = {d where d is NonatomicND of V,A: val.len val in dom d}
by NOMIN_1:def 18;
reconsider N = size-2 as Element of NAT by A13,A12,XXREAL_0:2,INT_1:5;
2-2 < size-2 by A14,XREAL_1:14;
then
A18: 0+1 <= N by NAT_1:13;
A19: N < len L by A7,XREAL_1:44; then
A20: L.(N+1) =
local_overlapping(V,A,L.N,denaming(V,A,val.(N+1)).(L.N),loc/.(N+1))
by A18,NOMIN_7:def 4;
A21: 1 <= len val by A6,A7,A18,A19,XXREAL_0:2;
A22: 1 <= N+1 by NAT_1:11;
A23: N+1 <= size by XREAL_1:44,NAT_1:13;
reconsider F1 = F(1) as NonatomicND of V,A
by A6,A7,A20,A23,NAT_1:11,NOMIN_7:def 6;
val.len val in dom(F1) by A1,A6,A21,A20,A22,A23,NOMIN_7:10;
then F(1) in dom D by A17;
hence F(k+1) in dom(S.(k+1)) by A15,A16,A5,A2,A6,A20;
end;
suppose
A24: k > 0;
then 0+1 <= k by NAT_1:13;
then
A25: 1+1 <= k+1 by XREAL_1:7;
A26: k+1 < size by A12,NAT_1:13;
set D = denaming(V,A,val.(len val-k));
A27: 0+1 <= k by A24,NAT_1:13;
k < k+2 by XREAL_1:29;
then k < size by A12,XXREAL_0:2; then
S.(k+1) = SC_Psuperpos(S.k,D,loc/.(len val-k)) by A6,A8,A27,Def9;
then
A28: dom(S.(k+1)) = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,D.d,loc/.(len val-k)) in dom(S.k) &
d in dom(D)} by NOMIN_2:def 11;
A29: dom(D) = {d where d is NonatomicND of V,A: val.(len val-k) in dom d}
by NOMIN_1:def 18;
A30: size-(k+1) < size by XREAL_1:44;
A31: k+1-k < size-k by A26,XREAL_1:9;
then
A32: 1-1 < size-k-1 by XREAL_1:9;
then
A33: 0+1 <= size-k-1 by INT_1:7;
reconsider s = size-k-1 as Element of NAT by A32,INT_1:3;
reconsider N = s-1 as Element of NAT by A33,INT_1:5;
k+1+1-k < size-k by A12,XREAL_1:9;
then 1+1-1 < size-k-1 by XREAL_1:9;
then 1-1 < N by XREAL_1:9;
then
A34: 0+1 <= N by INT_1:7;
N < s by XREAL_1:44;
then N < len L by A7,A30,XXREAL_0:2; then
A35: L.s =
local_overlapping(V,A,L.N,denaming(V,A,val.(N+1)).(L.N),loc/.(N+1))
by A34,NOMIN_7:def 4;
reconsider Fk1 = F(k+1) as NonatomicND of V,A
by A6,A7,A35,A30,A33,NOMIN_7:def 6;
reconsider M = size-k as Element of NAT by A31,INT_1:3;
M <= size by XREAL_1:43;
then val.(len val-k) in dom(Fk1) by A1,A6,A35,A30,A33,A31,NOMIN_7:10;
then F(k+1) in dom(D) by A29;
hence F(k+1) in dom(S.(k+1)) by A6,A11,A25,A28,A35,A12,NAT_1:13;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A9,A10);
hence thesis by A3,A4;
end;
theorem Th17:
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))
proof
let val be size-element FinSequence such that
A1: loc,val,size are_correct_wrt d1 and
A2: d = LocalOverlapSeq(A,loc,val,d1,size).(size-1) and
A3: local_overlapping(V,A,d,denaming(V,A,val.len val).d,loc/.len val) in dom p;
let m,n be Nat such that
A4: 1 <= m and
A5: m < size and
A6: 1 <= n and
A7: n < size;
set S = SC_Psuperpos_Seq(loc,val,p);
set L = LocalOverlapSeq(A,loc,val,d1,size);
defpred P[Nat] means
1 <= $1 < size implies S.m.(L.(size-m)) = S.$1.(L.(size-$1));
A8: P[0];
A9: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A10: P[k] and
1 <= k+1 and
A11: k+1 < size;
set D = denaming(V,A,val.(len val-k));
A12: len val = size by CARD_1:def 7;
A13: len S = len val by Def9;
A14: len L = size by NOMIN_7:def 4;
A15: k < size by A11,NAT_1:13;
per cases;
suppose
A16: k = 0;
defpred R[Nat] means
1 <= $1 < size implies S.$1.(L.(size-$1)) = S.1.(L.(size-1));
A17: R[0];
A18: for x being Nat st R[x] holds R[x+1]
proof
let x be Nat such that
A19: R[x] and
1 <= x+1 and
A20: x+1 < size;
per cases;
suppose x = 0;
hence thesis;
end;
suppose x > 0;
then
A21: 0+1 <= x by NAT_1:13;
set DD = denaming(V,A,val.(len val-x));
A22: x <= x+1 by NAT_1:11;
then x < len S by A13,A12,A20,XXREAL_0:2;
then
A23: S.(x+1) = SC_Psuperpos(S.x,DD,loc/.(len val-x)) by A21,Def9;
reconsider u = size-x-1 as Element of NAT
by A20,XREAL_1:19,INT_1:5;
x+1-x < size-x by A20,XREAL_1:9;
then 1-1 < size-x-1 by XREAL_1:9;
then
A24: 0+1 <= size-(x+1) by INT_1:7;
A25: size-(x+1) < size by XREAL_1:44;
then reconsider dd = L.u as NonatomicND of V,A
by A14,A24,NOMIN_7:def 6;
A26: dom(SC_Psuperpos(S.x,DD,loc/.(len val-x))) =
{d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,DD.d,loc/.(len val-x)) in dom(S.x) &
d in dom DD} by NOMIN_2:def 11;
1+1 <= x+1 by A21,XREAL_1:6;
then
A27: local_overlapping(V,A,dd,DD.dd,loc/.(len val-x)) in dom(S.x)
by A1,A2,A3,A20,Th16;
A28: dom DD = {d where d is NonatomicND of V,A:val.(len val-x) in dom d}
by NOMIN_1:def 18;
A29: 1 <= u+1 by NAT_1:11;
u+1 <= size by A25,INT_1:7;
then val.(u+1) in dom(L.u) by A1,A24,A25,A29,NOMIN_7:10;
then dd in dom DD by A12,A28;
then
A30: dd in dom(SC_Psuperpos(S.x,DD,loc/.(len val-x))) by A26,A27;
L.(u+1) =
local_overlapping(V,A,L.u,denaming(V,A,val.(u+1)).(L.u),loc/.(u+1))
by A14,A24,A25,NOMIN_7:def 4;
hence thesis by A22,A23,A30,A12,A19,A21,A20,XXREAL_0:2,NOMIN_2:35;
end;
end;
for x being Nat holds R[x] from NAT_1:sch 2(A17,A18);
hence S.m.(L.(size-m)) = S.(k+1).(L.(size-(k+1))) by A4,A5,A16;
end;
suppose k > 0;
then
A31: 0+1 <= k by NAT_1:13;
then
A32: S.(k+1) = SC_Psuperpos(S.k,D,loc/.(size-k)) by A12,A13,A15,Def9;
set D1 = L.(size-(k+1));
A33: k+1-k < size-k by A11,XREAL_1:9;
then reconsider w = size-k-1 as Element of NAT by INT_1:5;
1-1 < w by A33,XREAL_1:9;
then
A34: 0+1 <= w by NAT_1:13;
A35: size-(k+1) < size by XREAL_1:44;
then
A36: L.(w+1) =
local_overlapping(V,A,L.w,denaming(V,A,val.(w+1)).(L.w),loc/.(w+1))
by A14,A34,NOMIN_7:def 4;
reconsider D1 as NonatomicND of V,A by A14,A34,A35,NOMIN_7:def 6;
A37: dom(SC_Psuperpos(S.k,D,loc/.(len val-k))) =
{d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,D.d,loc/.(len val-k)) in dom(S.k) & d in dom D}
by NOMIN_2:def 11;
A38: D1 = L.(size-k-1);
1+1 <= k+1 by A31,XREAL_1:6; then
A39: local_overlapping(V,A,D1,D.D1,loc/.(len val-k)) in dom(S.k)
by A1,A11,A2,A3,A38,Th16;
A40: dom D = {d where d is NonatomicND of V,A: val.(len val-k) in dom d}
by NOMIN_1:def 18;
A41: 1 <= w+1 by NAT_1:11;
w+1 <= size by A35,INT_1:7;
then val.(w+1) in dom(L.w) by A1,A34,A35,A41,NOMIN_7:10;
then D1 in dom D by A12,A40;
then D1 in dom(SC_Psuperpos(S.k,D,loc/.(len val-k))) by A37,A39;
hence thesis by A10,A31,A32,A12,A36,A11,NAT_1:13,NOMIN_2:35;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A8,A9);
hence thesis by A6,A7;
end;
theorem
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)
proof
let val be size-element FinSequence;
let dx,dy be object;
let NN be Nat such that
A1: NN = size-2;
set S = SC_Psuperpos_Seq(loc,val,p);
set L = LocalOverlapSeq(A,loc,val,d1,size);
set D = denaming(V,A,val.len val);
assume that
A2: loc,val,size are_correct_wrt d1 and
A3: dx = LocalOverlapSeq(A,loc,val,d1,size).(size-1) and
A4: local_overlapping(V,A,dx,D.dx,loc/.len val) in dom p and
A5: dy = local_overlapping(V,A,L.NN,denaming(V,A,val.(NN+1)).(L.NN),
loc/.(NN+1)) and
A6: local_overlapping(V,A,dy,D.dy,loc/.len val) in dom p;
A7: 0+2 <= size-2+2 by A1,XREAL_1:6;
then
A8: 1 <= size by XXREAL_0:2;
reconsider N = size-1 as Element of NAT by A7,XXREAL_0:2,INT_1:5;
A9: len L = size by NOMIN_7:def 4;
A10: len val = size by CARD_1:def 7;
A11: S.1 = SC_Psuperpos(p,D,loc/.len val) by Def9;
A12: dom(SC_Psuperpos(p,D,loc/.len val)) =
{d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,D.d,loc/.len val) in dom p & d in dom D}
by NOMIN_2:def 11;
A13: 2-1 <= N by A7,XREAL_1:9;
then per cases by XXREAL_0:1;
suppose
A14: N = 1;
set D1 = denaming(V,A,val.1);
A15: L.1 = local_overlapping(V,A,d1,D1.d1,loc/.1) by NOMIN_7:def 4;
A16: L.(N+1) =
local_overlapping(V,A,L.N,denaming(V,A,val.(N+1)).(L.N),loc/.(N+1))
by A9,A14,NOMIN_7:def 4;
set dd = local_overlapping(V,A,d1,D1.d1,loc/.1);
dd in dom D by A2,A9,A10,A8,A15,Th15;
then dd in dom(SC_Psuperpos(p,D,loc/.len val)) by A12,A3,A4,A14,A15;
hence S.1.(L.(size-1)) = p.(L.size) by A14,A10,A15,A16,A11,NOMIN_2:35;
end;
suppose
A17: 1 < N;
then reconsider NN = N-1 as Element of NAT by INT_1:5;
1-1 < N-1 by A17,XREAL_1:9;
then
A18: 0+1 <= NN by INT_1:7;
A19: N-1 < N by XREAL_1:44;
A20: N < len L by A9,XREAL_1:44;
then NN < len L by A19,XXREAL_0:2;
then
A21: L.(NN+1) =
local_overlapping(V,A,L.NN,denaming(V,A,val.(NN+1)).(L.NN),loc/.(NN+1))
by A18,NOMIN_7:def 4;
A22: L.(N+1) =
local_overlapping(V,A,L.N,denaming(V,A,val.(N+1)).(L.N),loc/.(N+1))
by A17,A20,NOMIN_7:def 4;
set Dn = denaming(V,A,val.(NN+1));
set dd = local_overlapping(V,A,L.NN,Dn.(L.NN),loc/.(NN+1));
dd in dom D by A2,A9,A10,A8,A21,A13,A20,Th15;
then dd in dom(SC_Psuperpos(p,D,loc/.len val)) by A1,A5,A6,A12;
hence S.1.(L.(size-1)) = p.(L.size) by A10,A22,A11,A21,NOMIN_2:35;
end;
end;
theorem
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)
proof
let val be size-element FinSequence;
let p be SCPartialNominativePredicate of V,A;
set SE = SC_Psuperpos_Seq(loc,val,p);
set F = LocalOverlapSeq(A,loc,val,d1,size);
set dd = F.(size-1);
set D1 = denaming(V,A,val.1);
set D2 = denaming(V,A,val.2);
set P = SE.(size-2);
assume that
A1: 3 <= size and
A2: loc,val,size are_correct_wrt d1 and
A3: local_overlapping(V,A,dd,denaming(V,A,val.len val).dd,loc/.len val)
in dom p and
A4: local_overlapping(V,A,d1,D1.d1,loc/.1) in dom(SE.(size-1));
A5: len val = size by CARD_1:def 7;
A6: len SE = len val by Def9;
A7: len F = size by NOMIN_7:def 4;
A8: 2 < size by A1,XXREAL_0:2;
reconsider nn = size-2 as Element of NAT by A1,XXREAL_0:2,INT_1:5;
set N = nn+1;
A9: 3-2 <= nn by A1,XREAL_1:9;
then
A10: 1+1 <= nn+1 by XREAL_1:6;
A12: size-1 < size by XREAL_1:44;
A13: nn < size by XREAL_1:44;
A15: len val-N = 1 by A5;
A16: F.1 = local_overlapping(V,A,d1,D1.d1,loc/.1) by NOMIN_7:def 4;
A11: 1 <= N by A9,XREAL_1:29; then
A14: 1 < len F by A7,A12,XXREAL_0:2; then
A17: F.1 is NonatomicND of V,A by NOMIN_7:def 6;
A18: SE.(N+1) = SC_Psuperpos(SE.N,D1,loc/.1) by A6,A11,A12,A15,Def9;
A19: F.(1+1) =
local_overlapping(V,A,F.1,denaming(V,A,val.(1+1)).(F.1),loc/.(1+1))
by A14,NOMIN_7:def 4;
A20: dom SC_Psuperpos(P,D2,loc/.2) =
{d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,D2.d,loc/.2) in dom P & d in dom D2}
by NOMIN_2:def 11;
A21: local_overlapping(V,A,F.(size-nn-1),denaming(V,A,val.(len val-nn)).
(F.(size-nn-1)),loc/.(len val-nn)) in dom(P) by A2,A10,A3,XREAL_1:44,Th16;
A22: dom D2 = {d where d is NonatomicND of V,A: val.2 in dom d}
by NOMIN_1:def 18;
val.2 in dom(F.1) by A7,A2,A8,A14,NOMIN_7:10;
then F.1 in dom D2 by A17,A22;
then
A23: F.1 in dom(SC_Psuperpos(P,D2,loc/.2)) by A5,A17,A20,A21;
A24: dom SC_Psuperpos(SE.N,D1,loc/.1) =
{d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,D1.d,loc/.1) in dom(SE.N) & d in dom D1}
by NOMIN_2:def 11;
A25: dom D1 = {d where d is NonatomicND of V,A: val.1 in dom d}
by NOMIN_1:def 18;
A26: val is_valid_wrt d1 by A2;
1 in dom val by A5,A7,A14,FINSEQ_3:25;
then val.1 in rng val by FUNCT_1:def 3;
then d1 in dom D1 by A25,A26;
then d1 in dom(SC_Psuperpos(SE.N,D1,loc/.1)) by A24,A4;
hence (SE.len SE).d1 = SE.N.(F.(size-N)) by A5,A6,A18,A16,NOMIN_2:35
.= SE.nn.(F.(size-nn)) by A2,A3,A11,A12,A9,A13,Th17
.= SC_Psuperpos(P,D2,loc/.2).(F.1) by A17,A23,A19,NOMIN_2:35;
end;
definition
let V,A,loc,d1,pos;
let prg be FPrg(ND(V,A))-valued FinSequence such that
A1: len prg > 0;
defpred P[Nat,object,object] means
$3 = local_overlapping(V,A,$2,prg.($1+1).($2),loc/.(pos.($1+1)));
set X = local_overlapping(V,A,d1,(prg.1).d1,loc/.(pos.1));
func PrgLocalOverlapSeq(A,loc,d1,prg,pos) -> FinSequence of ND(V,A) means
:Def14:
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)));
existence
proof
A2: for n being Nat st 1 <= n < len prg
for x being Element of ND(V,A)
ex y being Element of ND(V,A) st P[n,x,y]
proof
let n be Nat;
assume 1 <= n & n < len prg;
let x be Element of ND(V,A);
set y = local_overlapping(V,A,x,prg.(n+1).x,loc/.(pos.(n+1)));
y in ND(V,A);
then reconsider y as Element of ND(V,A);
take y;
thus P[n,x,y];
end;
X in ND(V,A);
then reconsider X as Element of ND(V,A);
ex p being FinSequence of ND(V,A) st len p = len prg &
(p.1 = X or len prg = 0) &
for n st 1 <= n & n < len prg holds P[n,p.n,p.(n+1)]
from RECDEF_1:sch 4(A2);
hence thesis by A1;
end;
uniqueness
proof
set size = len prg;
let F,G be FinSequence of ND(V,A) such that
A3: len F = size and
A4: F.1 = X and
A5: for n being Nat st 1 <= n < len F holds
F.(n+1) =
local_overlapping(V,A,F.n,prg.(n+1).(F.n),loc/.(pos.(n+1))) and
A6: len G = size and
A7: G.1 = X and
A8: for n being Nat st 1 <= n < len G holds
G.(n+1) =
local_overlapping(V,A,G.n,prg.(n+1).(G.n),loc/.(pos.(n+1)));
A9: for n st 1 <= n & n < size for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2]
holds y1 = y2;
A10: len F = size & (F.1 = X or size = 0) & for n st 1 <= n & n < size
holds P[n,F.n,F.(n+1)] by A3,A4,A5;
A11: len G = size & (G.1 = X or size = 0) &
for n st 1 <= n & n < size holds P[n,G.n,G.(n+1)] by A6,A7,A8;
thus thesis from RECDEF_1:sch 7(A9,A10,A11);
end;
end;
registration
let V,A,loc,d1,prg,pos;
cluster PrgLocalOverlapSeq(A,loc,d1,prg,pos) -> (V,A)-NonatomicND-yielding;
coherence
proof
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
A1: len prg > 0;
let n such that
A2: 1 <= n <= len F;
set X = local_overlapping(V,A,d1,(prg.1).d1,loc/.(pos.1));
defpred P[Nat] means
1 <= $1 & $1 <= len F implies F.$1 is NonatomicND of V,A;
A3: P[0];
A4: for n st P[n] holds P[n+1]
proof
let n;
assume that
A5: P[n] and
1 <= n+1 and
A6: n+1 <= len F;
per cases;
suppose
A7: n = 0;
F.1 = X by A1,Def14;
hence F.(n+1) is NonatomicND of V,A by A7,NOMIN_2:9;
end;
suppose 0 < n;
then
A8: 0+1 <= n by NAT_1:13;
A9: n+0 < n+1 by XREAL_1:8;
then n < len F by A6,XXREAL_0:2;
then F.(n+1) =
local_overlapping(V,A,F.n,prg.(n+1).(F.n),loc/.(pos.(n+1)))
by A1,A8,Def14;
hence thesis by A5,A6,A8,A9,NOMIN_2:9,XXREAL_0:2;
end;
end;
for n holds P[n] from NAT_1:sch 2(A3,A4);
hence thesis by A2;
end;
end;
registration
let V,A,loc,d1,prg,pos,n;
cluster
PrgLocalOverlapSeq(A,loc,d1,prg,pos).n -> Function-like Relation-like;
coherence
proof
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
per cases;
suppose n in dom F;
then 1 <= n <= len F by FINSEQ_3:25;
hence thesis by NOMIN_7:def 6;
end;
suppose not n in dom F;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
definition
let V,A,loc,d1,prg,pos;
pred prg_doms_of loc,d1,prg,pos means
for n being Nat st 1 <= n < len prg holds
PrgLocalOverlapSeq(A,loc,d1,prg,pos).n in dom(prg.(n+1));
end;
theorem Th20:
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
proof
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
set P = prg.n;
assume that
A1: 1 <= n and
A2: n <= len prg and
A3: F.m in dom(P);
n in dom prg by A1,A2,FINSEQ_3:25;
then P in rng prg by FUNCT_1:def 3;
then
A4: rng(P) c= ND(V,A) by RELAT_1:def 19;
P.(F.m) in rng P by A3,FUNCT_1:def 3;
hence thesis by A4,NOMIN_1:39;
end;
theorem Th21:
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)
proof
set size = len prg;
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
assume that
A1: V is non empty and
A2: A is_without_nonatomicND_wrt V;
let n be Nat;
assume that
A3: 1 <= n and
A4: n < size and
A5: F.n in dom(prg.(n+1));
A6: len F = size by Def14;
reconsider Fn = F.n as NonatomicND of V,A by A3,A4,A6,NOMIN_7:def 6;
set v = loc/.(pos.(n+1));
set d2 = prg.(n+1).(F.n);
n+1 <= size by A4,NAT_1:13;
then d2 is TypeSCNominativeData of V,A by A5,NAT_1:11,Th20;
then dom local_overlapping(V,A,Fn,d2,v) = {v} \/ dom Fn
by A1,A2,NOMIN_4:4;
hence thesis by A3,A4,A6,Def14;
end;
theorem Th22:
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))
proof
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
assume
A1: V is non empty & A is_without_nonatomicND_wrt V;
let n be Nat;
assume 1 <= n & n < len prg & F.n in dom(prg.(n+1));
then dom(F.(n+1)) = { loc/.(pos.(n+1)) } \/ dom(F.n) by A1,Th21;
hence thesis by XBOOLE_1:7;
end;
theorem
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)
proof
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
assume that
A1: V is non empty and
A2: A is_without_nonatomicND_wrt V and
A3: dom F c= dom prg and
A4: d1 in dom(prg.1) and
A5: prg_doms_of loc,d1,prg,pos;
let n be Nat;
assume that
A6: 1 <= n and
A7: n <= len prg;
defpred P[Nat] means 1 <= $1 <= len prg implies dom(d1) c= dom(F.$1);
A8: P[0];
A9: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A10: P[k] and
A11: 1 <= k+1 and
A12: k+1 <= len prg;
A13: len F = len prg by Def14;
per cases;
suppose
A14: k = 0;
set v = loc/.(pos.1);
set D = prg.1;
1 <= len F by A11,A12,A13,XXREAL_0:2;
then 1 in dom F by FINSEQ_3:25;
then D in rng prg by A3,FUNCT_1:def 3;
then
reconsider d2 = D.d1 as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39,A4;
A15: F.1 = local_overlapping(V,A,d1,d2,v) by A7,Def14;
dom local_overlapping(V,A,d1,d2,v) = {v} \/ dom d1 by A1,A2,NOMIN_4:4;
hence thesis by A14,A15,XBOOLE_1:7;
end;
suppose k > 0;
then
A16: 0+1 <= k by NAT_1:13;
A17: k <= k+1 by NAT_1:12;
k+0 < k+1 by XREAL_1:8;
then
A18: k < len prg by A12,XXREAL_0:2;
then F.k in dom(prg.(k+1)) by A5,A16;
then dom(F.k) c= dom(F.(k+1)) by A1,A2,A16,A18,Th22;
hence thesis by A17,A10,A12,A16,XXREAL_0:2;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A8,A9);
hence thesis by A6,A7;
end;
theorem Th24:
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)
proof
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
assume that
A1: V is non empty & A is_without_nonatomicND_wrt V and
A2: prg_doms_of loc,d1,prg,pos;
let m,n be Nat;
assume that
A3: 1 <= n and
A4: n <= m and
A5: m <= len prg;
per cases by A4,XXREAL_0:1;
suppose n = m;
hence thesis;
end;
suppose
A6: n < m;
defpred P[Nat] means n < $1 <= len prg implies dom(F.n) c= dom(F.$1);
A7: P[0];
A8: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A9: P[k] and
A10: n < k+1 and
A11: k+1 <= len prg;
A12: n <= k by A10,NAT_1:13;
then
A13: 1 <= k by A3,XXREAL_0:2;
k+0 < k+1 by XREAL_1:8;
then
A14: k < len prg by A11,XXREAL_0:2;
then F.k in dom(prg.(k+1)) by A2,A13;
then dom(F.(k)) c= dom(F.(k+1)) by A1,A13,A14,Th22;
hence dom(F.n) c= dom(F.(k+1)) by A9,A12,A11,NAT_1:13,XXREAL_0:1;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A7,A8);
hence thesis by A5,A6;
end;
end;
theorem
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)
proof
set size = len prg;
set F = PrgLocalOverlapSeq(A,loc,d1,prg,pos);
assume that
A1: V is non empty and
A2: A is_without_nonatomicND_wrt V and
A3: dom F c= dom prg and
A4: d1 in dom(prg.1) and
A5: prg_doms_of loc,d1,prg,pos;
let m,n be Nat such that
A6: 1 <= n and
A7: n <= m and
A8: m <= size;
A9: 1 <= m by A6,A7,XXREAL_0:2;
A10: n <= size by A7,A8,XXREAL_0:2;
A11: len F = size by Def14;
reconsider i1 = n-1 as Element of NAT by A6,INT_1:5;
set v = loc/.(pos.n);
set D = prg.n;
A12: v in {v} by TARSKI:def 1;
n in dom F by A6,A10,A11,FINSEQ_3:25;
then
A13: D in rng prg by A3,FUNCT_1:def 3;
per cases;
suppose
A14: i1 = 0;
then reconsider d2 = D.d1 as TypeSCNominativeData of V,A
by A4,A13,PARTFUN1:4,NOMIN_1:39;
A15: F.1 = local_overlapping(V,A,d1,d2,v) by A8,A14,Def14;
A16: dom local_overlapping(V,A,d1,d2,v) = {v} \/ dom(d1) by A1,A2,NOMIN_4:4;
A17: dom(F.1) c= dom(F.m) by A1,A5,A2,A8,A9,Th24;
v in {v} \/ dom(d1) by A12,XBOOLE_0:def 3;
hence v in dom(F.m) by A15,A16,A17;
end;
suppose i1 > 0;
then
A18: 0+1 <= i1 by NAT_1:13;
n-1 < n-0 by XREAL_1:15;
then
A19: i1 < size by A10,XXREAL_0:2;
then reconsider dd = F.i1 as NonatomicND of V,A by A18,A11,NOMIN_7:def 6;
dd in dom(prg.(i1+1)) by A5,A18,A19;
then reconsider d2 = D.dd as TypeSCNominativeData of V,A
by PARTFUN1:4,NOMIN_1:39,A13;
A20: F.n = local_overlapping(V,A,dd,d2,loc/.(pos.(i1+1)))
by A11,A18,A19,Def14;
A21: dom local_overlapping(V,A,dd,d2,v) = {v} \/ dom(dd) by A1,A2,NOMIN_4:4;
A22: v in {v} \/ dom(dd) by A12,XBOOLE_0:def 3;
dom(F.n) c= dom(F.m) by A1,A5,A2,A6,A7,A8,Th24;
hence v in dom(F.m) by A22,A20,A21;
end;
end;