scpinvar.miz



    begin

    reserve m,n for Element of NAT ,

i,j for Instruction of SCMPDS ,

I for Program of SCMPDS ,

a for Int_position;

    theorem :: SCPINVAR:1

    

     Th1: (((i ';' j) ';' I) . 0 ) = i & (((i ';' j) ';' I) . 1) = j

    proof

      set jI = (j ';' I);

      

       A1: ((i ';' j) ';' I) = (i ';' jI) by SCMPDS_4: 16

      .= (( Load i) ';' jI) by SCMPDS_4:def 2;

       0 in ( dom ( Load i)) by COMPOS_1: 50;

      

      hence (((i ';' j) ';' I) . 0 ) = (( Load i) . 0 ) by A1, AFINSQ_1:def 3

      .= i;

      

       A2: 0 in ( dom ( Load j)) by COMPOS_1: 50;

       0 < ( card jI);

      then

       A3: ( card ( Load i)) = 1 & 0 in ( dom jI) by AFINSQ_1: 66, COMPOS_1: 54;

      

      thus (((i ';' j) ';' I) . 1) = ((( Load i) ';' jI) . ( 0 + 1)) by A1

      .= (jI . 0 ) by A3, AFINSQ_1:def 3

      .= ((( Load j) ';' I) . 0 ) by SCMPDS_4:def 2

      .= (( Load j) . 0 ) by A2, AFINSQ_1:def 3

      .= j;

    end;

    theorem :: SCPINVAR:2

    

     Th2: for a,b be Int_position holds ex f be Function of ( product ( the_Values_of SCMPDS )), NAT st for s be State of SCMPDS holds ((s . a) = (s . b) implies (f . s) = 0 ) & ((s . a) <> (s . b) implies (f . s) = ( max ( |.(s . a).|, |.(s . b).|)))

    proof

      let a,b be Int_position;

      defpred P[ set, set] means ex t be State of SCMPDS st t = $1 & ((t . a) = (t . b) implies $2 = 0 ) & ((t . a) <> (t . b) implies $2 = ( max ( |.(t . a).|, |.(t . b).|)));

       A1:

      now

        let s be Element of ( product ( the_Values_of SCMPDS ));

        per cases ;

          suppose

           A2: (s . a) = (s . b);

          reconsider y = 0 as Element of NAT ;

          take y;

          thus P[s, y] by A2;

        end;

          suppose

           A3: (s . a) <> (s . b);

          set mm = ( max ( |.(s . a).|, |.(s . b).|));

          reconsider y = mm as Element of NAT by XXREAL_0: 16;

          take y;

          thus P[s, y] by A3;

        end;

      end;

      consider f be Function of ( product ( the_Values_of SCMPDS )), NAT such that

       A4: for s be Element of ( product ( the_Values_of SCMPDS )) holds P[s, (f . s)] from FUNCT_2:sch 3( A1);

      

       A5: for s be State of SCMPDS holds P[s, (f . s)]

      proof

        let s be State of SCMPDS ;

        reconsider s as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

         P[s, (f . s)] by A4;

        hence thesis;

      end;

      take f;

      hereby

        let s be State of SCMPDS ;

         P[s, (f . s)] by A5;

        hence ((s . a) = (s . b) implies (f . s) = 0 ) & ((s . a) <> (s . b) implies (f . s) = ( max ( |.(s . a).|, |.(s . b).|)));

      end;

    end;

    theorem :: SCPINVAR:3

    

     Th3: ex f be Function of ( product ( the_Values_of SCMPDS )), NAT st for s be State of SCMPDS holds ((s . a) >= 0 implies (f . s) = 0 ) & ((s . a) < 0 implies (f . s) = ( - (s . a)))

    proof

      defpred P[ set, set] means ex t be State of SCMPDS st t = $1 & ((t . a) >= 0 implies $2 = 0 ) & ((t . a) < 0 implies $2 = ( - (t . a)));

       A1:

      now

        let s be Element of ( product ( the_Values_of SCMPDS ));

        per cases ;

          suppose

           A2: (s . a) >= 0 ;

          reconsider y = 0 as Element of NAT ;

          take y;

          thus P[s, y] by A2;

        end;

          suppose

           A3: (s . a) < 0 ;

          then ( - (s . a)) > 0 by XREAL_1: 58;

          then

          reconsider y = ( - (s . a)) as Element of NAT by INT_1: 3;

          take y;

          thus P[s, y] by A3;

        end;

      end;

      consider f be Function of ( product ( the_Values_of SCMPDS )), NAT such that

       A4: for s be Element of ( product ( the_Values_of SCMPDS )) holds P[s, (f . s)] from FUNCT_2:sch 3( A1);

      

       A5: for s be State of SCMPDS holds P[s, (f . s)]

      proof

        let s be State of SCMPDS ;

        reconsider s as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

         P[s, (f . s)] by A4;

        hence thesis;

      end;

      take f;

      hereby

        let s be State of SCMPDS ;

         P[s, (f . s)] by A5;

        hence ((s . a) >= 0 implies (f . s) = 0 ) & ((s . a) < 0 implies (f . s) = ( - (s . a)));

      end;

    end;

    set A = NAT , D = SCM-Data-Loc ;

    begin

    reserve Q,U,P for Instruction-Sequence of SCMPDS ;

    scheme :: SCPINVAR:sch1

    WhileLEnd { F( State of SCMPDS ) -> Element of NAT , s() -> 0 -started State of SCMPDS , P() -> Instruction-Sequence of SCMPDS , I() -> halt-free shiftable Program of SCMPDS , a() -> Int_position , i() -> Integer , P[ set] } :

F(Initialize) = 0 & P[( Initialize ( IExec (( while<0 (a(),i(),I())),P(),s())))]

      provided

       A1: for t be 0 -started State of SCMPDS st P[t] holds F(t) = 0 iff (t . ( DataLoc ((s() . a()),i()))) >= 0

       and

       A2: P[s()]

       and

       A3: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (s() . a()) & (t . ( DataLoc ((s() . a()),i()))) < 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))];

      set b = ( DataLoc ((s() . a()),i())), WHL = ( while<0 (a(),i(),I()));

      defpred Q[ Nat] means for t be 0 -started State of SCMPDS , Q st F(t) <= $1 & (t . a()) = (s() . a()) & P[t] holds F(Initialize) = 0 & P[( Initialize ( IExec (WHL,Q,t)))];

      

       A4: Q[ 0 ]

      proof

        let t be 0 -started State of SCMPDS , Q;

        

         A5: ( Initialize t) = t by MEMSTR_0: 44;

        assume that

         A6: F(t) <= 0 and

         A7: (t . a()) = (s() . a()) and

         A8: P[t];

        

         A9: F(t) = 0 by A6;

        then (t . ( DataLoc ((s() . a()),i()))) >= 0 by A1, A8;

        then for b be Int_position holds (( IExec (WHL,Q,t)) . b) = (t . b) by A7, SCMPDS_8: 12;

        hence thesis by A8, A9, A5, SCPISORT: 4;

      end;

       A10:

      now

        let k be Nat;

        assume

         A11: Q[k];

        now

          let u be 0 -started State of SCMPDS ;

          let U;

          assume that

           A12: F(u) <= (k + 1) and

           A13: (u . a()) = (s() . a()) and

           A14: P[u];

          per cases ;

            suppose F(u) = 0 ;

            hence F(Initialize) = 0 & P[( Initialize ( IExec (WHL,U,u)))] by A4, A13, A14;

          end;

            suppose

             A15: F(u) <> 0 ;

            set Iu = ( IExec (I(),U,u));

            

             A16: (u . b) < 0 by A1, A14, A15;

            then

             A17: (Iu . a()) = (s() . a()) & P[( Initialize Iu)] by A3, A13, A14;

            deffunc F( State of SCMPDS ) = F($1);

            

             A18: P[u] by A14;

            

             A19: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ( DataLoc ((u . a()),i()))) >= 0 by A1, A13;

             F(Initialize) < F(u) by A3, A13, A14, A16;

            then ( F(Initialize) + 1) <= F(u) by INT_1: 7;

            then ( F(Initialize) + 1) <= (k + 1) by A12, XXREAL_0: 2;

            then

             A20: F(Initialize) <= k by XREAL_1: 6;

            

             A21: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (u . a()) & (t . ( DataLoc ((u . a()),i()))) < 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))] by A3, A13;

            

             A22: (u . ( DataLoc ((u . a()),i()))) < 0 by A1, A13, A14, A15;

            

             A23: ( IExec (WHL,U,u)) = ( IExec (WHL,U,( Initialize Iu))) from SCMPDS_8:sch 2( A22, A19, A18, A21);

            (( Initialize Iu) . a()) = (Iu . a()) by SCMPDS_5: 15;

            hence F(Initialize) = 0 & P[( Initialize ( IExec (WHL,U,u)))] by A11, A20, A17, A23;

          end;

        end;

        hence Q[(k + 1)];

      end;

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

      then Q[F(s)];

      hence thesis by A2;

    end;

    set a1 = ( intpos 1), a2 = ( intpos 2), a3 = ( intpos 3);

    begin

    definition

      let n,p0 be Element of NAT ;

      :: SCPINVAR:def1

      func sum (n,p0) -> Program of SCMPDS equals ((((( GBP := 0 ) ';' (( intpos 1) := 0 )) ';' (( intpos 2) := ( - n))) ';' (( intpos 3) := (p0 + 1))) ';' ( while<0 ( GBP ,2,((( AddTo ( GBP ,1,( intpos 3), 0 )) ';' ( AddTo ( GBP ,2,1))) ';' ( AddTo ( GBP ,3,1))))));

      coherence ;

    end

    theorem :: SCPINVAR:4

    

     Th4: for s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,b,c be Int_position, n,i,p0 be Element of NAT , f be FinSequence of INT st f is_FinSequence_on (s,p0) & ( len f) = n & (s . b) = 0 & (s . a) = 0 & (s . ( intpos i)) = ( - n) & (s . c) = (p0 + 1) & (for t be 0 -started State of SCMPDS , Q st (ex g be FinSequence of INT st g is_FinSequence_on (s,p0) & ( len g) = ((t . ( intpos i)) + n) & (t . b) = ( Sum g) & (t . c) = ((p0 + 1) + ( len g))) & (t . a) = 0 & (t . ( intpos i)) < 0 & for i be Element of NAT st i > p0 holds (t . ( intpos i)) = (s . ( intpos i)) holds (( IExec (I,Q,t)) . a) = 0 & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec (I,Q,t)) . ( intpos i)) = ((t . ( intpos i)) + 1) & (ex g be FinSequence of INT st g is_FinSequence_on (s,p0) & ( len g) = (((t . ( intpos i)) + n) + 1) & (( IExec (I,Q,t)) . c) = ((p0 + 1) + ( len g)) & (( IExec (I,Q,t)) . b) = ( Sum g)) & for i be Element of NAT st i > p0 holds (( IExec (I,Q,t)) . ( intpos i)) = (s . ( intpos i))) holds (( IExec (( while<0 (a,i,I)),P,s)) . b) = ( Sum f) & ( while<0 (a,i,I)) is_closed_on (s,P) & ( while<0 (a,i,I)) is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,b,c be Int_position, n,i,p0 be Element of NAT , f be FinSequence of INT ;

      set Iw = ( IExec (( while<0 (a,i,I)),P,s)), Dw = ( Initialize Iw);

      set da = ( DataLoc ((s . a),i));

      defpred P[ State of SCMPDS ] means (for i be Element of NAT st i > p0 holds ($1 . ( intpos i)) = (s . ( intpos i))) & (ex g be FinSequence of INT st g is_FinSequence_on (s,p0) & ( len g) = (($1 . ( intpos i)) + n) & ($1 . b) = ( Sum g) & ($1 . ( intpos i)) <= 0 & ($1 . c) = ((p0 + 1) + ( len g)));

      assume that

       A1: f is_FinSequence_on (s,p0) and

       A2: ( len f) = n and

       A3: (s . b) = 0 and

       A4: (s . a) = 0 and

       A5: (s . ( intpos i)) = ( - n) and

       A6: (s . c) = (p0 + 1);

      consider ff be Function of ( product ( the_Values_of SCMPDS )), NAT such that

       A7: for t be State of SCMPDS holds ((t . da) >= 0 implies (ff . t) = 0 ) & ((t . da) < 0 implies (ff . t) = ( - (t . da))) by Th3;

      deffunc F( State of SCMPDS ) = (ff . $1);

      assume

       A8: for t be 0 -started State of SCMPDS , Q st (ex g be FinSequence of INT st g is_FinSequence_on (s,p0) & ( len g) = ((t . ( intpos i)) + n) & (t . b) = ( Sum g) & (t . c) = ((p0 + 1) + ( len g))) & (t . a) = 0 & (t . ( intpos i)) < 0 & for i be Element of NAT st i > p0 holds (t . ( intpos i)) = (s . ( intpos i)) holds (( IExec (I,Q,t)) . a) = 0 & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec (I,Q,t)) . ( intpos i)) = ((t . ( intpos i)) + 1) & (ex g be FinSequence of INT st g is_FinSequence_on (s,p0) & ( len g) = (((t . ( intpos i)) + n) + 1) & (( IExec (I,Q,t)) . c) = ((p0 + 1) + ( len g)) & (( IExec (I,Q,t)) . b) = ( Sum g)) & for i be Element of NAT st i > p0 holds (( IExec (I,Q,t)) . ( intpos i)) = (s . ( intpos i));

      

       A9: for t be 0 -started State of SCMPDS st P[t] holds ( F(t) = 0 & (t . da) < 0 implies contradiction) & ((t . da) >= 0 implies F(t) = 0 )

      proof

        let t be 0 -started State of SCMPDS ;

        assume P[t];

        hereby

          assume

           A10: F(t) = 0 ;

          assume

           A11: (t . da) < 0 ;

          then (t . da) < 0 ;

          then F(t) = ( - (t . da)) by A7;

          hence contradiction by A10, A11;

        end;

        assume (t . da) >= 0 ;

        then (t . da) >= 0 ;

        hence F(t) = 0 by A7;

      end;

       A12:

      now

        let t be 0 -started State of SCMPDS , Q;

        assume that

         A13: P[t] and

         A14: (t . a) = (s . a) and

         A15: (t . ( DataLoc ((s . a),i))) < 0 ;

        consider h be FinSequence of INT such that

         A16: h is_FinSequence_on (s,p0) and

         A17: ( len h) = ((t . ( intpos i)) + n) & (t . b) = ( Sum h) and

         A18: (t . c) = ((p0 + 1) + ( len h)) by A13;

        

         A19: (t . c) = ((p0 + 1) + ( len h)) by A18;

        set It = ( IExec (I,Q,t));

        set Dit = ( Initialize It);

        

         A20: for i be Element of NAT st i > p0 holds (t . ( intpos i)) = (s . ( intpos i)) by A13;

        

         A21: ( intpos ( 0 + i)) = da by A4, SCMP_GCD: 1;

        

         A22: ( len h) = ((t . ( intpos i)) + n) & (t . b) = ( Sum h) by A17;

        hence (( IExec (I,Q,t)) . a) = (t . a) by A4, A8, A14, A15, A20, A16, A19, A21;

        consider g be FinSequence of INT such that

         A23: g is_FinSequence_on (s,p0) and

         A24: ( len g) = (((t . ( intpos i)) + n) + 1) and

         A25: (( IExec (I,Q,t)) . c) = ((p0 + 1) + ( len g)) and

         A26: (( IExec (I,Q,t)) . b) = ( Sum g) by A4, A8, A14, A15, A20, A16, A22, A19, A21;

        thus I is_closed_on (t,Q) & I is_halting_on (t,Q) by A4, A8, A14, A15, A20, A16, A22, A19, A21;

        

         A27: (It . ( intpos i)) = ((t . ( intpos i)) + 1) by A4, A8, A14, A15, A20, A16, A22, A19, A21;

        hereby

          per cases ;

            suppose (It . ( intpos i)) >= 0 ;

            then (Dit . da) >= 0 by A21, SCMPDS_5: 15;

            then

             A28: F(Dit) = 0 by A7;

             F(t) <> 0 by A9, A13, A15;

            hence F(Dit) < F(t) by A28;

          end;

            suppose

             A29: (It . ( intpos i)) < 0 ;

            (t . da) < 0 by A15;

            

            then

             A30: F(t) = ( - (t . da)) by A7

            .= ( - (t . ( intpos i))) by A21;

            (Dit . da) < 0 by A21, A29, SCMPDS_5: 15;

            

            then F(Dit) = ( - (Dit . da)) by A7

            .= ( - ((t . ( intpos i)) + 1)) by A21, A27, SCMPDS_5: 15

            .= (( - (t . ( intpos i))) - 1);

            hence F(Dit) < F(t) by A30, XREAL_1: 146;

          end;

        end;

        thus P[( Initialize ( IExec (I,Q,t)))]

        proof

          hereby

            let i be Element of NAT ;

            assume

             A31: i > p0;

            

            thus (Dit . ( intpos i)) = (It . ( intpos i)) by SCMPDS_5: 15

            .= (s . ( intpos i)) by A4, A8, A14, A15, A20, A16, A22, A19, A21, A31;

          end;

          take g;

          thus g is_FinSequence_on (s,p0) by A23;

          

          thus ( len g) = ((( IExec (I,Q,t)) . ( intpos i)) + n) by A27, A24

          .= ((Dit . ( intpos i)) + n) by SCMPDS_5: 15;

          thus (Dit . b) = ( Sum g) by A26, SCMPDS_5: 15;

          (Dit . ( intpos i)) = ((t . ( intpos i)) + 1) by A27, SCMPDS_5: 15;

          hence (Dit . ( intpos i)) <= 0 by A15, A21, INT_1: 7;

          thus thesis by A25, SCMPDS_5: 15;

        end;

      end;

      

       A32: P[s]

      proof

        thus for i be Element of NAT st i > p0 holds (s . ( intpos i)) = (s . ( intpos i));

        consider h be FinSequence of INT such that

         A33: ( len h) = 0 and

         A34: h is_FinSequence_on (s,p0) by SCPISORT: 2;

        take h;

        thus h is_FinSequence_on (s,p0) by A34;

        

        thus ( len h) = ((s . ( intpos i)) + n) by A5, A33

        .= ((s . ( intpos i)) + n);

        h = ( <*> REAL ) by A33;

        hence (s . b) = ( Sum h) by A3, RVSUM_1: 72;

        thus (s . ( intpos i)) <= 0 by A5;

        thus thesis by A6, A33;

      end;

      

       A35: F(Dw) = 0 & P[Dw] from WhileLEnd( A9, A32, A12);

      then

      consider g be FinSequence of INT such that

       A36: g is_FinSequence_on (s,p0) and

       A37: ( len g) = ((Dw . ( intpos i)) + n) and

       A38: (Dw . b) = ( Sum g) and

       A39: (Dw . ( intpos i)) <= 0 ;

      

       A40: (Dw . ( intpos i)) = (Iw . ( intpos ( 0 + i))) by SCMPDS_5: 15

      .= (Iw . da) by A4, SCMP_GCD: 1;

      (Iw . da) = (Dw . da) by SCMPDS_5: 15;

      then (Dw . ( intpos i)) >= 0 by A9, A35, A40;

      then

       A41: (Dw . ( intpos i)) = 0 by A39;

      now

        let i be Nat;

        reconsider a = i as Element of NAT by ORDINAL1:def 12;

        assume i in ( dom f);

        then

         A42: 1 <= i & i <= n by A2, FINSEQ_3: 25;

        

        hence (f . i) = (s . ( intpos (p0 + a))) by A1, A2

        .= (g . i) by A36, A37, A41, A42;

      end;

      then f = g by A2, A37, A41, FINSEQ_2: 9;

      hence (Iw . b) = ( Sum f) by A38, SCMPDS_5: 15;

      

       A43: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . da) >= 0 by A9;

      ( while<0 (a,i,I)) is_closed_on (s,P) & ( while<0 (a,i,I)) is_halting_on (s,P) from SCMPDS_8:sch 1( A43, A32, A12);

      hence thesis;

    end;

    set j1 = ( AddTo ( GBP ,1,a3, 0 )), j2 = ( AddTo ( GBP ,2,1)), j3 = ( AddTo ( GBP ,3,1)), WB = ((j1 ';' j2) ';' j3), WH = ( while<0 ( GBP ,2,WB));

    

     Lm1: for s be 0 -started State of SCMPDS , m be Element of NAT st (s . GBP ) = 0 & (s . a3) = m holds (( IExec (WB,P,( Initialize s))) . GBP ) = 0 & (( IExec (WB,P,( Initialize s))) . a1) = ((s . a1) + (s . ( intpos m))) & (( IExec (WB,P,( Initialize s))) . a2) = ((s . a2) + 1) & (( IExec (WB,P,( Initialize s))) . a3) = (m + 1) & for i be Element of NAT st i > 3 holds (( IExec (WB,P,( Initialize s))) . ( intpos i)) = (s . ( intpos i))

    proof

      set a = GBP ;

      let s be 0 -started State of SCMPDS , m be Element of NAT ;

      assume that

       A1: (s . a) = 0 and

       A2: (s . a3) = m;

      set t0 = ( Initialize s), t1 = ( IExec (WB,P,( Initialize s))), t2 = ( IExec ((j1 ';' j2),P,( Initialize s))), t3 = ( Exec (j1,t0));

      

       A3: (t0 . a3) = m by A2, SCMPDS_5: 15;

      

       A4: (t0 . a) = 0 by A1, SCMPDS_5: 15;

      then 0 <> |.((t0 . GBP ) + 1).| by ABSVALUE:def 1;

      then a <> ( DataLoc ((t0 . GBP ),1)) by XTUPLE_0: 1;

      then

       A5: (t3 . a) = 0 by A4, SCMPDS_2: 49;

      then 0 <> |.((t3 . GBP ) + 2).| by ABSVALUE:def 1;

      then

       A6: a <> ( DataLoc ((t3 . GBP ),2)) by XTUPLE_0: 1;

      3 <> |.((t0 . GBP ) + 1).| by A4, ABSVALUE:def 1;

      then a3 <> ( DataLoc ((t0 . GBP ),1)) by XTUPLE_0: 1;

      then

       A7: (t3 . a3) = m by A3, SCMPDS_2: 49;

      3 <> |.((t3 . GBP ) + 2).| by A5, ABSVALUE:def 1;

      then

       A8: a3 <> ( DataLoc ((t3 . GBP ),2)) by XTUPLE_0: 1;

      

       A9: (t2 . a3) = (( Exec (j2,t3)) . a3) by SCMPDS_5: 42

      .= m by A7, A8, SCMPDS_2: 48;

      

       A10: (t0 . a1) = (s . a1) by SCMPDS_5: 15;

      

       A11: ( DataLoc ((t0 . a),1)) = ( intpos ( 0 + 1)) by A4, SCMP_GCD: 1;

      

      then

       A12: (t3 . a1) = ((t0 . a1) + (t0 . ( DataLoc ((t0 . a3), 0 )))) by SCMPDS_2: 49

      .= ((t0 . a1) + (t0 . ( intpos (m + 0 )))) by A3, SCMP_GCD: 1

      .= ((s . a1) + (s . ( intpos m))) by A10, SCMPDS_5: 15;

      1 <> |.((t3 . GBP ) + 2).| by A5, ABSVALUE:def 1;

      then

       A13: a1 <> ( DataLoc ((t3 . GBP ),2)) by XTUPLE_0: 1;

      

       A14: ( DataLoc ((t3 . a),2)) = ( intpos ( 0 + 2)) by A5, SCMP_GCD: 1;

      then

       A15: |.((t3 . a) + 2).| = ( 0 + 2) by XTUPLE_0: 1;

      2 <> |.((t0 . GBP ) + 1).| by A4, ABSVALUE:def 1;

      then a2 <> ( DataLoc ((t0 . GBP ),1)) by XTUPLE_0: 1;

      

      then

       A16: (t3 . a2) = (t0 . a2) by SCMPDS_2: 49

      .= (s . a2) by SCMPDS_5: 15;

      

       A17: (t2 . a) = (( Exec (j2,t3)) . a) by SCMPDS_5: 42

      .= 0 by A5, A6, SCMPDS_2: 48;

      then

       A18: ( DataLoc ((t2 . a),3)) = ( intpos ( 0 + 3)) by SCMP_GCD: 1;

      

       A19: (t2 . a2) = (( Exec (j2,t3)) . a2) by SCMPDS_5: 42

      .= ((s . a2) + 1) by A16, A14, SCMPDS_2: 48;

      

       A20: (t2 . a1) = (( Exec (j2,t3)) . a1) by SCMPDS_5: 42

      .= ((s . a1) + (s . ( intpos m))) by A12, A13, SCMPDS_2: 48;

       0 <> |.((t2 . GBP ) + 3).| by A17, ABSVALUE:def 1;

      then

       A21: a <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

      thus (t1 . a) = (( Exec (j3,t2)) . a) by SCMPDS_5: 41

      .= 0 by A17, A21, SCMPDS_2: 48;

      1 <> |.((t2 . GBP ) + 3).| by A17, ABSVALUE:def 1;

      then

       A22: a1 <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

      thus (t1 . a1) = (( Exec (j3,t2)) . a1) by SCMPDS_5: 41

      .= ((s . a1) + (s . ( intpos m))) by A20, A22, SCMPDS_2: 48;

      2 <> |.((t2 . GBP ) + 3).| by A17, ABSVALUE:def 1;

      then

       A23: a2 <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

      thus (t1 . a2) = (( Exec (j3,t2)) . a2) by SCMPDS_5: 41

      .= ((s . a2) + 1) by A19, A23, SCMPDS_2: 48;

      

      thus (t1 . a3) = (( Exec (j3,t2)) . a3) by SCMPDS_5: 41

      .= (m + 1) by A9, A18, SCMPDS_2: 48;

      

       A24: |.((t0 . a) + 1).| = ( 0 + 1) by A11, XTUPLE_0: 1;

      hereby

        let i be Element of NAT ;

        assume

         A25: i > 3;

        then

         A26: ( intpos i) <> ( DataLoc ((t2 . a),3)) by A18, XTUPLE_0: 1;

        i <> |.((t0 . a) + 1).| by A24, A25;

        then

         A27: ( intpos i) <> ( DataLoc ((t0 . a),1)) by XTUPLE_0: 1;

        i <> |.((t3 . a) + 2).| by A15, A25;

        then

         A28: ( intpos i) <> ( DataLoc ((t3 . a),2)) by XTUPLE_0: 1;

        

        thus (t1 . ( intpos i)) = (( Exec (j3,t2)) . ( intpos i)) by SCMPDS_5: 41

        .= (t2 . ( intpos i)) by A26, SCMPDS_2: 48

        .= (( Exec (j2,t3)) . ( intpos i)) by SCMPDS_5: 42

        .= (t3 . ( intpos i)) by A28, SCMPDS_2: 48

        .= (t0 . ( intpos i)) by A27, SCMPDS_2: 49

        .= (s . ( intpos i)) by SCMPDS_5: 15;

      end;

    end;

    

     Lm2: for s be 0 -started State of SCMPDS , n,p0 be Element of NAT , f be FinSequence of INT st p0 >= 3 & f is_FinSequence_on (s,p0) & ( len f) = n & (s . a1) = 0 & (s . GBP ) = 0 & (s . a2) = ( - n) & (s . a3) = (p0 + 1) holds (( IExec (WH,P,( Initialize s))) . a1) = ( Sum f) & WH is_closed_on (s,P) & WH is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , n,p0 be Element of NAT , f be FinSequence of INT ;

      set a = GBP ;

      

       A1: ( Initialize s) = s by MEMSTR_0: 44;

      assume that

       A2: p0 >= 3 and

       A3: f is_FinSequence_on (s,p0) & ( len f) = n & (s . a1) = 0 & (s . a) = 0 & (s . a2) = ( - n) & (s . a3) = (p0 + 1);

      now

        let t be 0 -started State of SCMPDS ;

        let Q;

        

         A4: ( Initialize t) = t by MEMSTR_0: 44;

        given g be FinSequence of INT such that

         A5: g is_FinSequence_on (s,p0) and

         A6: ( len g) = ((t . a2) + n) and

         A7: (t . a1) = ( Sum g) and

         A8: (t . a3) = ((p0 + 1) + ( len g));

        assume that

         A9: (t . a) = 0 and (t . a2) < 0 ;

        assume

         A10: for i be Element of NAT st i > p0 holds (t . ( intpos i)) = (s . ( intpos i));

        thus (( IExec (WB,Q,t)) . a) = 0 by A8, A9, Lm1, A4;

        thus WB is_closed_on (t,Q) & WB is_halting_on (t,Q) by SCMPDS_6: 20, SCMPDS_6: 21;

        thus (( IExec (WB,Q,t)) . a2) = ((t . a2) + 1) by A8, A9, Lm1, A4;

        thus ex g be FinSequence of INT st g is_FinSequence_on (s,p0) & ( len g) = (((t . a2) + n) + 1) & (( IExec (WB,Q,t)) . a3) = ((p0 + 1) + ( len g)) & (( IExec (WB,Q,t)) . a1) = ( Sum g)

        proof

          consider h be FinSequence of INT such that

           A11: ( len h) = (( len g) + 1) and

           A12: h is_FinSequence_on (s,p0) by SCPISORT: 2;

          take h;

          thus h is_FinSequence_on (s,p0) by A12;

          thus ( len h) = (((t . a2) + n) + 1) by A6, A11;

          

          thus (( IExec (WB,Q,t)) . a3) = (((p0 + 1) + ( len g)) + 1) by A8, A9, Lm1, A4

          .= ((p0 + 1) + ( len h)) by A11;

          

           A13: (p0 + 1) > p0 by XREAL_1: 29;

          set m = ( len h);

          

           A14: m >= 1 by A11, NAT_1: 11;

          then (p0 + m) >= (p0 + 1) by XREAL_1: 6;

          then

           A15: (p0 + m) > p0 by A13, XXREAL_0: 2;

          reconsider q = (h . m) as Element of INT by INT_1:def 2;

           A16:

          now

            let i be Nat;

            assume that

             A17: 1 <= i and

             A18: i <= ( len h);

            per cases ;

              suppose i = ( len h);

              hence (h . i) = ((g ^ <*q*>) . i) by A11, FINSEQ_1: 42;

            end;

              suppose i <> ( len h);

              then i < ( len h) by A18, XXREAL_0: 1;

              then

               A19: i <= ( len g) by A11, INT_1: 7;

              then i in ( Seg ( len g)) by A17, FINSEQ_1: 1;

              then

               A20: i in ( dom g) by FINSEQ_1:def 3;

              

              thus (h . i) = (s . ( intpos (p0 + i))) by A12, A17, A18

              .= (g . i) by A5, A17, A19

              .= ((g ^ <*q*>) . i) by A20, FINSEQ_1:def 7;

            end;

          end;

          ( len (g ^ <*q*>)) = ( len h) by A11, FINSEQ_2: 16;

          then

           A21: (g ^ <*q*>) = h by A16, FINSEQ_1: 14;

          (h . m) = (s . ( intpos (p0 + m))) by A12, A14

          .= (t . ( intpos ((p0 + 1) + ( len g)))) by A10, A11, A15;

          

          hence (( IExec (WB,Q,t)) . a1) = ((t . a1) + (h . m)) by A8, A9, Lm1, A4

          .= ( Sum h) by A7, A21, RVSUM_1: 74;

        end;

        hereby

          let i be Element of NAT ;

          assume

           A22: i > p0;

          then i > 3 by A2, XXREAL_0: 2;

          

          hence (( IExec (WB,Q,t)) . ( intpos i)) = (t . ( intpos i)) by A8, A9, Lm1, A4

          .= (s . ( intpos i)) by A10, A22;

        end;

      end;

      hence thesis by A3, Th4, A1;

    end;

    

     Lm3: for s be 0 -started State of SCMPDS , n,p0 be Element of NAT , f be FinSequence of INT st p0 >= 3 & f is_FinSequence_on (s,p0) & ( len f) = n holds (( IExec (( sum (n,p0)),P,s)) . a1) = ( Sum f) & ( sum (n,p0)) is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , n,p0 be Element of NAT , f be FinSequence of INT ;

      

       A1: ( Initialize s) = s by MEMSTR_0: 44;

      assume that

       A2: p0 >= 3 and

       A3: f is_FinSequence_on (s,p0) and

       A4: ( len f) = n;

      set a = GBP , i1 = (a := 0 ), i2 = (a1 := 0 ), i3 = (a2 := ( - n)), i4 = (a3 := (p0 + 1)), t0 = ( Initialize s), I4 = (((i1 ';' i2) ';' i3) ';' i4), t1 = ( IExec (I4,P,( Initialize s))), Q1 = P, t2 = ( IExec (((i1 ';' i2) ';' i3),P,( Initialize s))), t3 = ( IExec ((i1 ';' i2),P,( Initialize s))), t4 = ( Exec (i1,t0));

      now

        let i be Nat;

        assume that

         A5: 1 <= i and

         A6: i <= ( len f);

        

         A7: (p0 + 1) >= (3 + 1) by A2, XREAL_1: 6;

        

         A8: (p0 + i) >= (p0 + 1) by A5, XREAL_1: 6;

        then (p0 + i) <> 3 by A7, XXREAL_0: 2;

        then

         A9: ( intpos (p0 + i)) <> a3 by XTUPLE_0: 1;

        (p0 + i) <> 0 by A8;

        then

         A10: ( intpos (p0 + i)) <> a by XTUPLE_0: 1;

        (p0 + i) <> 1 by A7, A8, XXREAL_0: 2;

        then

         A11: ( intpos (p0 + i)) <> a1 by XTUPLE_0: 1;

        (p0 + i) <> 2 by A7, A8, XXREAL_0: 2;

        then

         A12: ( intpos (p0 + i)) <> a2 by XTUPLE_0: 1;

        

        thus (t1 . ( intpos (p0 + i))) = (( Exec (i4,t2)) . ( intpos (p0 + i))) by SCMPDS_5: 41

        .= (t2 . ( intpos (p0 + i))) by A9, SCMPDS_2: 45

        .= (( Exec (i3,t3)) . ( intpos (p0 + i))) by SCMPDS_5: 41

        .= (t3 . ( intpos (p0 + i))) by A12, SCMPDS_2: 45

        .= (( Exec (i2,t4)) . ( intpos (p0 + i))) by SCMPDS_5: 42

        .= (t4 . ( intpos (p0 + i))) by A11, SCMPDS_2: 45

        .= (t0 . ( intpos (p0 + i))) by A10, SCMPDS_2: 45

        .= (s . ( intpos (p0 + i))) by SCMPDS_5: 15

        .= (f . i) by A3, A5, A6;

      end;

      then

       A13: f is_FinSequence_on (t1,p0);

      

       A14: f is_FinSequence_on (( Initialize t1),p0)

      proof

        let i be Nat;

        assume 1 <= i & i <= ( len f);

        then (f . i) = (t1 . ( intpos (p0 + i))) by A13;

        hence thesis by SCMPDS_5: 15;

      end;

      

       A15: (t4 . a) = 0 by SCMPDS_2: 45;

      

       A16: (t3 . a) = (( Exec (i2,t4)) . a) by SCMPDS_5: 42

      .= 0 by A15, AMI_3: 10, SCMPDS_2: 45;

      

       A17: (t2 . a) = (( Exec (i3,t3)) . a) by SCMPDS_5: 41

      .= 0 by A16, AMI_3: 10, SCMPDS_2: 45;

      

       A18: (t1 . a3) = (( Exec (i4,t2)) . a3) by SCMPDS_5: 41

      .= (p0 + 1) by SCMPDS_2: 45;

      

       A19: (( Initialize t1) . a3) = (t1 . a3) by SCMPDS_5: 15;

      

       A20: (t3 . a1) = (( Exec (i2,t4)) . a1) by SCMPDS_5: 42

      .= 0 by SCMPDS_2: 45;

      

       A21: (t2 . a1) = (( Exec (i3,t3)) . a1) by SCMPDS_5: 41

      .= 0 by A20, AMI_3: 10, SCMPDS_2: 45;

      

       A22: (( Initialize t1) . a1) = (t1 . a1) by SCMPDS_5: 15;

      

       A23: (t1 . a1) = (( Exec (i4,t2)) . a1) by SCMPDS_5: 41

      .= 0 by A21, AMI_3: 10, SCMPDS_2: 45;

      

       A24: (t2 . a2) = (( Exec (i3,t3)) . a2) by SCMPDS_5: 41

      .= ( - n) by SCMPDS_2: 45;

      

       A25: (( Initialize t1) . a2) = (t1 . a2) by SCMPDS_5: 15;

      

       A26: (( Initialize t1) . a) = (t1 . a) by SCMPDS_5: 15;

      

       A27: (t1 . a2) = (( Exec (i4,t2)) . a2) by SCMPDS_5: 41

      .= ( - n) by A24, AMI_3: 10, SCMPDS_2: 45;

      

       A28: (t1 . a) = (( Exec (i4,t2)) . a) by SCMPDS_5: 41

      .= 0 by A17, AMI_3: 10, SCMPDS_2: 45;

      then WH is_closed_on (( Initialize t1),Q1) & WH is_halting_on (( Initialize t1),Q1) by A2, A4, A23, A27, A18, Lm2, A14, A19, A22, A25, A26;

      then

       A29: WH is_closed_on (t1,Q1) & WH is_halting_on (t1,Q1) by SCMPDS_6: 125, SCMPDS_6: 126;

      ( IExec (WH,Q1,( Initialize t1))) = ( IExec (WH,Q1,( Initialize ( Initialize t1))));

      then (( IExec (WH,Q1,( Initialize t1))) . a1) = ( Sum f) by A2, A4, A28, A23, A27, A18, Lm2, A14, A19, A22, A25, A26;

      hence (( IExec (( sum (n,p0)),P,s)) . a1) = ( Sum f) by A29, A1, SCPISORT: 7;

      thus thesis by A29, SCPISORT: 9;

    end;

    theorem :: SCPINVAR:5

    for s be 0 -started State of SCMPDS , n,p0 be Element of NAT , f be FinSequence of INT st p0 >= 3 & f is_FinSequence_on (s,p0) & ( len f) = n holds (( IExec (( sum (n,p0)),P,s)) . ( intpos 1)) = ( Sum f) & ( sum (n,p0)) is parahalting

    proof

      let s be 0 -started State of SCMPDS , n,p0 be Element of NAT , f be FinSequence of INT ;

      assume that

       A1: p0 >= 3 and

       A2: f is_FinSequence_on (s,p0) & ( len f) = n;

      thus (( IExec (( sum (n,p0)),P,s)) . a1) = ( Sum f) by A1, A2, Lm3;

      now

        let t be State of SCMPDS , Q;

        consider g be FinSequence of INT such that

         A3: ( len g) = n & g is_FinSequence_on (t,p0) by SCPISORT: 2;

        g is_FinSequence_on (( Initialize t),p0)

        proof

          let i be Nat;

          assume 1 <= i & i <= ( len g);

          then (g . i) = (t . ( intpos (p0 + i))) by A3;

          hence thesis by SCMPDS_5: 15;

        end;

        then ( sum (n,p0)) is_halting_on (( Initialize t),Q) by A1, Lm3, A3;

        hence ( sum (n,p0)) is_halting_on (t,Q) by SCMPDS_6: 126;

      end;

      hence thesis by SCMPDS_6: 21;

    end;

    begin

    scheme :: SCPINVAR:sch2

    WhileGEnd { F( State of SCMPDS ) -> Element of NAT , s() -> 0 -started State of SCMPDS , P() -> Instruction-Sequence of SCMPDS , I() -> halt-free shiftable Program of SCMPDS , a() -> Int_position , i() -> Integer , P[ set] } :

F(Initialize) = 0 & P[( Initialize ( IExec (( while>0 (a(),i(),I())),P(),s())))]

      provided

       A1: for t be 0 -started State of SCMPDS st P[t] holds F(t) = 0 iff (t . ( DataLoc ((s() . a()),i()))) <= 0

       and

       A2: P[s()]

       and

       A3: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (s() . a()) & (t . ( DataLoc ((s() . a()),i()))) > 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))];

      set b = ( DataLoc ((s() . a()),i())), WHL = ( while>0 (a(),i(),I()));

      defpred Q[ Nat] means for t be 0 -started State of SCMPDS , Q st F(t) <= $1 & (t . a()) = (s() . a()) & P[t] holds F(Initialize) = 0 & P[( Initialize ( IExec (WHL,Q,t)))];

      

       A4: Q[ 0 ]

      proof

        let t be 0 -started State of SCMPDS , Q;

        

         A5: ( Initialize t) = t by MEMSTR_0: 44;

        assume that

         A6: F(t) <= 0 and

         A7: (t . a()) = (s() . a()) and

         A8: P[t];

        

         A9: F(t) = 0 by A6;

        then (t . ( DataLoc ((s() . a()),i()))) <= 0 by A1, A8;

        then for b be Int_position holds (( IExec (WHL,Q,t)) . b) = (t . b) by A7, SCMPDS_8: 23;

        hence thesis by A8, A9, A5, SCPISORT: 4;

      end;

       A10:

      now

        let k be Nat;

        assume

         A11: Q[k];

        now

          let u be 0 -started State of SCMPDS ;

          let U;

          assume that

           A12: F(u) <= (k + 1) and

           A13: (u . a()) = (s() . a()) and

           A14: P[u];

          per cases ;

            suppose F(u) = 0 ;

            hence F(Initialize) = 0 & P[( Initialize ( IExec (WHL,U,u)))] by A4, A13, A14;

          end;

            suppose

             A15: F(u) <> 0 ;

            set Iu = ( IExec (I(),U,u));

            

             A16: (u . b) > 0 by A1, A14, A15;

            then

             A17: (Iu . a()) = (s() . a()) & P[( Initialize Iu)] by A3, A13, A14;

            deffunc F( State of SCMPDS ) = F($1);

            

             A18: P[u] by A14;

            

             A19: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ( DataLoc ((u . a()),i()))) <= 0 by A1, A13;

             F(Initialize) < F(u) by A3, A13, A14, A16;

            then ( F(Initialize) + 1) <= F(u) by INT_1: 7;

            then ( F(Initialize) + 1) <= (k + 1) by A12, XXREAL_0: 2;

            then

             A20: F(Initialize) <= k by XREAL_1: 6;

            

             A21: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (u . a()) & (t . ( DataLoc ((u . a()),i()))) > 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))] by A3, A13;

            

             A22: (u . ( DataLoc ((u . a()),i()))) > 0 by A1, A13, A14, A15;

            

             A23: ( IExec (WHL,U,u)) = ( IExec (WHL,U,( Initialize Iu))) from SCMPDS_8:sch 4( A22, A19, A18, A21);

            (( Initialize Iu) . a()) = (Iu . a()) by SCMPDS_5: 15;

            hence F(Initialize) = 0 & P[( Initialize ( IExec (WHL,U,u)))] by A11, A20, A17, A23;

          end;

        end;

        hence Q[(k + 1)];

      end;

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

      then Q[F(s)];

      hence thesis by A2;

    end;

    begin

    definition

      let n be Element of NAT ;

      :: SCPINVAR:def2

      func Fib-macro (n) -> Program of SCMPDS equals ((((( GBP := 0 ) ';' (( intpos 1) := 0 )) ';' (( intpos 2) := 1)) ';' (( intpos 3) := n)) ';' ( while>0 ( GBP ,3,((((( GBP ,4) := ( GBP ,2)) ';' ( AddTo ( GBP ,2, GBP ,1))) ';' (( GBP ,1) := ( GBP ,4))) ';' ( AddTo ( GBP ,3,( - 1)))))));

      coherence ;

    end

    theorem :: SCPINVAR:6

    

     Th6: for s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,f0,f1 be Int_position, n,i be Element of NAT st (s . a) = 0 & (s . f0) = 0 & (s . f1) = 1 & (s . ( intpos i)) = n & (for t be 0 -started State of SCMPDS , Q holds for k be Element of NAT st n = ((t . ( intpos i)) + k) & (t . f0) = ( Fib k) & (t . f1) = ( Fib (k + 1)) & (t . a) = 0 & (t . ( intpos i)) > 0 holds (( IExec (I,Q,t)) . a) = 0 & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec (I,Q,t)) . ( intpos i)) = ((t . ( intpos i)) - 1) & (( IExec (I,Q,t)) . f0) = ( Fib (k + 1)) & (( IExec (I,Q,t)) . f1) = ( Fib ((k + 1) + 1))) holds (( IExec (( while>0 (a,i,I)),P,s)) . f0) = ( Fib n) & (( IExec (( while>0 (a,i,I)),P,s)) . f1) = ( Fib (n + 1)) & ( while>0 (a,i,I)) is_closed_on (s,P) & ( while>0 (a,i,I)) is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,f0,f1 be Int_position, n,i be Element of NAT ;

      set Iw = ( IExec (( while>0 (a,i,I)),P,s)), Dw = ( Initialize Iw);

      set da = ( DataLoc ((s . a),i));

      defpred P[ State of SCMPDS ] means ($1 . ( intpos i)) >= 0 & ex k be Element of NAT st n = (($1 . ( intpos i)) + k) & ($1 . f0) = ( Fib k) & ($1 . f1) = ( Fib (k + 1));

      assume that

       A1: (s . a) = 0 and

       A2: (s . f0) = 0 and

       A3: (s . f1) = 1 and

       A4: (s . ( intpos i)) = n;

      consider ff be Function of ( product ( the_Values_of SCMPDS )), NAT such that

       A5: for t be State of SCMPDS holds ((t . da) <= 0 implies (ff . t) = 0 ) & ((t . da) > 0 implies (ff . t) = (t . da)) by SCMPDS_8: 5;

      

       A6: for t be 0 -started State of SCMPDS holds ((t . da) <= 0 implies (ff . t) = 0 ) & ((t . da) > 0 implies (ff . t) = (t . da)) by A5;

      deffunc F( State of SCMPDS ) = (ff . $1);

      

       A7: for t be 0 -started State of SCMPDS st P[t] holds not ( F(t) = 0 & (t . da) > 0 ) & ((t . da) <= 0 implies F(t) = 0 ) by A6;

      assume

       A8: for t be 0 -started State of SCMPDS , Q holds for k be Element of NAT st n = ((t . ( intpos i)) + k) & (t . f0) = ( Fib k) & (t . f1) = ( Fib (k + 1)) & (t . a) = 0 & (t . ( intpos i)) > 0 holds (( IExec (I,Q,t)) . a) = 0 & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec (I,Q,t)) . ( intpos i)) = ((t . ( intpos i)) - 1) & (( IExec (I,Q,t)) . f0) = ( Fib (k + 1)) & (( IExec (I,Q,t)) . f1) = ( Fib ((k + 1) + 1));

       A9:

      now

        let t be 0 -started State of SCMPDS , Q;

        assume that

         A10: P[t] and

         A11: (t . a) = (s . a) and

         A12: (t . ( DataLoc ((s . a),i))) > 0 ;

        set It = ( IExec (I,Q,t));

        set Dit = ( Initialize It);

        consider k be Element of NAT such that

         A13: n = ((t . ( intpos i)) + k) and

         A14: (t . f0) = ( Fib k) and

         A15: (t . f1) = ( Fib (k + 1)) by A10;

        

         A16: (t . f1) = ( Fib (k + 1)) by A15;

        

         A17: ( intpos ( 0 + i)) = da by A1, SCMP_GCD: 1;

        

         A18: n = ((t . ( intpos i)) + k) & (t . f0) = ( Fib k) by A13, A14;

        hence (( IExec (I,Q,t)) . a) = (t . a) by A1, A8, A11, A12, A16, A17;

        thus I is_closed_on (t,Q) & I is_halting_on (t,Q) by A1, A8, A11, A12, A18, A16, A17;

        

         A19: (It . ( intpos i)) = ((t . ( intpos i)) - 1) by A1, A8, A11, A12, A18, A16, A17;

        hereby

          per cases ;

            suppose (It . ( intpos i)) <= 0 ;

            then (Dit . da) <= 0 by A17, SCMPDS_5: 15;

            then

             A20: F(Dit) = 0 by A6;

             F(t) <> 0 by A7, A10, A12;

            hence F(Dit) < F(t) by A20;

          end;

            suppose

             A21: (It . ( intpos i)) > 0 ;

            (t . da) > 0 by A12;

            

            then

             A22: F(t) = (t . da) by A6

            .= (t . ( intpos i)) by A17;

            (Dit . da) > 0 by A17, A21, SCMPDS_5: 15;

            

            then F(Dit) = (Dit . da) by A6

            .= ((t . ( intpos i)) - 1) by A17, A19, SCMPDS_5: 15;

            hence F(Dit) < F(t) by A22, XREAL_1: 146;

          end;

        end;

        thus P[Dit]

        proof

          (t . ( intpos i)) >= (1 + 0 ) by A12, A17, INT_1: 7;

          then ((t . ( intpos i)) - 1) >= 0 by XREAL_1: 48;

          hence (Dit . ( intpos i)) >= 0 by A19, SCMPDS_5: 15;

          take m = (k + 1);

          

          thus n = ((((t . ( intpos i)) - 1) + 1) + k) by A13

          .= (((Dit . ( intpos i)) + 1) + k) by A19, SCMPDS_5: 15

          .= ((Dit . ( intpos i)) + m);

          (It . f0) = ( Fib m) & (It . f1) = ( Fib ((k + 1) + 1)) by A1, A8, A11, A12, A18, A16, A17;

          hence thesis by SCMPDS_5: 15;

        end;

      end;

      

       A23: P[s]

      proof

        (s . ( intpos i)) = n by A4;

        hence (s . ( intpos i)) >= 0 ;

        take k = 0 ;

        thus n = ((s . ( intpos i)) + k) by A4;

        thus (s . f0) = ( Fib k) by A2, PRE_FF: 1;

        thus thesis by A3, PRE_FF: 1;

      end;

      

       A24: F(Dw) = 0 & P[Dw] from WhileGEnd( A7, A23, A9);

      

       A25: (Dw . da) = (Iw . da) by SCMPDS_5: 15;

      (Dw . ( intpos i)) = (Iw . ( intpos ( 0 + i))) by SCMPDS_5: 15

      .= (Iw . da) by A1, SCMP_GCD: 1;

      then (Dw . ( intpos i)) <= 0 by A7, A24, A25;

      then (Dw . ( intpos i)) = 0 by A24;

      hence (Iw . f0) = ( Fib n) & (Iw . f1) = ( Fib (n + 1)) by A24, SCMPDS_5: 15;

      

       A26: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . da) <= 0 by A7;

      ( while>0 (a,i,I)) is_closed_on (s,P) & ( while>0 (a,i,I)) is_halting_on (s,P) from SCMPDS_8:sch 3( A26, A23, A9);

      hence thesis;

    end;

    set j1 = (( GBP ,4) := ( GBP ,2)), j2 = ( AddTo ( GBP ,2, GBP ,1)), j3 = (( GBP ,1) := ( GBP ,4)), j4 = ( AddTo ( GBP ,3,( - 1))), WB = (((j1 ';' j2) ';' j3) ';' j4), WH = ( while>0 ( GBP ,3,WB));

    

     Lm4: for s be 0 -started State of SCMPDS st (s . GBP ) = 0 holds (( IExec (WB,P,s)) . GBP ) = 0 & (( IExec (WB,P,s)) . a1) = (s . a2) & (( IExec (WB,P,s)) . a2) = ((s . a1) + (s . a2)) & (( IExec (WB,P,s)) . a3) = ((s . a3) - 1)

    proof

      set a = GBP ;

      let s be 0 -started State of SCMPDS ;

      set t0 = s, t1 = ( IExec (WB,P,s)), t2 = ( IExec (((j1 ';' j2) ';' j3),P,s)), Q0 = P, t3 = ( IExec ((j1 ';' j2),P,s)), t4 = ( Exec (j1,t0)), a4 = ( intpos 4);

      assume (s . a) = 0 ;

      then

       A1: (t0 . a) = 0 ;

      then ( DataLoc ((t0 . a),4)) = ( intpos ( 0 + 4)) by SCMP_GCD: 1;

      

      then

       A2: (t4 . a4) = (t0 . ( DataLoc ((t0 . a),2))) by SCMPDS_2: 47

      .= (t0 . ( intpos ( 0 + 2))) by A1, SCMP_GCD: 1

      .= (s . a2);

       0 <> |.((t0 . GBP ) + 4).| by A1, ABSVALUE:def 1;

      then a <> ( DataLoc ((t0 . GBP ),4)) by XTUPLE_0: 1;

      then

       A3: (t4 . a) = 0 by A1, SCMPDS_2: 47;

      then

       A4: ( DataLoc ((t4 . a),2)) = ( intpos ( 0 + 2)) by SCMP_GCD: 1;

       0 <> |.((t4 . GBP ) + 2).| by A3, ABSVALUE:def 1;

      then

       A5: a <> ( DataLoc ((t4 . GBP ),2)) by XTUPLE_0: 1;

      

       A6: (t3 . a) = (( Exec (j2,t4)) . a) by SCMPDS_5: 42

      .= 0 by A3, A5, SCMPDS_2: 49;

      then

       A7: ( DataLoc ((t3 . a),1)) = ( intpos ( 0 + 1)) by SCMP_GCD: 1;

      4 <> |.((t4 . GBP ) + 2).| by A3, ABSVALUE:def 1;

      then

       A8: a4 <> ( DataLoc ((t4 . GBP ),2)) by XTUPLE_0: 1;

      

       A9: (t3 . a4) = (( Exec (j2,t4)) . a4) by SCMPDS_5: 42

      .= (s . a2) by A2, A8, SCMPDS_2: 49;

      

       A10: (t2 . a1) = (( Exec (j3,t3)) . a1) by SCMPDS_5: 41

      .= (t3 . ( DataLoc ((t3 . a),4))) by A7, SCMPDS_2: 47

      .= (s . a2) by A6, A9, SCMP_GCD: 1;

      3 <> |.((t4 . GBP ) + 2).| by A3, ABSVALUE:def 1;

      then

       A11: a3 <> ( DataLoc ((t4 . GBP ),2)) by XTUPLE_0: 1;

      2 <> |.((t0 . GBP ) + 4).| by A1, ABSVALUE:def 1;

      then a2 <> ( DataLoc ((t0 . GBP ),4)) by XTUPLE_0: 1;

      

      then

       A12: (t4 . a2) = (t0 . a2) by SCMPDS_2: 47

      .= (s . a2);

      1 <> |.((t0 . GBP ) + 4).| by A1, ABSVALUE:def 1;

      then a1 <> ( DataLoc ((t0 . GBP ),4)) by XTUPLE_0: 1;

      

      then

       A13: (t4 . a1) = (t0 . a1) by SCMPDS_2: 47

      .= (s . a1);

      3 <> |.((t0 . GBP ) + 4).| by A1, ABSVALUE:def 1;

      then a3 <> ( DataLoc ((t0 . GBP ),4)) by XTUPLE_0: 1;

      

      then

       A14: (t4 . a3) = (t0 . a3) by SCMPDS_2: 47

      .= (s . a3);

       0 <> |.((t3 . GBP ) + 1).| by A6, ABSVALUE:def 1;

      then

       A15: a <> ( DataLoc ((t3 . GBP ),1)) by XTUPLE_0: 1;

      

       A16: (t2 . a) = (( Exec (j3,t3)) . a) by SCMPDS_5: 41

      .= 0 by A6, A15, SCMPDS_2: 47;

      then

       A17: ( DataLoc ((t2 . a),3)) = ( intpos ( 0 + 3)) by SCMP_GCD: 1;

      2 <> |.((t3 . GBP ) + 1).| by A6, ABSVALUE:def 1;

      then

       A18: a2 <> ( DataLoc ((t3 . GBP ),1)) by XTUPLE_0: 1;

      

       A19: (t3 . a2) = (( Exec (j2,t4)) . a2) by SCMPDS_5: 42

      .= ((t4 . a2) + (t4 . ( DataLoc ((t4 . a),1)))) by A4, SCMPDS_2: 49

      .= ((s . a2) + (s . a1)) by A3, A13, A12, SCMP_GCD: 1;

      

       A20: (t2 . a2) = (( Exec (j3,t3)) . a2) by SCMPDS_5: 41

      .= ((s . a2) + (s . a1)) by A19, A18, SCMPDS_2: 47;

      3 <> |.((t3 . GBP ) + 1).| by A6, ABSVALUE:def 1;

      then

       A21: a3 <> ( DataLoc ((t3 . GBP ),1)) by XTUPLE_0: 1;

       0 <> |.((t2 . GBP ) + 3).| by A16, ABSVALUE:def 1;

      then

       A22: a <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

      thus (t1 . a) = (( Exec (j4,t2)) . a) by SCMPDS_5: 41

      .= 0 by A16, A22, SCMPDS_2: 48;

      1 <> |.((t2 . GBP ) + 3).| by A16, ABSVALUE:def 1;

      then

       A23: a1 <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

      thus (t1 . a1) = (( Exec (j4,t2)) . a1) by SCMPDS_5: 41

      .= (s . a2) by A10, A23, SCMPDS_2: 48;

      2 <> |.((t2 . GBP ) + 3).| by A16, ABSVALUE:def 1;

      then

       A24: a2 <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

       A25: (t3 . a3) = (( Exec (j2,t4)) . a3) by SCMPDS_5: 42

      .= (s . a3) by A14, A11, SCMPDS_2: 49;

      

       A26: (t2 . a3) = (( Exec (j3,t3)) . a3) by SCMPDS_5: 41

      .= (s . a3) by A25, A21, SCMPDS_2: 47;

      

      thus (t1 . a2) = (( Exec (j4,t2)) . a2) by SCMPDS_5: 41

      .= ((s . a1) + (s . a2)) by A20, A24, SCMPDS_2: 48;

      

      thus (t1 . a3) = (( Exec (j4,t2)) . a3) by SCMPDS_5: 41

      .= ((t2 . a3) + ( - 1)) by A17, SCMPDS_2: 48

      .= ((s . a3) - 1) by A26;

    end;

    

     Lm5: for s be 0 -started State of SCMPDS , n be Element of NAT st (s . GBP ) = 0 & (s . a1) = 0 & (s . a2) = 1 & (s . a3) = n holds (( IExec (WH,P,s)) . a1) = ( Fib n) & (( IExec (WH,P,s)) . a2) = ( Fib (n + 1)) & WH is_closed_on (s,P) & WH is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , n be Element of NAT ;

      set a = GBP ;

       A1:

      now

        let t be 0 -started State of SCMPDS , Q;

        let k be Element of NAT ;

        assume that n = ((t . a3) + k) and

         A2: (t . a1) = ( Fib k) and

         A3: (t . a2) = ( Fib (k + 1)) and

         A4: (t . a) = 0 and (t . a3) > 0 ;

        thus (( IExec (WB,Q,t)) . a) = 0 by A4, Lm4;

        thus WB is_closed_on (t,Q) & WB is_halting_on (t,Q) by SCMPDS_6: 20, SCMPDS_6: 21;

        thus (( IExec (WB,Q,t)) . a3) = ((t . a3) - 1) by A4, Lm4;

        thus (( IExec (WB,Q,t)) . a1) = ( Fib (k + 1)) by A3, A4, Lm4;

        

        thus (( IExec (WB,Q,t)) . a2) = ((t . a1) + (t . a2)) by A4, Lm4

        .= ( Fib ((k + 1) + 1)) by A2, A3, PRE_FF: 1;

      end;

      assume (s . GBP ) = 0 & (s . a1) = 0 & (s . a2) = 1 & (s . a3) = n;

      hence thesis by A1, Th6;

    end;

    

     Lm6: for s be 0 -started State of SCMPDS , n be Element of NAT holds (( IExec (( Fib-macro n),P,s)) . a1) = ( Fib n) & (( IExec (( Fib-macro n),P,s)) . a2) = ( Fib (n + 1)) & ( Fib-macro n) is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , n be Element of NAT ;

      set a = GBP , i1 = (a := 0 ), i2 = (a1 := 0 ), i3 = (a2 := 1), i4 = (a3 := n), I4 = (((i1 ';' i2) ';' i3) ';' i4), t1 = ( IExec (I4,P,s)), t2 = ( IExec (((i1 ';' i2) ';' i3),P,s)), t3 = ( IExec ((i1 ';' i2),P,s)), t4 = ( Exec (i1,s));

      

       A1: ( Initialize s) = s by MEMSTR_0: 44;

      

       A2: (t4 . a) = 0 by SCMPDS_2: 45;

      

       A3: (t3 . a) = (( Exec (i2,t4)) . a) by SCMPDS_5: 42

      .= 0 by A2, AMI_3: 10, SCMPDS_2: 45;

      

       A4: (t2 . a) = (( Exec (i3,t3)) . a) by SCMPDS_5: 41

      .= 0 by A3, AMI_3: 10, SCMPDS_2: 45;

      

       A5: (t3 . a1) = (( Exec (i2,t4)) . a1) by SCMPDS_5: 42

      .= 0 by SCMPDS_2: 45;

      

       A6: (t2 . a1) = (( Exec (i3,t3)) . a1) by SCMPDS_5: 41

      .= 0 by A5, AMI_3: 10, SCMPDS_2: 45;

      

       A7: (t1 . a1) = (( Exec (i4,t2)) . a1) by SCMPDS_5: 41

      .= 0 by A6, AMI_3: 10, SCMPDS_2: 45;

      

       A8: (t2 . a2) = (( Exec (i3,t3)) . a2) by SCMPDS_5: 41

      .= 1 by SCMPDS_2: 45;

      

       A9: (t1 . a2) = (( Exec (i4,t2)) . a2) by SCMPDS_5: 41

      .= 1 by A8, AMI_3: 10, SCMPDS_2: 45;

      

       A10: (t1 . a3) = (( Exec (i4,t2)) . a3) by SCMPDS_5: 41

      .= n by SCMPDS_2: 45;

      

       A11: (t1 . a) = (( Exec (i4,t2)) . a) by SCMPDS_5: 41

      .= 0 by A4, AMI_3: 10, SCMPDS_2: 45;

      

       A12: (( Initialize t1) . GBP ) = (t1 . GBP ) by SCMPDS_5: 15;

      

       A13: (( Initialize t1) . a1) = (t1 . a1) by SCMPDS_5: 15;

      

       A14: (( Initialize t1) . a2) = (t1 . a2) by SCMPDS_5: 15;

      

       A15: (( Initialize t1) . a3) = (t1 . a3) by SCMPDS_5: 15;

      

       A16: WH is_closed_on (( Initialize t1),P) & WH is_halting_on (( Initialize t1),P) by A7, A9, A10, Lm5, A11, A12, A13, A14, A15;

      

       A17: WH is_closed_on (t1,P)

      proof

        for k be Nat holds ( IC ( Comput ((P +* ( stop WH)),( Initialize ( Initialize t1)),k))) in ( dom ( stop WH)) by A16, SCMPDS_6:def 2;

        hence thesis by SCMPDS_6:def 2;

      end;

      

       A18: WH is_halting_on (t1,P)

      proof

        (P +* ( stop WH)) halts_on ( Initialize ( Initialize t1)) by A16, SCMPDS_6:def 3;

        hence thesis by SCMPDS_6:def 3;

      end;

      (( IExec (WH,P,( Initialize t1))) . a1) = ( Fib n) by A11, A7, A9, A10, Lm5, A12, A13, A14, A15;

      hence (( IExec (( Fib-macro n),P,s)) . a1) = ( Fib n) by A17, A18, SCPISORT: 7;

      (( IExec (WH,P,( Initialize t1))) . a2) = ( Fib (n + 1)) by A11, A7, A9, A10, Lm5, A12, A13, A14, A15;

      hence (( IExec (( Fib-macro n),P,s)) . a2) = ( Fib (n + 1)) by A17, A18, SCPISORT: 7;

      thus thesis by A17, A18, A1, SCPISORT: 9;

    end;

    theorem :: SCPINVAR:7

    for s be 0 -started State of SCMPDS , n be Element of NAT holds (( IExec (( Fib-macro n),P,s)) . ( intpos 1)) = ( Fib n) & (( IExec (( Fib-macro n),P,s)) . ( intpos 2)) = ( Fib (n + 1)) & ( Fib-macro n) is parahalting

    proof

      let s be 0 -started State of SCMPDS , n be Element of NAT ;

      thus (( IExec (( Fib-macro n),P,s)) . a1) = ( Fib n) & (( IExec (( Fib-macro n),P,s)) . a2) = ( Fib (n + 1)) by Lm6;

      for t be State of SCMPDS , Q holds ( Fib-macro n) is_halting_on (t,Q)

      proof

        let t be State of SCMPDS , Q;

        ( Fib-macro n) is_halting_on (( Initialize t),Q) by Lm6;

        hence thesis by SCMPDS_6: 126;

      end;

      hence thesis by SCMPDS_6: 21;

    end;

    begin

    definition

      let a be Int_position, i be Integer;

      let I be Program of SCMPDS ;

      :: SCPINVAR:def3

      func while<>0 (a,i,I) -> Program of SCMPDS equals (((((a,i) <>0_goto 2) ';' ( goto (( card I) + 2))) ';' I) ';' ( goto ( - (( card I) + 2))));

      coherence ;

    end

    begin

    theorem :: SCPINVAR:8

    

     Th8: for a be Int_position, i be Integer, I be Program of SCMPDS holds ( card ( while<>0 (a,i,I))) = (( card I) + 3)

    proof

      let a be Int_position, i be Integer, I be Program of SCMPDS ;

      set i1 = ((a,i) <>0_goto 2), i2 = ( goto (( card I) + 2));

      set I4 = ((i1 ';' i2) ';' I);

      

      thus ( card ( while<>0 (a,i,I))) = (( card I4) + 1) by SCMP_GCD: 4

      .= ((( card (i1 ';' i2)) + ( card I)) + 1) by AFINSQ_1: 17

      .= ((2 + ( card I)) + 1) by SCMP_GCD: 5

      .= (( card I) + 3);

    end;

    

     Lm7: for a be Int_position, i be Integer, I be Program of SCMPDS holds ( card ( stop ( while<>0 (a,i,I)))) = (( card I) + 4)

    proof

      let a be Int_position, i be Integer, I be Program of SCMPDS ;

      

      thus ( card ( stop ( while<>0 (a,i,I)))) = (( card ( while<>0 (a,i,I))) + 1) by COMPOS_1: 55

      .= ((( card I) + 3) + 1) by Th8

      .= (( card I) + 4);

    end;

    theorem :: SCPINVAR:9

    

     Th9: for a be Int_position, i be Integer, m be Element of NAT , I be Program of SCMPDS holds m < (( card I) + 3) iff m in ( dom ( while<>0 (a,i,I)))

    proof

      let a be Int_position, i be Integer, m be Element of NAT , I be Program of SCMPDS ;

      ( card ( while<>0 (a,i,I))) = (( card I) + 3) by Th8;

      hence thesis by AFINSQ_1: 66;

    end;

    theorem :: SCPINVAR:10

    

     Th10: for a be Int_position, i be Integer, I be Program of SCMPDS holds 0 in ( dom ( while<>0 (a,i,I))) & 1 in ( dom ( while<>0 (a,i,I)))

    proof

      let a be Int_position, i be Integer, I be Program of SCMPDS ;

      3 <= (( card I) + 3) by NAT_1: 11;

      then 0 < (( card I) + 3) & 1 < (( card I) + 3) by XXREAL_0: 2;

      hence thesis by Th9;

    end;

    theorem :: SCPINVAR:11

    

     Th11: for a be Int_position, i be Integer, I be Program of SCMPDS holds (( while<>0 (a,i,I)) . 0 ) = ((a,i) <>0_goto 2) & (( while<>0 (a,i,I)) . 1) = ( goto (( card I) + 2)) & (( while<>0 (a,i,I)) . (( card I) + 2)) = ( goto ( - (( card I) + 2)))

    proof

      let a be Int_position, i be Integer, I be Program of SCMPDS ;

      set i1 = ((a,i) <>0_goto 2), i2 = ( goto (( card I) + 2)), i3 = ( goto ( - (( card I) + 2)));

      set I4 = ((i1 ';' i2) ';' I);

      set WHL = ( while<>0 (a,i,I));

      

       A1: WHL = ((i1 ';' i2) ';' (I ';' i3)) by SCMPDS_4: 11;

      hence (WHL . 0 ) = i1 by Th1;

      thus (WHL . 1) = i2 by A1, Th1;

      ( card I4) = (( card (i1 ';' i2)) + ( card I)) by AFINSQ_1: 17

      .= (( card I) + 2) by SCMP_GCD: 5;

      hence thesis by SCMP_GCD: 6;

    end;

    

     Lm8: for a be Int_position, i be Integer, I be Program of SCMPDS holds ( while<>0 (a,i,I)) = (((a,i) <>0_goto 2) ';' ((( goto (( card I) + 2)) ';' I) ';' ( goto ( - (( card I) + 2)))))

    proof

      let a be Int_position, i be Integer, I be Program of SCMPDS ;

      set i1 = ((a,i) <>0_goto 2), i2 = ( goto (( card I) + 2)), i3 = ( goto ( - (( card I) + 2)));

      

      thus ( while<>0 (a,i,I)) = ((i1 ';' (i2 ';' I)) ';' i3) by SCMPDS_4: 16

      .= (i1 ';' ((i2 ';' I) ';' i3)) by SCMPDS_4: 15;

    end;

    theorem :: SCPINVAR:12

    

     Th12: for s be State of SCMPDS , I be Program of SCMPDS , a be Int_position, i be Integer st (s . ( DataLoc ((s . a),i))) = 0 holds ( while<>0 (a,i,I)) is_closed_on (s,P) & ( while<>0 (a,i,I)) is_halting_on (s,P)

    proof

      let s be State of SCMPDS , I be Program of SCMPDS , a be Int_position, i be Integer;

      set b = ( DataLoc ((s . a),i));

      assume

       A1: (s . b) = 0 ;

      set WHL = ( while<>0 (a,i,I)), pWH = ( stop WHL), iWH = pWH, s3 = ( Initialize s), P3 = (P +* pWH), s4 = ( Comput (P3,s3,1)), s5 = ( Comput (P3,s3,2)), P4 = P3, P5 = P3;

      

       A2: not b in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

       not a in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

      

      then

       A3: (s3 . ( DataLoc ((s3 . a),i))) = (s3 . b) by FUNCT_4: 11

      .= 0 by A1, A2, FUNCT_4: 11;

      set i1 = ((a,i) <>0_goto 2), i2 = ( goto (( card I) + 2)), i3 = ( goto ( - (( card I) + 2)));

      

       A4: ( IC s3) = 0 by MEMSTR_0: 47;

      

       A5: WHL = (i1 ';' ((i2 ';' I) ';' i3)) by Lm8;

      ( Comput (P3,s3,( 0 + 1))) = ( Following (P3,( Comput (P3,s3, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s3))

      .= ( Exec (i1,s3)) by A5, SCMPDS_6: 11;

      

      then

       A6: ( IC s4) = (( IC s3) + 1) by A3, SCMPDS_2: 55

      .= ( 0 + 1) by A4;

      

       A7: iWH c= P3 by FUNCT_4: 25;

      then

       A8: pWH c= P4;

      

       A9: 1 in ( dom WHL) by Th10;

      then 1 in ( dom pWH) by COMPOS_1: 62;

      

      then

       A10: (P4 . 1) = (pWH . 1) by A8, GRFUNC_1: 2

      .= (WHL . 1) by A9, COMPOS_1: 63

      .= i2 by Th11;

      

       A11: ( card WHL) = (( card I) + 3) by Th8;

      then

       A12: (( card I) + 3) in ( dom pWH) by COMPOS_1: 64;

      

       A13: (P4 /. ( IC s4)) = (P4 . ( IC s4)) by PBOOLE: 143;

      ( Comput (P3,s3,(1 + 1))) = ( Following (P3,s4)) by EXTPRO_1: 3

      .= ( Exec (i2,s4)) by A6, A10, A13;

      

      then

       A14: ( IC s5) = ( ICplusConst (s4,(( card I) + 2))) by SCMPDS_2: 54

      .= ((( card I) + 2) + 1) by A6, SCMPDS_6: 12

      .= (( card I) + (2 + 1));

      

       A15: (P5 /. ( IC s5)) = (P5 . ( IC s5)) by PBOOLE: 143;

      pWH c= P5 by A7;

      

      then (P5 . (( card I) + 3)) = (pWH . (( card I) + 3)) by A12, GRFUNC_1: 2

      .= ( halt SCMPDS ) by A11, COMPOS_1: 64;

      then

       A16: ( CurInstr (P5,s5)) = ( halt SCMPDS ) by A14, A15;

      now

        let k be Nat;

        k = 0 or 0 < k;

        then

         A17: k = 0 or ( 0 + 1) <= k by INT_1: 7;

        per cases by A17, XXREAL_0: 1;

          suppose k = 0 ;

          then ( Comput (P3,s3,k)) = s3;

          hence ( IC ( Comput (P3,s3,k))) in ( dom pWH) by A4, COMPOS_1: 36;

        end;

          suppose k = 1;

          hence ( IC ( Comput (P3,s3,k))) in ( dom pWH) by A9, A6, COMPOS_1: 62;

        end;

          suppose 1 < k;

          then (1 + 1) <= k by INT_1: 7;

          hence ( IC ( Comput (P3,s3,k))) in ( dom pWH) by A12, A14, A16, EXTPRO_1: 5;

        end;

      end;

      hence WHL is_closed_on (s,P) by SCMPDS_6:def 2;

      P3 halts_on s3 by A16, EXTPRO_1: 29;

      hence thesis by SCMPDS_6:def 3;

    end;

    theorem :: SCPINVAR:13

    

     Th13: for s be State of SCMPDS , I be Program of SCMPDS , a,c be Int_position, i be Integer st (s . ( DataLoc ((s . a),i))) = 0 holds ( IExec (( while<>0 (a,i,I)),P,( Initialize s))) = (s +* ( Start-At ((( card I) + 3), SCMPDS )))

    proof

      let s be State of SCMPDS , I be Program of SCMPDS , a,c be Int_position, i be Integer;

      set b = ( DataLoc ((s . a),i));

      assume

       A1: (s . b) = 0 ;

      set i1 = ((a,i) <>0_goto 2), i2 = ( goto (( card I) + 2)), i3 = ( goto ( - (( card I) + 2)));

      set WHL = ( while<>0 (a,i,I)), pWH = ( stop WHL), iWH = pWH, s3 = ( Initialize s), P3 = (P +* pWH), s4 = ( Comput (P3,s3,1)), s5 = ( Comput (P3,s3,2)), P4 = P3, P5 = P3;

      

       A2: ( IC s3) = 0 by MEMSTR_0: 47;

      

       A3: iWH c= P3 by FUNCT_4: 25;

      then

       A4: pWH c= P4;

      

       A5: pWH c= P5 by A3;

      

       A6: not b in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

      

       A7: WHL = (i1 ';' ((i2 ';' I) ';' i3)) by Lm8;

      

       A8: ( Comput (P3,s3,( 0 + 1))) = ( Following (P3,( Comput (P3,s3, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s3))

      .= ( Exec (i1,s3)) by A7, SCMPDS_6: 11;

      

       A9: 1 in ( dom WHL) by Th10;

      then 1 in ( dom pWH) by COMPOS_1: 62;

      

      then

       A10: (P4 . 1) = (pWH . 1) by A4, GRFUNC_1: 2

      .= (WHL . 1) by A9, COMPOS_1: 63

      .= i2 by Th11;

      set SAl = ( Start-At ((( card I) + 3), SCMPDS ));

       not a in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

      

      then (s3 . ( DataLoc ((s3 . a),i))) = (s3 . b) by FUNCT_4: 11

      .= 0 by A1, A6, FUNCT_4: 11;

      

      then

       A11: ( IC s4) = (( IC s3) + 1) by A8, SCMPDS_2: 55

      .= ( 0 + 1) by A2;

      

       A12: (P3 /. ( IC s4)) = (P4 . ( IC s4)) by PBOOLE: 143;

      

       A13: ( Comput (P3,s3,(1 + 1))) = ( Following (P3,s4)) by EXTPRO_1: 3

      .= ( Exec (i2,s4)) by A11, A10, A12;

      

      then

       A14: ( IC s5) = ( ICplusConst (s4,(( card I) + 2))) by SCMPDS_2: 54

      .= ((( card I) + 2) + 1) by A11, SCMPDS_6: 12

      .= (( card I) + (2 + 1));

      

       A15: (P3 /. ( IC s5)) = (P5 . ( IC s5)) by PBOOLE: 143;

      

       A16: ( card WHL) = (( card I) + 3) by Th8;

      then (( card I) + 3) in ( dom pWH) by COMPOS_1: 64;

      

      then (P5 . (( card I) + 3)) = (pWH . (( card I) + 3)) by A5, GRFUNC_1: 2

      .= ( halt SCMPDS ) by A16, COMPOS_1: 64;

      then

       A17: ( CurInstr (P3,s5)) = ( halt SCMPDS ) by A14, A15;

      then P3 halts_on s3 by EXTPRO_1: 29;

      then

       A18: s5 = ( Result (P3,s3)) by A17, EXTPRO_1:def 9;

      

       A19: ( IExec (WHL,P,( Initialize s))) = ( Result (P3,s3)) by SCMPDS_4:def 5;

       A20:

      now

        let x be object;

        

         A21: ( dom SAl) = {( IC SCMPDS )} by FUNCOP_1: 13;

        assume

         A22: x in ( dom ( IExec (WHL,P,( Initialize s))));

        per cases by A22, SCMPDS_4: 6;

          suppose

           A23: x is Int_position;

          then x <> ( IC SCMPDS ) by SCMPDS_2: 43;

          then

           A24: not x in ( dom SAl) by A21, TARSKI:def 1;

          

           A25: not x in ( dom ( Start-At ( 0 , SCMPDS ))) by A23, SCMPDS_4: 18;

          

          thus (( IExec (WHL,P,( Initialize s))) . x) = (s5 . x) by A18, A19

          .= (s4 . x) by A13, A23, SCMPDS_2: 54

          .= (s3 . x) by A8, A23, SCMPDS_2: 55

          .= (s . x) by A25, FUNCT_4: 11

          .= ((s +* SAl) . x) by A24, FUNCT_4: 11;

        end;

          suppose

           A26: x = ( IC SCMPDS );

          

          hence (( IExec (WHL,P,( Initialize s))) . x) = (( card I) + 3) by A14, A18, A19

          .= ((s +* SAl) . x) by A26, FUNCT_4: 113;

        end;

      end;

      ( dom ( IExec (WHL,P,( Initialize s)))) = the carrier of SCMPDS by PARTFUN1:def 2

      .= ( dom (s +* SAl)) by PARTFUN1:def 2;

      hence thesis by A20, FUNCT_1: 2;

    end;

    theorem :: SCPINVAR:14

    for s be State of SCMPDS , I be Program of SCMPDS , a be Int_position, i be Integer st (s . ( DataLoc ((s . a),i))) = 0 holds ( IC ( IExec (( while<>0 (a,i,I)),P,( Initialize s)))) = (( card I) + 3)

    proof

      let s be State of SCMPDS , I be Program of SCMPDS , a be Int_position, i be Integer;

      assume (s . ( DataLoc ((s . a),i))) = 0 ;

      then ( IExec (( while<>0 (a,i,I)),P,( Initialize s))) = (s +* ( Start-At ((( card I) + 3), SCMPDS ))) by Th13;

      hence thesis by FUNCT_4: 113;

    end;

    theorem :: SCPINVAR:15

    

     Th15: for s be State of SCMPDS , I be Program of SCMPDS , a,b be Int_position, i be Integer st (s . ( DataLoc ((s . a),i))) = 0 holds (( IExec (( while<>0 (a,i,I)),P,( Initialize s))) . b) = (s . b)

    proof

      let s be State of SCMPDS , I be Program of SCMPDS , a,b be Int_position, i be Integer;

      assume (s . ( DataLoc ((s . a),i))) = 0 ;

      then

       A1: ( IExec (( while<>0 (a,i,I)),P,( Initialize s))) = (s +* ( Start-At ((( card I) + 3), SCMPDS ))) by Th13;

       not b in ( dom ( Start-At ((( card I) + 3), SCMPDS ))) by SCMPDS_4: 18;

      hence thesis by A1, FUNCT_4: 11;

    end;

    

     Lm9: for I be Program of SCMPDS , a be Int_position, i be Integer holds ( Shift (I,2)) c= ( while<>0 (a,i,I))

    proof

      let I be Program of SCMPDS , a be Int_position, i be Integer;

      set i1 = ((a,i) <>0_goto 2), i2 = ( goto (( card I) + 2)), i3 = ( goto ( - (( card I) + 2)));

      ( card (i1 ';' i2)) = 2 & ( while<>0 (a,i,I)) = (((i1 ';' i2) ';' I) ';' ( Load i3)) by SCMPDS_4:def 3, SCMP_GCD: 5;

      hence thesis by SCMPDS_7: 3;

    end;

    registration

      let I be shiftable Program of SCMPDS , a be Int_position, i be Integer;

      cluster ( while<>0 (a,i,I)) -> shiftable;

      correctness

      proof

        set WHL = ( while<>0 (a,i,I)), i1 = ((a,i) <>0_goto 2), i2 = ( goto (( card I) + 2)), PF = ((i1 ';' i2) ';' I);

        ( card PF) = (( card (i1 ';' i2)) + ( card I)) by AFINSQ_1: 17

        .= (2 + ( card I)) by SCMP_GCD: 5;

        then PF = ((( Load i1) ';' ( Load i2)) ';' I) & (( card PF) + ( - (( card I) + 2))) = 0 by SCMPDS_4:def 4;

        hence thesis by SCMPDS_4: 23;

      end;

    end

    registration

      let I be halt-free Program of SCMPDS , a be Int_position, i be Integer;

      cluster ( while<>0 (a,i,I)) -> halt-free;

      correctness

      proof

        reconsider i2 = ( goto (( card I) + 2)) as No-StopCode Instruction of SCMPDS by SCMPDS_5: 21;

        reconsider i3 = ( goto ( - (( card I) + 2))) as No-StopCode Instruction of SCMPDS by SCMPDS_5: 21;

        ( while<>0 (a,i,I)) = (((((a,i) <>0_goto 2) ';' i2) ';' I) ';' i3);

        hence thesis;

      end;

    end

    begin

    scheme :: SCPINVAR:sch3

    WhileNHalt { F( State of SCMPDS ) -> Element of NAT , s() -> 0 -started State of SCMPDS , P() -> Instruction-Sequence of SCMPDS , I() -> halt-free shiftable Program of SCMPDS , a() -> Int_position , i() -> Integer , P[ set] } :

( while<>0 (a(),i(),I())) is_closed_on (s(),P()) & ( while<>0 (a(),i(),I())) is_halting_on (s(),P())

      provided

       A1: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ( DataLoc ((s() . a()),i()))) = 0

       and

       A2: P[s()]

       and

       A3: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (s() . a()) & (t . ( DataLoc ((s() . a()),i()))) <> 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))];

      

       A4: ( Initialize s()) = s() by MEMSTR_0: 44;

      set i1 = ((a(),i()) <>0_goto 2), i2 = ( goto (( card I()) + 2)), i3 = ( goto ( - (( card I()) + 2)));

      set WHL = ( while<>0 (a(),i(),I())), pWH = ( stop WHL), pI = ( stop I());

      set b = ( DataLoc ((s() . a()),i()));

      defpred Q[ Nat] means for t be 0 -started State of SCMPDS , Q st F(Initialize) <= $1 & P[( Initialize t)] & (t . a()) = (s() . a()) holds WHL is_closed_on (t,Q) & WHL is_halting_on (t,Q);

      

       A5: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        assume

         A6: Q[k];

        now

          let t be 0 -started State of SCMPDS ;

          let Q;

          

           A7: ( Initialize t) = t by MEMSTR_0: 44;

          assume

           A8: F(Initialize) <= (k + 1);

          assume

           A9: P[( Initialize t)];

          assume

           A10: (t . a()) = (s() . a());

          per cases ;

            suppose (t . b) = 0 ;

            hence WHL is_closed_on (t,Q) & WHL is_halting_on (t,Q) by A10, Th12;

          end;

            suppose

             A11: (t . b) <> 0 ;

            

             A12: (( IExec (I(),Q,t)) . a()) = (t . a()) by A3, A9, A10, A11, A7;

            

             A13: 0 in ( dom pWH) by COMPOS_1: 36;

            

             A14: WHL = (i1 ';' ((i2 ';' I()) ';' i3)) by Lm8;

            

             A15: not b in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

            set t2 = ( Initialize t), Q2 = (Q +* pI), t3 = ( Initialize t), Q3 = (Q +* pWH), t4 = ( Comput (Q3,t3,1)), Q4 = Q3;

            

             A16: pI c= Q2 by FUNCT_4: 25;

            set m2 = ( LifeSpan (Q2,t2)), t5 = ( Comput (Q4,t4,m2)), Q5 = Q4, l2 = (( card I()) + 2);

            

             A17: ( IC t3) = 0 by MEMSTR_0: 47;

            set m3 = (m2 + 1);

            set t6 = ( Comput (Q3,t3,m3)), Q6 = Q3;

            set t7 = ( Comput (Q3,t3,(m3 + 1))), Q7 = Q3;

            (( card I()) + 2) < (( card I()) + 3) by XREAL_1: 6;

            then

             A18: l2 in ( dom WHL) by Th9;

            

             A19: pWH c= Q3 by FUNCT_4: 25;

            WHL c= pWH by AFINSQ_1: 74;

            then

             A20: WHL c= Q3 by A19, XBOOLE_1: 1;

            ( Shift (I(),2)) c= WHL by Lm9;

            then ( Shift (I(),2)) c= Q3 by A20, XBOOLE_1: 1;

            then

             A21: ( Shift (I(),2)) c= Q4;

            

             A22: ( Comput (Q3,t3,( 0 + 1))) = ( Following (Q3,( Comput (Q3,t3, 0 )))) by EXTPRO_1: 3

            .= ( Following (Q3,t3))

            .= ( Exec (i1,t3)) by A14, SCMPDS_6: 11;

            for a holds (t2 . a) = (t4 . a) by A22, SCMPDS_2: 55;

            then

             A23: ( DataPart t2) = ( DataPart t4) by SCMPDS_4: 8;

            I() is_halting_on (t,Q) by A3, A9, A10, A11, A7;

            then

             A24: Q2 halts_on t2 by SCMPDS_6:def 3;

            (Q2 +* pI) halts_on ( Initialize t2) by A24;

            then

             A25: I() is_halting_on (t2,Q2) by SCMPDS_6:def 3;

            

             A26: ( IExec (I(),Q,( Initialize t))) = ( Result (Q2,t2)) by SCMPDS_4:def 5;

            

             A27: P[( Initialize ( IExec (I(),Q,( Initialize t))))] by A3, A9, A10, A11, A7;

            

             A28: I() is_closed_on (t,Q) by A3, A9, A10, A11, A7;

            then

             A29: I() is_closed_on (t2,Q2) by SCMPDS_6: 24;

             not a() in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

            

            then (t3 . ( DataLoc ((t3 . a()),i()))) = (t3 . b) by A10, FUNCT_4: 11

            .= (t . b) by A15, FUNCT_4: 11;

            

            then

             A30: ( IC t4) = ( ICplusConst (t3,2)) by A11, A22, SCMPDS_2: 55

            .= ( 0 + 2) by A17, SCMPDS_6: 12;

            then

             A31: ( IC t5) = l2 by A16, A25, A29, A23, A21, SCMPDS_7: 18;

            

             A32: (Q6 /. ( IC t6)) = (Q6 . ( IC t6)) by PBOOLE: 143;

            

             A33: t6 = t5 by EXTPRO_1: 4;

            

            then

             A34: ( CurInstr (Q6,t6)) = (Q5 . l2) by A16, A25, A29, A30, A23, A21, A32, SCMPDS_7: 18

            .= (Q4 . l2)

            .= (Q3 . l2)

            .= (WHL . l2) by A18, A20, GRFUNC_1: 2

            .= i3 by Th11;

            

             A35: t7 = ( Following (Q3,t6)) by EXTPRO_1: 3

            .= ( Exec (i3,t6)) by A34;

            

            then ( IC t7) = ( ICplusConst (t6,( 0 - (( card I()) + 2)))) by SCMPDS_2: 54

            .= 0 by A31, A33, SCMPDS_7: 1;

            then

             A36: ( Initialize t7) = t7 by MEMSTR_0: 46;

            

             A37: (Q7 +* pWH) = Q7;

            

             A38: ( DataPart ( Comput (Q2,t2,m2))) = ( DataPart t5) by A16, A25, A29, A30, A23, A21, SCMPDS_7: 18;

            

            then

             A39: ( DataPart t5) = ( DataPart ( Result (Q2,t2))) by A24, EXTPRO_1: 23

            .= ( DataPart ( Result (Q2,t2)))

            .= ( DataPart ( IExec (I(),Q,( Initialize t)))) by SCMPDS_4:def 5;

            ( InsCode i3) = 14 by SCMPDS_2: 12;

            then ( InsCode i3) in { 0 , 4, 5, 6, 14} by ENUMSET1:def 3;

            

            then

             A40: ( Initialize t7) = ( Initialize t6) by A35, SCMPDS_8: 3

            .= ( Initialize ( IExec (I(),Q,( Initialize t)))) by A39, A33, MEMSTR_0: 80;

             A41:

            now

              F(Initialize) < F(Initialize) by A3, A9, A10, A11, A7;

              then

               A42: F(Initialize) < (k + 1) by A8, A40, XXREAL_0: 2;

              assume F(Initialize) > k;

              hence contradiction by A42, INT_1: 7;

            end;

            

             A43: (t5 . a()) = (( Comput (Q2,t2,m2)) . a()) by A38, SCMPDS_4: 8

            .= (( Result (Q2,t2)) . a()) by A24, EXTPRO_1: 23

            .= (s() . a()) by A10, A12, A26, A7;

            

             A44: (t7 . a()) = (t6 . a()) by A35, SCMPDS_2: 54

            .= (s() . a()) by A43, EXTPRO_1: 4;

            

             A45: (( Initialize t7) . a()) = (t7 . a()) by SCMPDS_5: 15;

            P[( Initialize ( Initialize t7))] by A27, A40;

            then

             A46: WHL is_closed_on (( Initialize t7),Q7) & WHL is_halting_on (( Initialize t7),Q7) by A6, A41, A44, A45;

            

             A47: WHL is_closed_on (t7,Q7)

            proof

              for k be Nat holds ( IC ( Comput ((Q7 +* ( stop WHL)),( Initialize ( Initialize t7)),k))) in ( dom ( stop WHL)) by A46, SCMPDS_6:def 2;

              hence thesis by SCMPDS_6:def 2;

            end;

            now

              let k be Nat;

              per cases ;

                suppose k < (m3 + 1);

                then

                 A48: k <= m3 by INT_1: 7;

                hereby

                  per cases by A48, NAT_1: 8;

                    suppose

                     A49: k <= m2;

                    hereby

                      per cases ;

                        suppose k = 0 ;

                        hence ( IC ( Comput (Q3,t3,k))) in ( dom pWH) by A13, A17;

                      end;

                        suppose k <> 0 ;

                        then

                        consider kn be Nat such that

                         A50: k = (kn + 1) by NAT_1: 6;

                        reconsider kn as Element of NAT by ORDINAL1:def 12;

                        reconsider lm = ( IC ( Comput (Q2,t2,kn))) as Element of NAT ;

                        kn < k by A50, XREAL_1: 29;

                        then kn < m2 by A49, XXREAL_0: 2;

                        then (( IC ( Comput (Q2,t2,kn))) + 2) = ( IC ( Comput (Q4,t4,kn))) by A16, A25, A29, A30, A23, A21, SCMPDS_7: 16;

                        then

                         A51: ( IC ( Comput (Q3,t3,k))) = (lm + 2) by A50, EXTPRO_1: 4;

                        ( IC ( Comput (Q2,t2,kn))) in ( dom pI) by A28, SCMPDS_6:def 2;

                        then lm < ( card pI) by AFINSQ_1: 66;

                        then lm < (( card I()) + 1) by COMPOS_1: 55;

                        then

                         A52: (lm + 2) < ((( card I()) + 1) + 2) by XREAL_1: 6;

                        (( card I()) + 3) < (( card I()) + 4) by XREAL_1: 6;

                        then (lm + 2) < (( card I()) + 4) by A52, XXREAL_0: 2;

                        then (lm + 2) < ( card pWH) by Lm7;

                        hence ( IC ( Comput (Q3,t3,k))) in ( dom pWH) by A51, AFINSQ_1: 66;

                      end;

                    end;

                  end;

                    suppose

                     A53: k = m3;

                    l2 in ( dom pWH) by A18, COMPOS_1: 62;

                    hence ( IC ( Comput (Q3,t3,k))) in ( dom pWH) by A16, A25, A29, A30, A23, A21, A33, A53, SCMPDS_7: 18;

                  end;

                end;

              end;

                suppose k >= (m3 + 1);

                then

                consider nn be Nat such that

                 A54: k = ((m3 + 1) + nn) by NAT_1: 10;

                reconsider nn as Element of NAT by ORDINAL1:def 12;

                ( Comput (Q3,t3,k)) = ( Comput ((Q7 +* pWH),( Initialize t7),nn)) by A54, A36, EXTPRO_1: 4;

                hence ( IC ( Comput (Q3,t3,k))) in ( dom pWH) by A47, SCMPDS_6:def 2;

              end;

            end;

            hence WHL is_closed_on (t,Q) by SCMPDS_6:def 2;

            WHL is_halting_on (t7,Q7)

            proof

              (Q7 +* ( stop WHL)) halts_on ( Initialize ( Initialize t7)) by A46, SCMPDS_6:def 3;

              hence thesis by SCMPDS_6:def 3;

            end;

            then Q7 halts_on t7 by A37, A36, SCMPDS_6:def 3;

            then Q3 halts_on t7;

            then Q3 halts_on t3 by EXTPRO_1: 22;

            hence WHL is_halting_on (t,Q) by SCMPDS_6:def 3;

          end;

        end;

        hence thesis;

      end;

      set n = F(s);

      

       A55: Q[ 0 ]

      proof

        let t be 0 -started State of SCMPDS , Q;

        assume that

         A56: F(Initialize) <= 0 & P[( Initialize t)] and

         A57: (t . a()) = (s() . a());

        (( Initialize t) . b) = (t . b) by SCMPDS_5: 15;

        then (t . b) = 0 by A1, A56, XXREAL_0: 1;

        hence thesis by A57, Th12;

      end;

      for k be Nat holds Q[k] from NAT_1:sch 2( A55, A5);

      then Q[n];

      hence thesis by A2, A4;

    end;

    scheme :: SCPINVAR:sch4

    WhileNExec { F( State of SCMPDS ) -> Element of NAT , s() -> 0 -started State of SCMPDS , P() -> Instruction-Sequence of SCMPDS , I() -> halt-free shiftable Program of SCMPDS , a() -> Int_position , i() -> Integer , P[ set] } :

( IExec (( while<>0 (a(),i(),I())),P(),s())) = ( IExec (( while<>0 (a(),i(),I())),P(),( Initialize ( IExec (I(),P(),s())))))

      provided

       A1: (s() . ( DataLoc ((s() . a()),i()))) <> 0

       and

       A2: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ( DataLoc ((s() . a()),i()))) = 0

       and

       A3: P[s()]

       and

       A4: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (s() . a()) & (t . ( DataLoc ((s() . a()),i()))) <> 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))];

      

       A5: ( Initialize s()) = s() by MEMSTR_0: 44;

      set WHL = ( while<>0 (a(),i(),I())), s1 = s(), P1 = (P() +* ( stop WHL));

      set sI = s(), PI = (P() +* ( stop I())), m1 = (( LifeSpan (PI,sI)) + 2), s2 = ( Initialize ( IExec (I(),P(),s()))), m2 = ( LifeSpan (P1,s2));

      

       A6: ( stop I()) c= PI by FUNCT_4: 25;

      I() is_closed_on (s(),P()) by A1, A3, A4;

      then

       A7: I() is_closed_on (sI,PI) by A5, SCMPDS_6: 24;

      I() is_halting_on (s(),P()) by A1, A3, A4;

      then

       A8: PI halts_on sI by A5, SCMPDS_6:def 3;

      (PI +* ( stop I())) halts_on ( Initialize sI) by A8, A5;

      then

       A9: I() is_halting_on (sI,PI) by SCMPDS_6:def 3;

      set s4 = ( Comput (P1,s1,1)), P4 = P1;

      set i1 = ((a(),i()) <>0_goto 2), i2 = ( goto (( card I()) + 2)), i3 = ( goto ( - (( card I()) + 2)));

      set b = ( DataLoc ((s() . a()),i()));

      

       A10: ( IC s1) = 0 by A5, MEMSTR_0: 47;

      set mI = ( LifeSpan (PI,sI)), s5 = ( Comput (P4,s4,mI)), P5 = P4, l2 = (( card I()) + 2);

      

       A11: WHL = (i1 ';' ((i2 ';' I()) ';' i3)) by Lm8;

      set m3 = (mI + 1);

      set s6 = ( Comput (P1,s1,m3)), P6 = P1;

      (( card I()) + 2) < (( card I()) + 3) by XREAL_1: 6;

      then

       A12: l2 in ( dom WHL) by Th9;

      set s7 = ( Comput (P1,s1,(m3 + 1))), P7 = P1;

      

       A13: ( IExec (I(),P(),s())) = ( Result (PI,sI)) by SCMPDS_4:def 5;

      

       A14: ( stop WHL) c= P1 by FUNCT_4: 25;

      WHL c= ( stop WHL) by AFINSQ_1: 74;

      then

       A15: WHL c= P1 by A14, XBOOLE_1: 1;

      deffunc F( State of SCMPDS ) = F($1);

      

       A16: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ( DataLoc ((s() . a()),i()))) = 0 by A2;

      

       A17: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (s() . a()) & (t . ( DataLoc ((s() . a()),i()))) <> 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))] by A4;

      

       A18: ( Comput (P1,s1,( 0 + 1))) = ( Following (P1,( Comput (P1,s1, 0 )))) by EXTPRO_1: 3

      .= ( Following (P1,s1))

      .= ( Exec (i1,s1)) by A11, A5, SCMPDS_6: 11;

      ( Shift (I(),2)) c= WHL by Lm9;

      then ( Shift (I(),2)) c= P1 by A15, XBOOLE_1: 1;

      then

       A19: ( Shift (I(),2)) c= P4;

      for a holds (sI . a) = (s4 . a) by A18, SCMPDS_2: 55;

      then

       A20: ( DataPart sI) = ( DataPart s4) by SCMPDS_4: 8;

      

       A21: ( IC s4) = ( ICplusConst (s1,2)) by A1, A18, SCMPDS_2: 55

      .= ( 0 + 2) by A10, SCMPDS_6: 12;

      then

       A22: ( IC s5) = l2 by A6, A9, A7, A20, A19, SCMPDS_7: 18;

      

       A23: (P6 /. ( IC s6)) = (P6 . ( IC s6)) by PBOOLE: 143;

      

       A24: s6 = s5 by EXTPRO_1: 4;

      

      then

       A25: ( CurInstr (P6,s6)) = (P5 . l2) by A6, A9, A7, A21, A20, A19, A23, SCMPDS_7: 18

      .= (P4 . l2)

      .= (P1 . l2)

      .= (WHL . l2) by A12, A15, GRFUNC_1: 2

      .= i3 by Th11;

      

       A26: s7 = ( Following (P1,s6)) by EXTPRO_1: 3

      .= ( Exec (i3,s6)) by A25;

      

      then ( IC s7) = ( ICplusConst (s6,( 0 - (( card I()) + 2)))) by SCMPDS_2: 54

      .= 0 by A22, A24, SCMPDS_7: 1;

      then

       A27: ( IC s2) = ( IC ( Comput (P1,s1,m1))) by MEMSTR_0: 47;

      

       A28: ( DataPart ( Comput (PI,sI,mI))) = ( DataPart s5) by A6, A9, A7, A21, A20, A19, SCMPDS_7: 18;

      now

        let x be Int_position;

        

         A29: not x in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

        (s5 . x) = (( Comput (PI,sI,mI)) . x) by A28, SCMPDS_4: 8

        .= (( Result (PI,sI)) . x) by A8, EXTPRO_1: 23

        .= (( IExec (I(),P(),s())) . x) by A13;

        

        hence (s7 . x) = (( IExec (I(),P(),s())) . x) by A24, A26, SCMPDS_2: 54

        .= (s2 . x) by A29, FUNCT_4: 11;

      end;

      then

       A30: ( DataPart s7) = ( DataPart s2) by SCMPDS_4: 8;

      set m0 = ( LifeSpan (P1,s1));

      

       A31: P[s()] by A3;

      WHL is_closed_on (s(),P()) & WHL is_halting_on (s(),P()) from WhileNHalt( A16, A31, A17);

      then

       A32: P1 halts_on s1 by A5, SCMPDS_6:def 3;

      deffunc F( State of SCMPDS ) = F($1);

      set Es = ( IExec (I(),P(),s())), bj = ( DataLoc ((Es . a()),i())), EP = P();

      

       A33: (( IExec (I(),P(),s())) . a()) = (s() . a()) by A1, A3, A4;

      

       A34: (( Initialize Es) . a()) = (Es . a()) by SCMPDS_5: 15;

      

       A35: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ( DataLoc ((( Initialize Es) . a()),i()))) = 0 by A2, A33, A34;

      

       A36: P[( Initialize Es)] by A1, A3, A4;

      

       A37: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (( Initialize Es) . a()) & (t . ( DataLoc ((( Initialize Es) . a()),i()))) <> 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))] by A4, A33, A34;

      

       A38: WHL is_closed_on (( Initialize Es),P()) & WHL is_halting_on (( Initialize Es),P()) from WhileNHalt( A35, A36, A37);

      WHL is_halting_on (Es,P())

      proof

        (P() +* ( stop WHL)) halts_on ( Initialize ( Initialize Es)) by A38, SCMPDS_6:def 3;

        hence thesis by SCMPDS_6:def 3;

      end;

      then

       A39: P1 halts_on s2 by SCMPDS_6:def 3;

      

       A40: ( Comput (P1,s1,m1)) = s2 by A30, A27, MEMSTR_0: 78;

      then ( CurInstr (P1,( Comput (P1,s1,m1)))) = i1 by A11, SCMPDS_6: 11;

      then m0 > m1 by A32, EXTPRO_1: 36, SCMPDS_6: 16;

      then

      consider nn be Nat such that

       A41: m0 = (m1 + nn) by NAT_1: 10;

      reconsider nn as Element of NAT by ORDINAL1:def 12;

      ( IC ( Comput (P1,s1,(m1 + m2)))) = ( IC ( Comput (P1,s2,m2))) by A40, EXTPRO_1: 4;

      

      then ( CurInstr (P1,( Comput (P1,s1,(m1 + m2))))) = ( CurInstr (P1,( Comput (P1,s2,m2))))

      .= ( halt SCMPDS ) by A39, EXTPRO_1:def 15;

      then (m1 + m2) >= m0 by A32, EXTPRO_1:def 15;

      then

       A42: m2 >= nn by A41, XREAL_1: 6;

      

       A43: ( Comput (P1,s1,m0)) = ( Comput (P1,s2,nn)) by A40, A41, EXTPRO_1: 4;

      then ( CurInstr (P1,( Comput (P1,s2,nn)))) = ( halt SCMPDS ) by A32, EXTPRO_1:def 15;

      then nn >= m2 by A39, EXTPRO_1:def 15;

      then nn = m2 by A42, XXREAL_0: 1;

      then ( Result (P1,s1)) = ( Comput (P1,s2,m2)) by A32, A43, EXTPRO_1: 23;

      

      hence ( IExec (WHL,P(),s())) = ( Comput (P1,s2,m2)) by SCMPDS_4:def 5

      .= ( Result (P1,s2)) by A39, EXTPRO_1: 23

      .= ( IExec (WHL,P(),( Initialize ( IExec (I(),P(),s()))))) by SCMPDS_4:def 5;

    end;

    scheme :: SCPINVAR:sch5

    WhileNEnd { F( State of SCMPDS ) -> Element of NAT , s() -> 0 -started State of SCMPDS , P() -> Instruction-Sequence of SCMPDS , I() -> halt-free shiftable Program of SCMPDS , a() -> Int_position , i() -> Integer , P[ set] } :

F(Initialize) = 0 & P[( Initialize ( IExec (( while<>0 (a(),i(),I())),P(),s())))]

      provided

       A1: for t be 0 -started State of SCMPDS st P[t] holds F(t) = 0 iff (t . ( DataLoc ((s() . a()),i()))) = 0

       and

       A2: P[s()]

       and

       A3: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (s() . a()) & (t . ( DataLoc ((s() . a()),i()))) <> 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))];

      set b = ( DataLoc ((s() . a()),i())), WHL = ( while<>0 (a(),i(),I()));

      defpred Q[ Nat] means for t be 0 -started State of SCMPDS , Q st F(t) <= $1 & (t . a()) = (s() . a()) & P[t] holds F(Initialize) = 0 & P[( Initialize ( IExec (WHL,Q,t)))];

      

       A4: Q[ 0 ]

      proof

        let t be 0 -started State of SCMPDS , Q;

        

         A5: ( Initialize t) = t by MEMSTR_0: 44;

        assume that

         A6: F(t) <= 0 and

         A7: (t . a()) = (s() . a()) and

         A8: P[t];

        

         A9: F(t) = 0 by A6;

        then (t . ( DataLoc ((t . a()),i()))) = 0 by A1, A7, A8;

        then for b be Int_position holds (( IExec (WHL,Q,t)) . b) = (t . b) by Th15, A5;

        hence thesis by A8, A9, A5, SCPISORT: 4;

      end;

       A10:

      now

        let k be Nat;

        assume

         A11: Q[k];

        now

          let u be 0 -started State of SCMPDS ;

          let U;

          assume that

           A12: F(u) <= (k + 1) and

           A13: (u . a()) = (s() . a()) and

           A14: P[u];

          per cases ;

            suppose F(u) = 0 ;

            hence F(Initialize) = 0 & P[( Initialize ( IExec (WHL,U,u)))] by A4, A13, A14;

          end;

            suppose

             A15: F(u) <> 0 ;

            set Iu = ( IExec (I(),U,u));

            

             A16: (u . b) <> 0 by A1, A14, A15;

            then

             A17: (Iu . a()) = (s() . a()) & P[( Initialize Iu)] by A3, A13, A14;

            deffunc F( State of SCMPDS ) = F($1);

            

             A18: P[u] by A14;

            

             A19: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ( DataLoc ((u . a()),i()))) = 0 by A1, A13;

             F(Initialize) < F(u) by A3, A13, A14, A16;

            then ( F(Initialize) + 1) <= F(u) by INT_1: 7;

            then ( F(Initialize) + 1) <= (k + 1) by A12, XXREAL_0: 2;

            then

             A20: F(Initialize) <= k by XREAL_1: 6;

            

             A21: for t be 0 -started State of SCMPDS , Q st P[t] & (t . a()) = (u . a()) & (t . ( DataLoc ((u . a()),i()))) <> 0 holds (( IExec (I(),Q,t)) . a()) = (t . a()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & F(Initialize) < F(t) & P[( Initialize ( IExec (I(),Q,t)))] by A3, A13;

            

             A22: (u . ( DataLoc ((u . a()),i()))) <> 0 by A1, A13, A14, A15;

            

             A23: ( IExec (WHL,U,u)) = ( IExec (WHL,U,( Initialize Iu))) from WhileNExec( A22, A19, A18, A21);

            (( Initialize Iu) . a()) = (Iu . a()) by SCMPDS_5: 15;

            hence F(Initialize) = 0 & P[( Initialize ( IExec (WHL,U,u)))] by A11, A20, A17, A23;

          end;

        end;

        hence Q[(k + 1)];

      end;

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

      then Q[F(s)];

      hence thesis by A2;

    end;

    theorem :: SCPINVAR:16

    

     Th16: for s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,b,c be Int_position, i,d be Integer st ( card I) > 0 & (s . a) = d & (s . b) > 0 & (s . c) > 0 & (s . ( DataLoc (d,i))) = ((s . b) - (s . c)) & (for t be 0 -started State of SCMPDS , Q st (t . b) > 0 & (t . c) > 0 & (t . a) = d & (t . ( DataLoc (d,i))) = ((t . b) - (t . c)) & (t . b) <> (t . c) holds (( IExec (I,Q,t)) . a) = d & I is_closed_on (t,Q) & I is_halting_on (t,Q) & ((t . b) > (t . c) implies (( IExec (I,Q,t)) . b) = ((t . b) - (t . c)) & (( IExec (I,Q,t)) . c) = (t . c)) & ((t . b) <= (t . c) implies (( IExec (I,Q,t)) . c) = ((t . c) - (t . b)) & (( IExec (I,Q,t)) . b) = (t . b)) & (( IExec (I,Q,t)) . ( DataLoc (d,i))) = ((( IExec (I,Q,t)) . b) - (( IExec (I,Q,t)) . c))) holds ( while<>0 (a,i,I)) is_closed_on (s,P) & ( while<>0 (a,i,I)) is_halting_on (s,P) & ((s . ( DataLoc ((s . a),i))) <> 0 implies ( IExec (( while<>0 (a,i,I)),P,s)) = ( IExec (( while<>0 (a,i,I)),P,( Initialize ( IExec (I,P,s))))))

    proof

      let s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,b,c be Int_position, i,d be Integer;

      set ci = ( DataLoc ((s . a),i));

      assume ( card I) > 0 ;

      consider f be Function of ( product ( the_Values_of SCMPDS )), NAT such that

       A1: for s be State of SCMPDS holds ((s . b) = (s . c) implies (f . s) = 0 ) & ((s . b) <> (s . c) implies (f . s) = ( max ( |.(s . b).|, |.(s . c).|))) by Th2;

      deffunc F( State of SCMPDS ) = (f . $1);

      defpred P[ set] means ex t be State of SCMPDS st t = $1 & (t . b) > 0 & (t . c) > 0 & (t . ( DataLoc (d,i))) = ((t . b) - (t . c));

      assume that

       A2: (s . a) = d and

       A3: (s . b) > 0 and

       A4: (s . c) > 0 and

       A5: (s . ( DataLoc (d,i))) = ((s . b) - (s . c));

      assume

       A6: for t be 0 -started State of SCMPDS , Q st (t . b) > 0 & (t . c) > 0 & (t . a) = d & (t . ( DataLoc (d,i))) = ((t . b) - (t . c)) & (t . b) <> (t . c) holds (( IExec (I,Q,t)) . a) = d & I is_closed_on (t,Q) & I is_halting_on (t,Q) & ((t . b) > (t . c) implies (( IExec (I,Q,t)) . b) = ((t . b) - (t . c)) & (( IExec (I,Q,t)) . c) = (t . c)) & ((t . b) <= (t . c) implies (( IExec (I,Q,t)) . c) = ((t . c) - (t . b)) & (( IExec (I,Q,t)) . b) = (t . b)) & (( IExec (I,Q,t)) . ( DataLoc (d,i))) = ((( IExec (I,Q,t)) . b) - (( IExec (I,Q,t)) . c));

       A7:

      now

        let t be 0 -started State of SCMPDS , Q;

        assume that

         A8: P[t] and

         A9: (t . a) = (s . a) and

         A10: (t . ci) <> 0 ;

        set It = ( IExec (I,Q,t)), t2 = ( Initialize It), t1 = t;

        set x = (( IExec (I,Q,t)) . b), y = (( IExec (I,Q,t)) . c);

        consider v be State of SCMPDS such that

         A11: v = t and

         A12: (v . b) > 0 and

         A13: (v . c) > 0 and

         A14: (v . ( DataLoc (d,i))) = ((v . b) - (v . c)) by A8;

        

         A15: (t . b) > 0 by A11, A12;

        

         A16: (t . c) > 0 by A11, A13;

        

         A17: (t . ( DataLoc (d,i))) = ((v . b) - (v . c)) by A11, A14

        .= ((t . b) - (v . c)) by A11

        .= ((t . b) - (t . c)) by A11;

        then

         A18: (t . b) <> (t . c) by A2, A10;

        hence (( IExec (I,Q,t)) . a) = (t . a) by A2, A6, A9, A15, A16, A17;

        thus I is_closed_on (t,Q) & I is_halting_on (t,Q) by A2, A6, A9, A15, A16, A17, A18;

         A19:

        now

          per cases ;

            suppose

             A20: (t . b) > (t . c);

            then ((t . b) - (t . c)) > 0 by XREAL_1: 50;

            hence x > 0 by A2, A6, A9, A16, A17, A20;

            thus y > 0 by A2, A6, A9, A16, A17, A20;

            

             A21: x = ((t . b) - (t . c)) by A2, A6, A9, A16, A17, A20;

            hereby

              

               A22: ( max ((t . b),(t . c))) = (t . b) by A20, XXREAL_0:def 10;

              per cases by XXREAL_0: 16;

                suppose ( max (x,y)) = x;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A16, A21, A22, XREAL_1: 44;

              end;

                suppose ( max (x,y)) = y;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A2, A6, A9, A16, A17, A20, A22;

              end;

            end;

          end;

            suppose

             A23: (t . b) <= (t . c);

            hence x > 0 by A2, A6, A9, A15, A17, A18;

            (t . b) < (t . c) by A18, A23, XXREAL_0: 1;

            then ((t . c) - (t . b)) > 0 by XREAL_1: 50;

            hence y > 0 by A2, A6, A9, A15, A17, A18, A23;

            

             A24: y = ((t . c) - (t . b)) by A2, A6, A9, A15, A17, A18, A23;

            

             A25: x = (t . b) by A2, A6, A9, A15, A17, A18, A23;

            hereby

              

               A26: ( max ((t . b),(t . c))) = (t . c) by A23, XXREAL_0:def 10;

              per cases by XXREAL_0: 16;

                suppose ( max (x,y)) = y;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A15, A24, A26, XREAL_1: 44;

              end;

                suppose ( max (x,y)) = x;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A18, A23, A25, A26, XXREAL_0: 1;

              end;

            end;

          end;

        end;

        thus F(t2) < F(t1)

        proof

          (t1 . b) <> (t . c) by A18;

          then (t1 . b) <> (t1 . c);

          

          then

           A27: F(t1) = ( max ( |.(t1 . b).|, |.(t1 . c).|)) by A1

          .= ( max ( |.(t . b).|, |.(t1 . c).|))

          .= ( max ( |.(t . b).|, |.(t . c).|))

          .= ( max ((t . b), |.(t . c).|)) by A15, ABSVALUE:def 1

          .= ( max ((t . b),(t . c))) by A16, ABSVALUE:def 1;

          then F(t1) >= (t . b) by XXREAL_0: 25;

          then

           A28: F(t1) > 0 by A15;

          per cases ;

            suppose (t2 . b) = (t2 . c);

            hence thesis by A1, A28;

          end;

            suppose (t2 . b) <> (t2 . c);

            

            then F(t2) = ( max ( |.(t2 . b).|, |.(t2 . c).|)) by A1

            .= ( max ( |.x.|, |.(t2 . c).|)) by SCMPDS_5: 15

            .= ( max ( |.x.|, |.y.|)) by SCMPDS_5: 15

            .= ( max (x, |.y.|)) by A19, ABSVALUE:def 1

            .= ( max (x,y)) by A19, ABSVALUE:def 1;

            hence thesis by A19, A27;

          end;

        end;

        

         A29: (( IExec (I,Q,t)) . ( DataLoc (d,i))) = ((( IExec (I,Q,t)) . b) - (( IExec (I,Q,t)) . c)) by A2, A6, A9, A15, A16, A17, A18;

        thus P[( Initialize It)]

        proof

          take v = ( Initialize It);

          thus v = ( Initialize It);

          thus (v . b) > 0 & (v . c) > 0 by A19, SCMPDS_5: 15;

          

          thus (v . ( DataLoc (d,i))) = (x - y) by A29, SCMPDS_5: 15

          .= ((v . b) - y) by SCMPDS_5: 15

          .= ((v . b) - (v . c)) by SCMPDS_5: 15;

        end;

      end;

      

       A30: for t be 0 -started State of SCMPDS st P[t] & F(t) = 0 holds (t . ci) = 0

      proof

        let t be 0 -started State of SCMPDS ;

        assume that

         A31: P[t] and

         A32: F(t) = 0 ;

        consider v be State of SCMPDS such that

         A33: v = t and

         A34: (v . b) > 0 and (v . c) > 0 and

         A35: (v . ( DataLoc (d,i))) = ((v . b) - (v . c)) by A31;

         A36:

        now

          assume (t . b) <> (t . c);

          then (t . b) <> (t . c);

          then (t . b) <> (t . c);

          

          then

           A37: F(t) = ( max ( |.(t . b).|, |.(t . c).|)) by A1

          .= ( max ( |.(t . b).|, |.(t . c).|))

          .= ( max ( |.(t . b).|, |.(t . c).|));

          (t . b) > 0 by A33, A34;

          then |.(t . b).| > 0 by COMPLEX1: 47;

          hence contradiction by A32, A37, XXREAL_0: 25;

        end;

        

        thus (t . ci) = ((v . b) - (v . c)) by A2, A33, A35

        .= ((t . b) - (v . c)) by A33

        .= ((t . b) - (t . c)) by A33

        .= 0 by A36;

      end;

      

       A38: P[s] by A3, A4, A5;

      ( while<>0 (a,i,I)) is_closed_on (s,P) & ( while<>0 (a,i,I)) is_halting_on (s,P) from WhileNHalt( A30, A38, A7);

      hence ( while<>0 (a,i,I)) is_closed_on (s,P) & ( while<>0 (a,i,I)) is_halting_on (s,P);

      assume

       A39: (s . ( DataLoc ((s . a),i))) <> 0 ;

      ( IExec (( while<>0 (a,i,I)),P,s)) = ( IExec (( while<>0 (a,i,I)),P,( Initialize ( IExec (I,P,s))))) from WhileNExec( A39, A30, A38, A7);

      hence thesis;

    end;

    begin

    definition

      :: SCPINVAR:def4

      func GCD-Algorithm -> Program of SCMPDS equals (((( GBP := 0 ) ';' (( GBP ,3) := ( GBP ,1))) ';' ( SubFrom ( GBP ,3, GBP ,2))) ';' ( while<>0 ( GBP ,3,((( if>0 ( GBP ,3,( Load ( SubFrom ( GBP ,1, GBP ,2))),( Load ( SubFrom ( GBP ,2, GBP ,1))))) ';' (( GBP ,3) := ( GBP ,1))) ';' ( SubFrom ( GBP ,3, GBP ,2))))));

      coherence ;

    end

    theorem :: SCPINVAR:17

    

     Th17: for s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,b,c be Int_position, i,d be Integer st (s . a) = d & (s . b) > 0 & (s . c) > 0 & (s . ( DataLoc (d,i))) = ((s . b) - (s . c)) & (for t be 0 -started State of SCMPDS , Q st (t . b) > 0 & (t . c) > 0 & (t . a) = d & (t . ( DataLoc (d,i))) = ((t . b) - (t . c)) & (t . b) <> (t . c) holds (( IExec (I,Q,t)) . a) = d & I is_closed_on (t,Q) & I is_halting_on (t,Q) & ((t . b) > (t . c) implies (( IExec (I,Q,t)) . b) = ((t . b) - (t . c)) & (( IExec (I,Q,t)) . c) = (t . c)) & ((t . b) <= (t . c) implies (( IExec (I,Q,t)) . c) = ((t . c) - (t . b)) & (( IExec (I,Q,t)) . b) = (t . b)) & (( IExec (I,Q,t)) . ( DataLoc (d,i))) = ((( IExec (I,Q,t)) . b) - (( IExec (I,Q,t)) . c))) holds (( IExec (( while<>0 (a,i,I)),P,s)) . b) = ((s . b) gcd (s . c)) & (( IExec (( while<>0 (a,i,I)),P,s)) . c) = ((s . b) gcd (s . c))

    proof

      let s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,b,c be Int_position, i,d be Integer;

      set ci = ( DataLoc ((s . a),i));

      consider f be Function of ( product ( the_Values_of SCMPDS )), NAT such that

       A1: for s be State of SCMPDS holds ((s . b) = (s . c) implies (f . s) = 0 ) & ((s . b) <> (s . c) implies (f . s) = ( max ( |.(s . b).|, |.(s . c).|))) by Th2;

      deffunc F( State of SCMPDS ) = (f . $1);

      set s1 = ( IExec (( while<>0 (a,i,I)),P,s)), ss = s1;

      defpred P[ set] means ex t be 0 -started State of SCMPDS st t = $1 & (t . b) > 0 & (t . c) > 0 & ((t . b) gcd (t . c)) = ((s . b) gcd (s . c)) & (t . ( DataLoc (d,i))) = ((t . b) - (t . c));

      assume that

       A2: (s . a) = d and

       A3: (s . b) > 0 and

       A4: (s . c) > 0 and

       A5: (s . ( DataLoc (d,i))) = ((s . b) - (s . c));

      assume

       A6: for t be 0 -started State of SCMPDS , Q st (t . b) > 0 & (t . c) > 0 & (t . a) = d & (t . ( DataLoc (d,i))) = ((t . b) - (t . c)) & (t . b) <> (t . c) holds (( IExec (I,Q,t)) . a) = d & I is_closed_on (t,Q) & I is_halting_on (t,Q) & ((t . b) > (t . c) implies (( IExec (I,Q,t)) . b) = ((t . b) - (t . c)) & (( IExec (I,Q,t)) . c) = (t . c)) & ((t . b) <= (t . c) implies (( IExec (I,Q,t)) . c) = ((t . c) - (t . b)) & (( IExec (I,Q,t)) . b) = (t . b)) & (( IExec (I,Q,t)) . ( DataLoc (d,i))) = ((( IExec (I,Q,t)) . b) - (( IExec (I,Q,t)) . c));

       A7:

      now

        let t be 0 -started State of SCMPDS , Q;

        assume that

         A8: P[t] and

         A9: (t . a) = (s . a) and

         A10: (t . ci) <> 0 ;

        set It = ( IExec (I,Q,t)), t2 = ( Initialize It), t1 = t;

        set x = (( IExec (I,Q,t)) . b), y = (( IExec (I,Q,t)) . c);

        consider v be State of SCMPDS such that

         A11: v = t and

         A12: (v . b) > 0 and

         A13: (v . c) > 0 and

         A14: ((v . b) gcd (v . c)) = ((s . b) gcd (s . c)) and

         A15: (v . ( DataLoc (d,i))) = ((v . b) - (v . c)) by A8;

        

         A16: (t . b) > 0 by A11, A12;

        

         A17: (t . c) > 0 by A11, A13;

        

         A18: (t . ( DataLoc (d,i))) = ((v . b) - (v . c)) by A11, A15

        .= ((t . b) - (v . c)) by A11

        .= ((t . b) - (t . c)) by A11;

        then

         A19: (t . b) > (t . c) implies (( IExec (I,Q,t)) . b) = ((t . b) - (t . c)) & (( IExec (I,Q,t)) . c) = (t . c) by A2, A6, A9, A17;

        

         A20: (t . b) <> (t . c) by A2, A10, A18;

        hence (( IExec (I,Q,t)) . a) = (t . a) by A2, A6, A9, A16, A17, A18;

        thus I is_closed_on (t,Q) & I is_halting_on (t,Q) by A2, A6, A9, A16, A17, A18, A20;

        

         A21: (t . b) <= (t . c) implies (( IExec (I,Q,t)) . c) = ((t . c) - (t . b)) & (( IExec (I,Q,t)) . b) = (t . b) by A2, A6, A9, A16, A18, A20;

         A22:

        now

          per cases ;

            suppose

             A23: (t . b) > (t . c);

            then ((t . b) - (t . c)) > 0 by XREAL_1: 50;

            hence x > 0 by A2, A6, A9, A17, A18, A23;

            thus y > 0 by A2, A6, A9, A17, A18, A23;

            thus (x gcd y) = ((t . b) gcd (t . c)) by A16, A17, A19, A21, PREPOWER: 97;

            

             A24: x = ((t . b) - (t . c)) by A2, A6, A9, A17, A18, A23;

            hereby

              

               A25: ( max ((t . b),(t . c))) = (t . b) by A23, XXREAL_0:def 10;

              per cases by XXREAL_0: 16;

                suppose ( max (x,y)) = x;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A17, A24, A25, XREAL_1: 44;

              end;

                suppose ( max (x,y)) = y;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A2, A6, A9, A17, A18, A23, A25;

              end;

            end;

          end;

            suppose

             A26: (t . b) <= (t . c);

            hence x > 0 by A2, A6, A9, A16, A18, A20;

            (t . b) < (t . c) by A20, A26, XXREAL_0: 1;

            then ((t . c) - (t . b)) > 0 by XREAL_1: 50;

            hence y > 0 by A2, A6, A9, A16, A18, A20, A26;

            thus (x gcd y) = ((t . b) gcd (t . c)) by A16, A17, A19, A21, PREPOWER: 97;

            

             A27: y = ((t . c) - (t . b)) by A2, A6, A9, A16, A18, A20, A26;

            

             A28: x = (t . b) by A2, A6, A9, A16, A18, A20, A26;

            hereby

              

               A29: ( max ((t . b),(t . c))) = (t . c) by A26, XXREAL_0:def 10;

              per cases by XXREAL_0: 16;

                suppose ( max (x,y)) = y;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A16, A27, A29, XREAL_1: 44;

              end;

                suppose ( max (x,y)) = x;

                hence ( max (x,y)) < ( max ((t . b),(t . c))) by A20, A26, A28, A29, XXREAL_0: 1;

              end;

            end;

          end;

        end;

        thus F(t2) < F(t1)

        proof

          (t1 . b) <> (t . c) by A20;

          then (t1 . b) <> (t1 . c);

          

          then

           A30: F(t1) = ( max ( |.(t1 . b).|, |.(t1 . c).|)) by A1

          .= ( max ( |.(t . b).|, |.(t1 . c).|))

          .= ( max ( |.(t . b).|, |.(t . c).|))

          .= ( max ((t . b), |.(t . c).|)) by A16, ABSVALUE:def 1

          .= ( max ((t . b),(t . c))) by A17, ABSVALUE:def 1;

          then F(t1) >= (t . b) by XXREAL_0: 25;

          then

           A31: F(t1) > 0 by A16;

          per cases ;

            suppose (t2 . b) = (t2 . c);

            hence thesis by A1, A31;

          end;

            suppose (t2 . b) <> (t2 . c);

            

            then F(t2) = ( max ( |.(t2 . b).|, |.(t2 . c).|)) by A1

            .= ( max ( |.x.|, |.(t2 . c).|)) by SCMPDS_5: 15

            .= ( max ( |.x.|, |.y.|)) by SCMPDS_5: 15

            .= ( max (x, |.y.|)) by A22, ABSVALUE:def 1

            .= ( max (x,y)) by A22, ABSVALUE:def 1;

            hence thesis by A22, A30;

          end;

        end;

        

         A32: (( IExec (I,Q,t)) . ( DataLoc (d,i))) = ((( IExec (I,Q,t)) . b) - (( IExec (I,Q,t)) . c)) by A2, A6, A9, A16, A17, A18, A20;

        thus P[( Initialize It)]

        proof

          take u = ( Initialize It);

          thus u = ( Initialize It);

          thus (u . b) > 0 & (u . c) > 0 by A22, SCMPDS_5: 15;

          

          thus ((u . b) gcd (u . c)) = ((It . b) gcd (u . c)) by SCMPDS_5: 15

          .= ((t . b) gcd (t . c)) by A22, SCMPDS_5: 15

          .= ((v . b) gcd (t . c)) by A11

          .= ((s . b) gcd (s . c)) by A11, A14;

          

          thus (u . ( DataLoc (d,i))) = (x - y) by A32, SCMPDS_5: 15

          .= ((u . b) - y) by SCMPDS_5: 15

          .= ((u . b) - (u . c)) by SCMPDS_5: 15;

        end;

      end;

      

       A33: for t be 0 -started State of SCMPDS st P[t] holds F(t) = 0 iff (t . ci) = 0

      proof

        let t be 0 -started State of SCMPDS ;

        assume P[t];

        then

        consider v be State of SCMPDS such that

         A34: v = t and

         A35: (v . b) > 0 and (v . c) > 0 and ((v . b) gcd (v . c)) = ((s . b) gcd (s . c)) and

         A36: (v . ( DataLoc (d,i))) = ((v . b) - (v . c));

        

         A37: (t . ci) = ((v . b) - (v . c)) by A2, A34, A36

        .= ((t . b) - (v . c)) by A34

        .= ((t . b) - (t . c)) by A34;

        hereby

          assume

           A38: F(t) = 0 ;

          now

            assume (t . b) <> (t . c);

            then (t . b) <> (t . c);

            then (t . b) <> (t . c);

            

            then

             A39: F(t) = ( max ( |.(t . b).|, |.(t . c).|)) by A1

            .= ( max ( |.(t . b).|, |.(t . c).|))

            .= ( max ( |.(t . b).|, |.(t . c).|));

            (t . b) > 0 by A34, A35;

            then |.(t . b).| > 0 by COMPLEX1: 47;

            hence contradiction by A38, A39, XXREAL_0: 25;

          end;

          hence (t . ci) = 0 by A37;

        end;

        thus (t . ci) = 0 implies F(t) = 0 by A1, A37;

      end;

      

       A40: P[s] by A3, A4, A5;

      

       A41: F(Initialize) = 0 & P[( Initialize ss)] from WhileNEnd( A33, A40, A7);

      then

      consider w be 0 -started State of SCMPDS such that

       A42: w = ( Initialize ss) and

       A43: (w . b) > 0 and (w . c) > 0 and

       A44: ((w . b) gcd (w . c)) = ((s . b) gcd (s . c)) and

       A45: (w . ( DataLoc (d,i))) = ((w . b) - (w . c));

      

       A46: (( Initialize ss) . ci) = (ss . ci) by SCMPDS_5: 15;

      

       A47: (( Initialize ss) . b) = (ss . b) by SCMPDS_5: 15;

      

       A48: (( Initialize ss) . c) = (ss . c) by SCMPDS_5: 15;

      

       A49: ((w . b) - (w . c)) = (s1 . ci) by A2, A42, A45, SCMPDS_5: 15

      .= 0 by A33, A41, A46;

      

      then

       A50: |.(w . b).| = ( |.(w . b).| gcd |.(w . c).|) by NAT_D: 32

      .= ((s . b) gcd (s . c)) by A44, INT_2: 34;

      

      thus (( IExec (( while<>0 (a,i,I)),P,s)) . b) = (ss . b)

      .= ((s . b) gcd (s . c)) by A42, A43, A50, A47, ABSVALUE:def 1;

      

      thus (( IExec (( while<>0 (a,i,I)),P,s)) . c) = (ss . c)

      .= ((s . b) gcd (s . c)) by A42, A43, A49, A50, A48, ABSVALUE:def 1;

    end;

    set i1 = ( GBP := 0 ), i2 = (( GBP ,3) := ( GBP ,1)), i3 = ( SubFrom ( GBP ,3, GBP ,2)), j1 = ( Load ( SubFrom ( GBP ,1, GBP ,2))), j2 = ( Load ( SubFrom ( GBP ,2, GBP ,1))), IF = ( if>0 ( GBP ,3,j1,j2)), k1 = (( GBP ,3) := ( GBP ,1)), k2 = ( SubFrom ( GBP ,3, GBP ,2)), WB = ((IF ';' k1) ';' k2), WH = ( while<>0 ( GBP ,3,WB));

    

     Lm10: ( card WB) = 6

    proof

      

      thus ( card WB) = (( card (IF ';' k1)) + 1) by SCMP_GCD: 4

      .= ((( card IF) + 1) + 1) by SCMP_GCD: 4

      .= ((((( card j1) + ( card j2)) + 2) + 1) + 1) by SCMPDS_6: 65

      .= ((((1 + ( card j2)) + 2) + 1) + 1) by COMPOS_1: 54

      .= ((((1 + 1) + 2) + 1) + 1) by COMPOS_1: 54

      .= 6;

    end;

    

     Lm11: ( card WH) = 9

    proof

      

      thus ( card WH) = (6 + 3) by Lm10, Th8

      .= 9;

    end;

    theorem :: SCPINVAR:18

    ( card GCD-Algorithm ) = 12

    proof

      

      thus ( card GCD-Algorithm ) = (( card ((i1 ';' i2) ';' i3)) + ( card WH)) by AFINSQ_1: 17

      .= ((( card (i1 ';' i2)) + 1) + ( card WH)) by SCMP_GCD: 4

      .= ((2 + 1) + 9) by Lm11, SCMP_GCD: 5

      .= 12;

    end;

    

     Lm12: for s be 0 -started State of SCMPDS st (s . GBP ) = 0 holds ((s . a3) > 0 implies (( IExec (WB,P,s)) . a1) = ((s . a1) - (s . a2)) & (( IExec (WB,P,s)) . a2) = (s . a2)) & ((s . a3) <= 0 implies (( IExec (WB,P,s)) . a2) = ((s . a2) - (s . a1)) & (( IExec (WB,P,s)) . a1) = (s . a1)) & (( IExec (WB,P,s)) . GBP ) = 0 & (( IExec (WB,P,s)) . a3) = ((( IExec (WB,P,s)) . a1) - (( IExec (WB,P,s)) . a2))

    proof

      let s be 0 -started State of SCMPDS ;

      set s1 = ( IExec (IF,P,s)), s2 = ( IExec ((IF ';' k1),P,s)), a = GBP , t0 = s, Q0 = P;

       A1:

      now

        assume

         A2: (s1 . GBP ) = 0 ;

        then

         A3: ( DataLoc ((s1 . a),3)) = ( intpos ( 0 + 3)) by SCMP_GCD: 1;

        

         A4: (s2 . a3) = (( Exec (k1,s1)) . a3) by SCMPDS_5: 41

        .= (s1 . ( DataLoc ((s1 . a),1))) by A3, SCMPDS_2: 47

        .= (s1 . ( intpos ( 0 + 1))) by A2, SCMP_GCD: 1;

        1 <> |.((s1 . GBP ) + 3).| by A2, ABSVALUE:def 1;

        then

         A5: a1 <> ( DataLoc ((s1 . GBP ),3)) by XTUPLE_0: 1;

        

         A6: (s2 . a1) = (( Exec (k1,s1)) . a1) by SCMPDS_5: 41

        .= (s1 . a1) by A5, SCMPDS_2: 47;

        2 <> |.((s1 . GBP ) + 3).| by A2, ABSVALUE:def 1;

        then

         A7: a2 <> ( DataLoc ((s1 . GBP ),3)) by XTUPLE_0: 1;

        

         A8: (s2 . a2) = (( Exec (k1,s1)) . a2) by SCMPDS_5: 41

        .= (s1 . a2) by A7, SCMPDS_2: 47;

         0 <> |.((s1 . GBP ) + 3).| by A2, ABSVALUE:def 1;

        then

         A9: a <> ( DataLoc ((s1 . GBP ),3)) by XTUPLE_0: 1;

        

         A10: (s2 . a) = (( Exec (k1,s1)) . a) by SCMPDS_5: 41

        .= 0 by A2, A9, SCMPDS_2: 47;

        then

         A11: ( DataLoc ((s2 . a),3)) = ( intpos ( 0 + 3)) by SCMP_GCD: 1;

         0 <> |.((s2 . GBP ) + 3).| by A10, ABSVALUE:def 1;

        then

         A12: a <> ( DataLoc ((s2 . GBP ),3)) by XTUPLE_0: 1;

        

        thus (( IExec (WB,P,s)) . a) = (( Exec (k2,s2)) . a) by SCMPDS_5: 41

        .= 0 by A10, A12, SCMPDS_2: 50;

        1 <> |.((s2 . GBP ) + 3).| by A10, ABSVALUE:def 1;

        then

         A13: a1 <> ( DataLoc ((s2 . GBP ),3)) by XTUPLE_0: 1;

        

        thus

         A14: (( IExec (WB,P,s)) . a1) = (( Exec (k2,s2)) . a1) by SCMPDS_5: 41

        .= (s1 . a1) by A6, A13, SCMPDS_2: 50;

        2 <> |.((s2 . GBP ) + 3).| by A10, ABSVALUE:def 1;

        then

         A15: a2 <> ( DataLoc ((s2 . GBP ),3)) by XTUPLE_0: 1;

        

        thus

         A16: (( IExec (WB,P,s)) . a2) = (( Exec (k2,s2)) . a2) by SCMPDS_5: 41

        .= (s1 . a2) by A8, A15, SCMPDS_2: 50;

        

        thus (( IExec (WB,P,s)) . a3) = (( Exec (k2,s2)) . a3) by SCMPDS_5: 41

        .= ((s2 . a3) - (s2 . ( DataLoc ((s2 . a),2)))) by A11, SCMPDS_2: 50

        .= ((( IExec (WB,P,s)) . a1) - (( IExec (WB,P,s)) . a2)) by A10, A8, A4, A14, A16, SCMP_GCD: 1;

      end;

      set s0 = s, m1 = ( SubFrom ( GBP ,1, GBP ,2)), m2 = ( SubFrom ( GBP ,2, GBP ,1));

      assume

       A17: (s . GBP ) = 0 ;

      then

       A18: (s0 . a) = 0 ;

      

       A19: ( DataLoc ((s . a),3)) = ( intpos ( 0 + 3)) by A17, SCMP_GCD: 1;

       A20:

      now

        2 <> |.((s0 . GBP ) + 1).| by A18, ABSVALUE:def 1;

        then

         A21: a2 <> ( DataLoc ((s0 . GBP ),1)) by XTUPLE_0: 1;

         0 <> |.((s0 . GBP ) + 1).| by A18, ABSVALUE:def 1;

        then

         A22: a <> ( DataLoc ((s0 . GBP ),1)) by XTUPLE_0: 1;

        assume

         A23: (s . a3) > 0 ;

        

        hence (s1 . a) = (( IExec (j1,P,s)) . a) by A19, SCMPDS_6: 73

        .= (( Exec (m1,s0)) . a) by SCMPDS_5: 40

        .= 0 by A18, A22, SCMPDS_2: 50;

        

         A24: ( DataLoc ((s0 . a),1)) = ( intpos ( 0 + 1)) by A18, SCMP_GCD: 1;

        

        thus (s1 . a1) = (( IExec (j1,P,s)) . a1) by A19, A23, SCMPDS_6: 73

        .= (( Exec (m1,s0)) . a1) by SCMPDS_5: 40

        .= ((s0 . a1) - (s0 . ( DataLoc ((s0 . a),2)))) by A24, SCMPDS_2: 50

        .= ((s0 . a1) - (s0 . ( intpos ( 0 + 2)))) by A18, SCMP_GCD: 1

        .= ((s . a1) - (s . a2));

        

        thus (s1 . a2) = (( IExec (j1,P,s)) . a2) by A19, A23, SCMPDS_6: 73

        .= (( Exec (m1,s0)) . a2) by SCMPDS_5: 40

        .= (s . a2) by A21, SCMPDS_2: 50;

      end;

      hence (s . a3) > 0 implies (( IExec (WB,P,s)) . a1) = ((s . a1) - (s . a2)) & (( IExec (WB,P,s)) . a2) = (s . a2) by A1;

       A25:

      now

        1 <> |.((s0 . GBP ) + 2).| by A18, ABSVALUE:def 1;

        then

         A26: a1 <> ( DataLoc ((s0 . GBP ),2)) by XTUPLE_0: 1;

         0 <> |.((s0 . GBP ) + 2).| by A18, ABSVALUE:def 1;

        then

         A27: a <> ( DataLoc ((s0 . GBP ),2)) by XTUPLE_0: 1;

        assume

         A28: (s . a3) <= 0 ;

        

        hence (s1 . a) = (( IExec (j2,P,s)) . a) by A19, SCMPDS_6: 74

        .= (( Exec (m2,s0)) . a) by SCMPDS_5: 40

        .= 0 by A18, A27, SCMPDS_2: 50;

        

         A29: ( DataLoc ((s0 . a),2)) = ( intpos ( 0 + 2)) by A18, SCMP_GCD: 1;

        

        thus (s1 . a2) = (( IExec (j2,P,s)) . a2) by A19, A28, SCMPDS_6: 74

        .= (( Exec (m2,s0)) . a2) by SCMPDS_5: 40

        .= ((s0 . a2) - (s0 . ( DataLoc ((s0 . a),1)))) by A29, SCMPDS_2: 50

        .= ((s0 . a2) - (s0 . ( intpos ( 0 + 1)))) by A18, SCMP_GCD: 1

        .= ((s . a2) - (s . a1));

        

        thus (s1 . a1) = (( IExec (j2,P,s)) . a1) by A19, A28, SCMPDS_6: 74

        .= (( Exec (m2,s0)) . a1) by SCMPDS_5: 40

        .= (s . a1) by A26, SCMPDS_2: 50;

      end;

      hence (s . a3) <= 0 implies (( IExec (WB,P,s)) . a2) = ((s . a2) - (s . a1)) & (( IExec (WB,P,s)) . a1) = (s . a1) by A1;

      now

        per cases ;

          suppose (s . a3) > 0 ;

          hence (s1 . a) = 0 by A20;

        end;

          suppose (s . a3) <= 0 ;

          hence (s1 . a) = 0 by A25;

        end;

      end;

      hence thesis by A1;

    end;

    

     Lm13: for s be 0 -started State of SCMPDS st (s . GBP ) = 0 & (s . a1) > 0 & (s . a2) > 0 & (s . a3) = ((s . a1) - (s . a2)) holds (( IExec (WH,P,s)) . a1) = ((s . a1) gcd (s . a2)) & (( IExec (WH,P,s)) . a2) = ((s . a1) gcd (s . a2)) & WH is_closed_on (s,P) & WH is_halting_on (s,P)

    proof

      set a = GBP ;

      let s be 0 -started State of SCMPDS ;

      

       A1: ( DataLoc ( 0 ,3)) = ( intpos ( 0 + 3)) by SCMP_GCD: 1;

       A2:

      now

        let t be 0 -started State of SCMPDS , Q;

        assume that (t . a1) > 0 and (t . a2) > 0 and

         A3: (t . a) = 0 and

         A4: (t . ( DataLoc ( 0 ,3))) = ((t . a1) - (t . a2)) and (t . a1) <> (t . a2);

        thus (( IExec (WB,Q,t)) . a) = 0 by A3, Lm12;

        thus WB is_closed_on (t,Q) by SCMPDS_6: 20;

        thus WB is_halting_on (t,Q) by SCMPDS_6: 21;

        hereby

          assume (t . a1) > (t . a2);

          then (t . a3) > 0 by A1, A4, XREAL_1: 50;

          hence (( IExec (WB,Q,t)) . a1) = ((t . a1) - (t . a2)) & (( IExec (WB,Q,t)) . a2) = (t . a2) by A3, Lm12;

        end;

        hereby

          assume (t . a1) <= (t . a2);

          then (t . a3) <= 0 by A1, A4, XREAL_1: 47;

          hence (( IExec (WB,Q,t)) . a2) = ((t . a2) - (t . a1)) & (( IExec (WB,Q,t)) . a1) = (t . a1) by A3, Lm12;

        end;

        thus (( IExec (WB,Q,t)) . ( DataLoc ( 0 ,3))) = ((( IExec (WB,Q,t)) . a1) - (( IExec (WB,Q,t)) . a2)) by A1, A3, Lm12;

      end;

      assume

       A5: (s . a) = 0 & (s . a1) > 0 & (s . a2) > 0 & (s . a3) = ((s . a1) - (s . a2));

      hence (( IExec (WH,P,s)) . a1) = ((s . a1) gcd (s . a2)) & (( IExec (WH,P,s)) . a2) = ((s . a1) gcd (s . a2)) by A1, A2, Th17;

      thus WH is_closed_on (s,P) & WH is_halting_on (s,P) by A5, A1, A2, Lm10, Th16;

    end;

    set GA = (((i1 ';' i2) ';' i3) ';' WH);

    

     Lm14: for s be 0 -started State of SCMPDS st (s . a1) > 0 & (s . a2) > 0 holds (( IExec (GA,P,s)) . a1) = ((s . a1) gcd (s . a2)) & (( IExec (GA,P,s)) . a2) = ((s . a1) gcd (s . a2)) & GA is_closed_on (s,P) & GA is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS ;

      

       A1: ( Initialize s) = s by MEMSTR_0: 44;

      assume

       A2: (s . a1) > 0 & (s . a2) > 0 ;

      set t0 = s, Q0 = P, t1 = ( IExec (((i1 ';' i2) ';' i3),P,s)), t2 = ( IExec ((i1 ';' i2),P,s)), Q1 = P, t3 = ( Exec (i1,t0)), a = GBP ;

      

       A3: (t3 . a1) = (t0 . a1) by AMI_3: 10, SCMPDS_2: 45

      .= (s . a1);

      

       A4: (t3 . a) = 0 by SCMPDS_2: 45;

      then

       A5: ( DataLoc ((t3 . a),3)) = ( intpos ( 0 + 3)) by SCMP_GCD: 1;

      1 <> |.((t3 . GBP ) + 3).| by A4, ABSVALUE:def 1;

      then

       A6: a1 <> ( DataLoc ((t3 . GBP ),3)) by XTUPLE_0: 1;

      

       A7: (t2 . a1) = (( Exec (i2,t3)) . a1) by SCMPDS_5: 42

      .= (s . a1) by A3, A6, SCMPDS_2: 47;

      

       A8: (t3 . a2) = (t0 . a2) by AMI_3: 10, SCMPDS_2: 45

      .= (s . a2);

      

       A9: (t2 . a3) = (( Exec (i2,t3)) . a3) by SCMPDS_5: 42

      .= (t3 . ( DataLoc ((t3 . a),1))) by A5, SCMPDS_2: 47

      .= (s . a1) by A4, A3, SCMP_GCD: 1;

      2 <> |.((t3 . GBP ) + 3).| by A4, ABSVALUE:def 1;

      then

       A10: a2 <> ( DataLoc ((t3 . GBP ),3)) by XTUPLE_0: 1;

      

       A11: (t2 . a2) = (( Exec (i2,t3)) . a2) by SCMPDS_5: 42

      .= (s . a2) by A8, A10, SCMPDS_2: 47;

       0 <> |.((t3 . GBP ) + 3).| by A4, ABSVALUE:def 1;

      then

       A12: a <> ( DataLoc ((t3 . GBP ),3)) by XTUPLE_0: 1;

      

       A13: (t2 . a) = (( Exec (i2,t3)) . a) by SCMPDS_5: 42

      .= 0 by A4, A12, SCMPDS_2: 47;

      then

       A14: ( DataLoc ((t2 . a),3)) = ( intpos ( 0 + 3)) by SCMP_GCD: 1;

       0 <> |.((t2 . GBP ) + 3).| by A13, ABSVALUE:def 1;

      then

       A15: a <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

       A16: (t1 . a) = (( Exec (i3,t2)) . a) by SCMPDS_5: 41

      .= 0 by A13, A15, SCMPDS_2: 50;

      1 <> |.((t2 . GBP ) + 3).| by A13, ABSVALUE:def 1;

      then

       A17: a1 <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

       A18: (t1 . a1) = (( Exec (i3,t2)) . a1) by SCMPDS_5: 41

      .= (s . a1) by A7, A17, SCMPDS_2: 50;

      2 <> |.((t2 . GBP ) + 3).| by A13, ABSVALUE:def 1;

      then

       A19: a2 <> ( DataLoc ((t2 . GBP ),3)) by XTUPLE_0: 1;

      

       A20: (t1 . a2) = (( Exec (i3,t2)) . a2) by SCMPDS_5: 41

      .= (s . a2) by A11, A19, SCMPDS_2: 50;

      

       A21: (( Initialize t1) . a1) = (t1 . a1) by SCMPDS_5: 15;

      

       A22: (( Initialize t1) . a2) = (t1 . a2) by SCMPDS_5: 15;

      

       A23: (t1 . a3) = (( Exec (i3,t2)) . a3) by SCMPDS_5: 41

      .= ((t2 . a3) - (t2 . ( DataLoc ((t2 . a),2)))) by A14, SCMPDS_2: 50

      .= ((t1 . a1) - (t1 . a2)) by A13, A11, A9, A18, A20, SCMP_GCD: 1;

      

       A24: (( Initialize t1) . GBP ) = (t1 . GBP ) by SCMPDS_5: 15;

      

       A25: (( Initialize t1) . a3) = (t1 . a3) by SCMPDS_5: 15;

      

       A26: WH is_closed_on (( Initialize t1),P) & WH is_halting_on (( Initialize t1),P) by A2, A16, A18, A20, Lm13, A21, A22, A23, A24, A25;

      

       A27: WH is_closed_on (t1,Q1)

      proof

        for k be Nat holds ( IC ( Comput ((Q1 +* ( stop WH)),( Initialize ( Initialize t1)),k))) in ( dom ( stop WH)) by A26, SCMPDS_6:def 2;

        hence thesis by SCMPDS_6:def 2;

      end;

      

       A28: WH is_halting_on (t1,Q1)

      proof

        (Q1 +* ( stop WH)) halts_on ( Initialize ( Initialize t1)) by A26, SCMPDS_6:def 3;

        hence thesis by SCMPDS_6:def 3;

      end;

      (( IExec (WH,Q1,( Initialize t1))) . a1) = ((t1 . a1) gcd (t1 . a2)) by A2, A16, A18, A20, A23, Lm13, A21, A22, A25, A24;

      hence (( IExec (GA,P,s)) . a1) = ((s . a1) gcd (s . a2)) by A18, A20, A27, A28, SCPISORT: 7;

      (( IExec (WH,Q1,( Initialize t1))) . a2) = ((t1 . a1) gcd (t1 . a2)) by A2, A16, A18, A20, A23, Lm13, A21, A22, A25, A24;

      hence (( IExec (GA,P,s)) . a2) = ((s . a1) gcd (s . a2)) by A18, A20, A27, A28, SCPISORT: 7;

      thus thesis by A27, A1, A28, SCPISORT: 9;

    end;

    theorem :: SCPINVAR:19

    for s be 0 -started State of SCMPDS , x,y be Integer st (s . ( intpos 1)) = x & (s . ( intpos 2)) = y & x > 0 & y > 0 holds (( IExec ( GCD-Algorithm ,P,s)) . ( intpos 1)) = (x gcd y) & (( IExec ( GCD-Algorithm ,P,s)) . ( intpos 2)) = (x gcd y) & GCD-Algorithm is_closed_on (s,P) & GCD-Algorithm is_halting_on (s,P) by Lm14;