nomin_8.miz



    begin

    registration

      let D be non empty set;

      cluster non emptyD -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 -valuedn -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;

      :: NOMIN_8:def1

      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

    ::$Notion-Name

    theorem :: NOMIN_8:1

    

     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;

      :: NOMIN_8:def2

      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

    ::$Notion-Name

    theorem :: NOMIN_8:2

    

     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;

      :: NOMIN_8:def3

      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

    ::$Notion-Name

    theorem :: NOMIN_8:3

    

     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;

      :: NOMIN_8:def4

      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

    ::$Notion-Name

    theorem :: NOMIN_8:4

     <*p1, f1, p2*> is SFHT of D & <*p2, f2, p3*> is SFHT of D & <*p3, f3, p4*> is SFHT of D & <*p4, f4, p5*> is SFHT of D & <*p5, f5, p6*> is SFHT of D & <*p6, f6, p7*> is SFHT of D & <*p7, f7, p8*> is SFHT of D & <*p8, f8, p9*> is SFHT of D & <*p9, f9, p10*> is SFHT of D & <*p10, f10, p11*> is SFHT of D & <*( PP_inversion p2), f2, p3*> is SFHT of D & <*( PP_inversion p3), f3, p4*> is SFHT of D & <*( PP_inversion p4), f4, p5*> is SFHT of D & <*( PP_inversion p5), f5, p6*> is SFHT of D & <*( PP_inversion p6), f6, p7*> is SFHT of D & <*( PP_inversion p7), f7, p8*> is SFHT of D & <*( PP_inversion p8), f8, p9*> is SFHT of D & <*( PP_inversion p9), f9, p10*> is SFHT of D & <*( PP_inversion p10), f10, p11*> is SFHT of D implies <*p1, ( PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)), p11*> is SFHT of D

    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 :: NOMIN_8:5

    

     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 :: NOMIN_8:6

    

     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 :: NOMIN_8:7

    

     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 :: NOMIN_8:8

    

     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 :: NOMIN_8:9

    

     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 :: NOMIN_8:10

    

     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 :: NOMIN_8:11

    

     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 :: NOMIN_8:12

    

     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 :: NOMIN_8:13

     <*p1, f1, q1*> is SFHT of D & <*q1, f2, q2*> is SFHT of D & <*q2, f3, q3*> is SFHT of D & <*q3, f4, q4*> is SFHT of D & <*q4, f5, q5*> is SFHT of D & <*q5, f6, q6*> is SFHT of D & <*q6, f7, q7*> is SFHT of D & <*q7, f8, q8*> is SFHT of D & <*q8, f9, q9*> is SFHT of D & <*q9, f10, p2*> is SFHT of D implies <*p1, ( PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)), p2*> is SFHT of D

    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;

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

      defpred P[ Nat, object, object] means ex g be PartFunc of D, D st g = $2 & $3 = ( PP_composition (g,(fD . ($1 + 1))));

      :: NOMIN_8:def5

      func PP_compositionSeq (fD) -> FinSequence of ( PFuncs (D,D)) means

      : Def5: ( len it ) = ( len fD) & (it . 1) = (fD . 1) & for n be 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) holds for x be Element of ( PFuncs (D,D)) holds ex y be 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 be 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 be FinSequence of ( PFuncs (D,D)) such that

         A6: ( len F1) = ( len fD) and

         A7: (F1 . 1) = (fD . 1) and

         A8: for n be 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 be 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) holds for x,y1,y2 be 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;

      :: NOMIN_8:def6

      func PP_composition (fD) -> BinominativeFunction of D equals (( PP_compositionSeq fD) . ( len ( PP_compositionSeq fD)));

      coherence ;

    end

    definition

      let D, fD, fB;

      :: NOMIN_8:def7

      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

    ::$Notion-Name

    theorem :: NOMIN_8:14

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

      :: NOMIN_8:def8

      func denamingSeq (V,A,val) -> FinSequence of ( PFuncs (( ND (V,A)),( ND (V,A)))) means ( len it ) = ( len val) & for n be Nat st 1 <= n <= ( len it ) holds (it . n) = ( denaming (V,A,(val . n)));

      existence

      proof

        

         A1: for n be Nat st n in ( Seg size) holds ex x be 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 be FinSequence of D such that

         A2: ( dom p) = ( Seg size) and

         A3: for n be 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 be FinSequence of D such that

         A4: ( len F1) = size and

         A5: for n be Nat st 1 <= n <= ( len F1) holds (F1 . n) = ( denaming (V,A,(val . n))) and

         A6: ( len F2) = size and

         A7: for n be 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 17;

      end;

    end

    definition

      let V, A, loc;

      let val be FinSequence;

      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 be SCPartialNominativePredicate of V, A st f = $2 & $3 = ( SC_Psuperpos (f,( denaming (V,A,(val . (( len val) - $1)))),(loc /. (( len val) - $1))));

      :: NOMIN_8:def9

      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 be 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 be Nat st 1 <= n & n < size holds for x be Element of D holds ex y be 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 be 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 be FinSequence of D such that

         A5: ( len F1) = size and

         A6: (F1 . 1) = X and

         A7: for n be 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 be 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 holds for x,y1,y2 be 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 :: NOMIN_8:15

    

     Th15: for size be non zero Nat holds for val be 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 be 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;

      :: NOMIN_8:def10

      pred inp is_valid_input V,A,val,d means ex d1 be NonatomicND of V, A st d = d1 & val is_valid_wrt d1 & for n be 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);

      :: NOMIN_8:def11

      func valid_input (V,A,val,inp) -> SCPartialNominativePredicate of V, A means

      : Def11: ( dom it ) = ( ND (V,A)) & for d be 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 be SCPartialNominativePredicate of V, A such that

         A2: ( dom p) = ( ND (V,A)) & (for d be 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 be SCPartialNominativePredicate of V, A st (( dom p) = ( ND (V,A)) & (for d be 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 be 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;

      :: NOMIN_8:def12

      pred res is_valid_output V,A,Z,d means ex d1 be NonatomicND of V, A st d = d1 & Z is_valid_wrt d1 & for n be 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 be TypeSCNominativeData of V, A : d in ( dom ( denaming (V,A,Z))) };

      defpred P[ object] means <*res*> is_valid_output (V,A, <*Z*>,$1);

      :: NOMIN_8:def13

      func valid_output (V,A,Z,res) -> SCPartialNominativePredicate of V, A means ( dom it ) = { d where d be TypeSCNominativeData of V, A : d in ( dom ( denaming (V,A,Z))) } & for d be 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 be TypeSCNominativeData of V, A st v = d & d in ( dom ( denaming (V,A,Z)));

          hence thesis;

        end;

        consider p be SCPartialNominativePredicate of V, A such that

         A2: ( dom p) = D & (for d be 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 be SCPartialNominativePredicate of V, A st (( dom p) = D & (for d be 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 be 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 :: NOMIN_8:16

    

     Th16: for val be 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 be 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 be 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 be 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() 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() in ( dom D) by A17;

          hence F(+) 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 be 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 be 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(+) 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(+) in ( dom D) by A29;

          hence F(+) in ( dom (S . (k + 1))) by A6, A11, A25, A28, A35, A12, NAT_1: 13;

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A9, A10);

      hence thesis by A3, A4;

    end;

    theorem :: NOMIN_8:17

    

     Th17: for val be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be Nat holds P[k] from NAT_1:sch 2( A8, A9);

      hence thesis by A6, A7;

    end;

    theorem :: NOMIN_8:18

    for val be size -element FinSequence holds for dx,dy be object holds for NN be 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 be 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;

      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 :: NOMIN_8:19

    for val be size -element FinSequence holds for p be 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 be 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 be 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 be 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 be 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;

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

      :: NOMIN_8:def14

      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 be 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 be Nat st 1 <= n < ( len prg) holds for x be Element of ( ND (V,A)) holds ex y be 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 be 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 be 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 be 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 holds for x,y1,y2 be 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;

      :: NOMIN_8:def15

      pred prg_doms_of loc,d1,prg,pos means for n be Nat st 1 <= n < ( len prg) holds (( PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) in ( dom (prg . (n + 1)));

    end

    theorem :: NOMIN_8:20

    

     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 :: NOMIN_8:21

    

     Th21: V is non empty & A is_without_nonatomicND_wrt V implies for n be 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 :: NOMIN_8:22

    

     Th22: V is non empty & A is_without_nonatomicND_wrt V implies for n be 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 :: NOMIN_8:23

    V is non empty & A is_without_nonatomicND_wrt V & ( dom ( PrgLocalOverlapSeq (A,loc,d1,prg,pos))) c= ( dom prg) & d1 in ( dom (prg . 1)) & prg_doms_of (loc,d1,prg,pos) implies for n be 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 be 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 be Nat holds P[k] from NAT_1:sch 2( A8, A9);

      hence thesis by A6, A7;

    end;

    theorem :: NOMIN_8:24

    

     Th24: V is non empty & A is_without_nonatomicND_wrt V & prg_doms_of (loc,d1,prg,pos) implies for m,n be 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 be 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 be Nat holds P[k] from NAT_1:sch 2( A7, A8);

        hence thesis by A5, A6;

      end;

    end;

    theorem :: NOMIN_8:25

    V is non empty & A is_without_nonatomicND_wrt V & ( dom ( PrgLocalOverlapSeq (A,loc,d1,prg,pos))) c= ( dom prg) & d1 in ( dom (prg . 1)) & prg_doms_of (loc,d1,prg,pos) implies for m,n be 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;