nomin_9.miz



    begin

    registration

      let n be Nat;

      let f be n -element FinSequence;

      reduce (f | ( Seg n)) to f;

      reducibility

      proof

        ( len f) = n by CARD_1:def 7;

        then (f | n) = f;

        hence thesis;

      end;

    end

    registration

      let A,B be set;

      let f1,f2,f3,f4,f5,f6 be PartFunc of A, B;

      cluster <*f1, f2, f3, f4, f5, f6*> -> ( PFuncs (A,B)) -valued;

      coherence

      proof

         {f1, f2, f3, f4, f5, f6} c= ( PFuncs (A,B))

        proof

          let x be object;

          assume x in {f1, f2, f3, f4, f5, f6};

          then x = f1 or x = f2 or x = f3 or x = f4 or x = f5 or x = f6 by ENUMSET1:def 4;

          hence thesis by PARTFUN1: 45;

        end;

        hence ( rng <*f1, f2, f3, f4, f5, f6*>) c= ( PFuncs (A,B)) by AOFA_A00: 21;

      end;

    end

    registration

      let V,A be set;

      let f1,f2,f3,f4,f5,f6 be SCBinominativeFunction of V, A;

      cluster <*f1, f2, f3, f4, f5, f6*> -> ( FPrg ( ND (V,A))) -valued;

      coherence ;

    end

    registration

      let a1,a2,a3,a4,a5,a6 be object;

      reduce ( <*a1, a2, a3, a4, a5, a6*> . 1) to a1;

      reducibility by AOFA_A00: 20;

      reduce ( <*a1, a2, a3, a4, a5, a6*> . 2) to a2;

      reducibility by AOFA_A00: 20;

      reduce ( <*a1, a2, a3, a4, a5, a6*> . 3) to a3;

      reducibility by AOFA_A00: 20;

      reduce ( <*a1, a2, a3, a4, a5, a6*> . 4) to a4;

      reducibility by AOFA_A00: 20;

      reduce ( <*a1, a2, a3, a4, a5, a6*> . 5) to a5;

      reducibility by AOFA_A00: 20;

      reduce ( <*a1, a2, a3, a4, a5, a6*> . 6) to a6;

      reducibility by AOFA_A00: 20;

    end

    definition

      let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;

      :: NOMIN_9:def1

      func <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> FinSequence equals ( <*a1, a2, a3, a4, a5, a6, a7, a8*> ^ <*a9*>);

      coherence ;

    end

    theorem :: NOMIN_9:1

    

     Th1: for a1,a2,a3,a4,a5,a6,a7,a8,a9 be object holds for f be FinSequence holds f = <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> iff ( len f) = 9 & (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 & (f . 9) = a9

    proof

      let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;

      let f be FinSequence;

      set AS1 = <*a9*>;

      set AS8 = <*a1, a2, a3, a4, a5, a6, a7, a8*>;

      set AS9 = <*a1, a2, a3, a4, a5, a6, a7, a8, a9*>;

       A1:

      now

        let f be FinSequence;

        assume

         A2: f = AS9;

        

        hence ( len f) = (( len AS8) + ( len AS1)) by FINSEQ_1: 22

        .= (8 + ( len AS1)) by AOFA_A00: 24

        .= (8 + 1) by FINSEQ_1: 39

        .= 9;

        ( dom AS8) = ( Seg 8) by FINSEQ_1: 89;

        then 1 in ( dom AS8) & 2 in ( dom AS8) & 3 in ( dom AS8) & 4 in ( dom AS8) & 5 in ( dom AS8) & 6 in ( dom AS8) & 7 in ( dom AS8) & 8 in ( dom AS8);

        then (f . 1) = (AS8 . 1) & (f . 2) = (AS8 . 2) & (f . 3) = (AS8 . 3) & (f . 4) = (AS8 . 4) & (f . 5) = (AS8 . 5) & (f . 6) = (AS8 . 6) & (f . 7) = (AS8 . 7) & (f . 8) = (AS8 . 8) by A2, FINSEQ_1:def 7;

        hence (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 by AOFA_A00: 24;

        ( len AS8) = 8 by AOFA_A00: 24;

        hence (f . 9) = a9 by A2;

      end;

      hence f = AS9 implies ( len f) = 9 & (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 & (f . 9) = a9;

      assume

       A3: ( len f) = 9;

      ( len AS9) = 9 by A1;

      then

       A4: ( dom f) = ( Seg 9) & ( dom AS9) = ( Seg 9) by A3, FINSEQ_1:def 3;

      assume

       A5: (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 & (f . 9) = a9;

      now

        let x be object;

        assume x in ( Seg 9);

        then x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 by AOFA_A00: 27, ENUMSET1:def 7;

        hence (f . x) = (AS9 . x) by A1, A5;

      end;

      hence f = AS9 by A4, FUNCT_1: 2;

    end;

    registration

      let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;

      cluster <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> -> 9 -element;

      coherence ;

    end

    registration

      let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 1) to a1;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 2) to a2;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 3) to a3;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 4) to a4;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 5) to a5;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 6) to a6;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 7) to a7;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 8) to a8;

      reducibility by Th1;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> . 9) to a9;

      reducibility by Th1;

    end

    theorem :: NOMIN_9:2

    

     Th2: for a1,a2,a3,a4,a5,a6,a7,a8,a9 be object holds ( rng <*a1, a2, a3, a4, a5, a6, a7, a8, a9*>) = {a1, a2, a3, a4, a5, a6, a7, a8, a9}

    proof

      let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;

      

      thus ( rng <*a1, a2, a3, a4, a5, a6, a7, a8, a9*>) = (( rng <*a1, a2, a3, a4, a5, a6, a7, a8*>) \/ ( rng <*a9*>)) by FINSEQ_1: 31

      .= ( {a1, a2, a3, a4, a5, a6, a7, a8} \/ ( rng <*a9*>)) by AOFA_A00: 25

      .= ( {a1, a2, a3, a4, a5, a6, a7, a8} \/ {a9}) by FINSEQ_1: 38

      .= {a1, a2, a3, a4, a5, a6, a7, a8, a9} by ENUMSET1: 84;

    end;

    definition

      let X be non empty set;

      let a1,a2,a3,a4,a5,a6,a7,a8,a9 be Element of X;

      :: original: <*

      redefine

      func <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> FinSequence of X ;

      coherence

      proof

         <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> = ( <*a1, a2, a3, a4, a5, a6, a7, a8*> ^ <*a9*>);

        hence thesis;

      end;

    end

    definition

      let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;

      :: NOMIN_9:def2

      func <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> FinSequence equals ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> ^ <*a10*>);

      coherence ;

    end

    theorem :: NOMIN_9:3

    

     Th3: for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object holds for f be FinSequence holds f = <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> iff ( len f) = 10 & (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 & (f . 9) = a9 & (f . 10) = a10

    proof

      let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;

      let f be FinSequence;

      set AS1 = <*a10*>;

      set AS9 = <*a1, a2, a3, a4, a5, a6, a7, a8, a9*>;

      set AS10 = <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*>;

       A1:

      now

        let f be FinSequence;

        assume

         A2: f = AS10;

        

        hence ( len f) = (( len AS9) + ( len AS1)) by FINSEQ_1: 22

        .= (9 + ( len AS1)) by Th1

        .= (9 + 1) by FINSEQ_1: 39

        .= 10;

        ( dom AS9) = ( Seg 9) by FINSEQ_1: 89;

        then 1 in ( dom AS9) & 2 in ( dom AS9) & 3 in ( dom AS9) & 4 in ( dom AS9) & 5 in ( dom AS9) & 6 in ( dom AS9) & 7 in ( dom AS9) & 8 in ( dom AS9) & 9 in ( dom AS9);

        then (f . 1) = (AS9 . 1) & (f . 2) = (AS9 . 2) & (f . 3) = (AS9 . 3) & (f . 4) = (AS9 . 4) & (f . 5) = (AS9 . 5) & (f . 6) = (AS9 . 6) & (f . 7) = (AS9 . 7) & (f . 8) = (AS9 . 8) & (f . 9) = (AS9 . 9) by A2, FINSEQ_1:def 7;

        hence (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 & (f . 9) = a9;

        ( len AS9) = 9 by Th1;

        hence (f . 10) = a10 by A2;

      end;

      hence f = AS10 implies ( len f) = 10 & (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 & (f . 9) = a9 & (f . 10) = a10;

      assume

       A3: ( len f) = 10;

      ( len AS10) = 10 by A1;

      then

       A4: ( dom f) = ( Seg 10) & ( dom AS10) = ( Seg 10) by A3, FINSEQ_1:def 3;

      assume

       A5: (f . 1) = a1 & (f . 2) = a2 & (f . 3) = a3 & (f . 4) = a4 & (f . 5) = a5 & (f . 6) = a6 & (f . 7) = a7 & (f . 8) = a8 & (f . 9) = a9 & (f . 10) = a10;

      now

        let x be object;

        assume x in ( Seg 10);

        then x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 by AOFA_A00: 28, ENUMSET1:def 8;

        hence (f . x) = (AS10 . x) by A1, A5;

      end;

      hence f = AS10 by A4, FUNCT_1: 2;

    end;

    registration

      let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;

      cluster <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> -> 10 -element;

      coherence ;

    end

    registration

      let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 1) to a1;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 2) to a2;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 3) to a3;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 4) to a4;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 5) to a5;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 6) to a6;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 7) to a7;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 8) to a8;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 9) to a9;

      reducibility by Th3;

      reduce ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> . 10) to a10;

      reducibility by Th3;

    end

    theorem :: NOMIN_9:4

    for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object holds ( rng <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*>) = {a1, a2, a3, a4, a5, a6, a7, a8, a9, a10}

    proof

      let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;

      

      thus ( rng <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*>) = (( rng <*a1, a2, a3, a4, a5, a6, a7, a8, a9*>) \/ ( rng <*a10*>)) by FINSEQ_1: 31

      .= ( {a1, a2, a3, a4, a5, a6, a7, a8, a9} \/ ( rng <*a10*>)) by Th2

      .= ( {a1, a2, a3, a4, a5, a6, a7, a8, a9} \/ {a10}) by FINSEQ_1: 38

      .= {a1, a2, a3, a4, a5, a6, a7, a8, a9, a10} by ENUMSET1: 85;

    end;

    definition

      let X be non empty set;

      let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be Element of X;

      :: original: <*

      redefine

      func <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> FinSequence of X ;

      coherence

      proof

         <*a1, a2, a3, a4, a5, a6, a7, a8, a9, a10*> = ( <*a1, a2, a3, a4, a5, a6, a7, a8, a9*> ^ <*a10*>);

        hence thesis;

      end;

    end

    begin

    definition

      let i,j be Integer;

      :: original: [

      redefine

      func [i,j] -> Element of [: INT , INT :] ;

      coherence

      proof

        reconsider i, j as Element of INT by INT_1:def 2;

         [i, j] is Element of [: INT , INT :];

        hence thesis;

      end;

    end

    reserve x,y,P,Q for Integer;

    reserve a,b,n for Nat;

    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 for object;

    reserve z for Element of V;

    reserve T for TypeSCNominativeData of V, A;

    reserve size for non zero Nat;

    reserve x0,y0,p0,q0 for Integer;

    reserve n0 for Nat;

    definition

      let x, y, P, Q;

      deffunc F( set, Element of [: INT , INT :]) = [($2 `2 ), ((P * ($2 `2 )) - (Q * ($2 `1 )))];

      :: NOMIN_9:def3

      func Lucas_Sequence (x,y,P,Q) -> sequence of [: INT , INT :] means

      : Def3: (it . 0 ) = [x, y] & for n be Nat holds (it . (n + 1)) = [((it . n) `2 ), ((P * ((it . n) `2 )) - (Q * ((it . n) `1 )))];

      existence

      proof

        ex L be sequence of [: INT , INT :] st (L . 0 ) = [x, y] & for n be Nat holds (L . (n + 1)) = F(n,.) from NAT_1:sch 12;

        hence thesis;

      end;

      uniqueness

      proof

        let L1,L2 be sequence of [: INT , INT :] such that

         A1: (L1 . 0 ) = [x, y] and

         A2: for n be Nat holds (L1 . (n + 1)) = F(n,.) and

         A3: (L2 . 0 ) = [x, y] and

         A4: for n be Nat holds (L2 . (n + 1)) = F(n,.);

        thus L1 = L2 from NAT_1:sch 16( A1, A2, A3, A4);

      end;

    end

    definition

      let x, y, P, Q, n;

      :: NOMIN_9:def4

      func Lucas (x,y,P,Q,n) -> Element of INT equals ((( Lucas_Sequence (x,y,P,Q)) . n) `1 );

      coherence ;

    end

    theorem :: NOMIN_9:5

    

     Th5: ( Lucas (x,y,P,Q, 0 )) = x & ( Lucas (x,y,P,Q,1)) = y & for n holds ( Lucas (x,y,P,Q,(n + 2))) = ((P * ( Lucas (x,y,P,Q,(n + 1)))) - (Q * ( Lucas (x,y,P,Q,n))))

    proof

      set L = ( Lucas_Sequence (x,y,P,Q));

      

      thus ( Lucas (x,y,P,Q, 0 )) = ( [x, y] `1 ) by Def3

      .= x;

      

      thus ( Lucas (x,y,P,Q,1)) = ((L . ( 0 + 1)) `1 )

      .= ( [((L . 0 ) `2 ), ((P * ((L . 0 ) `2 )) - (Q * ((L . 0 ) `1 )))] `1 ) by Def3

      .= ( [x, y] `2 ) by Def3

      .= y;

      let n;

      

       A1: ((L . (n + 1)) `1 ) = ( [((L . n) `2 ), ((P * ((L . n) `2 )) - (Q * ((L . n) `1 )))] `1 ) by Def3

      .= ((L . n) `2 );

      (n + 2) = ((n + 1) + 1);

      

      hence ( Lucas (x,y,P,Q,(n + 2))) = ( [((L . (n + 1)) `2 ), ((P * ((L . (n + 1)) `2 )) - (Q * ((L . (n + 1)) `1 )))] `1 ) by Def3

      .= ( [((L . n) `2 ), ((P * ((L . n) `2 )) - (Q * ((L . n) `1 )))] `2 ) by Def3

      .= ((P * ( Lucas (x,y,P,Q,(n + 1)))) - (Q * ( Lucas (x,y,P,Q,n)))) by A1;

    end;

    theorem :: NOMIN_9:6

    

     Th6: ( Lucas_Sequence ( 0 ,1,1,( - 1))) = Fib

    proof

      set L = ( Lucas_Sequence ( 0 ,1,1,( - 1)));

      set F = Fib ;

      ( dom F) = NAT & ( dom L) = NAT by FUNCT_2:def 1;

      hence ( dom L) = ( dom F);

      let n be object such that

       A1: n in ( dom L);

      defpred P[ Nat] means (L . $1) = (F . $1);

      (L . 0 ) = [ 0 , 1] by Def3;

      then

       A2: P[ 0 ] by PRE_FF:def 1;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A4: P[k];

        

        thus (L . (k + 1)) = [((L . k) `2 ), ((1 * ((L . k) `2 )) - (( - 1) * ((L . k) `1 )))] by Def3

        .= [((F . k) `2 ), (((F . k) `1 ) + ((F . k) `2 ))] by A4

        .= (F . (k + 1)) by PRE_FF:def 1;

      end;

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

      hence thesis by A1;

    end;

    theorem :: NOMIN_9:7

    ( Lucas ( 0 ,1,1,( - 1),n)) = ( Fib n) by Th6;

    theorem :: NOMIN_9:8

    

     Th8: ( Lucas_Sequence (a,b,1,( - 1))) = ( GenFib (a,b))

    proof

      set L = ( Lucas_Sequence (a,b,1,( - 1)));

      set F = ( GenFib (a,b));

      ( dom F) = NAT & ( dom L) = NAT by FUNCT_2:def 1;

      hence ( dom L) = ( dom F);

      let n be object such that

       A1: n in ( dom L);

      defpred P[ Nat] means (L . $1) = (F . $1);

      (L . 0 ) = [a, b] by Def3;

      then

       A2: P[ 0 ] by FIB_NUM3:def 3;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A4: P[k];

        

        thus (L . (k + 1)) = [((L . k) `2 ), ((1 * ((L . k) `2 )) - (( - 1) * ((L . k) `1 )))] by Def3

        .= [((F . k) `2 ), (((F . k) `1 ) + ((F . k) `2 ))] by A4

        .= (F . (k + 1)) by FIB_NUM3:def 3;

      end;

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

      hence thesis by A1;

    end;

    theorem :: NOMIN_9:9

    ( Lucas (a,b,1,( - 1),n)) = ( GenFib (a,b,n)) by Th8;

    theorem :: NOMIN_9:10

    

     Th10: ( Lucas_Sequence (2,1,1,( - 1))) = Lucas

    proof

      set L = ( Lucas_Sequence (2,1,1,( - 1)));

      set F = Lucas ;

      ( dom F) = NAT & ( dom L) = NAT by FUNCT_2:def 1;

      hence ( dom L) = ( dom F);

      let n be object such that

       A1: n in ( dom L);

      defpred P[ Nat] means (L . $1) = (F . $1);

      (L . 0 ) = [2, 1] by Def3;

      then

       A2: P[ 0 ] by FIB_NUM3:def 1;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A4: P[k];

        

        thus (L . (k + 1)) = [((L . k) `2 ), ((1 * ((L . k) `2 )) - (( - 1) * ((L . k) `1 )))] by Def3

        .= [((F . k) `2 ), (((F . k) `1 ) + ((F . k) `2 ))] by A4

        .= (F . (k + 1)) by FIB_NUM3:def 1;

      end;

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

      hence thesis by A1;

    end;

    theorem :: NOMIN_9:11

    ( Lucas (2,1,1,( - 1),n)) = ( Lucas n) by Th10;

    begin

    theorem :: NOMIN_9:12

    

     Th12: ( Seg 10) c= ( dom loc) & loc is_valid_wrt d1 implies {(loc /. 1), (loc /. 2), (loc /. 3), (loc /. 4), (loc /. 5), (loc /. 6), (loc /. 7), (loc /. 8), (loc /. 9), (loc /. 10)} c= ( dom d1)

    proof

      assume that

       A1: ( Seg 10) c= ( dom loc) and

       A2: ( rng loc) c= ( dom d1);

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

      let x be object;

      assume x in {i, j, n, s, b, c, p, q, ps, qc};

      then

       A3: x = i or x = j or x = n or x = s or x = b or x = c or x = p or x = q or x = ps or x = qc by ENUMSET1:def 8;

      

       A4: 1 in ( Seg 10) & ... & 10 in ( Seg 10);

      then

       A5: (loc . 1) in ( rng loc) & ... & (loc . 10) in ( rng loc) by A1, FUNCT_1:def 3;

      (loc . 1) = (loc /. 1) & ... & (loc . 10) = (loc /. 10) by A1, A4, PARTFUN1:def 6;

      hence thesis by A2, A3, A5;

    end;

    definition

      let V, A, loc;

      :: NOMIN_9:def5

      func Lucas_loop_body (A,loc) -> SCBinominativeFunction of V, A equals ( PP_composition (( SC_assignment (( denaming (V,A,(loc /. 4))),(loc /. 6))),( SC_assignment (( denaming (V,A,(loc /. 5))),(loc /. 4))),( SC_assignment (( multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))),( SC_assignment (( multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))),( SC_assignment (( subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))),( SC_assignment (( addition (A,(loc /. 1),(loc /. 2))),(loc /. 1)))));

      coherence ;

    end

    definition

      let V, A, loc;

      :: NOMIN_9:def6

      func Lucas_main_loop (A,loc) -> SCBinominativeFunction of V, A equals ( PP_while (( PP_not ( Equality (A,(loc /. 1),(loc /. 3)))),( Lucas_loop_body (A,loc))));

      coherence ;

    end

    definition

      let V, A, loc, val;

      :: NOMIN_9:def7

      func Lucas_main_part (A,loc,val) -> SCBinominativeFunction of V, A equals ( PP_composition (( initial_assignments (A,loc,val,10)),( Lucas_main_loop (A,loc))));

      coherence ;

    end

    definition

      let V, A, loc, val, z;

      :: NOMIN_9:def8

      func Lucas_program (A,loc,val,z) -> SCBinominativeFunction of V, A equals ( PP_composition (( Lucas_main_part (A,loc,val)),( SC_assignment (( denaming (V,A,(loc /. 4))),z))));

      coherence ;

    end

    definition

      let x0, y0, p0, q0, n0;

      :: NOMIN_9:def9

      func Lucas_input (x0,y0,p0,q0,n0) -> FinSequence equals <* 0 , 1, n0, x0, y0, x0, p0, q0, 0 , 0 *>;

      coherence ;

    end

    registration

      let x0, y0, p0, q0, n0;

      cluster ( Lucas_input (x0,y0,p0,q0,n0)) -> 10 -element;

      coherence ;

    end

    definition

      let V, A, x0, y0, p0, q0, n0, d;

      let val be FinSequence;

      :: NOMIN_9:def10

      pred valid_Lucas_input_pred V,A,val,x0,y0,p0,q0,n0,d means ( Lucas_input (x0,y0,p0,q0,n0)) is_valid_input (V,A,val,d);

    end

    definition

      let V, A, x0, y0, p0, q0, n0;

      let val be FinSequence;

      defpred P[ object] means valid_Lucas_input_pred (V,A,val,x0,y0,p0,q0,n0,$1);

      :: NOMIN_9:def11

      func valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) -> SCPartialNominativePredicate of V, A equals ( valid_input (V,A,val,( Lucas_input (x0,y0,p0,q0,n0))));

      coherence ;

    end

    registration

      let V, A, x0, y0, p0, q0, n0;

      let val be FinSequence;

      cluster ( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)) -> total;

      coherence ;

    end

    definition

      let V, A, z, x0, y0, p0, q0, n0, d;

      :: NOMIN_9:def12

      pred valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0,d means <*( Lucas (x0,y0,p0,q0,n0))*> is_valid_output (V,A, <*z*>,d);

    end

    definition

      let V, A, z, x0, y0, p0, q0, n0;

      :: NOMIN_9:def13

      func valid_Lucas_output (A,z,x0,y0,p0,q0,n0) -> SCPartialNominativePredicate of V, A equals ( valid_output (V,A,z,( Lucas (x0,y0,p0,q0,n0))));

      coherence ;

    end

    definition

      let V, A, loc, x0, y0, p0, q0, n0, d;

      :: NOMIN_9:def14

      pred Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d means ex d1 be NonatomicND of V, A st d = d1 & {(loc /. 1), (loc /. 2), (loc /. 3), (loc /. 4), (loc /. 5), (loc /. 6), (loc /. 7), (loc /. 8), (loc /. 9), (loc /. 10)} c= ( dom d1) & (d1 . (loc /. 2)) = 1 & (d1 . (loc /. 3)) = n0 & (d1 . (loc /. 7)) = p0 & (d1 . (loc /. 8)) = q0 & ex I be Nat st I = (d1 . (loc /. 1)) & (d1 . (loc /. 4)) = ( Lucas (x0,y0,p0,q0,I)) & (d1 . (loc /. 5)) = ( Lucas (x0,y0,p0,q0,(I + 1)));

    end

    definition

      let V, A, loc, x0, y0, p0, q0, n0;

      defpred P[ object] means Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,$1);

      :: NOMIN_9:def15

      func Lucas_inv (A,loc,x0,y0,p0,q0,n0) -> SCPartialNominativePredicate of V, A means

      : Def15: ( dom it ) = ( ND (V,A)) & for d be object st d in ( dom it ) holds ( Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,d) implies (it . d) = TRUE ) & ( not Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,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, loc, x0, y0, p0, q0, n0;

      cluster ( Lucas_inv (A,loc,x0,y0,p0,q0,n0)) -> total;

      coherence by Def15;

    end

    theorem :: NOMIN_9:13

    

     Th13: for val be 10 -element FinSequence holds V is non empty & A is_without_nonatomicND_wrt V & ( Seg 10) c= ( dom loc) & (loc | ( Seg 10)) is one-to-one & (loc,val) are_different_wrt 10 implies ( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)) ||= (( SC_Psuperpos_Seq (loc,val,( Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . ( len ( SC_Psuperpos_Seq (loc,val,( Lucas_inv (A,loc,x0,y0,p0,q0,n0))))))

    proof

      let val be 10 -element FinSequence;

      set size = 10;

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

      set i1 = (val . 1), j1 = (val . 2), n1 = (val . 3), s1 = (val . 4), b1 = (val . 5), c1 = (val . 6);

      set p1 = (val . 7), q1 = (val . 8), ps1 = (val . 9), qc1 = (val . 10);

      set EN = {i1, j1, n1, s1, b1, c1, p1, q1, ps1, qc1};

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

      set I = ( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0));

      set inv = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set DS = ( denamingSeq (V,A,val));

      set SE = ( SC_Psuperpos_Seq (loc,val,inv));

      set Q1 = ( SC_Psuperpos ((SE . 8),(DS . 2),j));

      set P1 = ( SC_Psuperpos (Q1,(DS . 1),i));

      set inp = ( Lucas_input (x0,y0,p0,q0,n0));

      assume that

       A1: V is non empty and

       A2: A is_without_nonatomicND_wrt V and

       A3: ( Seg 10) c= ( dom loc) and

       A4: (loc | ( Seg 10)) is one-to-one and

       A5: (loc,val) are_different_wrt 10;

      

       A6: ( Seg 10) = ( dom val) by FINSEQ_1: 89;

      

       A7: ( len val) = 10 by CARD_1:def 7;

      

       A8: ( len SE) = ( len val) by NOMIN_8:def 9;

      

       A9: ( len inp) = 10 by CARD_1:def 7;

      

       A10: ( len DS) = 10 by NOMIN_8:def 8, A7;

      

       A11: (DS . 1) = ( denaming (V,A,(val . 1))) by NOMIN_8:def 8, A10;

      

       A12: (DS . 2) = ( denaming (V,A,(val . 2))) by NOMIN_8:def 8, A10;

      

       A13: (DS . 9) = ( denaming (V,A,(val . 9))) by NOMIN_8:def 8, A10;

      

       A14: (DS . 10) = ( denaming (V,A,(val . 10))) by NOMIN_8:def 8, A10;

      

       A15: (SE . (8 + 1)) = ( SC_Psuperpos ((SE . 8),( denaming (V,A,(val . (( len val) - 8)))),(loc /. (( len val) - 8)))) by A7, A8, NOMIN_8:def 9

      .= Q1 by NOMIN_8:def 8, A10, A7;

      

       A16: (SE . (9 + 1)) = ( SC_Psuperpos ((SE . 9),( denaming (V,A,(val . (( len val) - 9)))),(loc /. (( len val) - 9)))) by A7, A8, NOMIN_8:def 9

      .= P1 by NOMIN_8:def 8, A10, A7, A15;

      let d be Element of D;

      assume d in ( dom I) & (I . d) = TRUE ;

      then ( Lucas_input (x0,y0,p0,q0,n0)) is_valid_input (V,A,val,d) by NOMIN_8:def 11;

      then

      consider d1 be NonatomicND of V, A such that

       A17: d = d1 and

       A18: val is_valid_wrt d1 and

       A19: for n be Nat st 1 <= n <= ( len inp) holds (d1 . (val . n)) = (inp . n);

      

       A20: (d1 . i1) = (inp . 1) by A9, A19

      .= 0 ;

      

       A21: (d1 . j1) = (inp . 2) by A9, A19

      .= 1;

      

       A22: (d1 . n1) = (inp . 3) by A9, A19

      .= n0;

      

       A23: (d1 . s1) = (inp . 4) by A9, A19

      .= x0;

      

       A24: (d1 . b1) = (inp . 5) by A9, A19

      .= y0;

      

       A25: (d1 . p1) = (inp . 7) by A9, A19

      .= p0;

      

       A26: (d1 . q1) = (inp . 8) by A9, A19

      .= q0;

      set F = ( LocalOverlapSeq (A,loc,val,d1,size));

      

       A27: ( len F) = size by NOMIN_7:def 4;

      then

       A28: (loc,val,size) are_correct_wrt d1 by A1, A2, A6, A18, FINSEQ_1:def 3;

      

       A29: ( dom (DS . 1)) = { d where d be NonatomicND of V, A : i1 in ( dom d) } by A11, NOMIN_1:def 18;

      

       A30: ( dom P1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,((DS . 1) . d),i)) in ( dom Q1) & d in ( dom (DS . 1)) } by NOMIN_2:def 11;

      

       A31: ( dom Q1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,((DS . 2) . d),j)) in ( dom (SE . 8)) & d in ( dom (DS . 2)) } by NOMIN_2:def 11;

      1 in ( dom val) by A6;

      then i1 in ( rng val) by FUNCT_1:def 3;

      then

       A32: d1 in ( dom (DS . 1)) by A18, A29;

      

       A33: (F . 1) is NonatomicND of V, A by A27, NOMIN_7:def 6;

      reconsider Lqc = (F . 10) as NonatomicND of V, A by A27, NOMIN_7:def 6;

      

       A34: (F . 1) = ( local_overlapping (V,A,d1,((DS . 1) . d1),i)) by A11, NOMIN_7:def 4;

      

       A35: (F . (1 + 1)) = ( local_overlapping (V,A,(F . 1),((DS . 2) . (F . 1)),j)) by A12, A27, NOMIN_7:def 4;

      

       A36: (F . 1) in ( dom (DS . 2)) by A12, A27, A28, NOMIN_8: 15;

      

       A37: ( dom inv) = D by Def15;

      then

       A38: Lqc in ( dom inv);

      

       A39: ((size - 8) - 1) = 1;

      

       A40: (8 + 1) < size;

      ( local_overlapping (V,A,(F . (size - 1)),(( denaming (V,A,(val . ( len val)))) . (F . (size - 1))),(loc /. ( len val)))) in ( dom inv) by A37;

      then (F . 2) in ( dom (SE . 8)) by A12, A7, A28, A35, A39, A40, NOMIN_8: 16;

      then

       A41: (F . 1) in ( dom Q1) by A35, A31, A33, A36;

      hence d in ( dom (SE . ( len SE))) by A34, A17, A30, A32, A7, A8, A16;

      

       A42: Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,Lqc)

      proof

        take Lqc;

        thus Lqc = Lqc;

        thus {i, j, n, s, b, c, p, q, ps, qc} c= ( dom Lqc)

        proof

          

           A43: i in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A44: j in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A45: n in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A46: s in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A47: b in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A48: c in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A49: p in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A50: q in ( dom Lqc) by A28, NOMIN_7: 9;

          

           A51: ps in ( dom Lqc) by A28, NOMIN_7: 9;

          qc in ( dom Lqc) by A28, NOMIN_7: 9;

          hence {i, j, n, s, b, c, p, q, ps, qc} c= ( dom Lqc) by A43, A44, A45, A46, A47, A48, A49, A50, A51, ENUMSET1:def 8;

        end;

        

        thus (Lqc . j) = (d1 . j1) by A3, A4, A5, A28, NOMIN_7: 13

        .= 1 by A21;

        

        thus (Lqc . n) = (d1 . n1) by A3, A4, A5, A28, NOMIN_7: 13

        .= n0 by A22;

        

        thus (Lqc . p) = (d1 . p1) by A3, A4, A5, A28, NOMIN_7: 13

        .= p0 by A25;

        

        thus (Lqc . q) = (d1 . q1) by A3, A4, A5, A28, NOMIN_7: 13

        .= q0 by A26;

        take 0 ;

        

        thus (Lqc . i) = (d1 . i1) by A3, A4, A5, A28, NOMIN_7: 13

        .= 0 by A20;

        

        thus (Lqc . s) = (d1 . s1) by A3, A4, A5, A28, NOMIN_7: 13

        .= x0 by A23

        .= ( Lucas (x0,y0,p0,q0, 0 )) by Th5;

        

        thus (Lqc . b) = (d1 . b1) by A3, A4, A5, A28, NOMIN_7: 13

        .= y0 by A24

        .= ( Lucas (x0,y0,p0,q0,( 0 + 1))) by Th5;

      end;

      

       A52: (10 - 9) = 1 & (10 - 1) = 9;

      

       A53: (8 + 1) = 9 & 8 = (10 - 2);

      

       A54: ( local_overlapping (V,A,(F . 9),((DS . 10) . (F . 9)),qc)) in ( dom inv) by A37;

      set dy = ( local_overlapping (V,A,(F . 8),((DS . 9) . (F . 8)),ps));

      

       A55: ( local_overlapping (V,A,dy,((DS . 10) . dy),qc)) in ( dom inv) by A37;

      

      thus ((SE . ( len SE)) . d) = (Q1 . (F . 1)) by A11, A12, A14, A7, A15, A17, A28, A34, A41, A52, A53, A54, NOMIN_8: 19

      .= ((SE . 1) . (F . 9)) by A14, A7, A15, A28, A52, A54, NOMIN_8: 17

      .= (inv . Lqc) by A13, A14, A7, A28, A52, A53, A54, A55, NOMIN_8: 18

      .= TRUE by A38, A42, Def15;

    end;

    theorem :: NOMIN_9:14

    

     Th14: for val be 10 -element FinSequence holds V is non empty & A is_without_nonatomicND_wrt V & ( Seg 10) c= ( dom loc) & (loc | ( Seg 10)) is one-to-one & (loc,val) are_different_wrt 10 implies <*( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)), ( initial_assignments (A,loc,val,10)), ( Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of ( ND (V,A))

    proof

      let val be 10 -element FinSequence;

      set size = 10;

      set G = ( initial_assignments_Seq (A,loc,val,size));

      

       A1: (G . 1) = ( SC_assignment (( denaming (V,A,(val . 1))),(loc /. 1))) by NOMIN_7:def 8;

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

      set i1 = (val . 1), j1 = (val . 2), n1 = (val . 3), s1 = (val . 4), b1 = (val . 5), c1 = (val . 6);

      set p1 = (val . 7), q1 = (val . 8), ps1 = (val . 9), qc1 = (val . 10);

      set EN = {i1, j1, n1, s1, b1, c1, p1, q1, ps1, qc1};

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

      set I = ( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0));

      set inv = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set DS = ( denamingSeq (V,A,val));

      set asi = ( SC_assignment ((DS . 1),i));

      set asj = ( SC_assignment ((DS . 2),j));

      set asn = ( SC_assignment ((DS . 3),n));

      set ass = ( SC_assignment ((DS . 4),s));

      set asb = ( SC_assignment ((DS . 5),b));

      set asc = ( SC_assignment ((DS . 6),c));

      set asp = ( SC_assignment ((DS . 7),p));

      set asq = ( SC_assignment ((DS . 8),q));

      set asps = ( SC_assignment ((DS . 9),ps));

      set asqc = ( SC_assignment ((DS . 10),qc));

      set SE = ( SC_Psuperpos_Seq (loc,val,inv));

      assume that

       A2: V is non empty and

       A3: A is_without_nonatomicND_wrt V and

       A4: ( Seg 10) c= ( dom loc) and

       A5: (loc | ( Seg 10)) is one-to-one and

       A6: (loc,val) are_different_wrt 10;

      

       A7: ( len val) = 10 by CARD_1:def 7;

      

       A8: ( len SE) = 10 by NOMIN_8:def 9, A7;

      

       A9: ( len DS) = 10 by NOMIN_8:def 8, A7;

      

       A10: 2 = (1 + 1) & 3 = (2 + 1) & 4 = (3 + 1) & 5 = (4 + 1) & 6 = (5 + 1) & 7 = (6 + 1) & 8 = (7 + 1) & 9 = (8 + 1) & 10 = (9 + 1);

      

       A11: (SE . 1) = ( SC_Psuperpos (inv,( denaming (V,A,(val . ( len val)))),(loc /. ( len val)))) by NOMIN_8:def 9;

      

       A12: (SE . 2) = ( SC_Psuperpos ((SE . 1),( denaming (V,A,(val . (( len val) - 1)))),(loc /. (( len val) - 1)))) by A10, A8, NOMIN_8:def 9;

      

       A13: (SE . 3) = ( SC_Psuperpos ((SE . 2),( denaming (V,A,(val . (( len val) - 2)))),(loc /. (( len val) - 2)))) by A10, A8, NOMIN_8:def 9;

      

       A14: (SE . 4) = ( SC_Psuperpos ((SE . 3),( denaming (V,A,(val . (( len val) - 3)))),(loc /. (( len val) - 3)))) by A10, A8, NOMIN_8:def 9;

      

       A15: (SE . 5) = ( SC_Psuperpos ((SE . 4),( denaming (V,A,(val . (( len val) - 4)))),(loc /. (( len val) - 4)))) by A10, A8, NOMIN_8:def 9;

      

       A16: (SE . 6) = ( SC_Psuperpos ((SE . 5),( denaming (V,A,(val . (( len val) - 5)))),(loc /. (( len val) - 5)))) by A10, A8, NOMIN_8:def 9;

      

       A17: (SE . 7) = ( SC_Psuperpos ((SE . 6),( denaming (V,A,(val . (( len val) - 6)))),(loc /. (( len val) - 6)))) by A10, A8, NOMIN_8:def 9;

      

       A18: (SE . 8) = ( SC_Psuperpos ((SE . 7),( denaming (V,A,(val . (( len val) - 7)))),(loc /. (( len val) - 7)))) by A10, A8, NOMIN_8:def 9;

      

       A19: (SE . 9) = ( SC_Psuperpos ((SE . 8),( denaming (V,A,(val . (( len val) - 8)))),(loc /. (( len val) - 8)))) by A10, A8, NOMIN_8:def 9;

      

       A20: (SE . 10) = ( SC_Psuperpos ((SE . 9),( denaming (V,A,(val . (( len val) - 9)))),(loc /. (( len val) - 9)))) by A10, A8, NOMIN_8:def 9;

      

       A21: (DS . 1) = ( denaming (V,A,(val . 1))) by NOMIN_8:def 8, A9;

      

       A22: (DS . 2) = ( denaming (V,A,(val . 2))) by NOMIN_8:def 8, A9;

      

       A23: (DS . 3) = ( denaming (V,A,(val . 3))) by NOMIN_8:def 8, A9;

      

       A24: (DS . 4) = ( denaming (V,A,(val . 4))) by NOMIN_8:def 8, A9;

      

       A25: (DS . 5) = ( denaming (V,A,(val . 5))) by NOMIN_8:def 8, A9;

      

       A26: (DS . 6) = ( denaming (V,A,(val . 6))) by NOMIN_8:def 8, A9;

      

       A27: (DS . 7) = ( denaming (V,A,(val . 7))) by NOMIN_8:def 8, A9;

      

       A28: (DS . 8) = ( denaming (V,A,(val . 8))) by NOMIN_8:def 8, A9;

      

       A29: (DS . 9) = ( denaming (V,A,(val . 9))) by NOMIN_8:def 8, A9;

      

       A30: (DS . 10) = ( denaming (V,A,(val . 10))) by NOMIN_8:def 8, A9;

      

       A31: <*(SE . 1), asqc, inv*> is SFHT of D by A7, A11, A30, NOMIN_3: 29;

      

       A32: <*(SE . 2), asps, (SE . 1)*> is SFHT of D by A7, A12, A29, NOMIN_3: 29;

      

       A33: <*(SE . 3), asq, (SE . 2)*> is SFHT of D by A7, A13, A28, NOMIN_3: 29;

      

       A34: <*(SE . 4), asp, (SE . 3)*> is SFHT of D by A7, A14, A27, NOMIN_3: 29;

      

       A35: <*(SE . 5), asc, (SE . 4)*> is SFHT of D by A7, A15, A26, NOMIN_3: 29;

      

       A36: <*(SE . 6), asb, (SE . 5)*> is SFHT of D by A7, A16, A25, NOMIN_3: 29;

      

       A37: <*(SE . 7), ass, (SE . 6)*> is SFHT of D by A7, A17, A24, NOMIN_3: 29;

      

       A38: <*(SE . 8), asn, (SE . 7)*> is SFHT of D by A7, A18, A23, NOMIN_3: 29;

      

       A39: <*(SE . 9), asj, (SE . 8)*> is SFHT of D by A7, A19, A22, NOMIN_3: 29;

      

       A40: <*(SE . 10), asi, (SE . 9)*> is SFHT of D by A7, A20, A21, NOMIN_3: 29;

      

       A41: (G . 2) = ( PP_composition (asi,asj)) by A10, A21, A22, A1, NOMIN_7:def 8;

      

       A42: (G . 3) = ( PP_composition ((G . 2),asn)) by A10, A23, NOMIN_7:def 8;

      

       A43: (G . 4) = ( PP_composition ((G . 3),ass)) by A10, A24, NOMIN_7:def 8;

      

       A44: (G . 5) = ( PP_composition ((G . 4),asb)) by A10, A25, NOMIN_7:def 8;

      

       A45: (G . 6) = ( PP_composition ((G . 5),asc)) by A10, A26, NOMIN_7:def 8;

      

       A46: (G . 7) = ( PP_composition ((G . 6),asp)) by A10, A27, NOMIN_7:def 8;

      

       A47: (G . 8) = ( PP_composition ((G . 7),asq)) by A10, A28, NOMIN_7:def 8;

      

       A48: (G . 9) = ( PP_composition ((G . 8),asps)) by A10, A29, NOMIN_7:def 8;

      

       A49: ( initial_assignments (A,loc,val,10)) = ( PP_composition (asi,asj,asn,ass,asb,asc,asp,asq,asps,asqc)) by A10, A30, A41, A42, A43, A44, A45, A46, A47, A48, NOMIN_7:def 8;

      I ||= (SE . 10) by A2, A3, A4, A5, A6, A8, Th13;

      then

       A50: <*I, asi, (SE . 9)*> is SFHT of D by A40, NOMIN_3: 15;

      

       A51: <*( PP_inversion (SE . 9)), asj, (SE . 8)*> is SFHT of D by A7, A19, A22, NOMIN_4: 16;

      

       A52: <*( PP_inversion (SE . 8)), asn, (SE . 7)*> is SFHT of D by A7, A18, A23, NOMIN_4: 16;

      

       A53: <*( PP_inversion (SE . 7)), ass, (SE . 6)*> is SFHT of D by A7, A17, A24, NOMIN_4: 16;

      

       A54: <*( PP_inversion (SE . 6)), asb, (SE . 5)*> is SFHT of D by A7, A16, A25, NOMIN_4: 16;

      

       A55: <*( PP_inversion (SE . 5)), asc, (SE . 4)*> is SFHT of D by A7, A15, A26, NOMIN_4: 16;

      

       A56: <*( PP_inversion (SE . 4)), asp, (SE . 3)*> is SFHT of D by A7, A14, A27, NOMIN_4: 16;

      

       A57: <*( PP_inversion (SE . 3)), asq, (SE . 2)*> is SFHT of D by A7, A13, A28, NOMIN_4: 16;

      

       A58: <*( PP_inversion (SE . 2)), asps, (SE . 1)*> is SFHT of D by A7, A12, A29, NOMIN_4: 16;

       <*( PP_inversion (SE . 1)), asqc, inv*> is SFHT of D by A7, A11, A30, NOMIN_4: 16;

      hence thesis by A49, A32, A31, A33, A34, A35, A36, A37, A38, A39, A50, A51, A52, A53, A54, A55, A56, A57, A58, NOMIN_8: 4;

    end;

    theorem :: NOMIN_9:15

    

     Th15: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & d1 in ( dom ( Lucas_loop_body (A,loc))) & loc is_valid_wrt d1 & ( Seg 10) c= ( dom loc) & (for T holds (loc /. 1) is_a_value_on T & (loc /. 2) is_a_value_on T & (loc /. 4) is_a_value_on T & (loc /. 6) is_a_value_on T & (loc /. 7) is_a_value_on T & (loc /. 8) is_a_value_on T & (loc /. 9) is_a_value_on T & (loc /. 10) is_a_value_on T) implies prg_doms_of (loc,d1, <*( denaming (V,A,(loc /. 4))), ( denaming (V,A,(loc /. 5))), ( multiplication (A,(loc /. 7),(loc /. 4))), ( multiplication (A,(loc /. 8),(loc /. 6))), ( subtraction (A,(loc /. 9),(loc /. 10))), ( addition (A,(loc /. 1),(loc /. 2)))*>, <*6, 4, 9, 10, 5, 1*>)

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

      set B = ( Lucas_loop_body (A,loc));

      assume that

       A1: V is non empty and

       A2: A is complex-containing and

       A3: A is_without_nonatomicND_wrt V and

       A4: d1 in ( dom B) and

       A5: loc is_valid_wrt d1 and

       A6: ( Seg 10) c= ( dom loc) and

       A7: for T holds i is_a_value_on T & j is_a_value_on T & s is_a_value_on T & c is_a_value_on T & p is_a_value_on T & q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T;

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

      set EN = {i, j, n, s, b, c, p, q, ps, qc};

      set Di = ( denaming (V,A,i));

      set Dj = ( denaming (V,A,j));

      set Dn = ( denaming (V,A,n));

      set Ds = ( denaming (V,A,s));

      set Db = ( denaming (V,A,b));

      set Dc = ( denaming (V,A,c));

      set Dp = ( denaming (V,A,p));

      set Dq = ( denaming (V,A,q));

      set Dps = ( denaming (V,A,ps));

      set Dqc = ( denaming (V,A,qc));

      set Aij = ( addition (A,i,j));

      set Mps = ( multiplication (A,p,s));

      set Mqc = ( multiplication (A,q,c));

      set Scs = ( subtraction (A,ps,qc));

      set AS1 = ( SC_assignment (Ds,c));

      set AS2 = ( SC_assignment (Db,s));

      set AS3 = ( SC_assignment (Mps,ps));

      set AS4 = ( SC_assignment (Mqc,qc));

      set AS5 = ( SC_assignment (Scs,b));

      set AS6 = ( SC_assignment (Aij,i));

      set prg = <*Ds, Db, Mps, Mqc, Scs, Aij*>;

      set pos = <*6, 4, 9, 10, 5, 1*>;

      set PS = ( PrgLocalOverlapSeq (A,loc,d1,prg,pos));

      

       A8: EN c= ( dom d1) by A5, A6, Th12;

      

       A9: i in EN by ENUMSET1:def 8;

      

       A10: j in EN by ENUMSET1:def 8;

      

       A11: b in EN by ENUMSET1:def 8;

      

       A12: p in EN by ENUMSET1:def 8;

      

       A13: q in EN by ENUMSET1:def 8;

      

       A14: ( len prg) = 6 by AOFA_A00: 20;

      

       A15: ( len PS) = ( len prg) by NOMIN_8:def 14;

      

       A16: (prg . 1) = Ds & (pos . 1) = 6;

      

       A17: (prg . 2) = Db & (pos . 2) = 4;

      

       A18: (prg . 3) = Mps & (pos . 3) = 9;

      

       A19: (prg . 4) = Mqc & (pos . 4) = 10;

      

       A20: (prg . 5) = Scs & (pos . 5) = 5;

      

       A21: ( dom AS1) = ( dom Ds) by NOMIN_2:def 7;

      

       A22: ( dom AS2) = ( dom Db) by NOMIN_2:def 7;

      ( PP_composition (( PP_composition (( PP_composition (( PP_composition (AS1,AS2)),AS3)),AS4)),AS5)) = ( PP_composition (( PP_composition (( PP_composition ((AS2 * AS1),AS3)),AS4)),AS5)) by PARTPR_2:def 1

      .= ( PP_composition (( PP_composition ((AS3 * (AS2 * AS1)),AS4)),AS5)) by PARTPR_2:def 1

      .= ( PP_composition ((AS4 * (AS3 * (AS2 * AS1))),AS5)) by PARTPR_2:def 1

      .= (AS5 * (AS4 * (AS3 * (AS2 * AS1)))) by PARTPR_2:def 1;

      then

       A23: B = (AS6 * (AS5 * (AS4 * (AS3 * (AS2 * AS1))))) by PARTPR_2:def 1;

      

       A24: ((((AS5 * AS4) * AS3) * AS2) * AS1) = (((AS5 * AS4) * AS3) * (AS2 * AS1)) by RELAT_1: 36

      .= ((AS5 * AS4) * (AS3 * (AS2 * AS1))) by RELAT_1: 36

      .= (AS5 * (AS4 * (AS3 * (AS2 * AS1)))) by RELAT_1: 36;

      

       A25: (AS5 * (AS4 * (AS3 * (AS2 * AS1)))) = (AS5 * ((AS4 * AS3) * (AS2 * AS1))) by RELAT_1: 36

      .= (AS5 * (((AS4 * AS3) * AS2) * AS1)) by RELAT_1: 36;

      

       A26: (((AS4 * AS3) * AS2) * AS1) = ((AS4 * AS3) * (AS2 * AS1)) by RELAT_1: 36

      .= (AS4 * (AS3 * (AS2 * AS1))) by RELAT_1: 36;

      

       A27: (AS4 * (AS3 * (AS2 * AS1))) = (AS4 * ((AS3 * AS2) * AS1)) by RELAT_1: 36;

      

       A28: ((AS3 * AS2) * AS1) = (AS3 * (AS2 * AS1)) by RELAT_1: 36;

      B = (AS6 * ((AS5 * AS4) * (AS3 * (AS2 * AS1)))) by A23, RELAT_1: 36

      .= (AS6 * (((AS5 * AS4) * AS3) * (AS2 * AS1))) by RELAT_1: 36

      .= (AS6 * ((((AS5 * AS4) * AS3) * AS2) * AS1)) by RELAT_1: 36;

      then

       A29: d1 in ( dom ((((AS5 * AS4) * AS3) * AS2) * AS1)) by A4, FUNCT_1: 11;

      then d1 in ( dom (((AS4 * AS3) * AS2) * AS1)) by A24, A25, FUNCT_1: 11;

      then d1 in ( dom ((AS3 * AS2) * AS1)) by A26, A27, FUNCT_1: 11;

      then

       A30: d1 in ( dom (AS2 * AS1)) by A28, FUNCT_1: 11;

      

       A31: ( dom Di) = { d where d be NonatomicND of V, A : i in ( dom d) } by NOMIN_1:def 18;

      

       A32: ( dom Dj) = { d where d be NonatomicND of V, A : j in ( dom d) } by NOMIN_1:def 18;

      

       A33: ( dom Ds) = { d where d be NonatomicND of V, A : s in ( dom d) } by NOMIN_1:def 18;

      

       A34: ( dom Db) = { d where d be NonatomicND of V, A : b in ( dom d) } by NOMIN_1:def 18;

      

       A35: ( dom Dc) = { d where d be NonatomicND of V, A : c in ( dom d) } by NOMIN_1:def 18;

      

       A36: ( dom Dp) = { d where d be NonatomicND of V, A : p in ( dom d) } by NOMIN_1:def 18;

      

       A37: ( dom Dq) = { d where d be NonatomicND of V, A : q in ( dom d) } by NOMIN_1:def 18;

      

       A38: ( dom Dps) = { d where d be NonatomicND of V, A : ps in ( dom d) } by NOMIN_1:def 18;

      

       A39: ( dom Dqc) = { d where d be NonatomicND of V, A : qc in ( dom d) } by NOMIN_1:def 18;

      

       A40: d1 in ( dom Ds) by A21, A29, FUNCT_1: 11;

      then

      reconsider Ad = (Ds . d1) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

      reconsider L1 = ( local_overlapping (V,A,d1,Ad,c)) as NonatomicND of V, A by NOMIN_2: 9;

      (AS1 . d1) = L1 by A21, A40, NOMIN_2:def 7;

      then L1 in ( dom AS2) by A30, FUNCT_1: 11;

      then

      reconsider DbL1 = (Db . L1) as TypeSCNominativeData of V, A by A22, PARTFUN1: 4, NOMIN_1: 39;

      reconsider L2 = ( local_overlapping (V,A,L1,DbL1,s)) as NonatomicND of V, A by NOMIN_2: 9;

      

       A41: ( dom L1) = ( {c} \/ ( dom d1)) by A3, A1, NOMIN_4: 4;

      

       A42: ( dom L2) = ( {s} \/ ( dom L1)) by A3, A1, NOMIN_4: 4;

      s in {s} by TARSKI:def 1;

      then s in ( dom L2) by A42, XBOOLE_0:def 3;

      then

       A43: L2 in ( dom Ds) by A33;

      p in ( dom L1) by A8, A12, A41, XBOOLE_0:def 3;

      then p in ( dom L2) by A42, XBOOLE_0:def 3;

      then L2 in ( dom Dp) by A36;

      then L2 in (( dom Ds) /\ ( dom Dp)) by A43, XBOOLE_0:def 4;

      then

       A44: L2 in ( dom <:Dp, Ds:>) by FUNCT_3:def 7;

      then

       A45: ( <:Dp, Ds:> . L2) = [(Dp . L2), (Ds . L2)] by FUNCT_3:def 7;

      

       A46: ( dom ( multiplication A)) = [:A, A:] by A2, FUNCT_2:def 1;

      p is_a_value_on L2 & s is_a_value_on L2 by A7;

      then [(Dp . L2), (Ds . L2)] in [:A, A:] by ZFMISC_1: 87;

      then

       A47: L2 in ( dom Mps) by A44, A46, A45, FUNCT_1: 11;

      then

      reconsider MpsL2 = (Mps . L2) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

      reconsider L3 = ( local_overlapping (V,A,L2,MpsL2,ps)) as NonatomicND of V, A by NOMIN_2: 9;

      

       A48: ( dom L3) = ( {ps} \/ ( dom L2)) by A1, A3, NOMIN_4: 4;

      q in ( dom L1) by A8, A13, A41, XBOOLE_0:def 3;

      then q in ( dom L2) by A42, XBOOLE_0:def 3;

      then

       A49: q in ( dom L3) by A48, XBOOLE_0:def 3;

      c in {c} by TARSKI:def 1;

      then c in ( dom L1) by A41, XBOOLE_0:def 3;

      then c in ( dom L2) by A42, XBOOLE_0:def 3;

      then

       A50: c in ( dom L3) by A48, XBOOLE_0:def 3;

      

       A51: L3 in ( dom Dq) by A49, A37;

      L3 in ( dom Dc) by A50, A35;

      then L3 in (( dom Dq) /\ ( dom Dc)) by A51, XBOOLE_0:def 4;

      then

       A52: L3 in ( dom <:Dq, Dc:>) by FUNCT_3:def 7;

      then

       A53: ( <:Dq, Dc:> . L3) = [(Dq . L3), (Dc . L3)] by FUNCT_3:def 7;

      q is_a_value_on L3 & c is_a_value_on L3 by A7;

      then [(Dq . L3), (Dc . L3)] in [:A, A:] by ZFMISC_1: 87;

      then

       A54: L3 in ( dom Mqc) by A52, A46, A53, FUNCT_1: 11;

      then

      reconsider MqcL3 = (Mqc . L3) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

      reconsider L4 = ( local_overlapping (V,A,L3,MqcL3,qc)) as NonatomicND of V, A by NOMIN_2: 9;

      

       A55: ( dom L4) = ( {qc} \/ ( dom L3)) by A1, A3, NOMIN_4: 4;

      qc in {qc} by TARSKI:def 1;

      then

       A56: qc in ( dom L4) by A55, XBOOLE_0:def 3;

      ps in {ps} by TARSKI:def 1;

      then ps in ( dom L3) by A48, XBOOLE_0:def 3;

      then

       A57: ps in ( dom L4) by A55, XBOOLE_0:def 3;

      

       A58: b in ( dom L1) by A8, A11, A41, XBOOLE_0:def 3;

      

       A59: L4 in ( dom Dps) by A57, A38;

      L4 in ( dom Dqc) by A56, A39;

      then L4 in (( dom Dps) /\ ( dom Dqc)) by A59, XBOOLE_0:def 4;

      then

       A60: L4 in ( dom <:Dps, Dqc:>) by FUNCT_3:def 7;

      then

       A61: ( <:Dps, Dqc:> . L4) = [(Dps . L4), (Dqc . L4)] by FUNCT_3:def 7;

      

       A62: ( dom ( subtraction A)) = [:A, A:] by A2, FUNCT_2:def 1;

      ps is_a_value_on L4 & qc is_a_value_on L4 by A7;

      then [(Dps . L4), (Dqc . L4)] in [:A, A:] by ZFMISC_1: 87;

      then

       A63: L4 in ( dom Scs) by A60, A62, A61, FUNCT_1: 11;

      then

      reconsider ScsL4 = (Scs . L4) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

      reconsider L5 = ( local_overlapping (V,A,L4,ScsL4,b)) as NonatomicND of V, A by NOMIN_2: 9;

      

       A64: ( dom L5) = ( {b} \/ ( dom L4)) by A1, A3, NOMIN_4: 4;

      i in ( dom L1) by A8, A9, A41, XBOOLE_0:def 3;

      then i in ( dom L2) by A42, XBOOLE_0:def 3;

      then i in ( dom L3) by A48, XBOOLE_0:def 3;

      then i in ( dom L4) by A55, XBOOLE_0:def 3;

      then i in ( dom L5) by A64, XBOOLE_0:def 3;

      then

       A65: L5 in ( dom Di) by A31;

      j in ( dom L1) by A8, A10, A41, XBOOLE_0:def 3;

      then j in ( dom L2) by A42, XBOOLE_0:def 3;

      then j in ( dom L3) by A48, XBOOLE_0:def 3;

      then j in ( dom L4) by A55, XBOOLE_0:def 3;

      then j in ( dom L5) by A64, XBOOLE_0:def 3;

      then

       A66: L5 in ( dom Dj) by A32;

      L5 in (( dom Di) /\ ( dom Dj)) by A65, A66, XBOOLE_0:def 4;

      then

       A67: L5 in ( dom <:Di, Dj:>) by FUNCT_3:def 7;

      then

       A68: ( <:Di, Dj:> . L5) = [(Di . L5), (Dj . L5)] by FUNCT_3:def 7;

      

       A69: ( dom ( addition A)) = [:A, A:] by A2, FUNCT_2:def 1;

      i is_a_value_on L5 & j is_a_value_on L5 by A7;

      then [(Di . L5), (Dj . L5)] in [:A, A:] by ZFMISC_1: 87;

      then

       A70: L5 in ( dom Aij) by A69, A67, A68, FUNCT_1: 11;

      

       A71: 2 = (1 + 1) & 3 = (2 + 1) & 4 = (3 + 1) & 5 = (4 + 1) & 6 = (5 + 1);

      

       A72: (PS . 1) = L1 by A14, A16, NOMIN_8:def 14;

      

       A73: (PS . 2) = L2 by A71, A14, A15, A17, A72, NOMIN_8:def 14;

      

       A74: (PS . 3) = L3 by A71, A14, A15, A18, A73, NOMIN_8:def 14;

      

       A75: (PS . 4) = L4 by A71, A14, A15, A19, A74, NOMIN_8:def 14;

      let y be Nat;

      assume

       A76: 1 <= y;

      assume y < ( len prg);

      then ((y + 1) - 1) <= (6 - 1) by A14, NAT_1: 13;

      then y = (1 + 0 ) or ... or y = (1 + 4) by A76, NAT_1: 62;

      per cases ;

        suppose y = 1;

        hence thesis by A72, A34, A58;

      end;

        suppose y = 2;

        hence thesis by A47, A71, A14, A15, A17, A72, NOMIN_8:def 14;

      end;

        suppose y = 3;

        hence thesis by A54, A71, A14, A15, A18, A73, NOMIN_8:def 14;

      end;

        suppose y = 4;

        hence thesis by A63, A71, A14, A15, A19, A74, NOMIN_8:def 14;

      end;

        suppose y = 5;

        hence thesis by A70, A71, A14, A15, A20, A75, NOMIN_8:def 14;

      end;

    end;

    theorem :: NOMIN_9:16

    

     Th16: for V be non empty set holds for loc be V -valued10 -element FinSequence holds A is complex-containing & A is_without_nonatomicND_wrt V & (for T be TypeSCNominativeData of V, A holds (loc /. 1) is_a_value_on T & (loc /. 2) is_a_value_on T & (loc /. 4) is_a_value_on T & (loc /. 6) is_a_value_on T & (loc /. 7) is_a_value_on T & (loc /. 8) is_a_value_on T & (loc /. 9) is_a_value_on T & (loc /. 10) is_a_value_on T) & loc is one-to-one implies <*( Lucas_inv (A,loc,x0,y0,p0,q0,n0)), ( Lucas_loop_body (A,loc)), ( Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of ( ND (V,A))

    proof

      let V be non empty set;

      let loc be V -valued10 -element FinSequence;

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

      assume that

       A1: A is complex-containing and

       A2: A is_without_nonatomicND_wrt V and

       A3: for T be TypeSCNominativeData of V, A holds i is_a_value_on T & j is_a_value_on T & s is_a_value_on T & c is_a_value_on T & p is_a_value_on T & q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T;

      assume

       A4: loc is one-to-one;

      

       A5: ( Seg 10) = ( dom loc) by FINSEQ_1: 89;

      

       A6: (loc | ( Seg 10)) = loc;

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

      set EN = {i, j, n, s, b, c, p, q, ps, qc};

      set inv = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set B = ( Lucas_loop_body (A,loc));

      set Di = ( denaming (V,A,i));

      set Dj = ( denaming (V,A,j));

      set Dn = ( denaming (V,A,n));

      set Ds = ( denaming (V,A,s));

      set Db = ( denaming (V,A,b));

      set Dc = ( denaming (V,A,c));

      set Dp = ( denaming (V,A,p));

      set Dq = ( denaming (V,A,q));

      set Dps = ( denaming (V,A,ps));

      set Dqc = ( denaming (V,A,qc));

      set Aij = ( addition (A,i,j));

      set Mps = ( multiplication (A,p,s));

      set Mqc = ( multiplication (A,q,c));

      set Scs = ( subtraction (A,ps,qc));

      set AS1 = ( SC_assignment (Ds,c));

      set AS2 = ( SC_assignment (Db,s));

      set AS3 = ( SC_assignment (Mps,ps));

      set AS4 = ( SC_assignment (Mqc,qc));

      set AS5 = ( SC_assignment (Scs,b));

      set AS6 = ( SC_assignment (Aij,i));

      now

        let d be TypeSCNominativeData of V, A such that

         A7: d in ( dom inv) and

         A8: (inv . d) = TRUE and

         A9: d in ( dom B) and

         A10: (B . d) in ( dom inv);

         Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,d) by A7, A8, Def15;

        then

        consider d1 be NonatomicND of V, A such that

         A11: d = d1 and

         A12: EN c= ( dom d1) and

         A13: (d1 . j) = 1 and

         A14: (d1 . n) = n0 and

         A15: (d1 . p) = p0 and

         A16: (d1 . q) = q0 and

         A17: ex I be Nat st I = (d1 . i) & (d1 . s) = ( Lucas (x0,y0,p0,q0,I)) & (d1 . b) = ( Lucas (x0,y0,p0,q0,(I + 1)));

        

         A18: i in EN by ENUMSET1:def 8;

        

         A19: j in EN by ENUMSET1:def 8;

        

         A20: n in EN by ENUMSET1:def 8;

        

         A21: s in EN by ENUMSET1:def 8;

        

         A22: b in EN by ENUMSET1:def 8;

        

         A23: p in EN by ENUMSET1:def 8;

        

         A24: q in EN by ENUMSET1:def 8;

        consider I be Nat such that

         A25: I = (d1 . i) and

         A26: (d1 . s) = ( Lucas (x0,y0,p0,q0,I)) and

         A27: (d1 . b) = ( Lucas (x0,y0,p0,q0,(I + 1))) by A17;

        set prg = <*Ds, Db, Mps, Mqc, Scs, Aij*>;

        set pos = <*6, 4, 9, 10, 5, 1*>;

        reconsider prg as non empty( FPrg ( ND (V,A))) -valued FinSequence;

        set PS = ( PrgLocalOverlapSeq (A,loc,d1,prg,pos));

        

         A28: ( len prg) = 6 by AOFA_A00: 20;

        

         A29: ( len PS) = ( len prg) by NOMIN_8:def 14;

        

         A30: (prg . 1) = Ds & (pos . 1) = 6;

        

         A31: (prg . 2) = Db & (pos . 2) = 4;

        

         A32: (prg . 3) = Mps & (pos . 3) = 9;

        

         A33: (prg . 4) = Mqc & (pos . 4) = 10;

        

         A34: (prg . 5) = Scs & (pos . 5) = 5;

        

         A35: (prg . 6) = Aij & (pos . 6) = 1;

        ( rng loc) c= EN

        proof

          let y be object;

          assume y in ( rng loc);

          then

          consider w be object such that

           A36: w in ( dom loc) and

           A37: (loc . w) = y by FUNCT_1:def 3;

          

           A38: w = 1 or ... or w = 10 by A5, A36, FINSEQ_1: 91;

          1 in ( Seg 10) & ... & 10 in ( Seg 10);

          then (loc . 1) = (loc /. 1) & ... & (loc . 10) = (loc /. 10) by A5, PARTFUN1:def 6;

          hence thesis by A37, A38, ENUMSET1:def 8;

        end;

        then ( rng loc) c= ( dom d1) by A12;

        then

         A39: loc is_valid_wrt d1;

        

         A40: ( dom AS1) = ( dom Ds) by NOMIN_2:def 7;

        

         A41: ( dom AS2) = ( dom Db) by NOMIN_2:def 7;

        ( PP_composition (( PP_composition (( PP_composition (( PP_composition (AS1,AS2)),AS3)),AS4)),AS5)) = ( PP_composition (( PP_composition (( PP_composition ((AS2 * AS1),AS3)),AS4)),AS5)) by PARTPR_2:def 1

        .= ( PP_composition (( PP_composition ((AS3 * (AS2 * AS1)),AS4)),AS5)) by PARTPR_2:def 1

        .= ( PP_composition ((AS4 * (AS3 * (AS2 * AS1))),AS5)) by PARTPR_2:def 1

        .= (AS5 * (AS4 * (AS3 * (AS2 * AS1)))) by PARTPR_2:def 1;

        then

         A42: B = (AS6 * (AS5 * (AS4 * (AS3 * (AS2 * AS1))))) by PARTPR_2:def 1;

        

         A43: ((((AS5 * AS4) * AS3) * AS2) * AS1) = (((AS5 * AS4) * AS3) * (AS2 * AS1)) by RELAT_1: 36

        .= ((AS5 * AS4) * (AS3 * (AS2 * AS1))) by RELAT_1: 36

        .= (AS5 * (AS4 * (AS3 * (AS2 * AS1)))) by RELAT_1: 36;

        

         A44: (AS5 * (AS4 * (AS3 * (AS2 * AS1)))) = (AS5 * ((AS4 * AS3) * (AS2 * AS1))) by RELAT_1: 36

        .= (AS5 * (((AS4 * AS3) * AS2) * AS1)) by RELAT_1: 36;

        

         A45: (((AS4 * AS3) * AS2) * AS1) = ((AS4 * AS3) * (AS2 * AS1)) by RELAT_1: 36

        .= (AS4 * (AS3 * (AS2 * AS1))) by RELAT_1: 36;

        

         A46: (AS4 * (AS3 * (AS2 * AS1))) = (AS4 * ((AS3 * AS2) * AS1)) by RELAT_1: 36;

        

         A47: ((AS3 * AS2) * AS1) = (AS3 * (AS2 * AS1)) by RELAT_1: 36;

        B = (AS6 * ((AS5 * AS4) * (AS3 * (AS2 * AS1)))) by A42, RELAT_1: 36

        .= (AS6 * (((AS5 * AS4) * AS3) * (AS2 * AS1))) by RELAT_1: 36

        .= (AS6 * ((((AS5 * AS4) * AS3) * AS2) * AS1)) by RELAT_1: 36;

        then

         A48: d in ( dom ((((AS5 * AS4) * AS3) * AS2) * AS1)) by A9, FUNCT_1: 11;

        then

         A49: d in ( dom (((AS4 * AS3) * AS2) * AS1)) by A43, A44, FUNCT_1: 11;

        then d in ( dom ((AS3 * AS2) * AS1)) by A45, A46, FUNCT_1: 11;

        then

         A50: d in ( dom (AS2 * AS1)) by A47, FUNCT_1: 11;

        then

         A51: ((AS2 * AS1) . d) = (AS2 . (AS1 . d)) by FUNCT_1: 12;

        

         A52: ( dom Di) = { d where d be NonatomicND of V, A : i in ( dom d) } by NOMIN_1:def 18;

        

         A53: ( dom Dj) = { d where d be NonatomicND of V, A : j in ( dom d) } by NOMIN_1:def 18;

        

         A54: ( dom Ds) = { d where d be NonatomicND of V, A : s in ( dom d) } by NOMIN_1:def 18;

        

         A55: ( dom Db) = { d where d be NonatomicND of V, A : b in ( dom d) } by NOMIN_1:def 18;

        

         A56: ( dom Dc) = { d where d be NonatomicND of V, A : c in ( dom d) } by NOMIN_1:def 18;

        

         A57: ( dom Dp) = { d where d be NonatomicND of V, A : p in ( dom d) } by NOMIN_1:def 18;

        

         A58: ( dom Dq) = { d where d be NonatomicND of V, A : q in ( dom d) } by NOMIN_1:def 18;

        

         A59: ( dom Dps) = { d where d be NonatomicND of V, A : ps in ( dom d) } by NOMIN_1:def 18;

        

         A60: ( dom Dqc) = { d where d be NonatomicND of V, A : qc in ( dom d) } by NOMIN_1:def 18;

        

         A61: d in ( dom AS1) by A48, FUNCT_1: 11;

        then

        reconsider Ad = (Ds . d1) as TypeSCNominativeData of V, A by A40, A11, PARTFUN1: 4, NOMIN_1: 39;

        reconsider L1 = ( local_overlapping (V,A,d1,Ad,c)) as NonatomicND of V, A by NOMIN_2: 9;

        

         A62: (PS . 1) = L1 by A28, A30, NOMIN_8:def 14;

        

         A63: (AS1 . d) = L1 by A11, A61, NOMIN_2:def 7;

        then

         A64: L1 in ( dom AS2) by A50, FUNCT_1: 11;

        then

        reconsider DbL1 = (Db . L1) as TypeSCNominativeData of V, A by A41, PARTFUN1: 4, NOMIN_1: 39;

        reconsider L2 = ( local_overlapping (V,A,L1,DbL1,s)) as NonatomicND of V, A by NOMIN_2: 9;

        

         A65: 2 = (1 + 1) & 3 = (2 + 1) & 4 = (3 + 1) & 5 = (4 + 1) & 6 = (5 + 1);

        

         A66: (PS . 2) = L2 by A65, A28, A29, A31, A62, NOMIN_8:def 14;

        

         A67: (AS2 . L1) = L2 by A64, NOMIN_2:def 7;

        

         A68: ( dom L1) = ( {c} \/ ( dom d1)) by A2, NOMIN_4: 4;

        

         A69: ( dom L2) = ( {s} \/ ( dom L1)) by A2, NOMIN_4: 4;

        

         A70: d1 in ( dom Ds) by A12, A21, A54;

        

         A71: ( dom PS) = ( dom prg) by A29, FINSEQ_3: 29;

        

         A72: s in ( dom L2) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A66, NOMIN_8: 25;

        then

         A73: L2 in ( dom Ds) by A54;

        

         A74: p in ( dom L1) by A12, A23, A68, XBOOLE_0:def 3;

        then

         A75: p in ( dom L2) by A69, XBOOLE_0:def 3;

        then L2 in ( dom Dp) by A57;

        then L2 in (( dom Ds) /\ ( dom Dp)) by A73, XBOOLE_0:def 4;

        then

         A76: L2 in ( dom <:Dp, Ds:>) by FUNCT_3:def 7;

        then

         A77: ( <:Dp, Ds:> . L2) = [(Dp . L2), (Ds . L2)] by FUNCT_3:def 7;

        

         A78: ( dom ( multiplication A)) = [:A, A:] by A1, FUNCT_2:def 1;

        p is_a_value_on L2 & s is_a_value_on L2 by A3;

        then [(Dp . L2), (Ds . L2)] in [:A, A:] by ZFMISC_1: 87;

        then

         A79: L2 in ( dom Mps) by A76, A78, A77, FUNCT_1: 11;

        then

        reconsider MpsL2 = (Mps . L2) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

        reconsider L3 = ( local_overlapping (V,A,L2,MpsL2,ps)) as NonatomicND of V, A by NOMIN_2: 9;

        

         A80: (PS . 3) = L3 by A65, A28, A29, A32, A66, NOMIN_8:def 14;

        

         A81: ( dom L3) = ( {ps} \/ ( dom L2)) by A2, NOMIN_4: 4;

        

         A82: s in ( dom L3) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A80, NOMIN_8: 25;

        

         A83: q in ( dom L1) by A12, A24, A68, XBOOLE_0:def 3;

        then

         A84: q in ( dom L2) by A69, XBOOLE_0:def 3;

        then

         A85: q in ( dom L3) by A81, XBOOLE_0:def 3;

        

         A86: c in ( dom L1) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A62, NOMIN_8: 25;

        

         A87: c in ( dom L2) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A66, NOMIN_8: 25;

        

         A88: c in ( dom L3) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A80, NOMIN_8: 25;

        

         A89: L3 in ( dom Dq) by A85, A58;

        L3 in ( dom Dc) by A88, A56;

        then L3 in (( dom Dq) /\ ( dom Dc)) by A89, XBOOLE_0:def 4;

        then

         A90: L3 in ( dom <:Dq, Dc:>) by FUNCT_3:def 7;

        then

         A91: ( <:Dq, Dc:> . L3) = [(Dq . L3), (Dc . L3)] by FUNCT_3:def 7;

        q is_a_value_on L3 & c is_a_value_on L3 by A3;

        then [(Dq . L3), (Dc . L3)] in [:A, A:] by ZFMISC_1: 87;

        then

         A92: L3 in ( dom Mqc) by A90, A78, A91, FUNCT_1: 11;

        then

        reconsider MqcL3 = (Mqc . L3) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

        reconsider L4 = ( local_overlapping (V,A,L3,MqcL3,qc)) as NonatomicND of V, A by NOMIN_2: 9;

        

         A93: (PS . 4) = L4 by A65, A28, A29, A33, A80, NOMIN_8:def 14;

        

         A94: ( dom L4) = ( {qc} \/ ( dom L3)) by A2, NOMIN_4: 4;

        

         A95: qc in ( dom L4) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A33, A93, NOMIN_8: 25;

        

         A96: ps in ( dom L3) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A32, A80, NOMIN_8: 25;

        

         A97: ps in ( dom L4) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A32, A93, NOMIN_8: 25;

        

         A98: b in ( dom L1) by A12, A22, A68, XBOOLE_0:def 3;

        

         A99: L4 in ( dom Dps) by A97, A59;

        L4 in ( dom Dqc) by A95, A60;

        then L4 in (( dom Dps) /\ ( dom Dqc)) by A99, XBOOLE_0:def 4;

        then

         A100: L4 in ( dom <:Dps, Dqc:>) by FUNCT_3:def 7;

        then

         A101: ( <:Dps, Dqc:> . L4) = [(Dps . L4), (Dqc . L4)] by FUNCT_3:def 7;

        

         A102: ( dom ( subtraction A)) = [:A, A:] by A1, FUNCT_2:def 1;

        ps is_a_value_on L4 & qc is_a_value_on L4 by A3;

        then [(Dps . L4), (Dqc . L4)] in [:A, A:] by ZFMISC_1: 87;

        then

         A103: L4 in ( dom Scs) by A100, A102, A101, FUNCT_1: 11;

        then

        reconsider ScsL4 = (Scs . L4) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

        reconsider L5 = ( local_overlapping (V,A,L4,ScsL4,b)) as NonatomicND of V, A by NOMIN_2: 9;

        

         A104: (PS . 5) = L5 by A65, A28, A29, A34, A93, NOMIN_8:def 14;

        

         A105: ( dom L5) = ( {b} \/ ( dom L4)) by A2, NOMIN_4: 4;

        

         A106: i in ( dom L1) by A12, A18, A68, XBOOLE_0:def 3;

        then

         A107: i in ( dom L2) by A69, XBOOLE_0:def 3;

        then

         A108: i in ( dom L3) by A81, XBOOLE_0:def 3;

        then

         A109: i in ( dom L4) by A94, XBOOLE_0:def 3;

        then

         A110: i in ( dom L5) by A105, XBOOLE_0:def 3;

        then

         A111: L5 in ( dom Di) by A52;

        

         A112: j in ( dom L1) by A12, A19, A68, XBOOLE_0:def 3;

        then

         A113: j in ( dom L2) by A69, XBOOLE_0:def 3;

        then

         A114: j in ( dom L3) by A81, XBOOLE_0:def 3;

        then

         A115: j in ( dom L4) by A94, XBOOLE_0:def 3;

        then

         A116: j in ( dom L5) by A105, XBOOLE_0:def 3;

        then

         A117: L5 in ( dom Dj) by A53;

        L5 in (( dom Di) /\ ( dom Dj)) by A111, A117, XBOOLE_0:def 4;

        then

         A118: L5 in ( dom <:Di, Dj:>) by FUNCT_3:def 7;

        then

         A119: ( <:Di, Dj:> . L5) = [(Di . L5), (Dj . L5)] by FUNCT_3:def 7;

        

         A120: ( dom ( addition A)) = [:A, A:] by A1, FUNCT_2:def 1;

        i is_a_value_on L5 & j is_a_value_on L5 by A3;

        then [(Di . L5), (Dj . L5)] in [:A, A:] by ZFMISC_1: 87;

        then

         A121: L5 in ( dom Aij) by A120, A118, A119, FUNCT_1: 11;

        then

        reconsider AijL5 = (Aij . L5) as TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

        reconsider L6 = ( local_overlapping (V,A,L5,AijL5,i)) as NonatomicND of V, A by NOMIN_2: 9;

        

         A122: (PS . 6) = L6 by A28, A29, A35, A104, NOMIN_8:def 14;

        

         A123: ( dom L6) = ( {i} \/ ( dom L5)) by A2, NOMIN_4: 4;

        

         A124: d in ( dom (AS3 * (AS2 * AS1))) by A45, A49, FUNCT_1: 11;

        then L2 in ( dom AS3) by A51, A63, A67, FUNCT_1: 11;

        then

         A125: (AS3 . L2) = L3 by NOMIN_2:def 7;

        

         A126: ((AS3 * (AS2 * AS1)) . d) = (AS3 . ((AS2 * AS1) . d)) by A124, FUNCT_1: 12;

        then L3 in ( dom AS4) by A49, A45, A125, A67, A51, A63, FUNCT_1: 11;

        then

         A127: (AS4 . L3) = L4 by NOMIN_2:def 7;

        

         A128: ((AS4 * (AS3 * (AS2 * AS1))) . d) = (AS4 . ((AS3 * (AS2 * AS1)) . d)) by A49, A45, FUNCT_1: 12;

        then L4 in ( dom AS5) by A43, A48, A127, A125, A67, A63, A126, A51, FUNCT_1: 11;

        then

         A129: (AS5 . L4) = L5 by NOMIN_2:def 7;

        

         A130: ((AS5 * (AS4 * (AS3 * (AS2 * AS1)))) . d) = (AS5 . ((AS4 * (AS3 * (AS2 * AS1))) . d)) by A43, A48, FUNCT_1: 12;

        B = ((AS6 * AS5) * (AS4 * (AS3 * (AS2 * AS1)))) by A42, RELAT_1: 36

        .= (((AS6 * AS5) * AS4) * (AS3 * (AS2 * AS1))) by RELAT_1: 36

        .= ((((AS6 * AS5) * AS4) * AS3) * (AS2 * AS1)) by RELAT_1: 36

        .= (((((AS6 * AS5) * AS4) * AS3) * AS2) * AS1) by RELAT_1: 36;

        then (AS1 . d) in ( dom ((((AS6 * AS5) * AS4) * AS3) * AS2)) by A9, FUNCT_1: 11;

        then (AS2 . L1) in ( dom (((AS6 * AS5) * AS4) * AS3)) by A63, FUNCT_1: 11;

        then (AS3 . L2) in ( dom ((AS6 * AS5) * AS4)) by A67, FUNCT_1: 11;

        then (AS4 . L3) in ( dom (AS6 * AS5)) by A125, FUNCT_1: 11;

        then (AS5 . L4) in ( dom AS6) by A127, FUNCT_1: 11;

        

        then

         A131: L6 = (AS6 . L5) by A129, NOMIN_2:def 7

        .= (B . d) by A129, A127, A125, A67, A63, A51, A130, A128, A126, A9, A42, FUNCT_1: 12;

         Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,L6)

        proof

          take L6;

          thus L6 = L6;

          

           A132: i in ( dom L6) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A35, A122, NOMIN_8: 25;

          

           A133: j in ( dom L6) by A116, A123, XBOOLE_0:def 3;

          

           A134: n in ( dom L1) by A12, A20, A68, XBOOLE_0:def 3;

          then

           A135: n in ( dom L2) by A69, XBOOLE_0:def 3;

          then

           A136: n in ( dom L3) by A81, XBOOLE_0:def 3;

          then

           A137: n in ( dom L4) by A94, XBOOLE_0:def 3;

          then

           A138: n in ( dom L5) by A105, XBOOLE_0:def 3;

          then

           A139: n in ( dom L6) by A123, XBOOLE_0:def 3;

          

           A140: s in ( dom L4) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A93, NOMIN_8: 25;

          

           A141: s in ( dom L5) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A104, NOMIN_8: 25;

          

           A142: s in ( dom L6) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A31, A122, NOMIN_8: 25;

          

           A143: b in ( dom L5) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A34, A104, NOMIN_8: 25;

          

           A144: b in ( dom L6) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A34, A122, NOMIN_8: 25;

          

           A145: c in ( dom L6) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A30, A28, A122, NOMIN_8: 25;

          

           A146: p in ( dom L3) by A75, A81, XBOOLE_0:def 3;

          then

           A147: p in ( dom L4) by A94, XBOOLE_0:def 3;

          then

           A148: p in ( dom L5) by A105, XBOOLE_0:def 3;

          then

           A149: p in ( dom L6) by A123, XBOOLE_0:def 3;

          

           A150: q in ( dom L4) by A85, A94, XBOOLE_0:def 3;

          then

           A151: q in ( dom L5) by A105, XBOOLE_0:def 3;

          then

           A152: q in ( dom L6) by A123, XBOOLE_0:def 3;

          

           A153: ps in ( dom L6) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A32, A122, NOMIN_8: 25;

          qc in ( dom L6) by A1, A2, A3, A5, A9, A11, Th15, A39, A71, A70, A28, A30, A33, A122, NOMIN_8: 25;

          hence EN c= ( dom L6) by A132, A133, A139, A142, A144, A145, A149, A152, A153, ENUMSET1:def 8;

          

           A154: (L5 . j) = (L4 . j) by A2, A4, A5, A6, A115, NOMIN_5: 3, NOMIN_7: 1

          .= (L3 . j) by A2, A4, A5, A6, A114, NOMIN_5: 3, NOMIN_7: 1

          .= (L2 . j) by A2, A4, A5, A6, A113, NOMIN_5: 3, NOMIN_7: 1

          .= (L1 . j) by A2, A4, A5, A6, A112, NOMIN_5: 3, NOMIN_7: 1

          .= 1 by A2, A4, A5, A6, A12, A13, A19, NOMIN_5: 3, NOMIN_7: 1;

          hence (L6 . j) = 1 by A2, A4, A5, A6, A116, NOMIN_5: 3, NOMIN_7: 1;

          

          thus (L6 . n) = (L5 . n) by A2, A4, A5, A6, A138, NOMIN_5: 3, NOMIN_7: 1

          .= (L4 . n) by A2, A4, A5, A6, A137, NOMIN_5: 3, NOMIN_7: 1

          .= (L3 . n) by A2, A4, A5, A6, A136, NOMIN_5: 3, NOMIN_7: 1

          .= (L2 . n) by A2, A4, A5, A6, A135, NOMIN_5: 3, NOMIN_7: 1

          .= (L1 . n) by A2, A4, A5, A6, A134, NOMIN_5: 3, NOMIN_7: 1

          .= n0 by A2, A4, A5, A6, A12, A14, A20, NOMIN_5: 3, NOMIN_7: 1;

          

          thus (L6 . p) = (L5 . p) by A2, A4, A5, A6, A148, NOMIN_5: 3, NOMIN_7: 1

          .= (L4 . p) by A2, A4, A5, A6, A147, NOMIN_5: 3, NOMIN_7: 1

          .= (L3 . p) by A2, A4, A5, A6, A146, NOMIN_5: 3, NOMIN_7: 1

          .= (L2 . p) by A2, A4, A5, A6, A75, NOMIN_5: 3, NOMIN_7: 1

          .= (L1 . p) by A2, A4, A5, A6, A74, NOMIN_5: 3, NOMIN_7: 1

          .= p0 by A2, A4, A5, A6, A12, A15, A23, NOMIN_5: 3, NOMIN_7: 1;

          

          thus (L6 . q) = (L5 . q) by A2, A4, A5, A6, A151, NOMIN_5: 3, NOMIN_7: 1

          .= (L4 . q) by A2, A4, A5, A6, A150, NOMIN_5: 3, NOMIN_7: 1

          .= (L3 . q) by A2, A4, A5, A6, A85, NOMIN_5: 3, NOMIN_7: 1

          .= (L2 . q) by A2, A4, A5, A6, A84, NOMIN_5: 3, NOMIN_7: 1

          .= (L1 . q) by A2, A4, A5, A6, A83, NOMIN_5: 3, NOMIN_7: 1

          .= q0 by A2, A4, A5, A6, A12, A16, A24, NOMIN_5: 3, NOMIN_7: 1;

          take I1 = (I + 1);

          

           A155: (L5 . i) = (L4 . i) by A2, A4, A5, A6, A109, NOMIN_5: 3, NOMIN_7: 1

          .= (L3 . i) by A2, A4, A5, A6, A108, NOMIN_5: 3, NOMIN_7: 1

          .= (L2 . i) by A2, A4, A5, A6, A107, NOMIN_5: 3, NOMIN_7: 1

          .= (L1 . i) by A2, A4, A5, A6, A106, NOMIN_5: 3, NOMIN_7: 1

          .= I by A2, A4, A5, A6, A12, A18, A25, NOMIN_5: 3, NOMIN_7: 1;

          

          thus (L6 . i) = (Aij . L5) by NOMIN_2: 10

          .= I1 by A1, A121, A110, A116, A154, A155, NOMIN_5: 4;

          

           A156: L1 in ( dom Db) by A55, A98;

          

           A157: (L2 . s) = (Db . L1) by NOMIN_2: 10

          .= ( denaming (b,L1)) by A156, NOMIN_1:def 18

          .= (L1 . b) by A98, NOMIN_1:def 12

          .= ( Lucas (x0,y0,p0,q0,I1)) by A2, A4, A5, A6, A27, A12, A22, NOMIN_5: 3, NOMIN_7: 1;

          

          thus (L6 . s) = (L5 . s) by A2, A4, A5, A6, A141, NOMIN_5: 3, NOMIN_7: 1

          .= (L4 . s) by A2, A4, A5, A6, A140, NOMIN_5: 3, NOMIN_7: 1

          .= (L3 . s) by A2, A4, A5, A6, A82, NOMIN_5: 3, NOMIN_7: 1

          .= ( Lucas (x0,y0,p0,q0,I1)) by A2, A4, A5, A6, A72, A157, NOMIN_5: 3, NOMIN_7: 1;

          

           A158: (L2 . p) = (L1 . p) by A2, A4, A5, A6, A74, NOMIN_5: 3, NOMIN_7: 1

          .= p0 by A2, A4, A5, A6, A12, A15, A23, NOMIN_5: 3, NOMIN_7: 1;

          

           A159: (L4 . ps) = (L3 . ps) by A2, A4, A5, A6, A96, NOMIN_5: 3, NOMIN_7: 1

          .= (Mps . L2) by NOMIN_2: 10

          .= (p0 * ( Lucas (x0,y0,p0,q0,I1))) by A1, A79, A75, A72, A157, A158, NOMIN_5: 5;

          

           A160: (L3 . q) = (L2 . q) by A2, A4, A5, A6, A84, NOMIN_5: 3, NOMIN_7: 1

          .= (L1 . q) by A2, A4, A5, A6, A83, NOMIN_5: 3, NOMIN_7: 1

          .= q0 by A2, A4, A5, A6, A12, A16, A24, NOMIN_5: 3, NOMIN_7: 1;

          

           A161: (L3 . c) = (L2 . c) by A2, A4, A5, A6, A87, NOMIN_5: 3, NOMIN_7: 1

          .= (L1 . c) by A2, A4, A5, A6, A86, NOMIN_5: 3, NOMIN_7: 1

          .= (Ds . d1) by NOMIN_2: 10

          .= ( denaming (s,d1)) by A70, NOMIN_1:def 18

          .= ( Lucas (x0,y0,p0,q0,I)) by A12, A21, A26, NOMIN_1:def 12;

          

           A162: (L4 . qc) = (Mqc . L3) by NOMIN_2: 10

          .= (q0 * ( Lucas (x0,y0,p0,q0,I))) by A1, A92, A88, A85, A160, A161, NOMIN_5: 5;

          

           A163: (I1 + 1) = (I + 2);

          

          thus (L6 . b) = (L5 . b) by A2, A4, A5, A6, A143, NOMIN_7: 1, NOMIN_5: 3

          .= (Scs . L4) by NOMIN_2: 10

          .= ((p0 * ( Lucas (x0,y0,p0,q0,I1))) - (q0 * ( Lucas (x0,y0,p0,q0,I)))) by A1, A103, A97, A95, A159, A162, NOMIN_4: 15

          .= ( Lucas (x0,y0,p0,q0,(I1 + 1))) by Th5, A163;

        end;

        hence (inv . (B . d)) = TRUE by A10, A131, Def15;

      end;

      hence thesis by NOMIN_3: 28;

    end;

    theorem :: NOMIN_9:17

    

     Th17: for V be non empty set holds for loc be V -valued10 -element FinSequence holds A is complex-containing & A is_without_nonatomicND_wrt V & (for T be TypeSCNominativeData of V, A holds (loc /. 1) is_a_value_on T & (loc /. 2) is_a_value_on T & (loc /. 4) is_a_value_on T & (loc /. 6) is_a_value_on T & (loc /. 7) is_a_value_on T & (loc /. 8) is_a_value_on T & (loc /. 9) is_a_value_on T & (loc /. 10) is_a_value_on T) & loc is one-to-one implies <*( Lucas_inv (A,loc,x0,y0,p0,q0,n0)), ( Lucas_main_loop (A,loc)), ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( Lucas_inv (A,loc,x0,y0,p0,q0,n0))))*> is SFHT of ( ND (V,A))

    proof

      let V be non empty set;

      let loc be V -valued10 -element FinSequence;

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

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

      set inv = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set B = ( Lucas_loop_body (A,loc));

      set E = ( Equality (A,i,n));

      set N = ( PP_inversion inv);

      assume A is complex-containing & A is_without_nonatomicND_wrt V & (for T be TypeSCNominativeData of V, A holds i is_a_value_on T & j is_a_value_on T & s is_a_value_on T & c is_a_value_on T & p is_a_value_on T & q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T) & loc is one-to-one;

      then <*inv, B, inv*> is SFHT of D by Th16;

      then

       A1: <*( PP_and (( PP_not E),inv)), B, inv*> is SFHT of D by NOMIN_3: 3, NOMIN_3: 15;

       <*N, B, inv*> is SFHT of D by NOMIN_3: 19;

      then <*( PP_and (( PP_not E),N)), B, inv*> is SFHT of D by NOMIN_3: 3, NOMIN_3: 15;

      hence thesis by A1, NOMIN_3: 26;

    end;

    theorem :: NOMIN_9:18

    

     Th18: for V be non empty set holds for loc be V -valued10 -element FinSequence holds for val be 10 -element FinSequence holds A is complex-containing & A is_without_nonatomicND_wrt V & (for T be TypeSCNominativeData of V, A holds (loc /. 1) is_a_value_on T & (loc /. 2) is_a_value_on T & (loc /. 4) is_a_value_on T & (loc /. 6) is_a_value_on T & (loc /. 7) is_a_value_on T & (loc /. 8) is_a_value_on T & (loc /. 9) is_a_value_on T & (loc /. 10) is_a_value_on T) & loc is one-to-one & (loc,val) are_different_wrt 10 implies <*( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)), ( Lucas_main_part (A,loc,val)), ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( Lucas_inv (A,loc,x0,y0,p0,q0,n0))))*> is SFHT of ( ND (V,A))

    proof

      let V be non empty set;

      let loc be V -valued10 -element FinSequence;

      let val be 10 -element FinSequence;

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

      set i1 = (val . 1), j1 = (val . 2), n1 = (val . 3), s1 = (val . 4), b1 = (val . 5), c1 = (val . 6);

      set p1 = (val . 7), q1 = (val . 8), ps1 = (val . 9), qc1 = (val . 10);

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

      set P = ( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0));

      set f = ( initial_assignments (A,loc,val,10));

      set g = ( Lucas_main_loop (A,loc));

      set Q = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set R = ( PP_and (( Equality (A,i,n)),( Lucas_inv (A,loc,x0,y0,p0,q0,n0))));

      assume that

       A1: A is complex-containing & A is_without_nonatomicND_wrt V & (for T be TypeSCNominativeData of V, A holds i is_a_value_on T & j is_a_value_on T & s is_a_value_on T & c is_a_value_on T & p is_a_value_on T & q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T) and

       A2: loc is one-to-one and

       A3: (loc,val) are_different_wrt 10;

      

       A4: ( Seg 10) c= ( dom loc) by FINSEQ_1: 89;

      (loc | ( Seg 10)) is one-to-one by A2;

      then

       A5: <*P, f, Q*> is SFHT of D by A1, A3, A4, Th14;

      

       A6: <*Q, g, R*> is SFHT of D by A1, A2, Th17;

       <*( PP_inversion Q), g, R*> is SFHT of D by NOMIN_3: 19;

      hence thesis by A5, A6, NOMIN_3: 25;

    end;

    theorem :: NOMIN_9:19

    

     Th19: V is non empty & A is_without_nonatomicND_wrt V & (for T holds (loc /. 1) is_a_value_on T & (loc /. 3) is_a_value_on T) implies ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) ||= ( SC_Psuperpos (( valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),( denaming (V,A,(loc /. 4))),z))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

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

      set res = ( Lucas (x0,y0,p0,q0,n0));

      set inv = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set Di = ( denaming (V,A,i));

      set Dn = ( denaming (V,A,n));

      set Ds = ( denaming (V,A,s));

      set Dz = ( denaming (V,A,z));

      set ass = ( SC_assignment (Ds,z));

      set out = ( valid_Lucas_output (A,z,x0,y0,p0,q0,n0));

      set F = ( SC_Psuperpos (out,Ds,z));

      set E = ( Equality (A,i,n));

      set EM = {i, j, n, s, b, c, p, q, ps, qc};

      assume that

       A1: V is non empty & A is_without_nonatomicND_wrt V and

       A2: for T holds i is_a_value_on T & n is_a_value_on T;

      let d be Element of D such that

       A3: d in ( dom ( PP_and (E,inv))) and

       A4: (( PP_and (E,inv)) . d) = TRUE ;

      

       A5: ( dom F) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(Ds . d),z)) in ( dom out) & d in ( dom Ds) } by NOMIN_2:def 11;

      

       A6: ( dom out) = { d where d be TypeSCNominativeData of V, A : d in ( dom Dz) } by NOMIN_8:def 13;

      

       A7: ( dom Ds) = { d where d be NonatomicND of V, A : s in ( dom d) } by NOMIN_1:def 18;

      

       A8: ( dom Dz) = { d where d be NonatomicND of V, A : z in ( dom d) } by NOMIN_1:def 18;

      

       A9: d in ( dom E) by A3, A4, PARTPR_1: 23;

      

       A10: d in ( dom inv) by A3, A4, PARTPR_1: 23;

      

       A11: ( dom E) = (( dom Di) /\ ( dom Dn)) by A2, NOMIN_4: 11;

      then

       A12: d in ( dom Di) by A9, XBOOLE_0:def 4;

      (inv . d) = TRUE by A3, A4, PARTPR_1: 23;

      then Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,d) by A10, Def15;

      then

      consider d1 be NonatomicND of V, A such that

       A13: d = d1 and

       A14: EM c= ( dom d1) and (d1 . j) = 1 and

       A15: (d1 . n) = n0 and (d1 . p) = p0 and (d1 . q) = q0 and

       A16: ex I be Nat st I = (d1 . i) & (d1 . s) = ( Lucas (x0,y0,p0,q0,I)) & (d1 . b) = ( Lucas (x0,y0,p0,q0,(I + 1)));

      

       A17: i in EM by ENUMSET1:def 8;

      

       A18: n in EM by ENUMSET1:def 8;

      

       A19: s in EM by ENUMSET1:def 8;

      reconsider dd = d as TypeSCNominativeData of V, A by NOMIN_1: 39;

      set L = ( local_overlapping (V,A,dd,(Ds . dd),z));

      

       A20: dd in ( dom Ds) by A7, A13, A14, A19;

      then (Ds . d1) in D by A13, PARTFUN1: 4;

      then

       A21: ex d2 be TypeSCNominativeData of V, A st (Ds . d1) = d2;

      then

       A22: L in ( dom Dz) by A1, A13, NOMIN_4: 6;

      then

       A23: L in ( dom out) by A6;

      hence

       A24: d in ( dom F) by A5, A20;

       valid_Lucas_output_pred (A,z,x0,y0,p0,q0,n0,L)

      proof

        consider I be Nat such that

         A25: I = (d1 . i) and

         A26: (d1 . s) = ( Lucas (x0,y0,p0,q0,I)) and (d1 . b) = ( Lucas (x0,y0,p0,q0,(I + 1))) by A16;

        

         A27: ex d be NonatomicND of V, A st L = d & z in ( dom d) by A8, A22;

        then

        reconsider dlo = L as NonatomicND of V, A;

        take dlo;

        thus L = dlo;

        ( rng <*z*>) = {z} by FINSEQ_1: 38;

        hence ( rng <*z*>) c= ( dom dlo) by A27, ZFMISC_1: 31;

        let nn be Nat such that

         A28: 1 <= nn and

         A29: nn <= ( len <*z*>);

        ( len <*z*>) = 1 by FINSEQ_1: 39;

        then

         A30: nn = 1 by A28, A29, XXREAL_0: 1;

        

         A31: i is_a_value_on dd by A2;

        

         A32: n is_a_value_on dd by A2;

        

         A33: ( dom <:Di, Dn:>) = (( dom Di) /\ ( dom Dn)) by FUNCT_3:def 7;

        d in ( dom <:Di, Dn:>) by A9, A11, FUNCT_3:def 7;

        then

         A34: (E . d) = (( Equality A) . ( <:Di, Dn:> . d)) by FUNCT_1: 13;

        

         A35: d in ( dom Dn) by A9, A11, XBOOLE_0:def 4;

        

         A36: ( <:Di, Dn:> . d) = [(Di . d), (Dn . d)] by A9, A11, A33, FUNCT_3:def 7;

        

         A37: (Di . d) = ( denaming (i,d1)) by A13, A12, NOMIN_1:def 18

        .= (d1 . i) by A14, A17, NOMIN_1:def 12;

        

         A38: (Dn . d) = ( denaming (n,d1)) by A13, A35, NOMIN_1:def 18

        .= (d1 . n) by A14, A18, NOMIN_1:def 12;

        

         A39: (Ds . d) = ( denaming (s,d1)) by A20, A13, NOMIN_1:def 18

        .= (d1 . s) by A14, A19, NOMIN_1:def 12;

        (( Equality A) . ((Di . d),(Dn . d))) <> FALSE by A3, A4, A34, A36, PARTPR_1: 23;

        then (Di . d) = (Dn . d) by A31, A32, NOMIN_4:def 9;

        hence thesis by A1, A13, A15, A30, A21, A25, A26, A37, A38, A39, NOMIN_2: 10;

      end;

      

      hence TRUE = (out . L) by A23, NOMIN_8:def 13

      .= (F . d) by A24, NOMIN_2: 35;

    end;

    theorem :: NOMIN_9:20

    

     Th20: V is non empty & A is_without_nonatomicND_wrt V & (for T holds (loc /. 1) is_a_value_on T & (loc /. 3) is_a_value_on T) implies <*( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( Lucas_inv (A,loc,x0,y0,p0,q0,n0)))), ( SC_assignment (( denaming (V,A,(loc /. 4))),z)), ( valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of ( ND (V,A))

    proof

      set s = (loc /. 4);

       <*( SC_Psuperpos (( valid_Lucas_output (A,z,x0,y0,p0,q0,n0)),( denaming (V,A,s)),z)), ( SC_assignment (( denaming (V,A,s)),z)), ( valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of ( ND (V,A)) by NOMIN_3: 29;

      hence thesis by Th19, NOMIN_3: 15;

    end;

    theorem :: NOMIN_9:21

    

     Th21: (for T holds (loc /. 1) is_a_value_on T & (loc /. 3) is_a_value_on T) implies <*( PP_inversion ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( Lucas_inv (A,loc,x0,y0,p0,q0,n0))))), ( SC_assignment (( denaming (V,A,(loc /. 4))),z)), ( valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of ( ND (V,A))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

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

      set inv = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set O = ( valid_Lucas_output (A,z,x0,y0,p0,q0,n0));

      set Di = ( denaming (V,A,i));

      set Dn = ( denaming (V,A,n));

      set Ds = ( denaming (V,A,s));

      set E = ( Equality (A,i,n));

      set F = ( PP_and (E,inv));

      set G = ( SC_assignment (Ds,z));

      set N = ( PP_inversion F);

      assume

       A1: for T holds i is_a_value_on T & n is_a_value_on T;

      now

        let d be TypeSCNominativeData of V, A such that

         A2: d in ( dom N) and (N . d) = TRUE and d in ( dom G) and (G . d) in ( dom O);

        

         A3: ( dom F) = { d where d be Element of D : d in ( dom E) & (E . d) = FALSE or d in ( dom inv) & (inv . d) = FALSE or d in ( dom E) & (E . d) = TRUE & d in ( dom inv) & (inv . d) = TRUE } by PARTPR_1: 16;

        

         A4: ( dom Di) = { d where d be NonatomicND of V, A : i in ( dom d) } by NOMIN_1:def 18;

        

         A5: ( dom Dn) = { d where d be NonatomicND of V, A : n in ( dom d) } by NOMIN_1:def 18;

        

         A6: ( dom E) = (( dom Di) /\ ( dom Dn)) by A1, NOMIN_4: 11;

        

         A7: not d in ( dom F) by A2, PARTPR_2: 9;

        ( dom E) c= ( dom F) by PARTPR_2: 3;

        then not d in ( dom E) by A2, PARTPR_2: 9;

        then

         A8: not d in ( dom Di) or not d in ( dom Dn) by A6, XBOOLE_0:def 4;

        ( dom inv) = D by Def15;

        then

         A9: d in ( dom inv);

        then (inv . d) <> FALSE by A3, A7;

        then Lucas_inv_pred (A,loc,x0,y0,p0,q0,n0,d) by A9, Def15;

        then

        consider d1 be NonatomicND of V, A such that

         A10: d = d1 and

         A11: {i, j, n, s, b, c, p, q, ps, qc} c= ( dom d1) and (d1 . j) = 1 & (d1 . n) = n0 & (d1 . p) = p0 & (d1 . q) = q0 & ex I be Nat st I = (d1 . i) & (d1 . s) = ( Lucas (x0,y0,p0,q0,I)) & (d1 . b) = ( Lucas (x0,y0,p0,q0,(I + 1)));

        i in {i, j, n, s, b, c, p, q, ps, qc} & n in {i, j, n, s, b, c, p, q, ps, qc} by ENUMSET1:def 8;

        hence (O . (G . d)) = TRUE by A4, A5, A8, A10, A11;

      end;

      hence thesis by NOMIN_3: 28;

    end;

    ::$Notion-Name

    theorem :: NOMIN_9:22

    for V be non empty set holds for loc be V -valued10 -element FinSequence holds for val be 10 -element FinSequence holds for z be Element of V holds A is complex-containing & A is_without_nonatomicND_wrt V & (for T be TypeSCNominativeData of V, A holds (loc /. 1) is_a_value_on T & (loc /. 2) is_a_value_on T & (loc /. 3) is_a_value_on T & (loc /. 4) is_a_value_on T & (loc /. 6) is_a_value_on T & (loc /. 7) is_a_value_on T & (loc /. 8) is_a_value_on T & (loc /. 9) is_a_value_on T & (loc /. 10) is_a_value_on T) & loc is one-to-one & (loc,val) are_different_wrt 10 implies <*( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)), ( Lucas_program (A,loc,val,z)), ( valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of ( ND (V,A))

    proof

      let V be non empty set;

      let loc be V -valued10 -element FinSequence;

      let val be 10 -element FinSequence;

      let z be Element of V;

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4), b = (loc /. 5), c = (loc /. 6);

      set p = (loc /. 7), q = (loc /. 8), ps = (loc /. 9), qc = (loc /. 10);

      set i1 = (val . 1), j1 = (val . 2), n1 = (val . 3), s1 = (val . 4);

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

      set P = ( valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0));

      set F = ( Lucas_main_part (A,loc,val));

      set G = ( SC_assignment (( denaming (V,A,s)),z));

      set Q = ( valid_Lucas_output (A,z,x0,y0,p0,q0,n0));

      set inv = ( Lucas_inv (A,loc,x0,y0,p0,q0,n0));

      set E = ( Equality (A,i,n));

      assume that

       A1: A is complex-containing & A is_without_nonatomicND_wrt V and

       A2: for T be TypeSCNominativeData of V, A holds i is_a_value_on T & j is_a_value_on T & n is_a_value_on T & s is_a_value_on T & c is_a_value_on T & p is_a_value_on T & q is_a_value_on T & ps is_a_value_on T & qc is_a_value_on T;

      assume loc is one-to-one & (loc,val) are_different_wrt 10;

      then

       A3: <*P, F, ( PP_and (E,inv))*> is SFHT of D by A1, A2, Th18;

      

       A4: <*( PP_and (E,inv)), G, Q*> is SFHT of D by A1, A2, Th20;

       <*( PP_inversion ( PP_and (E,inv))), G, Q*> is SFHT of D by A2, Th21;

      hence thesis by A3, A4, NOMIN_3: 25;

    end;