:: by Adrian Jaszczak

::

:: Received October 25, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

registration

let D be non empty set ;

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is D -valued )

end;
cluster non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like for set ;

existence ex b

( not b

proof end;

registration

let D be non empty set ;

let n be Nat;

ex b_{1} being FinSequence st

( b_{1} is D -valued & b_{1} is n -element )

end;
let n be Nat;

cluster Relation-like NAT -defined D -valued Function-like V34() n -element FinSequence-like FinSubsequence-like for set ;

existence ex b

( b

proof end;

definition

let D be non empty set ;

let f1, f2, f3, f4, f5, f6, f7 be BinominativeFunction of D;

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6)),f7) is BinominativeFunction of D ;

end;
let f1, f2, f3, f4, f5, f6, f7 be BinominativeFunction of D;

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);

coherence PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6)),f7);

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6)),f7) is BinominativeFunction of D ;

:: deftheorem defines PP_composition NOMIN_8:def 1 :

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6)),f7);

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6)),f7);

:: Unconditional composition rule for 7 programs

theorem Th1: :: NOMIN_8:1

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p8*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p8*> is SFHT of D

proof end;

definition

let D be non empty set ;

let f1, f2, f3, f4, f5, f6, f7, f8 be BinominativeFunction of D;

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7)),f8) is BinominativeFunction of D ;

end;
let f1, f2, f3, f4, f5, f6, f7, f8 be BinominativeFunction of D;

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);

coherence PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7)),f8);

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7)),f8) is BinominativeFunction of D ;

:: deftheorem defines PP_composition NOMIN_8:def 2 :

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7,f8) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7)),f8);

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7,f8) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7)),f8);

theorem Th2: :: NOMIN_8:2

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8, p9 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),p9*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7, f8 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8, p9 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),p9*> is SFHT of D

proof end;

definition

let D be non empty set ;

let f1, f2, f3, f4, f5, f6, f7, f8, f9 be BinominativeFunction of D;

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),f9) is BinominativeFunction of D ;

end;
let f1, f2, f3, f4, f5, f6, f7, f8, f9 be BinominativeFunction of D;

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);

coherence PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),f9);

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),f9) is BinominativeFunction of D ;

:: deftheorem defines PP_composition NOMIN_8:def 3 :

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),f9);

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),f9);

theorem Th3: :: NOMIN_8:3

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8, p9, p10 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),p10*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7, f8, f9 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8, p9, p10 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),p10*> is SFHT of D

proof end;

definition

let D be non empty set ;

let f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 be BinominativeFunction of D;

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),f10) is BinominativeFunction of D ;

end;
let f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 be BinominativeFunction of D;

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);

coherence PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),f10);

PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),f10) is BinominativeFunction of D ;

:: deftheorem defines PP_composition NOMIN_8:def 4 :

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),f10);

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),f10);

theorem :: NOMIN_8:4

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p11*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D

for p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11 being PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p11*> is SFHT of D

proof end;

theorem Th5: :: NOMIN_8:5

for D being non empty set

for f1, f2 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D holds

<*p1,(PP_composition (f1,f2)),p2*> is SFHT of D

for f1, f2 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D holds

<*p1,(PP_composition (f1,f2)),p2*> is SFHT of D

proof end;

theorem Th6: :: NOMIN_8:6

for D being non empty set

for f1, f2, f3 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,p2*> is SFHT of D holds

<*p1,(PP_composition (f1,f2,f3)),p2*> is SFHT of D

for f1, f2, f3 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,p2*> is SFHT of D holds

<*p1,(PP_composition (f1,f2,f3)),p2*> is SFHT of D

proof end;

theorem Th7: :: NOMIN_8:7

for D being non empty set

for f1, f2, f3, f4 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4)),p2*> is SFHT of D

for f1, f2, f3, f4 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4)),p2*> is SFHT of D

proof end;

theorem Th8: :: NOMIN_8:8

for D being non empty set

for f1, f2, f3, f4, f5 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5)),p2*> is SFHT of D

for f1, f2, f3, f4, f5 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5)),p2*> is SFHT of D

proof end;

theorem Th9: :: NOMIN_8:9

for D being non empty set

for f1, f2, f3, f4, f5, f6 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6)),p2*> is SFHT of D

for f1, f2, f3, f4, f5, f6 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6)),p2*> is SFHT of D

proof end;

theorem Th10: :: NOMIN_8:10

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p2*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p2*> is SFHT of D

proof end;

theorem Th11: :: NOMIN_8:11

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6, q7 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),p2*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7, f8 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6, q7 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),p2*> is SFHT of D

proof end;

theorem Th12: :: NOMIN_8:12

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6, q7, q8 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),p2*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7, f8, f9 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6, q7, q8 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),p2*> is SFHT of D

proof end;

theorem :: NOMIN_8:13

for D being non empty set

for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6, q7, q8, q9 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D

for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D

for p1, p2 being PartialPredicate of D

for q1, q2, q3, q4, q5, q6, q7, q8, q9 being total PartialPredicate of D st <*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 holds

<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D

proof end;

definition

let D be non empty set ;

let fD be PFuncs (D,D) -valued FinSequence;

assume A1: 0 < len fD ;

reconsider X = fD . 1 as Element of PFuncs (D,D) by PARTFUN1:45;

defpred S_{1}[ Nat, object , object ] means ex g being PartFunc of D,D st

( g = $2 & $3 = PP_composition (g,(fD . ($1 + 1))) );

ex b_{1} being FinSequence of PFuncs (D,D) st

( len b_{1} = len fD & b_{1} . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds

b_{1} . (n + 1) = PP_composition ((b_{1} . n),(fD . (n + 1))) ) )

for b_{1}, b_{2} being FinSequence of PFuncs (D,D) st len b_{1} = len fD & b_{1} . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds

b_{1} . (n + 1) = PP_composition ((b_{1} . n),(fD . (n + 1))) ) & len b_{2} = len fD & b_{2} . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds

b_{2} . (n + 1) = PP_composition ((b_{2} . n),(fD . (n + 1))) ) holds

b_{1} = b_{2}

end;
let fD be PFuncs (D,D) -valued FinSequence;

assume A1: 0 < len fD ;

reconsider X = fD . 1 as Element of PFuncs (D,D) by PARTFUN1:45;

defpred S

( g = $2 & $3 = PP_composition (g,(fD . ($1 + 1))) );

func PP_compositionSeq fD -> FinSequence of PFuncs (D,D) means :Def5: :: NOMIN_8:def 5

( len it = len fD & it . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds

it . (n + 1) = PP_composition ((it . n),(fD . (n + 1))) ) );

existence ( len it = len fD & it . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds

it . (n + 1) = PP_composition ((it . n),(fD . (n + 1))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines PP_compositionSeq NOMIN_8:def 5 :

for D being non empty set

for fD being PFuncs (b_{1},b_{1}) -valued FinSequence st 0 < len fD holds

for b_{3} being FinSequence of PFuncs (D,D) holds

( b_{3} = PP_compositionSeq fD iff ( len b_{3} = len fD & b_{3} . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds

b_{3} . (n + 1) = PP_composition ((b_{3} . n),(fD . (n + 1))) ) ) );

for D being non empty set

for fD being PFuncs (b

for b

( b

b

definition

let D be non empty set ;

let fD be PFuncs (D,D) -valued FinSequence;

(PP_compositionSeq fD) . (len (PP_compositionSeq fD)) is BinominativeFunction of D ;

end;
let fD be PFuncs (D,D) -valued FinSequence;

func PP_composition fD -> BinominativeFunction of D equals :: NOMIN_8:def 6

(PP_compositionSeq fD) . (len (PP_compositionSeq fD));

coherence (PP_compositionSeq fD) . (len (PP_compositionSeq fD));

(PP_compositionSeq fD) . (len (PP_compositionSeq fD)) is BinominativeFunction of D ;

:: deftheorem defines PP_composition NOMIN_8:def 6 :

for D being non empty set

for fD being PFuncs (b_{1},b_{1}) -valued FinSequence holds PP_composition fD = (PP_compositionSeq fD) . (len (PP_compositionSeq fD));

for D being non empty set

for fD being PFuncs (b

definition

let D be non empty set ;

let fD be PFuncs (D,D) -valued FinSequence;

let fB be PFuncs (D,BOOLEAN) -valued FinSequence;

end;
let fD be PFuncs (D,D) -valued FinSequence;

let fB be PFuncs (D,BOOLEAN) -valued FinSequence;

pred fD,fB are_composable means :: NOMIN_8:def 7

( 1 <= len fD & len fB = (len fD) + 1 & ( for n being Nat st 1 <= n & n <= len fD holds

<*(fB . n),(fD . n),(fB . (n + 1))*> is SFHT of D ) & ( for n being Nat st 2 <= n & n <= len fD holds

<*(PP_inversion (fB . n)),(fD . n),(fB . (n + 1))*> is SFHT of D ) );

( 1 <= len fD & len fB = (len fD) + 1 & ( for n being Nat st 1 <= n & n <= len fD holds

<*(fB . n),(fD . n),(fB . (n + 1))*> is SFHT of D ) & ( for n being Nat st 2 <= n & n <= len fD holds

<*(PP_inversion (fB . n)),(fD . n),(fB . (n + 1))*> is SFHT of D ) );

:: deftheorem defines are_composable NOMIN_8:def 7 :

for D being non empty set

for fD being PFuncs (b_{1},b_{1}) -valued FinSequence

for fB being PFuncs (b_{1},BOOLEAN) -valued FinSequence holds

( fD,fB are_composable iff ( 1 <= len fD & len fB = (len fD) + 1 & ( for n being Nat st 1 <= n & n <= len fD holds

<*(fB . n),(fD . n),(fB . (n + 1))*> is SFHT of D ) & ( for n being Nat st 2 <= n & n <= len fD holds

<*(PP_inversion (fB . n)),(fD . n),(fB . (n + 1))*> is SFHT of D ) ) );

for D being non empty set

for fD being PFuncs (b

for fB being PFuncs (b

( fD,fB are_composable iff ( 1 <= len fD & len fB = (len fD) + 1 & ( for n being Nat st 1 <= n & n <= len fD holds

<*(fB . n),(fD . n),(fB . (n + 1))*> is SFHT of D ) & ( for n being Nat st 2 <= n & n <= len fD holds

<*(PP_inversion (fB . n)),(fD . n),(fB . (n + 1))*> is SFHT of D ) ) );

theorem :: NOMIN_8:14

for D being non empty set

for fD being PFuncs (b_{1},b_{1}) -valued FinSequence

for fB being PFuncs (b_{1},BOOLEAN) -valued FinSequence st fD,fB are_composable holds

<*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D

for fD being PFuncs (b

for fB being PFuncs (b

<*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D

proof end;

definition

let V, A be set ;

let val be FinSequence;

set size = len val;

set D = PFuncs ((ND (V,A)),(ND (V,A)));

defpred S_{1}[ Nat, object ] means $2 = denaming (V,A,(val . $1));

ex b_{1} being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) st

( len b_{1} = len val & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = denaming (V,A,(val . n)) ) )

for b_{1}, b_{2} being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) st len b_{1} = len val & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = denaming (V,A,(val . n)) ) & len b_{2} = len val & ( for n being Nat st 1 <= n & n <= len b_{2} holds

b_{2} . n = denaming (V,A,(val . n)) ) holds

b_{1} = b_{2}

end;
let val be FinSequence;

set size = len val;

set D = PFuncs ((ND (V,A)),(ND (V,A)));

defpred S

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 & n <= len it holds

it . n = denaming (V,A,(val . n)) ) );

existence ( len it = len val & ( for n being Nat st 1 <= n & n <= len it holds

it . n = denaming (V,A,(val . n)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines denamingSeq NOMIN_8:def 8 :

for V, A being set

for val being FinSequence

for b_{4} being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) holds

( b_{4} = denamingSeq (V,A,val) iff ( len b_{4} = len val & ( for n being Nat st 1 <= n & n <= len b_{4} holds

b_{4} . n = denaming (V,A,(val . n)) ) ) );

for V, A being set

for val being FinSequence

for b

( b

b

definition

let V, A be set ;

let loc be V -valued Function;

let val be FinSequence;

assume 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 S_{1}[ 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))) );

ex b_{1} being FinSequence of PFuncs ((ND (V,A)),BOOLEAN) st

( len b_{1} = len val & b_{1} . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = SC_Psuperpos ((b_{1} . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) )

for b_{1}, b_{2} being FinSequence of PFuncs ((ND (V,A)),BOOLEAN) st len b_{1} = len val & b_{1} . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = SC_Psuperpos ((b_{1} . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) & len b_{2} = len val & b_{2} . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) & ( for n being Nat st 1 <= n & n < len b_{2} holds

b_{2} . (n + 1) = SC_Psuperpos ((b_{2} . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) holds

b_{1} = b_{2}

end;
let loc be V -valued Function;

let val be FinSequence;

assume 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 S

( 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: :: 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 & n < len it holds

it . (n + 1) = SC_Psuperpos ((it . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) );

existence ( 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 & n < len it holds

it . (n + 1) = SC_Psuperpos ((it . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines SC_Psuperpos_Seq NOMIN_8:def 9 :

for V, A being set

for loc being b_{1} -valued Function

for val being FinSequence st len val > 0 holds

for p being SCPartialNominativePredicate of V,A

for b_{6} being FinSequence of PFuncs ((ND (V,A)),BOOLEAN) holds

( b_{6} = SC_Psuperpos_Seq (loc,val,p) iff ( len b_{6} = len val & b_{6} . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) & ( for n being Nat st 1 <= n & n < len b_{6} holds

b_{6} . (n + 1) = SC_Psuperpos ((b_{6} . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) ) );

for V, A being set

for loc being b

for val being FinSequence st len val > 0 holds

for p being SCPartialNominativePredicate of V,A

for b

( b

b

theorem Th15: :: NOMIN_8:15

for n, m being Nat

for V, A being set

for loc being b_{3} -valued Function

for d1 being NonatomicND of V,A

for size being non zero Nat

for val being b_{7} -element FinSequence st 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)) holds

(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for size being non zero Nat

for val being b

(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))

proof end;

definition

let V, A be set ;

let inp be FinSequence;

let d be object ;

let val be FinSequence;

end;
let inp be FinSequence;

let d be object ;

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 & n <= len inp holds

d1 . (val . n) = inp . n ) );

ex d1 being NonatomicND of V,A st

( d = d1 & val is_valid_wrt d1 & ( for n being Nat st 1 <= n & n <= len inp holds

d1 . (val . n) = inp . n ) );

:: deftheorem defines is_valid_input NOMIN_8:def 10 :

for V, A being set

for inp being FinSequence

for d being object

for val being FinSequence holds

( inp is_valid_input V,A,val,d iff ex d1 being NonatomicND of V,A st

( d = d1 & val is_valid_wrt d1 & ( for n being Nat st 1 <= n & n <= len inp holds

d1 . (val . n) = inp . n ) ) );

for V, A being set

for inp being FinSequence

for d being object

for val being FinSequence holds

( inp is_valid_input V,A,val,d iff ex d1 being NonatomicND of V,A st

( d = d1 & val is_valid_wrt d1 & ( for n being Nat st 1 <= n & n <= len inp holds

d1 . (val . n) = inp . n ) ) );

definition

let V, A be set ;

let inp, val be FinSequence;

defpred S_{1}[ object ] means inp is_valid_input V,A,val,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( inp is_valid_input V,A,val,d implies b_{1} . d = TRUE ) & ( not inp is_valid_input V,A,val,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( inp is_valid_input V,A,val,d implies b_{1} . d = TRUE ) & ( not inp is_valid_input V,A,val,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = ND (V,A) & ( for d being object st d in dom b_{2} holds

( ( inp is_valid_input V,A,val,d implies b_{2} . d = TRUE ) & ( not inp is_valid_input V,A,val,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let inp, val be FinSequence;

defpred S

func valid_input (V,A,val,inp) -> SCPartialNominativePredicate of V,A means :Def11: :: 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 ) ) ) );

existence ( 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 ) ) ) );

ex b

( dom b

( ( inp is_valid_input V,A,val,d implies b

proof end;

uniqueness for b

( ( inp is_valid_input V,A,val,d implies b

( ( inp is_valid_input V,A,val,d implies b

b

proof end;

:: deftheorem Def11 defines valid_input NOMIN_8:def 11 :

for V, A being set

for inp, val being FinSequence

for b_{5} being SCPartialNominativePredicate of V,A holds

( b_{5} = valid_input (V,A,val,inp) iff ( dom b_{5} = ND (V,A) & ( for d being object st d in dom b_{5} holds

( ( inp is_valid_input V,A,val,d implies b_{5} . d = TRUE ) & ( not inp is_valid_input V,A,val,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for inp, val being FinSequence

for b

( b

( ( inp is_valid_input V,A,val,d implies b

registration

let V, A be set ;

let inp, val be FinSequence;

coherence

valid_input (V,A,val,inp) is total by Def11;

end;
let inp, val be FinSequence;

coherence

valid_input (V,A,val,inp) is total by Def11;

definition

let V, A be set ;

let d be object ;

let Z, res be FinSequence;

end;
let d be object ;

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 & n <= len Z holds

d1 . (Z . n) = res . n ) );

ex d1 being NonatomicND of V,A st

( d = d1 & Z is_valid_wrt d1 & ( for n being Nat st 1 <= n & n <= len Z holds

d1 . (Z . n) = res . n ) );

:: deftheorem defines is_valid_output NOMIN_8:def 12 :

for V, A being set

for d being object

for Z, res being FinSequence holds

( res is_valid_output V,A,Z,d iff ex d1 being NonatomicND of V,A st

( d = d1 & Z is_valid_wrt d1 & ( for n being Nat st 1 <= n & n <= len Z holds

d1 . (Z . n) = res . n ) ) );

for V, A being set

for d being object

for Z, res being FinSequence holds

( res is_valid_output V,A,Z,d iff ex d1 being NonatomicND of V,A st

( d = d1 & Z is_valid_wrt d1 & ( for n being Nat st 1 <= n & n <= len Z holds

d1 . (Z . n) = res . n ) ) );

definition

let V, A be set ;

let Z, res be object ;

set D = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,Z)) } ;

defpred S_{1}[ object ] means <*res*> is_valid_output V,A,<*Z*>,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,Z)) } & ( for d being object st d in dom b_{1} holds

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b_{1} . d = TRUE ) & ( not <*res*> is_valid_output V,A,<*Z*>,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,Z)) } & ( for d being object st d in dom b_{1} holds

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b_{1} . d = TRUE ) & ( not <*res*> is_valid_output V,A,<*Z*>,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,Z)) } & ( for d being object st d in dom b_{2} holds

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b_{2} . d = TRUE ) & ( not <*res*> is_valid_output V,A,<*Z*>,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let Z, res be object ;

set D = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,Z)) } ;

defpred S

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 ) ) ) );

existence ( 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 ) ) ) );

ex b

( dom b

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b

proof end;

uniqueness for b

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b

b

proof end;

:: deftheorem defines valid_output NOMIN_8:def 13 :

for V, A being set

for Z, res being object

for b_{5} being SCPartialNominativePredicate of V,A holds

( b_{5} = valid_output (V,A,Z,res) iff ( dom b_{5} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,Z)) } & ( for d being object st d in dom b_{5} holds

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b_{5} . d = TRUE ) & ( not <*res*> is_valid_output V,A,<*Z*>,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for Z, res being object

for b

( b

( ( <*res*> is_valid_output V,A,<*Z*>,d implies b

theorem Th16: :: NOMIN_8:16

for n being Nat

for V, A being set

for loc being b_{2} -valued Function

for d1 being NonatomicND of V,A

for p being SCPartialNominativePredicate of V,A

for d being object

for size being non zero Nat

for val being b_{8} -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & 2 <= n + 1 & n + 1 < size & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds

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)

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for p being SCPartialNominativePredicate of V,A

for d being object

for size being non zero Nat

for val being b

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 end;

theorem Th17: :: NOMIN_8:17

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for p being SCPartialNominativePredicate of V,A

for d being object

for size being non zero Nat

for val being b_{7} -element FinSequence st 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 holds

for m, n being Nat st 1 <= m & m < size & 1 <= n & 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))

for loc being b

for d1 being NonatomicND of V,A

for p being SCPartialNominativePredicate of V,A

for d being object

for size being non zero Nat

for val being b

for m, n being Nat st 1 <= m & m < size & 1 <= n & 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 end;

theorem :: NOMIN_8:18

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for p being SCPartialNominativePredicate of V,A

for size being non zero Nat

for val being b_{6} -element FinSequence

for dx, dy being object

for NN being Nat st NN = size - 2 & 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 holds

((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)

for loc being b

for d1 being NonatomicND of V,A

for p being SCPartialNominativePredicate of V,A

for size being non zero Nat

for val being b

for dx, dy being object

for NN being Nat st NN = size - 2 & 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 holds

((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)

proof end;

theorem :: NOMIN_8:19

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for size being non zero Nat

for val being b_{5} -element FinSequence

for p being SCPartialNominativePredicate of V,A st 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)) holds

((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)

for loc being b

for d1 being NonatomicND of V,A

for size being non zero Nat

for val being b

for p being SCPartialNominativePredicate of V,A st 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)) holds

((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 end;

definition

let V, A be set ;

let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let pos be FinSequence;

let prg be FPrg (ND (V,A)) -valued FinSequence;

assume A1: len prg > 0 ;

defpred S_{1}[ 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)));

ex b_{1} being FinSequence of ND (V,A) st

( len b_{1} = len prg & b_{1} . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = local_overlapping (V,A,(b_{1} . n),((prg . (n + 1)) . (b_{1} . n)),(loc /. (pos . (n + 1)))) ) )

for b_{1}, b_{2} being FinSequence of ND (V,A) st len b_{1} = len prg & b_{1} . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = local_overlapping (V,A,(b_{1} . n),((prg . (n + 1)) . (b_{1} . n)),(loc /. (pos . (n + 1)))) ) & len b_{2} = len prg & b_{2} . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len b_{2} holds

b_{2} . (n + 1) = local_overlapping (V,A,(b_{2} . n),((prg . (n + 1)) . (b_{2} . n)),(loc /. (pos . (n + 1)))) ) holds

b_{1} = b_{2}

end;
let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let pos be FinSequence;

let prg be FPrg (ND (V,A)) -valued FinSequence;

assume A1: len prg > 0 ;

defpred S

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: :: 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 & n < len it holds

it . (n + 1) = local_overlapping (V,A,(it . n),((prg . (n + 1)) . (it . n)),(loc /. (pos . (n + 1)))) ) );

existence ( len it = len prg & it . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len it holds

it . (n + 1) = local_overlapping (V,A,(it . n),((prg . (n + 1)) . (it . n)),(loc /. (pos . (n + 1)))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def14 defines PrgLocalOverlapSeq NOMIN_8:def 14 :

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being FPrg (ND (b_{1},b_{2})) -valued FinSequence st len prg > 0 holds

for b_{7} being FinSequence of ND (V,A) holds

( b_{7} = PrgLocalOverlapSeq (A,loc,d1,prg,pos) iff ( len b_{7} = len prg & b_{7} . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len b_{7} holds

b_{7} . (n + 1) = local_overlapping (V,A,(b_{7} . n),((prg . (n + 1)) . (b_{7} . n)),(loc /. (pos . (n + 1)))) ) ) );

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being FPrg (ND (b

for b

( b

b

registration

let V, A be set ;

let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let prg be non empty FPrg (ND (V,A)) -valued FinSequence;

let pos be FinSequence;

coherence

PrgLocalOverlapSeq (A,loc,d1,prg,pos) is V,A -NonatomicND-yielding

end;
let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let prg be non empty FPrg (ND (V,A)) -valued FinSequence;

let pos be FinSequence;

coherence

PrgLocalOverlapSeq (A,loc,d1,prg,pos) is V,A -NonatomicND-yielding

proof end;

registration

let V, A be set ;

let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let prg be non empty FPrg (ND (V,A)) -valued FinSequence;

let pos be FinSequence;

let n be Nat;

coherence

( (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Function-like & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Relation-like )

end;
let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let prg be non empty FPrg (ND (V,A)) -valued FinSequence;

let pos be FinSequence;

let n be Nat;

coherence

( (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Function-like & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Relation-like )

proof end;

definition

let V, A be set ;

let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let prg be non empty FPrg (ND (V,A)) -valued FinSequence;

let pos be FinSequence;

end;
let loc be V -valued Function;

let d1 be NonatomicND of V,A;

let prg be non empty FPrg (ND (V,A)) -valued FinSequence;

let pos be FinSequence;

pred prg_doms_of loc,d1,prg,pos means :: NOMIN_8:def 15

for n being Nat st 1 <= n & n < len prg holds

(PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1));

for n being Nat st 1 <= n & n < len prg holds

(PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1));

:: deftheorem defines prg_doms_of NOMIN_8:def 15 :

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for prg being non empty FPrg (ND (b_{1},b_{2})) -valued FinSequence

for pos being FinSequence holds

( prg_doms_of loc,d1,prg,pos iff for n being Nat st 1 <= n & n < len prg holds

(PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) );

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for prg being non empty FPrg (ND (b

for pos being FinSequence holds

( prg_doms_of loc,d1,prg,pos iff for n being Nat st 1 <= n & n < len prg holds

(PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) );

theorem Th20: :: NOMIN_8:20

for n, m being Nat

for V, A being set

for loc being b_{3} -valued Function

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b_{3},b_{4})) -valued FinSequence st 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) holds

(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A

for V, A being set

for loc being b

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b

(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A

proof end;

theorem Th21: :: NOMIN_8:21

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b_{1},b_{2})) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V holds

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))

for loc being b

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b

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 end;

theorem Th22: :: NOMIN_8:22

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b_{1},b_{2})) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V holds

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))

for loc being b

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b

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 end;

theorem :: NOMIN_8:23

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b_{1},b_{2})) -valued FinSequence st not V is 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 holds

for n being Nat st 1 <= n & n <= len prg holds

dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)

for loc being b

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b

for n being Nat st 1 <= n & n <= len prg holds

dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)

proof end;

theorem Th24: :: NOMIN_8:24

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b_{1},b_{2})) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V & prg_doms_of loc,d1,prg,pos holds

for m, n being Nat st 1 <= n & n <= m & m <= len prg holds

dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)

for loc being b

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b

for m, n being Nat st 1 <= n & n <= m & m <= len prg holds

dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)

proof end;

theorem :: NOMIN_8:25

for V, A being set

for loc being b_{1} -valued Function

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b_{1},b_{2})) -valued FinSequence st not V is 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 holds

for m, n being Nat st 1 <= n & n <= m & m <= len prg holds

loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)

for loc being b

for d1 being NonatomicND of V,A

for pos being FinSequence

for prg being non empty FPrg (ND (b

for m, n being Nat st 1 <= n & n <= m & m <= len prg holds

loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)

proof end;