scpisort.miz



    begin

    reserve x for Int_position,

n,p0 for Nat;

    definition

      let f be FinSequence of INT , s be State of SCMPDS , m be Nat;

      :: SCPISORT:def1

      pred f is_FinSequence_on s,m means for i be Nat st 1 <= i & i <= ( len f) holds (f . i) = (s . ( intpos (m + i)));

    end

    theorem :: SCPISORT:1

    

     Th1: for s be State of SCMPDS , n,m be Nat holds ex f be FinSequence of INT st ( len f) = n & for i be Nat st 1 <= i & i <= ( len f) holds (f . i) = (s . ( intpos (m + i)))

    proof

      let s be State of SCMPDS , n,m be Nat;

      deffunc U( Nat) = (s . ( intpos (m + $1)));

      consider f be FinSequence such that

       A1: ( len f) = n & for i be Nat st i in ( dom f) holds (f . i) = U(i) from FINSEQ_1:sch 2;

      now

        let i be Nat;

        reconsider a = i as Nat;

        assume i in ( dom f);

        then (f . i) = (s . ( intpos (m + a))) by A1;

        hence (f . i) in INT by INT_1:def 2;

      end;

      then

      reconsider f as FinSequence of INT by FINSEQ_2: 12;

      take f;

      thus ( len f) = n by A1;

      thus for i be Nat st 1 <= i <= ( len f) holds (f . i) = (s . ( intpos (m + i))) by A1, FINSEQ_3: 25;

    end;

    theorem :: SCPISORT:2

    for s be State of SCMPDS , n,m be Nat holds ex f be FinSequence of INT st ( len f) = n & f is_FinSequence_on (s,m)

    proof

      let s be State of SCMPDS , n,m be Nat;

      consider f be FinSequence of INT such that

       A1: ( len f) = n and

       A2: for i be Nat st 1 <= i & i <= ( len f) holds (f . i) = (s . ( intpos (m + i))) by Th1;

      take f;

      thus ( len f) = n by A1;

      thus thesis by A2;

    end;

    theorem :: SCPISORT:3

    

     Th3: for f,g be FinSequence of INT , m,n be Nat st 1 <= n & n <= ( len f) & 1 <= m & m <= ( len f) & ( len f) = ( len g) & (f . m) = (g . n) & (f . n) = (g . m) & (for k be Nat st k <> m & k <> n & 1 <= k & k <= ( len f) holds (f . k) = (g . k)) holds (f,g) are_fiberwise_equipotent

    proof

      let f,g be FinSequence of INT , m,n be Nat;

      assume that

       A1: 1 <= n & n <= ( len f) and

       A2: 1 <= m & m <= ( len f) and

       A3: ( len f) = ( len g) and

       A4: (f . m) = (g . n) & (f . n) = (g . m) and

       A5: for k be Nat st k <> m & k <> n & 1 <= k & k <= ( len f) holds (f . k) = (g . k);

      

       A6: m in ( Seg ( len f)) by A2, FINSEQ_1: 1;

      

       A7: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

       A8:

      now

        let k be set;

        assume that

         A9: k <> m & k <> n and

         A10: k in ( dom f);

        reconsider i = k as Nat by A10;

        1 <= i & i <= ( len f) by A7, A10, FINSEQ_1: 1;

        hence (f . k) = (g . k) by A5, A9;

      end;

      n in ( dom f) & ( dom f) = ( dom g) by A1, A3, A7, FINSEQ_1: 1, FINSEQ_1:def 3;

      hence thesis by A4, A7, A6, A8, RFINSEQ: 28;

    end;

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

    theorem :: SCPISORT:4

    

     Th4: for s1,s2 be State of SCMPDS st (for a be Int_position holds (s1 . a) = (s2 . a)) holds ( Initialize s1) = ( Initialize s2)

    proof

      let s1,s2 be State of SCMPDS ;

      assume for a be Int_position holds (s1 . a) = (s2 . a);

      then ( DataPart s1) = ( DataPart s2) by SCMPDS_4: 8;

      hence thesis by MEMSTR_0: 80;

    end;

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

    theorem :: SCPISORT:5

    

     Th5: for s be State of SCMPDS , I be halt-free Program of SCMPDS , j be parahalting shiftable Instruction of SCMPDS st I is_closed_on (s,P) & I is_halting_on (s,P) holds (I ';' j) is_closed_on (s,P) & (I ';' j) is_halting_on (s,P)

    proof

      let s be State of SCMPDS , I be halt-free Program of SCMPDS , j be parahalting shiftable Instruction of SCMPDS ;

      set Mj = ( Load j);

      

       A1: Mj is_closed_on (( IExec (I,P,( Initialize s))),P) & Mj is_halting_on (( IExec (I,P,( Initialize s))),P) by SCMPDS_6: 20, SCMPDS_6: 21;

      assume I is_closed_on (s,P) & I is_halting_on (s,P);

      then (I ';' Mj) is_closed_on (s,P) & (I ';' Mj) is_halting_on (s,P) by A1, SCMPDS_7: 24;

      hence thesis by SCMPDS_4:def 3;

    end;

    theorem :: SCPISORT:6

    for s be 0 -started State of SCMPDS , I be halt-free Program of SCMPDS , J be shiftable parahalting Program of SCMPDS , a be Int_position st I is_closed_on (s,P) & I is_halting_on (s,P) holds (( IExec ((I ';' J),P,s)) . a) = (( IExec (J,P,( Initialize ( IExec (I,P,s))))) . a)

    proof

      let s be 0 -started State of SCMPDS , I be halt-free Program of SCMPDS , J be shiftable parahalting Program of SCMPDS , a be Int_position;

      J is_closed_on (( IExec (I,P,s)),P) & J is_halting_on (( IExec (I,P,s)),P) by SCMPDS_6: 20, SCMPDS_6: 21;

      hence thesis by SCMPDS_7: 30;

    end;

    theorem :: SCPISORT:7

    for s be 0 -started State of SCMPDS , I be halt-free parahalting Program of SCMPDS , J be shiftable Program of SCMPDS , a be Int_position st J is_closed_on (( IExec (I,P,s)),P) & J is_halting_on (( IExec (I,P,s)),P) holds (( IExec ((I ';' J),P,s)) . a) = (( IExec (J,P,( Initialize ( IExec (I,P,s))))) . a)

    proof

      let s be 0 -started State of SCMPDS , I be halt-free parahalting Program of SCMPDS , J be shiftable Program of SCMPDS , a be Int_position;

      I is_closed_on (s,P) & I is_halting_on (s,P) by SCMPDS_6: 20, SCMPDS_6: 21;

      hence thesis by SCMPDS_7: 30;

    end;

    theorem :: SCPISORT:8

    for s be State of SCMPDS , I be Program of SCMPDS , J be shiftable parahalting Program of SCMPDS st I is_closed_on (s,P) & I is_halting_on (s,P) holds (I ';' J) is_closed_on (s,P) & (I ';' J) is_halting_on (s,P)

    proof

      let s be State of SCMPDS , I be Program of SCMPDS , J be shiftable parahalting Program of SCMPDS ;

      

       A1: J is_closed_on (( IExec (I,P,( Initialize s))),P) & J is_halting_on (( IExec (I,P,( Initialize s))),P) by SCMPDS_6: 20, SCMPDS_6: 21;

      assume I is_closed_on (s,P) & I is_halting_on (s,P);

      hence thesis by A1, SCMPDS_7: 24;

    end;

    theorem :: SCPISORT:9

    for s be State of SCMPDS , I be parahalting Program of SCMPDS , J be shiftable Program of SCMPDS st J is_closed_on (( IExec (I,P,( Initialize s))),P) & J is_halting_on (( IExec (I,P,( Initialize s))),P) holds (I ';' J) is_closed_on (s,P) & (I ';' J) is_halting_on (s,P)

    proof

      let s be State of SCMPDS , I be parahalting Program of SCMPDS , J be shiftable Program of SCMPDS ;

      

       A1: I is_closed_on (s,P) & I is_halting_on (s,P) by SCMPDS_6: 20, SCMPDS_6: 21;

      assume J is_closed_on (( IExec (I,P,( Initialize s))),P) & J is_halting_on (( IExec (I,P,( Initialize s))),P);

      hence thesis by A1, SCMPDS_7: 24;

    end;

    theorem :: SCPISORT:10

    for s be State of SCMPDS , I be Program of SCMPDS , j be parahalting shiftable Instruction of SCMPDS st I is_closed_on (s,P) & I is_halting_on (s,P) holds (I ';' j) is_closed_on (s,P) & (I ';' j) is_halting_on (s,P)

    proof

      let s be State of SCMPDS , I be Program of SCMPDS , j be shiftable parahalting Instruction of SCMPDS ;

      

       A1: ( Load j) is_closed_on (( IExec (I,P,( Initialize s))),P) & ( Load j) is_halting_on (( IExec (I,P,( Initialize s))),P) by SCMPDS_6: 20, SCMPDS_6: 21;

      assume I is_closed_on (s,P) & I is_halting_on (s,P);

      then (I ';' ( Load j)) is_closed_on (s,P) & (I ';' ( Load j)) is_halting_on (s,P) by A1, SCMPDS_7: 24;

      hence thesis by SCMPDS_4:def 3;

    end;

    

     Lm1: for a be Int_position, i be Integer, n be Nat, I be Program of SCMPDS holds ( card ( stop ( for-down (a,i,n,I)))) = (( card I) + 4)

    proof

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

      

      thus ( card ( stop ( for-down (a,i,n,I)))) = (( card ( for-down (a,i,n,I))) + 1) by COMPOS_1: 55

      .= ((( card I) + 3) + 1) by SCMPDS_7: 41

      .= (( card I) + 4);

    end;

    

     Lm2: for a be Int_position, i be Integer, n be Nat, I be Program of SCMPDS holds ( for-down (a,i,n,I)) = (((a,i) <=0_goto (( card I) + 3)) ';' ((I ';' ( AddTo (a,i,( - n)))) ';' ( goto ( - (( card I) + 2)))))

    proof

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

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

      

      thus ( for-down (a,i,n,I)) = (((i1 ';' I) ';' i2) ';' i3) by SCMPDS_7:def 2

      .= (i1 ';' ((I ';' i2) ';' i3)) by SCMPDS_7: 2;

    end;

    

     Lm3: for I be Program of SCMPDS , a be Int_position, i be Integer, n be Nat holds ( Shift ((I ';' ( AddTo (a,i,( - n)))),1)) c= ( for-down (a,i,n,I))

    proof

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

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

      

       A1: ( for-down (a,i,n,I)) = (((i1 ';' I) ';' i2) ';' i3) by SCMPDS_7:def 2

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

      .= ((( Load i1) ';' (I ';' i2)) ';' i3) by SCMPDS_4:def 2

      .= ((( Load i1) ';' (I ';' i2)) ';' ( Load i3)) by SCMPDS_4:def 3;

      ( card ( Load i1)) = 1 by COMPOS_1: 54;

      hence thesis by A1, SCMPDS_7: 3;

    end;

    begin

    scheme :: SCPISORT:sch1

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

( for-down (a(),i(),n(),I())) is_closed_on (s(),P()) & ( for-down (a(),i(),n(),I())) is_halting_on (s(),P())

      provided

       A1: n() > 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() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . a()) = (t . a()) & (( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . ( DataLoc ((s() . a()),i()))) = ((t . ( DataLoc ((s() . a()),i()))) - n()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & P[( Initialize ( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)))];

      set i1 = ((a(),i()) <=0_goto (( card I()) + 3)), J = (I() ';' ( AddTo (a(),i(),( - n())))), i3 = ( goto ( - (( card I()) + 2)));

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

      set FOR = ( for-down (a(),i(),n(),I())), pFOR = ( stop FOR), pJ = ( stop J);

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

      

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

      proof

        let k be Nat;

        assume

         A5: Q[k];

        now

          let t be 0 -started State of SCMPDS ;

          let Q;

          

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

          assume

           A7: (t . b) <= (k + 1);

          assume

           A8: P[t];

          assume

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

          per cases ;

            suppose (t . b) <= 0 ;

            hence FOR is_closed_on (t,Q) & FOR is_halting_on (t,Q) by A9, SCMPDS_7: 44;

          end;

            suppose

             A10: (t . b) > 0 ;

            

             A11: 0 in ( dom pFOR) by COMPOS_1: 36;

            ( - ( - n())) > 0 by A1;

            then ( - n()) < 0 ;

            then ( - n()) <= ( - 1) by INT_1: 8;

            then

             A12: (( - n()) + (t . b)) <= (( - 1) + (t . b)) by XREAL_1: 6;

            ((t . b) - 1) <= k by A7, XREAL_1: 20;

            then

             A13: (( - n()) + (t . b)) <= k by A12, XXREAL_0: 2;

            set Q2 = (Q +* pJ), Q3 = (Q +* pFOR), t4 = ( Comput (Q3,t,1)), Q4 = Q3, Jt = ( IExec (J,Q,t));

            

             A14: pJ c= Q2 by FUNCT_4: 25;

            

             A15: FOR = (i1 ';' (J ';' i3)) by Lm2;

            

             A16: ( Comput (Q3,t,( 0 + 1))) = ( Following (Q3,( Comput (Q3,t, 0 )))) by EXTPRO_1: 3

            .= ( Following (Q3,t)) by EXTPRO_1: 2

            .= ( Exec (i1,t)) by A15, A6, SCMPDS_6: 11;

            for x holds (t . x) = (t4 . x) by A16, SCMPDS_2: 56;

            then

             A17: ( DataPart t) = ( DataPart t4) by SCMPDS_4: 8;

            

             A18: (Jt . b) = ((t . b) - n()) by A3, A8, A9, A10;

            

             A19: (Jt . a()) = (t . a()) by A3, A8, A9, A10;

            set m2 = ( LifeSpan (Q2,t)), t5 = ( Comput (Q4,t4,m2)), Q5 = Q4, l1 = (( card J) + 1);

            

             A20: ( card J) = (( card I()) + 1) by SCMP_GCD: 4;

            

             A21: (t . ( DataLoc ((t . a()),i()))) = (t . b) by A9;

            

             A22: ( IC t) = 0 by A6, MEMSTR_0: 47;

            

             A23: I() is_closed_on (t,Q) & I() is_halting_on (t,Q) by A3, A8, A9, A10;

            then

             A24: J is_closed_on (t,Q) by Th5;

            then

             A25: J is_closed_on (t,Q2) by A6, SCMPDS_6: 24;

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

            then

             A26: l1 in ( dom FOR) by A20, SCMPDS_7: 42;

            set m3 = (m2 + 1);

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

            

             A27: t6 = t5 by EXTPRO_1: 4;

            

             A28: J is_halting_on (t,Q) by A23, Th5;

            then

             A29: Q2 halts_on t by A6, SCMPDS_6:def 3;

            (Q2 +* pJ) halts_on t by A28, A6, SCMPDS_6:def 3;

            then

             A30: J is_halting_on (t,Q2) by A6, SCMPDS_6:def 3;

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

            

             A31: pFOR c= Q3 by FUNCT_4: 25;

            

             A32: FOR c= pFOR by AFINSQ_1: 74;

            then

             A33: FOR c= Q3 by A31, XBOOLE_1: 1;

            ( Shift (J,1)) c= FOR by Lm3;

            then ( Shift (J,1)) c= pFOR by A32, XBOOLE_1: 1;

            then

             A34: ( Shift (J,1)) c= Q4 by A31, XBOOLE_1: 1;

            

             A35: ( IC t4) = (( IC t) + 1) by A10, A16, A21, SCMPDS_2: 56

            .= ( 0 + 1) by A22;

            then

             A36: ( DataPart ( Comput (Q2,t,m2))) = ( DataPart t5) by A14, A30, A25, A17, A34, SCMPDS_7: 18;

            

            then

             A37: ( DataPart t5) = ( DataPart ( Result (Q2,t))) by A29, EXTPRO_1: 23

            .= ( DataPart Jt) by SCMPDS_4:def 5;

            

             A38: ( IC t5) = l1 by A14, A30, A25, A35, A17, A34, SCMPDS_7: 18;

            

            then

             A39: ( CurInstr (Q6,t6)) = (Q4 . l1) by A27, PBOOLE: 143

            .= (FOR . l1) by A26, A33, GRFUNC_1: 2

            .= i3 by A20, SCMPDS_7: 43;

            

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

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

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

            .= 0 by A20, A38, A27, SCMPDS_7: 1;

            then

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

            ( InsCode i3) = 14 by SCMPDS_2: 12;

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

            

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

            .= ( Initialize Jt) by A37, A27, MEMSTR_0: 80;

            then

             A42: P[t7] by A3, A8, A9, A10;

            

             A43: (Q7 +* pFOR) = Q7;

            (t5 . b) = (( Comput (Q2,t,m2)) . b) by A36, SCMPDS_4: 8

            .= (( Result (Q2,t)) . b) by A29, EXTPRO_1: 23

            .= ((t . b) - n()) by A18, SCMPDS_4:def 5;

            then

             A44: (t7 . b) = (( - n()) + (t . b)) by A27, A40, SCMPDS_2: 54;

            (t5 . a()) = (( Comput (Q2,t,m2)) . a()) by A36, SCMPDS_4: 8

            .= (( Result (Q2,t)) . a()) by A29, EXTPRO_1: 23

            .= (s() . a()) by A9, A19, SCMPDS_4:def 5;

            then

             A45: (t7 . a()) = (s() . a()) by A27, A40, SCMPDS_2: 54;

            then

             A46: FOR is_closed_on (t7,Q7) by A5, A42, A44, A13, A41;

            now

              let k be Nat;

              per cases ;

                suppose k < m4;

                then

                 A47: k <= m3 by INT_1: 7;

                hereby

                  per cases by A47, NAT_1: 8;

                    suppose

                     A48: k <= m2;

                    per cases ;

                      suppose k = 0 ;

                      hence ( IC ( Comput (Q3,t,k))) in ( dom pFOR) by A11, A22, EXTPRO_1: 2;

                    end;

                      suppose k <> 0 ;

                      then

                      consider kn be Nat such that

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

                      reconsider kn as Nat;

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

                      kn < k by A49, XREAL_1: 29;

                      then kn < m2 by A48, XXREAL_0: 2;

                      then (( IC ( Comput (Q2,t,kn))) + 1) = ( IC ( Comput (Q4,t4,kn))) by A14, A30, A25, A35, A17, A34, SCMPDS_7: 16;

                      then

                       A50: ( IC ( Comput (Q3,t,k))) = (lm + 1) by A49, EXTPRO_1: 4;

                      ( IC ( Comput (Q2,t,kn))) in ( dom pJ) by A24, A6, SCMPDS_6:def 2;

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

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

                      then

                       A51: (lm + 1) <= (( card J) + 1) by INT_1: 7;

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

                      then (lm + 1) < (( card I()) + 4) by A20, A51, XXREAL_0: 2;

                      then (lm + 1) < ( card pFOR) by Lm1;

                      hence ( IC ( Comput (Q3,t,k))) in ( dom pFOR) by A50, AFINSQ_1: 66;

                    end;

                  end;

                    suppose

                     A52: k = m3;

                    l1 in ( dom pFOR) by A26, COMPOS_1: 62;

                    hence ( IC ( Comput (Q3,t,k))) in ( dom pFOR) by A14, A30, A25, A35, A17, A34, A27, A52, SCMPDS_7: 18;

                  end;

                end;

              end;

                suppose k >= m4;

                then

                consider nn be Nat such that

                 A53: k = (m4 + nn) by NAT_1: 10;

                reconsider nn as Nat;

                ( Comput (Q3,t,k)) = ( Comput (Q3,( Comput (Q3,t,m4)),nn)) by A53, EXTPRO_1: 4

                .= ( Comput ((Q7 +* pFOR),t7,nn));

                hence ( IC ( Comput (Q3,t,k))) in ( dom pFOR) by A46, A41, SCMPDS_6:def 2;

              end;

            end;

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

            FOR is_halting_on (t7,Q7) by A5, A45, A42, A44, A13, A41;

            then Q7 halts_on t7 by A43, A41, SCMPDS_6:def 3;

            then Q3 halts_on t by EXTPRO_1: 22;

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

          end;

        end;

        hence thesis;

      end;

      

       A54: Q[ 0 ] by SCMPDS_7: 44;

      

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

      per cases ;

        suppose (s() . b) <= 0 ;

        hence thesis by SCMPDS_7: 44;

      end;

        suppose (s() . b) > 0 ;

        then

        reconsider m = (s() . b) as Element of NAT by INT_1: 3;

         Q[m] by A55;

        hence thesis by A2;

      end;

    end;

    scheme :: SCPISORT:sch2

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

( IExec (( for-down (a(),i(),n(),I())),P(),s())) = ( IExec (( for-down (a(),i(),n(),I())),P(),( Initialize ( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),P(),s())))))

      provided

       A1: n() > 0

       and

       A2: (s() . ( 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() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . a()) = (t . a()) & (( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . ( DataLoc ((s() . a()),i()))) = ((t . ( DataLoc ((s() . a()),i()))) - n()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & P[( Initialize ( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)))];

      set i1 = ((a(),i()) <=0_goto (( card I()) + 3)), J = (I() ';' ( AddTo (a(),i(),( - n())))), i3 = ( goto ( - (( card I()) + 2)));

      set FOR = ( for-down (a(),i(),n(),I())), pFOR = ( stop FOR), P1 = (P() +* pFOR);

      set PJ = (P() +* ( stop J)), mJ = ( LifeSpan (PJ,s())), m1 = (mJ + 2), s2 = ( Initialize ( IExec (J,P(),s()))), m2 = ( LifeSpan (P1,s2));

      

       A5: ( stop J) c= PJ by FUNCT_4: 25;

      

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

      

       A7: I() is_closed_on (s(),P()) & I() is_halting_on (s(),P()) by A2, A3, A4;

      then J is_closed_on (s(),P()) by Th5;

      then

       A8: J is_closed_on (s(),PJ) by A6, SCMPDS_6: 24;

      

       A9: J is_halting_on (s(),P()) by A7, Th5;

      then

       A10: PJ halts_on s() by A6, SCMPDS_6:def 3;

      (PJ +* ( stop J)) halts_on ( Initialize s()) by A9, SCMPDS_6:def 3;

      then

       A11: J is_halting_on (s(),PJ) by SCMPDS_6:def 3;

      

       A12: FOR = (i1 ';' (J ';' i3)) by Lm2;

      

       A13: ( Comput (P1,s(),( 0 + 1))) = ( Following (P1,( Comput (P1,s(), 0 )))) by EXTPRO_1: 3

      .= ( Following (P1,s())) by EXTPRO_1: 2

      .= ( Exec (i1,s())) by A12, A6, SCMPDS_6: 11;

      set m3 = (mJ + 1);

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

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

      

       A14: ( card J) = (( card I()) + 1) by SCMP_GCD: 4;

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

      set s5 = ( Comput (P4,s4,mJ)), l1 = (( card J) + 1), P5 = P4;

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

      then

       A15: l1 in ( dom FOR) by A14, SCMPDS_7: 42;

      

       A16: s6 = s5 by EXTPRO_1: 4;

      for x holds (s() . x) = (s4 . x) by A13, SCMPDS_2: 56;

      then

       A17: ( DataPart s()) = ( DataPart s4) by SCMPDS_4: 8;

      

       A18: ( IC s()) = 0 by MEMSTR_0:def 12;

      

       A19: pFOR c= P1 by FUNCT_4: 25;

      

       A20: FOR c= pFOR by AFINSQ_1: 74;

      then

       A21: FOR c= P1 by A19, XBOOLE_1: 1;

      ( Shift (J,1)) c= FOR by Lm3;

      then ( Shift (J,1)) c= pFOR by A20, XBOOLE_1: 1;

      then

       A22: ( Shift (J,1)) c= P4 by A19, XBOOLE_1: 1;

      set m0 = ( LifeSpan (P1,s()));

      set m4 = (m3 + 1), s7 = ( Comput (P1,s(),m4));

      

       A23: ( IC s4) = (( IC s()) + 1) by A2, A13, SCMPDS_2: 56

      .= ( 0 + 1) by A18;

      then

       A24: ( IC s5) = l1 by A5, A11, A8, A17, A22, SCMPDS_7: 18;

      

      then

       A25: ( CurInstr (P6,s6)) = (P4 . l1) by A16, PBOOLE: 143

      .= (FOR . l1) by A15, A21, GRFUNC_1: 2

      .= i3 by A14, SCMPDS_7: 43;

      

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

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

      

       A27: ( DataPart ( Comput (PJ,s(),mJ))) = ( DataPart s5) by A5, A11, A8, A23, A17, A22, SCMPDS_7: 18;

      now

        let x be Int_position;

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

        then

         A28: (s2 . x) = (( IExec (J,P(),s())) . x) by FUNCT_4: 11;

        (s5 . x) = (( Comput (PJ,s(),mJ)) . x) by A27, SCMPDS_4: 8

        .= (( Result (PJ,s())) . x) by A10, EXTPRO_1: 23

        .= (( IExec (J,P(),s())) . x) by SCMPDS_4:def 5;

        hence (s7 . x) = (s2 . x) by A16, A26, A28, SCMPDS_2: 54;

      end;

      then

       A29: ( DataPart s7) = ( DataPart s2) by SCMPDS_4: 8;

      

       A30: 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() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . a()) = (t . a()) & (( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . ( DataLoc ((s() . a()),i()))) = ((t . ( DataLoc ((s() . a()),i()))) - n()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & P[( Initialize ( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)))] by A4;

      

       A31: P[s()] by A3;

      ( for-down (a(),i(),n(),I())) is_closed_on (s(),P()) & ( for-down (a(),i(),n(),I())) is_halting_on (s(),P()) from ForDownHalt( A1, A31, A30);

      then

       A32: P1 halts_on s() by A6, SCMPDS_6:def 3;

      set Es = ( IExec (J,P(),s())), bj = ( DataLoc ((( Initialize Es) . a()),i()));

      (( Initialize Es) . a()) = (Es . a()) by SCMPDS_5: 15

      .= (s() . a()) by A2, A3, A4;

      then

       A33: 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() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . a()) = (t . a()) & (( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)) . ( DataLoc ((( Initialize Es) . a()),i()))) = ((t . ( DataLoc ((( Initialize Es) . a()),i()))) - n()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & P[( Initialize ( IExec ((I() ';' ( AddTo (a(),i(),( - n())))),Q,t)))] by A4;

      

       A34: P[( Initialize Es)] by A2, A3, A4;

      FOR is_closed_on (( Initialize Es),P()) & FOR is_halting_on (( Initialize Es),P()) from ForDownHalt( A1, A34, A33);

      then

       A35: P1 halts_on ( Initialize s2) by SCMPDS_6:def 3;

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

      .= 0 by A14, A24, A16, SCMPDS_7: 1;

      then

       A36: ( IC s2) = ( IC ( Comput (P1,s(),m1))) by MEMSTR_0: 47;

      

       A37: ( Comput (P1,s(),m1)) = s2 by A29, A36, MEMSTR_0: 78;

      then ( CurInstr (P1,( Comput (P1,s(),m1)))) = i1 by A12, SCMPDS_6: 11;

      then m0 > m1 by A32, EXTPRO_1: 36, SCMPDS_6: 17;

      then

      consider nn be Nat such that

       A38: m0 = (m1 + nn) by NAT_1: 10;

      reconsider nn as Nat;

      ( Comput (P1,s(),(m1 + m2))) = ( Comput (P1,s2,m2)) by A37, EXTPRO_1: 4;

      then ( CurInstr (P1,( Comput (P1,s(),(m1 + m2))))) = ( halt SCMPDS ) by A35, EXTPRO_1:def 15;

      then (m1 + m2) >= m0 by A32, EXTPRO_1:def 15;

      then

       A39: m2 >= nn by A38, XREAL_1: 6;

      

       A40: ( Comput (P1,s(),m0)) = ( Comput (P1,s2,nn)) by A37, A38, EXTPRO_1: 4;

      then ( CurInstr (P1,( Comput (P1,s2,nn)))) = ( halt SCMPDS ) by A32, EXTPRO_1:def 15;

      then nn >= m2 by A35, EXTPRO_1:def 15;

      then nn = m2 by A39, XXREAL_0: 1;

      then ( Result (P1,s())) = ( Comput (P1,s2,m2)) by A32, A40, EXTPRO_1: 23;

      

      hence ( IExec (FOR,P(),s())) = ( Comput (P1,s2,m2)) by SCMPDS_4:def 5

      .= ( Result (P1,s2)) by A35, EXTPRO_1: 23

      .= ( IExec (FOR,P(),( Initialize ( IExec (J,P(),s()))))) by SCMPDS_4:def 5;

    end;

    scheme :: SCPISORT:sch3

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

(( IExec (( for-down (a(),i(),n(),I())),P(),s())) . ( DataLoc ((s() . a()),i()))) <= 0 & P[( Initialize ( IExec (( for-down (a(),i(),n(),I())),P(),s())))]

      provided

       A1: n() > 0

       and

       A2: P[s()]

       and

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

      set b = ( DataLoc ((s() . a()),i())), FR = ( for-down (a(),i(),n(),I()));

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

      

       A4: Q[ 0 qua Nat]

      proof

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

        assume that

         A5: (t . b) <= 0 & (t . a()) = (s() . a()) and

         A6: P[t];

        

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

        hence (( IExec (FR,Q,t)) . b) <= 0 by A5, SCMPDS_7: 47;

        for x be Int_position holds (( IExec (FR,Q,t)) . x) = (t . x) by A5, A7, SCMPDS_7: 47;

        hence thesis by A6, Th4, A7;

      end;

       A8:

      now

        let k be Nat;

        assume

         A9: Q[k];

        thus Q[(k + 1)]

        proof

          let u be 0 -started State of SCMPDS ;

          let U;

          assume that

           A10: (u . b) <= (k + 1) and

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

           A12: P[u];

          per cases ;

            suppose (u . b) <= 0 ;

            hence (( IExec (FR,U,u)) . b) <= 0 & P[( Initialize ( IExec (FR,U,u)))] by A4, A11, A12;

          end;

            suppose

             A13: (u . b) > 0 ;

            set Ad = ( AddTo (a(),i(),( - n())));

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

            

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

            (Iu . b) = ((u . b) - n()) by A3, A11, A12, A13;

            then ((Iu . b) + 1) <= (u . b) by A1, INT_1: 7, XREAL_1: 44;

            then ((Iu . b) + 1) <= (k + 1) by A10, XXREAL_0: 2;

            then

             A15: (Iu . b) <= k by XREAL_1: 6;

            

             A16: P[u] by A12;

            

             A17: 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() ';' Ad),Q,t)) . a()) = (t . a()) & (( IExec ((I() ';' Ad),Q,t)) . ( DataLoc ((u . a()),i()))) = ((t . ( DataLoc ((u . a()),i()))) - n()) & I() is_closed_on (t,Q) & I() is_halting_on (t,Q) & P[( Initialize ( IExec ((I() ';' Ad),Q,t)))] by A3, A11;

            

             A18: (u . ( DataLoc ((u . a()),i()))) > 0 by A11, A13;

            

             A19: (( Initialize Iu) . b) = (Iu . b) by SCMPDS_5: 15;

            

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

            ( IExec (FR,U,u)) = ( IExec (FR,U,( Initialize Iu))) from ForDownExec( A1, A18, A16, A17);

            hence (( IExec (FR,U,u)) . b) <= 0 & P[( Initialize ( IExec (FR,U,u)))] by A9, A15, A14, A19, A20;

          end;

        end;

      end;

      

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

      per cases ;

        suppose (s() . b) > 0 ;

        then

        reconsider m = (s() . b) as Element of NAT by INT_1: 3;

         Q[m] by A21;

        hence thesis by A2;

      end;

        suppose (s() . b) <= 0 ;

        hence thesis by A2, A4;

      end;

    end;

    theorem :: SCPISORT:11

    

     Th11: for s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,x,y be Int_position, i,c be Integer, n be Nat st n > 0 & (s . x) >= ((s . y) + c) & for t be 0 -started State of SCMPDS , Q st (t . x) >= ((t . y) + c) & (t . a) = (s . a) & (t . ( DataLoc ((s . a),i))) > 0 holds (( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . a) = (t . a) & (( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . ( DataLoc ((s . a),i))) = ((t . ( DataLoc ((s . a),i))) - n) & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . x) >= ((( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . y) + c) holds ( for-down (a,i,n,I)) is_closed_on (s,P) & ( for-down (a,i,n,I)) is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,x,y be Int_position, i,c be Integer, n be Nat;

      set b = ( DataLoc ((s . a),i)), J = (I ';' ( AddTo (a,i,( - n))));

      assume

       A1: n > 0 ;

      defpred P[ set] means ex t be State of SCMPDS st t = $1 & (t . x) >= ((t . y) + c);

      assume

       A2: (s . x) >= ((s . y) + c);

      

       A3: P[s] by A2;

      assume

       A4: for t be 0 -started State of SCMPDS , Q st (t . x) >= ((t . y) + c) & (t . a) = (s . a) & (t . b) > 0 holds (( IExec (J,Q,t)) . a) = (t . a) & (( IExec (J,Q,t)) . b) = ((t . b) - n) & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec (J,Q,t)) . x) >= ((( IExec (J,Q,t)) . y) + c);

       A5:

      now

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

        assume that

         A6: P[t] and

         A7: (t . a) = (s . a) & (t . b) > 0 ;

        consider v be State of SCMPDS such that

         A8: v = t and

         A9: (v . x) >= ((v . y) + c) by A6;

        thus (( IExec (J,Q,t)) . a) = (t . a) & (( IExec (J,Q,t)) . b) = ((t . b) - n) & I is_closed_on (t,Q) & I is_halting_on (t,Q) by A4, A7, A8, A9;

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

        proof

          take v = ( Initialize ( IExec (J,Q,t)));

          thus v = ( Initialize ( IExec (J,Q,t)));

          (v . x) = (( IExec (J,Q,t)) . x) by SCMPDS_5: 15;

          then (v . x) >= ((( IExec (J,Q,t)) . y) + c) by A4, A7, A8, A9;

          hence thesis by SCMPDS_5: 15;

        end;

      end;

      ( for-down (a,i,n,I)) is_closed_on (s,P) & ( for-down (a,i,n,I)) is_halting_on (s,P) from ForDownHalt( A1, A3, A5);

      hence thesis;

    end;

    theorem :: SCPISORT:12

    

     Th12: for s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,x,y be Int_position, i,c be Integer, n be Nat st n > 0 & (s . x) >= ((s . y) + c) & (s . ( DataLoc ((s . a),i))) > 0 & for t be 0 -started State of SCMPDS , Q st (t . x) >= ((t . y) + c) & (t . a) = (s . a) & (t . ( DataLoc ((s . a),i))) > 0 holds (( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . a) = (t . a) & (( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . ( DataLoc ((s . a),i))) = ((t . ( DataLoc ((s . a),i))) - n) & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . x) >= ((( IExec ((I ';' ( AddTo (a,i,( - n)))),Q,t)) . y) + c) holds ( IExec (( for-down (a,i,n,I)),P,s)) = ( IExec (( for-down (a,i,n,I)),P,( Initialize ( IExec ((I ';' ( AddTo (a,i,( - n)))),P,s)))))

    proof

      let s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a,x,y be Int_position, i,c be Integer, n be Nat;

      set b = ( DataLoc ((s . a),i)), J = (I ';' ( AddTo (a,i,( - n))));

      assume

       A1: n > 0 ;

      defpred P[ set] means ex t be State of SCMPDS st t = $1 & (t . x) >= ((t . y) + c);

      assume

       A2: (s . x) >= ((s . y) + c);

      

       A3: P[s] by A2;

      assume

       A4: (s . b) > 0 ;

      assume

       A5: for t be 0 -started State of SCMPDS , Q st (t . x) >= ((t . y) + c) & (t . a) = (s . a) & (t . b) > 0 holds (( IExec (J,Q,t)) . a) = (t . a) & (( IExec (J,Q,t)) . b) = ((t . b) - n) & I is_closed_on (t,Q) & I is_halting_on (t,Q) & (( IExec (J,Q,t)) . x) >= ((( IExec (J,Q,t)) . y) + c);

       A6:

      now

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

        assume that

         A7: P[t] and

         A8: (t . a) = (s . a) & (t . b) > 0 ;

        consider v be State of SCMPDS such that

         A9: v = t and

         A10: (v . x) >= ((v . y) + c) by A7;

        thus (( IExec (J,Q,t)) . a) = (t . a) & (( IExec (J,Q,t)) . b) = ((t . b) - n) & I is_closed_on (t,Q) & I is_halting_on (t,Q) by A5, A8, A9, A10;

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

        proof

          take v = ( Initialize ( IExec (J,Q,t)));

          thus v = ( Initialize ( IExec (J,Q,t)));

          (v . x) = (( IExec (J,Q,t)) . x) by SCMPDS_5: 15;

          then (v . x) >= ((( IExec (J,Q,t)) . y) + c) by A5, A8, A9, A10;

          hence thesis by SCMPDS_5: 15;

        end;

      end;

      ( IExec (( for-down (a,i,n,I)),P,s)) = ( IExec (( for-down (a,i,n,I)),P,( Initialize ( IExec ((I ';' ( AddTo (a,i,( - n)))),P,s))))) from ForDownExec( A1, A4, A3, A6);

      hence thesis;

    end;

    theorem :: SCPISORT:13

    for s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a be Int_position, i be Integer, n be Nat st (s . ( DataLoc ((s . a),i))) > 0 & n > 0 & a <> ( DataLoc ((s . a),i)) & (for t be 0 -started State of SCMPDS , Q st (t . a) = (s . a) holds (( IExec (I,Q,t)) . a) = (t . a) & (( IExec (I,Q,t)) . ( DataLoc ((s . a),i))) = (t . ( DataLoc ((s . a),i))) & I is_closed_on (t,Q) & I is_halting_on (t,Q)) holds ( for-down (a,i,n,I)) is_closed_on (s,P) & ( for-down (a,i,n,I)) is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS , I be halt-free shiftable Program of SCMPDS , a be Int_position, i be Integer, n be Nat;

      assume that

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

       A2: for t be 0 -started State of SCMPDS , Q st (t . a) = (s . a) holds (( IExec (I,Q,t)) . a) = (t . a) & (( IExec (I,Q,t)) . ( DataLoc ((s . a),i))) = (t . ( DataLoc ((s . a),i))) & I is_closed_on (t,Q) & I is_halting_on (t,Q);

      for t be 0 -started State of SCMPDS , Q st (for x be Int_position st x in {} holds (t . x) = (s . x)) & (t . a) = (s . a) holds (( IExec (I,Q,t)) . a) = (t . a) & (( IExec (I,Q,t)) . ( DataLoc ((s . a),i))) = (t . ( DataLoc ((s . a),i))) & I is_closed_on (t,Q) & I is_halting_on (t,Q) & for y be Int_position st y in {} holds (( IExec (I,Q,t)) . y) = (t . y) by A2;

      hence thesis by A1, SCMPDS_7: 48;

    end;

    begin

    definition

      let n,p0 be Nat;

      :: SCPISORT:def2

      func insert-sort (n,p0) -> Program of SCMPDS equals ((((( GBP := 0 ) ';' (( GBP ,1) := 0 )) ';' (( GBP ,2) := (n - 1))) ';' (( GBP ,3) := p0)) ';' ( for-down ( GBP ,2,1,((((( AddTo ( GBP ,3,1)) ';' (( GBP ,4) := ( GBP ,3))) ';' ( AddTo ( GBP ,1,1))) ';' (( GBP ,6) := ( GBP ,1))) ';' ( while>0 ( GBP ,6,(((( GBP ,5) := (( intpos 4),( - 1))) ';' ( SubFrom ( GBP ,5,( intpos 4), 0 ))) ';' ( if>0 ( GBP ,5,(((((( GBP ,5) := (( intpos 4),( - 1))) ';' ((( intpos 4),( - 1)) := (( intpos 4), 0 ))) ';' ((( intpos 4), 0 ) := ( GBP ,5))) ';' ( AddTo ( GBP ,4,( - 1)))) ';' ( AddTo ( GBP ,6,( - 1)))),( Load (( GBP ,6) := 0 )))))))))));

      coherence ;

    end

    set j1 = ( AddTo ( GBP ,3,1)), j2 = (( GBP ,4) := ( GBP ,3)), j3 = ( AddTo ( GBP ,1,1)), j4 = (( GBP ,6) := ( GBP ,1)), k1 = (( GBP ,5) := (( intpos 4),( - 1))), k2 = ( SubFrom ( GBP ,5,( intpos 4), 0 )), k3 = (( GBP ,5) := (( intpos 4),( - 1))), k4 = ((( intpos 4),( - 1)) := (( intpos 4), 0 )), k5 = ((( intpos 4), 0 ) := ( GBP ,5)), k6 = ( AddTo ( GBP ,4,( - 1))), k7 = ( AddTo ( GBP ,6,( - 1))), FA = ( Load (( GBP ,6) := 0 )), TR = (((((( GBP ,5) := (( intpos 4),( - 1))) ';' ((( intpos 4),( - 1)) := (( intpos 4), 0 ))) ';' ((( intpos 4), 0 ) := ( GBP ,5))) ';' ( AddTo ( GBP ,4,( - 1)))) ';' ( AddTo ( GBP ,6,( - 1)))), IF = ( if>0 ( GBP ,5,TR,FA)), B1 = (((( GBP ,5) := (( intpos 4),( - 1))) ';' ( SubFrom ( GBP ,5,( intpos 4), 0 ))) ';' ( if>0 ( GBP ,5,TR,FA))), WH = ( while>0 ( GBP ,6,B1)), J4 = (((j1 ';' j2) ';' j3) ';' j4), B2 = (J4 ';' WH), FR = ( for-down ( GBP ,2,1,B2));

    

     Lm4: ( card B1) = 10

    proof

      

      thus ( card B1) = (( card (k1 ';' k2)) + ( card IF)) by AFINSQ_1: 17

      .= (2 + ( card IF)) by SCMP_GCD: 5

      .= (2 + ((( card TR) + ( card FA)) + 2)) by SCMPDS_6: 65

      .= (2 + (((( card (((k3 ';' k4) ';' k5) ';' k6)) + 1) + ( card FA)) + 2)) by SCMP_GCD: 4

      .= (2 + ((((( card ((k3 ';' k4) ';' k5)) + 1) + 1) + ( card FA)) + 2)) by SCMP_GCD: 4

      .= (2 + (((((( card (k3 ';' k4)) + 1) + 1) + 1) + ( card FA)) + 2)) by SCMP_GCD: 4

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

      .= (2 + (((((2 + 1) + 1) + 1) + 1) + 2)) by COMPOS_1: 54

      .= 10;

    end;

    

     Lm5: ( card B2) = 16

    proof

      

      thus ( card B2) = (( card (((j1 ';' j2) ';' j3) ';' j4)) + ( card WH)) by AFINSQ_1: 17

      .= ((( card ((j1 ';' j2) ';' j3)) + 1) + ( card WH)) by SCMP_GCD: 4

      .= (((( card (j1 ';' j2)) + 1) + 1) + ( card WH)) by SCMP_GCD: 4

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

      .= (((2 + 1) + 1) + (10 + 2)) by Lm4, SCMPDS_8: 17

      .= 16;

    end;

    set a1 = ( intpos 1), a2 = ( intpos 2), a3 = ( intpos 3), a4 = ( intpos 4), a5 = ( intpos 5), a6 = ( intpos 6);

    

     Lm6: for s be 0 -started State of SCMPDS st (s . a4) >= (7 + (s . a6)) & (s . GBP ) = 0 & (s . a6) > 0 holds (( IExec (B1,P,s)) . GBP ) = 0 & (( IExec (B1,P,s)) . a1) = (s . a1)

    proof

      let s be 0 -started State of SCMPDS ;

      set a = GBP , x = ( DataLoc ((s . a4),( - 1))), y = ( DataLoc ((s . a4), 0 ));

      assume that

       A1: (s . a4) >= (7 + (s . a6)) and

       A2: (s . a) = 0 and

       A3: (s . a6) > 0 ;

      

       A4: (7 + (s . a6)) > (7 + 0 ) by A3, XREAL_1: 6;

      set t0 = s, t1 = ( Exec (k1,t0)), t2 = ( IExec ((k1 ';' k2),P,s)), Q2 = P;

      

       A5: ( DataLoc ((t0 . a),5)) = ( intpos ( 0 + 5)) by A2, SCMP_GCD: 1;

      then

       A6: (t1 . a) = 0 by A2, AMI_3: 10, SCMPDS_2: 47;

      then

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

      

       A8: (t1 . a4) = (s . a4) by A5, AMI_3: 10, SCMPDS_2: 47;

      

       A9: (s . a4) >= (1 + (6 + (s . a6))) by A1;

      then

       A10: ((s . a4) - 1) >= (6 + (s . a6)) by XREAL_1: 19;

      set Fi = ((a,6) := 0 ), t02 = ( Initialize t2), Q02 = Q2, t3 = ( IExec ((((k3 ';' k4) ';' k5) ';' k6),Q2,( Initialize t2))), t4 = ( IExec (((k3 ';' k4) ';' k5),Q2,( Initialize t2))), t5 = ( IExec ((k3 ';' k4),Q2,( Initialize t2))), t6 = ( Exec (k3,t02));

      (t2 . a) = (( Exec (k2,t1)) . a) by SCMPDS_5: 42

      .= 0 by A6, A7, AMI_3: 10, SCMPDS_2: 50;

      then

       A11: (t02 . a) = 0 by SCMPDS_5: 15;

      then

       A12: ( DataLoc ((t02 . a),5)) = ( intpos ( 0 + 5)) by SCMP_GCD: 1;

      then

       A13: (t6 . a) = 0 by A11, AMI_3: 10, SCMPDS_2: 47;

      (t2 . a4) = (( Exec (k2,t1)) . a4) by SCMPDS_5: 42

      .= (s . a4) by A8, A7, AMI_3: 10, SCMPDS_2: 50;

      then (t02 . a4) = (s . a4) by SCMPDS_5: 15;

      then

       A14: (t6 . a4) = (s . a4) by A12, AMI_3: 10, SCMPDS_2: 47;

      

       A15: (6 + (s . a6)) > (6 + 0 ) by A3, XREAL_1: 6;

      then 0 <> |.((t6 . a4) + ( - 1)).| by A10, A14, ABSVALUE:def 1;

      then

       A16: a <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      ((s . a4) - 1) > 0 by A3, A9, XREAL_1: 19;

      then

       A17: |.((t6 . a4) + ( - 1)).| = ((s . a4) - 1) by A14, ABSVALUE:def 1;

      then 4 <> |.((t6 . a4) + ( - 1)).| by A10, A15, XXREAL_0: 2;

      then

       A18: a4 <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      

       A19: (t5 . a4) = (( Exec (k4,t6)) . a4) by SCMPDS_5: 42

      .= (s . a4) by A14, A18, SCMPDS_2: 47;

      then 0 <> |.((t5 . a4) + 0 ).| by A1, A4, ABSVALUE:def 1;

      then

       A20: a <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      

       A21: (t5 . a) = (( Exec (k4,t6)) . a) by SCMPDS_5: 42

      .= 0 by A13, A16, SCMPDS_2: 47;

      

       A22: (t4 . a) = (( Exec (k5,t5)) . a) by SCMPDS_5: 41

      .= 0 by A21, A20, SCMPDS_2: 47;

      then

       A23: a <> ( DataLoc ((t4 . a),4)) by AMI_3: 10, SCMP_GCD: 1;

      

       A24: (t1 . a1) = (s . a1) by A5, AMI_3: 10, SCMPDS_2: 47;

      (t2 . a1) = (( Exec (k2,t1)) . a1) by SCMPDS_5: 42

      .= (s . a1) by A24, A7, AMI_3: 10, SCMPDS_2: 50;

      then

       A25: (t02 . a1) = (s . a1) by SCMPDS_5: 15;

      then

       A26: (t6 . a1) = (s . a1) by A12, AMI_3: 10, SCMPDS_2: 47;

      

       A27: (t3 . a) = (( Exec (k6,t4)) . a) by SCMPDS_5: 41

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

      then

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

      

       A29: ( DataLoc ((t02 . a),6)) = ( intpos ( 0 + 6)) by A11, SCMP_GCD: 1;

      now

        per cases ;

          suppose (( Initialize t2) . ( DataLoc ((( Initialize t2) . a),5))) <= 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a) = (( IExec (FA,Q2,( Initialize t2))) . a) by SCMPDS_6: 74

          .= (( Exec (Fi,t02)) . a) by SCMPDS_5: 40

          .= 0 by A11, A29, AMI_3: 10, SCMPDS_2: 46;

        end;

          suppose (( Initialize t2) . ( DataLoc ((( Initialize t2) . a),5))) > 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a) = (( IExec (TR,Q2,( Initialize t2))) . a) by SCMPDS_6: 73

          .= (( Exec (k7,t3)) . a) by SCMPDS_5: 41

          .= 0 by A27, A28, AMI_3: 10, SCMPDS_2: 48;

        end;

      end;

      hence (( IExec (B1,P,s)) . a) = 0 by SCMPDS_5: 35;

      

       A30: a1 <> ( DataLoc ((t4 . a),4)) by A22, AMI_3: 10, SCMP_GCD: 1;

       |.((t5 . a4) + 0 ).| = (s . a4) by A1, A4, A19, ABSVALUE:def 1;

      then 1 <> |.((t5 . a4) + 0 ).| by A1, A4, XXREAL_0: 2;

      then

       A31: a1 <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      1 <> |.((t6 . a4) + ( - 1)).| by A10, A15, A17, XXREAL_0: 2;

      then

       A32: a1 <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      

       A33: (t5 . a1) = (( Exec (k4,t6)) . a1) by SCMPDS_5: 42

      .= (s . a1) by A26, A32, SCMPDS_2: 47;

      

       A34: (t4 . a1) = (( Exec (k5,t5)) . a1) by SCMPDS_5: 41

      .= (s . a1) by A33, A31, SCMPDS_2: 47;

      

       A35: (t3 . a1) = (( Exec (k6,t4)) . a1) by SCMPDS_5: 41

      .= (s . a1) by A34, A30, SCMPDS_2: 48;

      now

        per cases ;

          suppose (( Initialize t2) . ( DataLoc ((( Initialize t2) . a),5))) <= 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a1) = (( IExec (FA,Q2,( Initialize t2))) . a1) by SCMPDS_6: 74

          .= (( Exec (Fi,t02)) . a1) by SCMPDS_5: 40

          .= (s . a1) by A25, A29, AMI_3: 10, SCMPDS_2: 46;

        end;

          suppose (( Initialize t2) . ( DataLoc ((( Initialize t2) . a),5))) > 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a1) = (( IExec (TR,Q2,( Initialize t2))) . a1) by SCMPDS_6: 73

          .= (( Exec (k7,t3)) . a1) by SCMPDS_5: 41

          .= (s . a1) by A35, A28, AMI_3: 10, SCMPDS_2: 48;

        end;

      end;

      hence thesis by SCMPDS_5: 35;

    end;

    

     Lm7: for s be 0 -started State of SCMPDS st (s . a4) >= (7 + (s . a6)) & (s . GBP ) = 0 & (s . a6) > 0 holds (( IExec (B1,P,s)) . a2) = (s . a2) & (( IExec (B1,P,s)) . a3) = (s . a3) & (( IExec (B1,P,s)) . a6) < (s . a6) & (( IExec (B1,P,s)) . a4) >= (7 + (( IExec (B1,P,s)) . a6)) & (for i be Nat st i >= 7 & i <> ((s . a4) - 1) & i <> (s . a4) holds (( IExec (B1,P,s)) . ( intpos i)) = (s . ( intpos i))) & ((s . ( DataLoc ((s . a4),( - 1)))) > (s . ( DataLoc ((s . a4), 0 ))) implies (( IExec (B1,P,s)) . ( DataLoc ((s . a4),( - 1)))) = (s . ( DataLoc ((s . a4), 0 ))) & (( IExec (B1,P,s)) . ( DataLoc ((s . a4), 0 ))) = (s . ( DataLoc ((s . a4),( - 1)))) & (( IExec (B1,P,s)) . a6) = ((s . a6) - 1) & (( IExec (B1,P,s)) . a4) = ((s . a4) - 1)) & ((s . ( DataLoc ((s . a4),( - 1)))) <= (s . ( DataLoc ((s . a4), 0 ))) implies (( IExec (B1,P,s)) . ( DataLoc ((s . a4),( - 1)))) = (s . ( DataLoc ((s . a4),( - 1)))) & (( IExec (B1,P,s)) . ( DataLoc ((s . a4), 0 ))) = (s . ( DataLoc ((s . a4), 0 ))) & (( IExec (B1,P,s)) . a6) = 0 )

    proof

      let s be 0 -started State of SCMPDS ;

      set a = GBP , x = ( DataLoc ((s . a4),( - 1))), y = ( DataLoc ((s . a4), 0 ));

      assume that

       A1: (s . a4) >= (7 + (s . a6)) and

       A2: (s . a) = 0 and

       A3: (s . a6) > 0 ;

      set t0 = s, t1 = ( Exec (k1,t0)), t2 = ( IExec ((k1 ';' k2),P,s)), Q2 = P;

      

       A4: (7 + (s . a6)) > (7 + 0 ) by A3, XREAL_1: 6;

      then

       A5: |.(s . a4).| = (s . a4) by A1, ABSVALUE:def 1;

      set Fi = ((a,6) := 0 ), t02 = ( Initialize t2), Q02 = Q2, t3 = ( IExec ((((k3 ';' k4) ';' k5) ';' k6),Q2,( Initialize t2))), t4 = ( IExec (((k3 ';' k4) ';' k5),Q2,( Initialize t2))), t5 = ( IExec ((k3 ';' k4),Q2,( Initialize t2))), t6 = ( Exec (k3,t02));

      

       A6: ( DataLoc ((t0 . a),5)) = ( intpos ( 0 + 5)) by A2, SCMP_GCD: 1;

      then

       A7: (t1 . a) = 0 by A2, AMI_3: 10, SCMPDS_2: 47;

      then

       A8: ( DataLoc ((t1 . a),5)) = ( intpos ( 0 + 5)) by SCMP_GCD: 1;

      then

       A9: |.((t1 . a) + 5).| = ( 0 + 5) by XTUPLE_0: 1;

      then |.((s . a4) + 0 ).| <> |.((t1 . a) + 5).| by A1, A4, A5, XXREAL_0: 2;

      then

       A10: y <> ( DataLoc ((t1 . a),5)) by XTUPLE_0: 1;

      

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

      then |.((s . a4) + 0 ).| <> |.((t0 . a) + 5).| by A1, A4, A5, XXREAL_0: 2;

      then (t0 . y) = (s . y) & y <> ( DataLoc ((t0 . a),5)) by XTUPLE_0: 1;

      then

       A12: (t1 . y) = (s . y) by SCMPDS_2: 47;

      

       A13: (t1 . a5) = (s . x) by A6, SCMPDS_2: 47;

      

       A14: (t1 . a4) = (s . a4) by A6, AMI_3: 10, SCMPDS_2: 47;

      (t2 . y) = (( Exec (k2,t1)) . y) by SCMPDS_5: 42

      .= (s . y) by A12, A10, SCMPDS_2: 50;

      then

       A15: (t02 . y) = (s . y) by SCMPDS_5: 15;

      

       A16: (t02 . a) = (t2 . a) by SCMPDS_5: 15

      .= (( Exec (k2,t1)) . a) by SCMPDS_5: 42

      .= 0 by A7, A8, AMI_3: 10, SCMPDS_2: 50;

      

       A17: ( DataLoc ((t02 . a),5)) = ( intpos ( 0 + 5)) by A16, SCMP_GCD: 1;

      then

       A18: (t6 . a) = 0 by A16, AMI_3: 10, SCMPDS_2: 47;

       |.((t02 . a) + 5).| = ( 0 + 5) by A17, XTUPLE_0: 1;

      then |.((s . a4) + 0 ).| <> |.((t02 . a) + 5).| by A1, A4, A5, XXREAL_0: 2;

      then y <> ( DataLoc ((t02 . a),5)) by XTUPLE_0: 1;

      then

       A19: (t6 . y) = (s . y) by A15, SCMPDS_2: 47;

      (t2 . a4) = (( Exec (k2,t1)) . a4) by SCMPDS_5: 42

      .= (s . a4) by A14, A8, AMI_3: 10, SCMPDS_2: 50;

      then

       A20: (t02 . a4) = (s . a4) by SCMPDS_5: 15;

      then

       A21: (t6 . a4) = (s . a4) by A17, AMI_3: 10, SCMPDS_2: 47;

      

      then

       A22: (t5 . x) = (( Exec (k4,t6)) . ( DataLoc ((t6 . a4),( - 1)))) by SCMPDS_5: 42

      .= (s . y) by A21, A19, SCMPDS_2: 47;

      

       A23: (t1 . a3) = (s . a3) by A6, AMI_3: 10, SCMPDS_2: 47;

      (t2 . a3) = (( Exec (k2,t1)) . a3) by SCMPDS_5: 42

      .= (s . a3) by A23, A8, AMI_3: 10, SCMPDS_2: 50;

      then

       A24: (t02 . a3) = (s . a3) by SCMPDS_5: 15;

      then

       A25: (t6 . a3) = (s . a3) by A17, AMI_3: 10, SCMPDS_2: 47;

      

       A26: (s . a4) >= (1 + (6 + (s . a6))) by A1;

      then

       A27: ((s . a4) - 1) >= (6 + (s . a6)) by XREAL_1: 19;

      

       A28: (t1 . a2) = (s . a2) by A6, AMI_3: 10, SCMPDS_2: 47;

      (t2 . a2) = (( Exec (k2,t1)) . a2) by SCMPDS_5: 42

      .= (s . a2) by A28, A8, AMI_3: 10, SCMPDS_2: 50;

      then

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

      then

       A30: (t6 . a2) = (s . a2) by A17, AMI_3: 10, SCMPDS_2: 47;

      

       A31: (t1 . a6) = (s . a6) by A6, AMI_3: 10, SCMPDS_2: 47;

      (t2 . a6) = (( Exec (k2,t1)) . a6) by SCMPDS_5: 42

      .= (s . a6) by A31, A8, AMI_3: 10, SCMPDS_2: 50;

      then (t02 . a6) = (s . a6) by SCMPDS_5: 15;

      then

       A32: (t6 . a6) = (s . a6) by A17, AMI_3: 10, SCMPDS_2: 47;

      

       A33: ( DataLoc ((t02 . a),6)) = ( intpos ( 0 + 6)) by A16, SCMP_GCD: 1;

       A34:

      now

        assume (t02 . ( DataLoc ((t02 . a),5))) <= 0 ;

        

        then (( IExec (IF,Q2,( Initialize t2))) . a6) = (( IExec (FA,Q2,( Initialize t2))) . a6) by SCMPDS_6: 74

        .= (( Exec (Fi,t02)) . a6) by SCMPDS_5: 40

        .= 0 by A33, SCMPDS_2: 46;

        hence (( IExec (B1,P,s)) . a6) = 0 by SCMPDS_5: 35;

      end;

      

       A35: (6 + (s . a6)) > (6 + 0 ) by A3, XREAL_1: 6;

      then 0 <> |.((t6 . a4) + ( - 1)).| by A27, A21, ABSVALUE:def 1;

      then

       A36: a <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      

       A37: ((s . a4) - 1) > 0 by A3, A26, XREAL_1: 19;

      then

       A38: |.((t6 . a4) + ( - 1)).| = ((s . a4) - 1) by A21, ABSVALUE:def 1;

      then 4 <> |.((t6 . a4) + ( - 1)).| by A27, A35, XXREAL_0: 2;

      then

       A39: a4 <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      

       A40: (t5 . a4) = (( Exec (k4,t6)) . a4) by SCMPDS_5: 42

      .= (s . a4) by A21, A39, SCMPDS_2: 47;

      then

       A41: |.((t5 . a4) + 0 ).| = (s . a4) by A1, A4, ABSVALUE:def 1;

      then 4 <> |.((t5 . a4) + 0 ).| by A1, A4, XXREAL_0: 2;

      then

       A42: a4 <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      3 <> |.((t6 . a4) + ( - 1)).| by A27, A35, A38, XXREAL_0: 2;

      then

       A43: a3 <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      3 <> |.((t5 . a4) + 0 ).| by A1, A4, A41, XXREAL_0: 2;

      then

       A44: a3 <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      

       A45: (t5 . a3) = (( Exec (k4,t6)) . a3) by SCMPDS_5: 42

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

      

       A46: (t4 . a3) = (( Exec (k5,t5)) . a3) by SCMPDS_5: 41

      .= (s . a3) by A45, A44, SCMPDS_2: 47;

      2 <> |.((t5 . a4) + 0 ).| by A1, A4, A41, XXREAL_0: 2;

      then

       A47: a2 <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      

       A48: (t4 . a4) = (( Exec (k5,t5)) . a4) by SCMPDS_5: 41

      .= (s . a4) by A40, A42, SCMPDS_2: 47;

      

       A49: (t5 . a) = (( Exec (k4,t6)) . a) by SCMPDS_5: 42

      .= 0 by A18, A36, SCMPDS_2: 47;

      

       A50: ((2 * |.((s . a4) + ( - 1)).|) + 1) = ((2 * ((s . a4) - 1)) + 1) by A27, A35, ABSVALUE:def 1;

      then |.((s . a4) + ( - 1)).| <> |.((t1 . a) + 5).| by A3, A27, A9, XREAL_1: 6;

      then

       A51: x <> ( DataLoc ((t1 . a),5)) by XTUPLE_0: 1;

       0 <> |.((t5 . a4) + 0 ).| by A1, A4, A40, ABSVALUE:def 1;

      then

       A52: a <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      

       A53: (t4 . a) = (( Exec (k5,t5)) . a) by SCMPDS_5: 41

      .= 0 by A49, A52, SCMPDS_2: 47;

      then

       A54: a <> ( DataLoc ((t4 . a),4)) by AMI_3: 10, SCMP_GCD: 1;

      2 <> |.((t6 . a4) + ( - 1)).| by A27, A35, A38, XXREAL_0: 2;

      then

       A55: a2 <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      

       A56: (t5 . a2) = (( Exec (k4,t6)) . a2) by SCMPDS_5: 42

      .= (s . a2) by A30, A55, SCMPDS_2: 47;

      

       A57: (t4 . a2) = (( Exec (k5,t5)) . a2) by SCMPDS_5: 41

      .= (s . a2) by A56, A47, SCMPDS_2: 47;

      

       A58: a2 <> ( DataLoc ((t4 . a),4)) by A53, AMI_3: 10, SCMP_GCD: 1;

      (t3 . a) = (( Exec (k6,t4)) . a) by SCMPDS_5: 41

      .= 0 by A53, A54, SCMPDS_2: 48;

      then

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

      then

       A60: |.((t3 . a) + 6).| = ( 0 + 6) by XTUPLE_0: 1;

      

       A61: ( DataLoc ((t4 . a),4)) = ( intpos ( 0 + 4)) by A53, SCMP_GCD: 1;

      then

       A62: |.((t4 . a) + 4).| = ( 0 + 4) by XTUPLE_0: 1;

      then |.((s . a4) + ( - 1)).| <> |.((t4 . a) + 4).| by A27, A35, A50, XXREAL_0: 2;

      then

       A63: x <> ( DataLoc ((t4 . a),4)) by XTUPLE_0: 1;

      

       A64: (t3 . a2) = (( Exec (k6,t4)) . a2) by SCMPDS_5: 41

      .= (s . a2) by A57, A58, SCMPDS_2: 48;

      now

        per cases ;

          suppose (t02 . ( DataLoc ((t02 . a),5))) <= 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a2) = (( IExec (FA,Q2,( Initialize t2))) . a2) by SCMPDS_6: 74

          .= (( Exec (Fi,t02)) . a2) by SCMPDS_5: 40

          .= (s . a2) by A29, A33, AMI_3: 10, SCMPDS_2: 46;

        end;

          suppose (t02 . ( DataLoc ((t02 . a),5))) > 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a2) = (( IExec (TR,Q2,( Initialize t2))) . a2) by SCMPDS_6: 73

          .= (( Exec (k7,t3)) . a2) by SCMPDS_5: 41

          .= (s . a2) by A64, A59, AMI_3: 10, SCMPDS_2: 48;

        end;

      end;

      hence (( IExec (B1,P,s)) . a2) = (s . a2) by SCMPDS_5: 35;

      

       A65: a3 <> ( DataLoc ((t4 . a),4)) by A53, AMI_3: 10, SCMP_GCD: 1;

      

       A66: (t3 . a3) = (( Exec (k6,t4)) . a3) by SCMPDS_5: 41

      .= (s . a3) by A46, A65, SCMPDS_2: 48;

      now

        per cases ;

          suppose (t02 . ( DataLoc ((t02 . a),5))) <= 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a3) = (( IExec (FA,Q2,( Initialize t2))) . a3) by SCMPDS_6: 74

          .= (( Exec (Fi,t02)) . a3) by SCMPDS_5: 40

          .= (s . a3) by A24, A33, AMI_3: 10, SCMPDS_2: 46;

        end;

          suppose (t02 . ( DataLoc ((t02 . a),5))) > 0 ;

          

          hence (( IExec (IF,Q2,( Initialize t2))) . a3) = (( IExec (TR,Q2,( Initialize t2))) . a3) by SCMPDS_6: 73

          .= (( Exec (k7,t3)) . a3) by SCMPDS_5: 41

          .= (s . a3) by A66, A59, AMI_3: 10, SCMPDS_2: 48;

        end;

      end;

      hence (( IExec (B1,P,s)) . a3) = (s . a3) by SCMPDS_5: 35;

      

       A67: a6 <> ( DataLoc ((t4 . a),4)) by A53, AMI_3: 10, SCMP_GCD: 1;

      6 <> |.((t6 . a4) + ( - 1)).| by A26, A35, A38, XREAL_1: 19;

      then

       A68: a6 <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      

       A69: (t5 . a6) = (( Exec (k4,t6)) . a6) by SCMPDS_5: 42

      .= (s . a6) by A32, A68, SCMPDS_2: 47;

      6 <> |.((t5 . a4) + 0 ).| by A1, A4, A41, XXREAL_0: 2;

      then

       A70: a6 <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      

       A71: (t4 . a6) = (( Exec (k5,t5)) . a6) by SCMPDS_5: 41

      .= (s . a6) by A69, A70, SCMPDS_2: 47;

      

       A72: (t3 . a6) = (( Exec (k6,t4)) . a6) by SCMPDS_5: 41

      .= (s . a6) by A71, A67, SCMPDS_2: 48;

      

       A73: (t3 . a4) = (( Exec (k6,t4)) . a4) by SCMPDS_5: 41

      .= ((t4 . a4) + ( - 1)) by A61, SCMPDS_2: 48

      .= ((s . a4) - 1) by A48;

       A74:

      now

        assume

         A75: (t02 . ( DataLoc ((t02 . a),5))) > 0 ;

        

        then (( IExec (IF,Q2,( Initialize t2))) . a6) = (( IExec (TR,Q2,( Initialize t2))) . a6) by SCMPDS_6: 73

        .= (( Exec (k7,t3)) . a6) by SCMPDS_5: 41

        .= ((s . a6) + ( - 1)) by A72, A59, SCMPDS_2: 48

        .= ((s . a6) - 1);

        hence (( IExec (B1,P,s)) . a6) = ((s . a6) - 1) by SCMPDS_5: 35;

        (( IExec (IF,Q2,( Initialize t2))) . a4) = (( IExec (TR,Q2,( Initialize t2))) . a4) by A75, SCMPDS_6: 73

        .= (( Exec (k7,t3)) . a4) by SCMPDS_5: 41

        .= ((s . a4) - 1) by A73, A59, AMI_3: 10, SCMPDS_2: 48;

        hence (( IExec (B1,P,s)) . a4) = ((s . a4) - 1) by SCMPDS_5: 35;

      end;

      hereby

        per cases ;

          suppose (t02 . ( DataLoc ((t02 . a),5))) <= 0 ;

          hence (( IExec (B1,P,s)) . a6) < (s . a6) by A3, A34;

        end;

          suppose (t02 . ( DataLoc ((t02 . a),5))) > 0 ;

          hence (( IExec (B1,P,s)) . a6) < (s . a6) by A74, XREAL_1: 146;

        end;

      end;

      hereby

        per cases ;

          suppose

           A76: (t02 . ( DataLoc ((t02 . GBP ),5))) <= 0 ;

          

          then (( IExec (IF,Q2,( Initialize t2))) . a4) = (( IExec (FA,Q2,( Initialize t2))) . a4) by SCMPDS_6: 74

          .= (( Exec (Fi,t02)) . a4) by SCMPDS_5: 40

          .= (s . a4) by A20, A33, AMI_3: 10, SCMPDS_2: 46;

          then (( IExec (B1,P,s)) . a4) = (s . a4) by SCMPDS_5: 35;

          hence (( IExec (B1,P,s)) . a4) >= (7 + (( IExec (B1,P,s)) . a6)) by A1, A4, A34, A76, XXREAL_0: 2;

        end;

          suppose

           A77: (t02 . ( DataLoc ((t02 . a),5))) > 0 ;

          ((s . a4) - 1) >= ((7 + (s . a6)) - 1) by A1, XREAL_1: 9;

          hence (( IExec (B1,P,s)) . a4) >= (7 + (( IExec (B1,P,s)) . a6)) by A74, A77;

        end;

      end;

       A78:

      now

        let i be Nat;

        assume that

         A79: i >= 7 and i <> ((s . a4) - 1) and i <> (s . a4);

        i > 5 by A79, XXREAL_0: 2;

        hence (t1 . ( intpos i)) = (s . ( intpos i)) by A6, AMI_3: 10, SCMPDS_2: 47;

      end;

       A80:

      now

        let i be Nat;

        assume that

         A81: i >= 7 and

         A82: i <> ((s . a4) - 1) & i <> (s . a4);

        

         A83: i > 5 by A81, XXREAL_0: 2;

        

        thus (t2 . ( intpos i)) = (( Exec (k2,t1)) . ( intpos i)) by SCMPDS_5: 42

        .= (t1 . ( intpos i)) by A8, A83, AMI_3: 10, SCMPDS_2: 50

        .= (s . ( intpos i)) by A78, A81, A82;

      end;

       A84:

      now

        let i be Nat;

        assume that

         A85: i >= 7 and

         A86: i <> ((s . a4) - 1) & i <> (s . a4);

        i > 5 by A85, XXREAL_0: 2;

        

        hence (t6 . ( intpos i)) = (t02 . ( intpos i)) by A17, AMI_3: 10, SCMPDS_2: 47

        .= (t2 . ( intpos i)) by SCMPDS_5: 15

        .= (s . ( intpos i)) by A80, A85, A86;

      end;

       A87:

      now

        let i be Nat;

        assume that

         A88: i >= 7 and

         A89: i <> ((s . a4) - 1) and

         A90: i <> (s . a4);

        

         A91: ( intpos i) <> ( DataLoc ((t6 . a4),( - 1)))

        proof

          assume ( intpos i) = ( DataLoc ((t6 . a4),( - 1)));

          then i = |.((t6 . a4) + ( - 1)).| by XTUPLE_0: 1;

          hence contradiction by A37, A21, A89, ABSVALUE:def 1;

        end;

        

        thus (t5 . ( intpos i)) = (( Exec (k4,t6)) . ( intpos i)) by SCMPDS_5: 42

        .= (t6 . ( intpos i)) by A91, SCMPDS_2: 47

        .= (s . ( intpos i)) by A84, A88, A89, A90;

      end;

       A92:

      now

        let i be Nat;

        assume that

         A93: i >= 7 & i <> ((s . a4) - 1) and

         A94: i <> (s . a4);

        

         A95: ( intpos i) <> ( DataLoc ((t5 . a4), 0 ))

        proof

          assume ( intpos i) = ( DataLoc ((t5 . a4), 0 ));

          then i = |.((t5 . a4) + 0 ).| by XTUPLE_0: 1;

          hence contradiction by A1, A4, A40, A94, ABSVALUE:def 1;

        end;

        

        thus (t4 . ( intpos i)) = (( Exec (k5,t5)) . ( intpos i)) by SCMPDS_5: 41

        .= (t5 . ( intpos i)) by A95, SCMPDS_2: 47

        .= (s . ( intpos i)) by A87, A93, A94;

      end;

       A96:

      now

        let i be Nat;

        assume that

         A97: i >= 7 and

         A98: i <> ((s . a4) - 1) & i <> (s . a4);

        i > 4 by A97, XXREAL_0: 2;

        then

         A99: ( intpos i) <> ( DataLoc ((t4 . a),4)) by A53, AMI_3: 10, SCMP_GCD: 1;

        

        thus (t3 . ( intpos i)) = (( Exec (k6,t4)) . ( intpos i)) by SCMPDS_5: 41

        .= (t4 . ( intpos i)) by A99, SCMPDS_2: 48

        .= (s . ( intpos i)) by A92, A97, A98;

      end;

      hereby

        let i be Nat;

        set xi = ( intpos i);

        assume that

         A100: i >= 7 and

         A101: i <> ((s . a4) - 1) & i <> (s . a4);

        

         A102: i > 6 by A100, XXREAL_0: 2;

        per cases ;

          suppose (t02 . ( DataLoc ((t02 . a),5))) <= 0 ;

          

          then (( IExec (IF,Q2,( Initialize t2))) . xi) = (( IExec (FA,Q2,( Initialize t2))) . xi) by SCMPDS_6: 74

          .= (( Exec (Fi,t02)) . xi) by SCMPDS_5: 40

          .= (t02 . xi) by A33, A102, AMI_3: 10, SCMPDS_2: 46

          .= (t2 . xi) by SCMPDS_5: 15

          .= (s . xi) by A80, A100, A101;

          hence (( IExec (B1,P,s)) . xi) = (s . xi) by SCMPDS_5: 35;

        end;

          suppose (t02 . ( DataLoc ((t02 . a),5))) > 0 ;

          

          then (( IExec (IF,Q2,( Initialize t2))) . xi) = (( IExec (TR,Q2,( Initialize t2))) . xi) by SCMPDS_6: 73

          .= (( Exec (k7,t3)) . xi) by SCMPDS_5: 41

          .= (t3 . xi) by A59, A102, AMI_3: 10, SCMPDS_2: 48

          .= (s . xi) by A96, A100, A101;

          hence (( IExec (B1,P,s)) . xi) = (s . xi) by SCMPDS_5: 35;

        end;

      end;

      

       A103: (t02 . a5) = (t2 . a5) by SCMPDS_5: 15

      .= (( Exec (k2,t1)) . a5) by SCMPDS_5: 42

      .= ((s . x) - (s . y)) by A14, A13, A12, A8, SCMPDS_2: 50;

      then

       A104: (t02 . ( DataLoc ((t02 . a),5))) = ((s . x) - (s . y)) by A16, SCMP_GCD: 1;

       |.((s . a4) + ( - 1)).| <> |.((t0 . a) + 5).| by A3, A27, A50, A11, XREAL_1: 6;

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

      then

       A105: (t1 . x) = (s . x) by SCMPDS_2: 47;

      (t2 . x) = (( Exec (k2,t1)) . x) by SCMPDS_5: 42

      .= (s . x) by A105, A51, SCMPDS_2: 50;

      then

       A106: (t02 . x) = (s . x) by SCMPDS_5: 15;

      then

       A107: (t6 . a5) = (s . x) by A20, A17, SCMPDS_2: 47;

      5 <> |.((t6 . a4) + ( - 1)).| by A27, A35, A38, XXREAL_0: 2;

      then

       A108: a5 <> ( DataLoc ((t6 . a4),( - 1))) by XTUPLE_0: 1;

      

       A109: (t5 . a5) = (( Exec (k4,t6)) . a5) by SCMPDS_5: 42

      .= (s . x) by A107, A108, SCMPDS_2: 47;

       |.((s . a4) + 0 ).| <> |.((t4 . a) + 4).| by A1, A4, A5, A62, XXREAL_0: 2;

      then

       A110: y <> ( DataLoc ((t4 . a),4)) by XTUPLE_0: 1;

      

       A111: (t4 . y) = (( Exec (k5,t5)) . ( DataLoc ((t5 . a4), 0 ))) by A40, SCMPDS_5: 41

      .= (t5 . ( DataLoc ((t5 . a),5))) by SCMPDS_2: 47

      .= (s . x) by A49, A109, SCMP_GCD: 1;

      

       A112: (t3 . y) = (( Exec (k6,t4)) . y) by SCMPDS_5: 41

      .= (s . x) by A111, A110, SCMPDS_2: 48;

       |.((s . a4) + ( - 1)).| <> |.((t5 . a4) + 0 ).| by A50, A41;

      then

       A113: x <> ( DataLoc ((t5 . a4), 0 )) by XTUPLE_0: 1;

      

       A114: (t4 . x) = (( Exec (k5,t5)) . x) by SCMPDS_5: 41

      .= (s . y) by A22, A113, SCMPDS_2: 47;

      

       A115: (t3 . x) = (( Exec (k6,t4)) . x) by SCMPDS_5: 41

      .= (s . y) by A114, A63, SCMPDS_2: 48;

      hereby

        

         A116: x <> ( DataLoc ((t3 . a),6)) by A27, A35, A50, A59, XTUPLE_0: 1;

        assume (s . x) > (s . y);

        then

         A117: ((s . x) - (s . y)) > ((s . y) - (s . y)) by XREAL_1: 9;

        

        then (( IExec (IF,Q2,( Initialize t2))) . x) = (( IExec (TR,Q2,( Initialize t2))) . x) by A104, SCMPDS_6: 73

        .= (( Exec (k7,t3)) . x) by SCMPDS_5: 41

        .= (s . y) by A115, A116, SCMPDS_2: 48;

        hence (( IExec (B1,P,s)) . x) = (s . y) by SCMPDS_5: 35;

         |.((s . a4) + 0 ).| <> |.((t3 . a) + 6).| by A1, A4, A5, A60, XXREAL_0: 2;

        then

         A118: y <> ( DataLoc ((t3 . a),6)) by XTUPLE_0: 1;

        (( IExec (IF,Q2,( Initialize t2))) . y) = (( IExec (TR,Q2,( Initialize t2))) . y) by A104, A117, SCMPDS_6: 73

        .= (( Exec (k7,t3)) . y) by SCMPDS_5: 41

        .= (s . x) by A112, A118, SCMPDS_2: 48;

        hence (( IExec (B1,P,s)) . y) = (s . x) by SCMPDS_5: 35;

        thus (( IExec (B1,P,s)) . a6) = ((s . a6) - 1) & (( IExec (B1,P,s)) . a4) = ((s . a4) - 1) by A16, A103, A74, A117, SCMP_GCD: 1;

      end;

      

       A119: |.((t02 . a) + 6).| = ( 0 + 6) by A33, XTUPLE_0: 1;

      hereby

        

         A120: x <> ( DataLoc ((t02 . a),6)) by A27, A35, A50, A33, XTUPLE_0: 1;

        assume (s . x) <= (s . y);

        then

         A121: ((s . x) - (s . y)) <= ((s . y) - (s . y)) by XREAL_1: 9;

        

        then (( IExec (IF,Q2,( Initialize t2))) . x) = (( IExec (FA,Q2,( Initialize t2))) . x) by A104, SCMPDS_6: 74

        .= (( Exec (Fi,t02)) . x) by SCMPDS_5: 40

        .= (s . x) by A106, A120, SCMPDS_2: 46;

        hence (( IExec (B1,P,s)) . x) = (s . x) by SCMPDS_5: 35;

         |.((s . a4) + 0 ).| <> |.((t02 . a) + 6).| by A1, A4, A5, A119, XXREAL_0: 2;

        then

         A122: y <> ( DataLoc ((t02 . a),6)) by XTUPLE_0: 1;

        (( IExec (IF,Q2,( Initialize t2))) . y) = (( IExec (FA,Q2,( Initialize t2))) . y) by A104, A121, SCMPDS_6: 74

        .= (( Exec (Fi,t02)) . y) by SCMPDS_5: 40

        .= (s . y) by A15, A122, SCMPDS_2: 46;

        hence (( IExec (B1,P,s)) . y) = (s . y) by SCMPDS_5: 35;

        thus (( IExec (B1,P,s)) . a6) = 0 by A16, A103, A34, A121, SCMP_GCD: 1;

      end;

    end;

    

     Lm8: for s be 0 -started State of SCMPDS st (s . a4) >= (7 + (s . ( DataLoc ((s . GBP ),6)))) & (s . GBP ) = 0 holds WH is_closed_on (s,P) & WH is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS ;

      set a = GBP , b = ( DataLoc ((s . a),6));

      assume that

       A1: (s . a4) >= (7 + (s . b)) and

       A2: (s . a) = 0 ;

      

       A3: b = ( intpos ( 0 + 6)) by A2, SCMP_GCD: 1;

       A4:

      now

        let t be 0 -started State of SCMPDS ;

        let Q;

        assume that

         A5: for x st x in {a4} holds (t . x) >= (7 + (t . b)) and

         A6: (t . a) = (s . a) & (t . b) > 0 ;

        set Bt = ( IExec (B1,Q,t));

        

         A7: a4 in {a4} by TARSKI:def 1;

        then

         A8: (t . a4) >= (7 + (t . a6)) by A3, A5;

        hence (( IExec (B1,Q,t)) . a) = (t . a) by A2, A3, A6, Lm6;

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

        thus (( IExec (B1,Q,t)) . b) < (t . b) by A2, A3, A6, A8, Lm7;

        (t . a4) >= (7 + (t . b)) by A5, A7;

        then (Bt . a4) >= (7 + (Bt . a6)) by A2, A3, A6, Lm7;

        hence for x st x in {a4} holds (( IExec (B1,Q,t)) . x) >= (7 + (( IExec (B1,Q,t)) . b)) by A3, TARSKI:def 1;

      end;

      for x st x in {a4} holds (s . x) >= (7 + (s . b)) by A1, TARSKI:def 1;

      hence thesis by A4, SCMPDS_8: 29;

    end;

    

     Lm9: for s be 0 -started State of SCMPDS st (s . a4) >= (7 + (s . ( DataLoc ((s . GBP ),6)))) & (s . GBP ) = 0 holds (( IExec (WH,P,s)) . GBP ) = 0 & (( IExec (WH,P,s)) . a1) = (s . a1) & (( IExec (WH,P,s)) . a2) = (s . a2) & (( IExec (WH,P,s)) . a3) = (s . a3)

    proof

      let s be 0 -started State of SCMPDS ;

      set b = ( DataLoc ((s . GBP ),6)), a = GBP ;

      assume that

       A1: (s . a4) >= (7 + (s . b)) and

       A2: (s . a) = 0 ;

      

       A3: b = ( intpos ( 0 + 6)) by A2, SCMP_GCD: 1;

      defpred P[ Nat] means for t be 0 -started State of SCMPDS , Q st (t . a6) <= $1 & (t . a4) >= (7 + (t . a6)) & (t . a) = 0 holds (( IExec (WH,Q,t)) . a) = 0 & (( IExec (WH,Q,t)) . a1) = (t . a1) & (( IExec (WH,Q,t)) . a2) = (t . a2) & (( IExec (WH,Q,t)) . a3) = (t . a3);

      

       A4: P[ 0 qua Nat]

      proof

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

        assume that

         A5: (t . a6) <= 0 and (t . a4) >= (7 + (t . a6)) and

         A6: (t . a) = 0 ;

        

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

        hence (( IExec (WH,Q,t)) . a) = 0 by A5, A6, SCMPDS_8: 23;

        thus thesis by A5, A7, SCMPDS_8: 23;

      end;

      

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

      proof

        let k be Nat;

        assume

         A9: P[k];

        thus P[(k + 1)]

        proof

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

          set bt = ( DataLoc ((t . a),6));

          assume that

           A10: (t . a6) <= (k + 1) and

           A11: (t . a4) >= (7 + (t . a6)) and

           A12: (t . a) = 0 ;

          

           A13: bt = ( intpos ( 0 + 6)) by A12, SCMP_GCD: 1;

          per cases ;

            suppose (t . bt) <= 0 ;

            hence thesis by A12, SCMPDS_8: 23;

          end;

            suppose

             A14: (t . bt) > 0 ;

            

             A15: (for v be 0 -started State of SCMPDS , Q st (for x st x in {a4} holds (v . x) >= (7 + (v . ( DataLoc ((t . GBP ),6))))) & (v . GBP ) = (t . GBP ) & (v . ( DataLoc ((t . GBP ),6))) > 0 holds (( IExec (B1,Q,v)) . GBP ) = (v . GBP ) & B1 is_closed_on (v,Q) & B1 is_halting_on (v,Q) & (( IExec (B1,Q,v)) . ( DataLoc ((t . GBP ),6))) < (v . ( DataLoc ((t . GBP ),6))) & for x st x in {a4} holds (( IExec (B1,Q,v)) . x) >= (7 + (( IExec (B1,Q,v)) . ( DataLoc ((t . GBP ),6)))))

            proof

              let v be 0 -started State of SCMPDS ;

              let V;

              

               A16: ( Initialize v) = v by MEMSTR_0: 44;

              assume that

               A17: for x st x in {a4} holds (v . x) >= (7 + (v . bt)) and

               A18: (v . a) = (t . a) & (v . bt) > 0 ;

              set Iv = ( IExec (B1,V,( Initialize ( Initialize v))));

              

               A19: (v . a) = (( Initialize v) . a) by SCMPDS_5: 15;

              

               A20: (v . a4) = (( Initialize v) . a4) by SCMPDS_5: 15;

              

               A21: (v . a6) = (( Initialize v) . a6) by SCMPDS_5: 15;

              

               A22: a4 in {a4} by TARSKI:def 1;

              then

               A23: (v . a4) >= (7 + (v . a6)) by A13, A17;

              hence (( IExec (B1,V,v)) . a) = (v . a) by A12, A13, A18, Lm6;

              thus B1 is_closed_on (v,V) & B1 is_halting_on (v,V) by SCMPDS_6: 20, SCMPDS_6: 21;

              thus (( IExec (B1,V,v)) . bt) < (v . bt) by A12, A13, A18, A23, Lm7;

              (v . a4) >= (7 + (v . bt)) by A17, A22;

              then (Iv . a4) >= (7 + (Iv . a6)) by A12, A13, A18, Lm7, A19, A20, A21;

              hence for x st x in {a4} holds (( IExec (B1,V,v)) . x) >= (7 + (( IExec (B1,V,v)) . bt)) by A13, A16, TARSKI:def 1;

            end;

            set It = ( IExec (B1,Q,t)), IT = Q;

            

             A24: (It . a1) = (( Initialize It) . a1) by SCMPDS_5: 15;

            

             A25: (It . a6) = (( Initialize It) . a6) by SCMPDS_5: 15;

            

             A26: (It . a4) = (( Initialize It) . a4) by SCMPDS_5: 15;

            

             A27: (It . GBP ) = (( Initialize It) . GBP ) by SCMPDS_5: 15;

            

             A28: (It . a2) = (( Initialize It) . a2) by SCMPDS_5: 15;

            

             A29: (It . a3) = (( Initialize It) . a3) by SCMPDS_5: 15;

            (It . a6) < (t . a6) by A11, A12, A13, A14, Lm7;

            then ((It . a6) + 1) <= (t . a6) by INT_1: 7;

            then ((It . a6) + 1) <= (k + 1) by A10, XXREAL_0: 2;

            then

             A30: (It . a6) <= k by XREAL_1: 6;

            

             A31: (It . GBP ) = 0 & (It . a4) >= (7 + (It . a6)) by A11, A12, A13, A14, Lm6, Lm7;

            then

             A32: (( IExec (WH,IT,( Initialize It))) . a1) = (It . a1) by A9, A30, A24, A25, A26, A27;

            

             A33: (( IExec (WH,IT,( Initialize It))) . a3) = (It . a3) by A9, A31, A30, A25, A26, A27, A29;

            

             A34: (( IExec (WH,IT,( Initialize It))) . a2) = (It . a2) by A9, A31, A30, A25, A26, A27, A28;

            

             A35: for x st x in {a4} holds (t . x) >= (7 + (t . bt)) by A11, A13, TARSKI:def 1;

            (( IExec (WH,IT,( Initialize It))) . a) = 0 by A9, A31, A30, A25, A26, A27;

            hence (( IExec (WH,Q,t)) . a) = 0 by A14, A35, A15, SCMPDS_8: 29;

            (It . a1) = (t . a1) by A11, A12, A13, A14, Lm6;

            hence (( IExec (WH,Q,t)) . a1) = (t . a1) by A14, A35, A15, A32, SCMPDS_8: 29;

            (It . a2) = (t . a2) by A11, A12, A13, A14, Lm7;

            hence (( IExec (WH,Q,t)) . a2) = (t . a2) by A14, A35, A15, A34, SCMPDS_8: 29;

            (It . a3) = (t . a3) by A11, A12, A13, A14, Lm7;

            hence thesis by A14, A35, A15, A33, SCMPDS_8: 29;

          end;

        end;

      end;

      per cases ;

        suppose (s . a6) <= 0 ;

        hence thesis by A2, A3, SCMPDS_8: 23;

      end;

        suppose (s . a6) > 0 ;

        then

        reconsider m = (s . a6) as Element of NAT by INT_1: 3;

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

        then P[m];

        hence thesis by A1, A2, A3;

      end;

    end;

    

     Lm10: for s be 0 -started State of SCMPDS st (s . GBP ) = 0 holds (( IExec (J4,P,s)) . GBP ) = 0 & (( IExec (J4,P,s)) . a1) = ((s . a1) + 1) & (( IExec (J4,P,s)) . a2) = (s . a2) & (( IExec (J4,P,s)) . a3) = ((s . a3) + 1) & (( IExec (J4,P,s)) . a4) = ((s . a3) + 1) & (( IExec (J4,P,s)) . a6) = ((s . a1) + 1) & for i be Nat st i >= 7 holds (( IExec (J4,P,s)) . ( intpos i)) = (s . ( intpos i))

    proof

      set a = GBP ;

      let s be 0 -started State of SCMPDS ;

      

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

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

      assume

       A2: (s . a) = 0 ;

      then

       A3: (t0 . a) = 0 by SCMPDS_5: 15;

      then

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

      then

       A5: (t4 . a) = 0 by A3, A2, AMI_3: 10, SCMPDS_2: 48;

      then

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

      

       A7: (t4 . a2) = (s . a2) by A4, A2, A3, AMI_3: 10, SCMPDS_2: 48;

      

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

      .= (s . a2) by A7, A6, AMI_3: 10, SCMPDS_2: 47;

      

       A9: (t4 . a1) = (s . a1) by A4, A2, A3, AMI_3: 10, SCMPDS_2: 48;

      

       A10: (t3 . a1) = (( Exec (j2,t4)) . a1) by SCMPDS_5: 42

      .= (s . a1) by A9, A6, AMI_3: 10, SCMPDS_2: 47;

      

       A11: (t4 . a3) = ((s . a3) + 1) by A4, A1, SCMPDS_2: 48;

      

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

      .= 0 by A5, A6, AMI_3: 10, SCMPDS_2: 47;

      then

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

      

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

      

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

      .= ((s . a3) + 1) by A11, A6, A14, SCMPDS_2: 47;

      

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

      .= ((s . a3) + 1) by A15, A13, AMI_3: 10, SCMPDS_2: 48;

      

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

      .= (s . a2) by A8, A13, AMI_3: 10, SCMPDS_2: 48;

      

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

      .= ((s . a1) + 1) by A10, A13, SCMPDS_2: 48;

      

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

      .= ((s . a3) + 1) by A11, A6, AMI_3: 10, SCMPDS_2: 47;

      

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

      .= ((s . a3) + 1) by A19, A13, AMI_3: 10, SCMPDS_2: 48;

      

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

      .= 0 by A12, A13, AMI_3: 10, SCMPDS_2: 48;

      then

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

      

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

      .= 0 by A21, A22, AMI_3: 10, SCMPDS_2: 47;

      

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

      .= ((s . a1) + 1) by A18, A22, AMI_3: 10, SCMPDS_2: 47;

      

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

      .= (s . a2) by A17, A22, AMI_3: 10, SCMPDS_2: 47;

      

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

      

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

      .= ((s . a3) + 1) by A20, A22, AMI_3: 10, SCMPDS_2: 47;

      

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

      .= ((s . a3) + 1) by A16, A22, AMI_3: 10, SCMPDS_2: 47;

      

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

      .= ((s . a1) + 1) by A18, A22, A23, SCMPDS_2: 47;

       A24:

      now

        let i be Nat;

        assume i >= 7;

        then i > 3 by XXREAL_0: 2;

        

        hence (t4 . ( intpos i)) = (t0 . ( intpos i)) by A4, A1, AMI_3: 10, SCMPDS_2: 48

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

      end;

       A25:

      now

        let i be Nat;

        assume

         A26: i >= 7;

        then

         A27: i > 4 by XXREAL_0: 2;

        

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

        .= (t4 . ( intpos i)) by A6, A27, AMI_3: 10, SCMPDS_2: 47

        .= (s . ( intpos i)) by A24, A26;

      end;

       A28:

      now

        let i be Nat;

        assume

         A29: i >= 7;

        then

         A30: i > 1 by XXREAL_0: 2;

        

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

        .= (t3 . ( intpos i)) by A13, A30, AMI_3: 10, SCMPDS_2: 48

        .= (s . ( intpos i)) by A25, A29;

      end;

      hereby

        let i be Nat;

        assume

         A31: i >= 7;

        then

         A32: i > 6 by XXREAL_0: 2;

        

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

        .= (t2 . ( intpos i)) by A22, A32, AMI_3: 10, SCMPDS_2: 47

        .= (s . ( intpos i)) by A28, A31;

      end;

    end;

    set jf = ( AddTo ( GBP ,2,( - 1))), B3 = (B2 ';' jf);

    

     Lm11: for s be 0 -started State of SCMPDS st (s . a3) >= ((s . a1) + 7) & (s . GBP ) = 0 holds (( IExec (B3,P,s)) . GBP ) = 0 & (( IExec (B3,P,s)) . a2) = ((s . a2) - 1) & (( IExec (B3,P,s)) . a3) = ((s . a3) + 1) & (( IExec (B3,P,s)) . a1) = ((s . a1) + 1) & for i be Nat st i <> 2 holds (( IExec (B3,P,s)) . ( intpos i)) = (( IExec (WH,P,( Initialize ( IExec (J4,P,s))))) . ( intpos i))

    proof

      set a = GBP ;

      let s be 0 -started State of SCMPDS ;

      set s1 = ( IExec (J4,P,s)), Bt = ( IExec (B2,P,s)), P1 = P;

      

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

      

       A2: (s1 . a) = (( Initialize s1) . a) by SCMPDS_5: 15;

      

       A3: (s1 . a4) = (( Initialize s1) . a4) by SCMPDS_5: 15;

      

       A4: (s1 . a6) = (( Initialize s1) . a6) by SCMPDS_5: 15;

      

       A5: (s1 . a3) = (( Initialize s1) . a3) by SCMPDS_5: 15;

      

       A6: (s1 . a1) = (( Initialize s1) . a1) by SCMPDS_5: 15;

      

       A7: (s1 . a2) = (( Initialize s1) . a2) by SCMPDS_5: 15;

      assume that

       A8: (s . a3) >= ((s . a1) + 7) and

       A9: (s . a) = 0 ;

      

       A10: (s1 . a1) = ((s . a1) + 1) by A9, Lm10;

      

       A11: (s1 . a3) = ((s . a3) + 1) by A9, Lm10;

      

       A12: (s1 . a2) = (s . a2) by A9, Lm10;

      (s1 . a6) = ((s . a1) + 1) & ((s . a3) + 1) >= ((7 + (s . a1)) + 1) by A8, A9, Lm10, XREAL_1: 6;

      then

       A13: (s1 . a4) >= (7 + (s1 . a6)) by A9, Lm10;

      

       A14: (s1 . GBP ) = 0 by A9, Lm10;

      then

       A15: ( DataLoc ((s1 . a),6)) = ( intpos ( 0 + 6)) by SCMP_GCD: 1;

      then WH is_closed_on (( Initialize s1),P1) & WH is_halting_on (( Initialize s1),P1) by A14, A13, Lm8, A2, A3, A4;

      then

       A16: WH is_closed_on (s1,P1) & WH is_halting_on (s1,P1) by SCMPDS_6: 125, SCMPDS_6: 126;

      

       A17: J4 is_closed_on (s,P) & J4 is_halting_on (s,P) by SCMPDS_6: 20, SCMPDS_6: 21;

      

      then

       A18: (Bt . a) = (( IExec (WH,P1,( Initialize s1))) . a) by A16, SCMPDS_7: 30

      .= 0 by A14, A15, A13, Lm9, A2, A3, A4;

      then

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

      

       A20: B2 is_closed_on (s,P) & B2 is_halting_on (s,P) by A16, A17, A1, SCMPDS_7: 24;

      

      hence (( IExec (B3,P,s)) . a) = (( Exec (jf,Bt)) . a) by SCMPDS_7: 31

      .= 0 by A18, A19, AMI_3: 10, SCMPDS_2: 48;

      

      thus (( IExec (B3,P,s)) . a2) = (( Exec (jf,Bt)) . a2) by A20, SCMPDS_7: 31

      .= ((Bt . a2) + ( - 1)) by A19, SCMPDS_2: 48

      .= ((Bt . a2) - 1)

      .= ((( IExec (WH,P1,( Initialize s1))) . a2) - 1) by A16, A17, SCMPDS_7: 30

      .= ((s . a2) - 1) by A14, A12, A15, A13, Lm9, A2, A3, A4, A7;

      

      thus (( IExec (B3,P,s)) . a3) = (( Exec (jf,Bt)) . a3) by A20, SCMPDS_7: 31

      .= (Bt . a3) by A19, AMI_3: 10, SCMPDS_2: 48

      .= (( IExec (WH,P1,( Initialize s1))) . a3) by A16, A17, SCMPDS_7: 30

      .= ((s . a3) + 1) by A14, A11, A15, A13, Lm9, A2, A3, A4, A5;

      

      thus (( IExec (B3,P,s)) . a1) = (( Exec (jf,Bt)) . a1) by A20, SCMPDS_7: 31

      .= (Bt . a1) by A19, AMI_3: 10, SCMPDS_2: 48

      .= (( IExec (WH,P1,( Initialize s1))) . a1) by A16, A17, SCMPDS_7: 30

      .= ((s . a1) + 1) by A14, A10, A15, A13, Lm9, A2, A3, A4, A6;

      hereby

        let i be Nat;

        assume

         A21: i <> 2;

        

        thus (( IExec (B3,P,s)) . ( intpos i)) = (( Exec (jf,Bt)) . ( intpos i)) by A20, SCMPDS_7: 31

        .= (Bt . ( intpos i)) by A19, A21, AMI_3: 10, SCMPDS_2: 48

        .= (( IExec (WH,P1,( Initialize s1))) . ( intpos i)) by A16, A17, SCMPDS_7: 30;

      end;

    end;

    

     Lm12: for s be 0 -started State of SCMPDS st (s . a3) >= ((s . a1) + 7) & (s . GBP ) = 0 holds FR is_closed_on (s,P) & FR is_halting_on (s,P)

    proof

      let s be 0 -started State of SCMPDS ;

      set a = GBP , b = ( DataLoc ((s . a),2));

      assume that

       A1: (s . a3) >= ((s . a1) + 7) and

       A2: (s . a) = 0 ;

      

       A3: b = ( intpos ( 0 + 2)) by A2, SCMP_GCD: 1;

      now

        let t be 0 -started State of SCMPDS ;

        let Q;

        

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

        assume that

         A5: (t . a3) >= ((t . a1) + 7) and

         A6: (t . a) = (s . a) and (t . b) > 0 ;

        set t1 = ( IExec (J4,Q,t)), Q1 = Q;

        

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

        

         A8: (t1 . a4) = (( Initialize t1) . a4) by SCMPDS_5: 15;

        

         A9: (t1 . a6) = (( Initialize t1) . a6) by SCMPDS_5: 15;

        

         A10: ((t . a3) + 1) >= ((7 + (t . a1)) + 1) by A5, XREAL_1: 6;

        thus (( IExec (B3,Q,t)) . a) = (t . a) by A2, A5, A6, Lm11;

        thus (( IExec (B3,Q,t)) . b) = ((t . b) - 1) by A2, A3, A5, A6, Lm11;

        

         A11: J4 is_closed_on (t,Q) & J4 is_halting_on (t,Q) by SCMPDS_6: 20, SCMPDS_6: 21;

        (t1 . a6) = ((t . a1) + 1) by A2, A6, Lm10;

        then

         A12: (t1 . a4) >= (7 + (t1 . a6)) by A2, A6, A10, Lm10;

        

         A13: (t1 . a) = 0 by A2, A6, Lm10;

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

        then WH is_closed_on (( Initialize t1),Q1) & WH is_halting_on (( Initialize t1),Q1) by A13, A12, Lm8, A8, A9, A7;

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

        hence B2 is_closed_on (t,Q) & B2 is_halting_on (t,Q) by A11, A4, SCMPDS_7: 24;

        (( IExec (B3,Q,t)) . a1) = ((t . a1) + 1) by A2, A5, A6, Lm11;

        hence (( IExec (B3,Q,t)) . a3) >= ((( IExec (B3,Q,t)) . a1) + 7) by A2, A5, A6, A10, Lm11;

      end;

      hence thesis by A1, Th11;

    end;

    

     Lm13: for s be 0 -started State of SCMPDS st (s . a3) >= ((s . a1) + 7) & (s . GBP ) = 0 & (s . a2) > 0 holds ( IExec (FR,P,s)) = ( IExec (FR,P,( Initialize ( IExec (B3,P,s)))))

    proof

      let s be 0 -started State of SCMPDS ;

      set a = GBP , b = ( DataLoc ((s . a),2));

      assume that

       A1: (s . a3) >= ((s . a1) + 7) and

       A2: (s . a) = 0 and

       A3: (s . a2) > 0 ;

      

       A4: b = ( intpos ( 0 + 2)) by A2, SCMP_GCD: 1;

      now

        let t be 0 -started State of SCMPDS ;

        let Q;

        

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

        assume that

         A6: (t . a3) >= ((t . a1) + 7) and

         A7: (t . a) = (s . a) and (t . b) > 0 ;

        set t1 = ( IExec (J4,Q,t)), Q1 = Q;

        

         A8: ((t . a3) + 1) >= ((7 + (t . a1)) + 1) by A6, XREAL_1: 6;

        thus (( IExec (B3,Q,t)) . a) = (t . a) by A2, A6, A7, Lm11;

        thus (( IExec (B3,Q,t)) . b) = ((t . b) - 1) by A2, A4, A6, A7, Lm11;

        

         A9: J4 is_closed_on (t,Q) & J4 is_halting_on (t,Q) by SCMPDS_6: 20, SCMPDS_6: 21;

        (t1 . a6) = ((t . a1) + 1) by A2, A7, Lm10;

        then

         A10: (t1 . a4) >= (7 + (t1 . a6)) by A2, A7, A8, Lm10;

        

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

        

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

        

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

        

         A14: (t1 . a) = 0 by A2, A7, Lm10;

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

        then WH is_closed_on (( Initialize t1),Q1) & WH is_halting_on (( Initialize t1),Q1) by A14, A10, Lm8, A11, A12, A13;

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

        hence B2 is_closed_on (t,Q) & B2 is_halting_on (t,Q) by A9, A5, SCMPDS_7: 24;

        (( IExec (B3,Q,t)) . a1) = ((t . a1) + 1) by A2, A6, A7, Lm11;

        hence (( IExec (B3,Q,t)) . a3) >= ((( IExec (B3,Q,t)) . a1) + 7) by A2, A6, A7, A8, Lm11;

      end;

      hence thesis by A1, A3, A4, Th12;

    end;

    begin

    theorem :: SCPISORT:14

    ( card ( insert-sort (n,p0))) = 23

    proof

      set i1 = ( GBP := 0 ), i2 = (( GBP ,1) := 0 ), i3 = (( GBP ,2) := (n - 1)), i4 = (( GBP ,3) := p0);

      

      thus ( card ( insert-sort (n,p0))) = (( card (((i1 ';' i2) ';' i3) ';' i4)) + ( card FR)) by AFINSQ_1: 17

      .= ((( card ((i1 ';' i2) ';' i3)) + 1) + ( card FR)) by SCMP_GCD: 4

      .= (((( card (i1 ';' i2)) + 1) + 1) + ( card FR)) by SCMP_GCD: 4

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

      .= (4 + (( card B2) + 3)) by SCMPDS_7: 41

      .= 23 by Lm5;

    end;

    theorem :: SCPISORT:15

    p0 >= 7 implies ( insert-sort (n,p0)) is parahalting

    proof

      set a = GBP , i1 = (a := 0 ), i2 = ((a,1) := 0 ), i3 = ((a,2) := (n - 1)), i4 = ((a,3) := p0), I = (((i1 ';' i2) ';' i3) ';' i4);

      assume

       A1: p0 >= 7;

      now

        let s be State of SCMPDS ;

        let P;

        set s1 = ( IExec (I,P,( Initialize s))), s2 = ( IExec (((i1 ';' i2) ';' i3),P,( Initialize s))), P1 = P, s3 = ( IExec ((i1 ';' i2),P,( Initialize s))), s4 = ( Exec (i1,( Initialize s)));

        

         A2: (s1 . a) = (( Initialize s1) . a) by SCMPDS_5: 15;

        

         A3: (s1 . a1) = (( Initialize s1) . a1) by SCMPDS_5: 15;

        

         A4: (s1 . a3) = (( Initialize s1) . a3) by SCMPDS_5: 15;

        

         A5: I is_closed_on (s,P) & I is_halting_on (s,P) by SCMPDS_6: 20, SCMPDS_6: 21;

        

         A6: (s4 . a) = 0 by SCMPDS_2: 45;

        then

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

        

         A8: (s3 . a) = (( Exec (i2,s4)) . a) by SCMPDS_5: 42

        .= 0 by A6, A7, AMI_3: 10, SCMPDS_2: 46;

        then

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

        

         A10: (s3 . a1) = (( Exec (i2,s4)) . a1) by SCMPDS_5: 42

        .= 0 by A7, SCMPDS_2: 46;

        

         A11: (s2 . a1) = (( Exec (i3,s3)) . a1) by SCMPDS_5: 41

        .= 0 by A10, A9, AMI_3: 10, SCMPDS_2: 46;

        

         A12: (s2 . a) = (( Exec (i3,s3)) . a) by SCMPDS_5: 41

        .= 0 by A8, A9, AMI_3: 10, SCMPDS_2: 46;

        then

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

        

         A14: (s1 . a3) = (( Exec (i4,s2)) . a3) by SCMPDS_5: 41

        .= p0 by A13, SCMPDS_2: 46;

        (s1 . a1) = (( Exec (i4,s2)) . a1) by SCMPDS_5: 41

        .= 0 by A11, A13, AMI_3: 10, SCMPDS_2: 46;

        then

         A15: (s1 . a3) >= ((s1 . a1) + 7) by A1, A14;

        (s1 . a) = (( Exec (i4,s2)) . a) by SCMPDS_5: 41

        .= 0 by A12, A13, AMI_3: 10, SCMPDS_2: 46;

        then FR is_closed_on (( Initialize s1),P1) & FR is_halting_on (( Initialize s1),P1) by A15, Lm12, A2, A3, A4;

        then FR is_closed_on (s1,P1) & FR is_halting_on (s1,P1) by SCMPDS_6: 125, SCMPDS_6: 126;

        hence ( insert-sort (n,p0)) is_halting_on (s,P) by A5, SCMPDS_7: 24;

      end;

      hence thesis by SCMPDS_6: 21;

    end;

    

     Lm14: for s be 0 -started State of SCMPDS st (s . a4) >= (7 + (s . a6)) & (s . GBP ) = 0 & (s . a6) > 0 holds ( IExec (WH,P,s)) = ( IExec (WH,P,( Initialize ( IExec (B1,P,s)))))

    proof

      let s be 0 -started State of SCMPDS ;

      set a = GBP , b = ( DataLoc ((s . a),6));

      assume that

       A1: (s . a4) >= (7 + (s . a6)) and

       A2: (s . a) = 0 and

       A3: (s . a6) > 0 ;

      

       A4: b = ( intpos ( 0 + 6)) by A2, SCMP_GCD: 1;

       A5:

      now

        let t be 0 -started State of SCMPDS ;

        let Q;

        

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

        assume that

         A7: for x st x in {a4} holds (t . x) >= (7 + (t . b)) and

         A8: (t . a) = (s . a) & (t . b) > 0 ;

        set Bt = ( IExec (B1,Q,( Initialize t)));

        

         A9: a4 in {a4} by TARSKI:def 1;

        then

         A10: (t . a4) >= (7 + (t . a6)) by A4, A7;

        hence (( IExec (B1,Q,t)) . a) = (t . a) by A2, A4, A8, Lm6;

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

        thus (( IExec (B1,Q,t)) . b) < (t . b) by A2, A4, A8, A10, Lm7;

        (t . a4) >= (7 + (t . b)) by A7, A9;

        then (Bt . a4) >= (7 + (Bt . a6)) by A2, A4, A8, Lm7, A6;

        hence for x st x in {a4} holds (( IExec (B1,Q,t)) . x) >= (7 + (( IExec (B1,Q,t)) . b)) by A4, A6, TARSKI:def 1;

      end;

      for x st x in {a4} holds (s . x) >= (7 + (s . b)) by A1, A4, TARSKI:def 1;

      hence thesis by A3, A4, A5, SCMPDS_8: 29;

    end;

    theorem :: SCPISORT:16

    

     Th16: for s be 0 -started State of SCMPDS , f,g be FinSequence of INT , k0,k be Nat st (s . ( intpos 4)) >= (7 + (s . ( intpos 6))) & (s . GBP ) = 0 & k = (s . ( intpos 6)) & k0 = (((s . ( intpos 4)) - (s . ( intpos 6))) - 1) & f is_FinSequence_on (s,k0) & g is_FinSequence_on (( IExec (( while>0 ( GBP ,6,(((( GBP ,5) := (( intpos 4),( - 1))) ';' ( SubFrom ( GBP ,5,( intpos 4), 0 ))) ';' ( if>0 ( GBP ,5,(((((( GBP ,5) := (( intpos 4),( - 1))) ';' ((( intpos 4),( - 1)) := (( intpos 4), 0 ))) ';' ((( intpos 4), 0 ) := ( GBP ,5))) ';' ( AddTo ( GBP ,4,( - 1)))) ';' ( AddTo ( GBP ,6,( - 1)))),( Load (( GBP ,6) := 0 ))))))),P,s)),k0) & ( len f) = ( len g) & ( len f) > k & f is_non_decreasing_on (1,k) holds (f,g) are_fiberwise_equipotent & g is_non_decreasing_on (1,(k + 1)) & (for i be Nat st i > (k + 1) & i <= ( len f) holds (f . i) = (g . i)) & for i be Nat st 1 <= i & i <= (k + 1) holds ex j be Nat st 1 <= j & j <= (k + 1) & (g . i) = (f . j)

    proof

      set a = GBP ;

      let s be 0 -started State of SCMPDS , f,g be FinSequence of INT , m,n be Nat;

      assume

       A1: (s . a4) >= (7 + (s . a6)) & (s . a) = 0 & n = (s . a6) & m = (((s . a4) - (s . a6)) - 1);

      defpred P[ Nat] means for t be 0 -started State of SCMPDS , Q holds for f1,f2 be FinSequence of INT st (t . a4) >= (7 + (t . a6)) & (t . a) = 0 & $1 = (t . a6) & m = (((t . a4) - (t . a6)) - 1) & f1 is_FinSequence_on (t,m) & f2 is_FinSequence_on (( IExec (WH,Q,t)),m) & ( len f1) = ( len f2) & ( len f1) > $1 & f1 is_non_decreasing_on (1,$1) holds (f1,f2) are_fiberwise_equipotent & f2 is_non_decreasing_on (1,($1 + 1)) & (for i be Nat st i > ($1 + 1) & i <= ( len f1) holds (f1 . i) = (f2 . i)) & (for i be Nat st 1 <= i & i <= ($1 + 1) holds ex j be Nat st 1 <= j & j <= ($1 + 1) & (f2 . i) = (f1 . j));

      assume

       A2: f is_FinSequence_on (s,m) & g is_FinSequence_on (( IExec (WH,P,s)),m);

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        thus P[(k + 1) qua Nat]

        proof

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

          let f1,f2 be FinSequence of INT ;

          

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

          assume that

           A6: (t . a4) >= (7 + (t . a6)) and

           A7: (t . a) = 0 and

           A8: (k + 1) = (t . a6) and

           A9: m = (((t . a4) - (t . a6)) - 1) and

           A10: f1 is_FinSequence_on (t,m) and

           A11: f2 is_FinSequence_on (( IExec (WH,Q,t)),m) and

           A12: ( len f1) = ( len f2) and

           A13: ( len f1) > (k + 1) and

           A14: f1 is_non_decreasing_on (1,(k + 1));

          set Bt = ( IExec (B1,Q,t)), x = ( DataLoc ((t . a4),( - 1))), y = ( DataLoc ((t . a4), 0 ));

          

           A15: (Bt . a) = 0 by A6, A7, A8, Lm6;

          ((m + 1) + (k + 1)) >= (7 + (t . a6)) by A6, A8, A9;

          then

           A16: (m + 1) >= 7 by A8, XREAL_1: 6;

          

           A17: x = ( DataLoc (m,(k + 1))) by A8, A9

          .= ( intpos (m + (k + 1))) by SCMP_GCD: 1;

          

           A18: (Bt . a6) = (( Initialize Bt) . a6) by SCMPDS_5: 15;

          

           A19: (Bt . a4) = (( Initialize Bt) . a4) by SCMPDS_5: 15;

          

           A20: (( Initialize Bt) . a) = (Bt . a) by SCMPDS_5: 15;

          

           A21: (t . x) > (t . y) implies (Bt . x) = (t . y) & (Bt . y) = (t . x) & (Bt . a6) = ((t . a6) - 1) & (Bt . a4) = ((t . a4) - 1) by A6, A7, A8, Lm7;

          

           A22: (t . x) <= (t . y) implies (Bt . x) = (t . x) & (Bt . y) = (t . y) & (Bt . a6) = 0 by A6, A7, A8, Lm7;

          

           A23: y = ( intpos (m + (k + 2))) by A8, A9, SCMP_GCD: 1;

          

           A24: (Bt . a4) >= (7 + (Bt . a6)) by A6, A7, A8, Lm7;

          per cases ;

            suppose

             A25: (t . x) > (t . y);

            now

              let i be Nat;

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

              

              hence (f2 . i) = (( IExec (WH,Q,t)) . ( intpos (m + i))) by A11

              .= (( IExec (WH,Q,( Initialize Bt))) . ( intpos (m + i))) by A6, A7, A8, Lm14;

            end;

            then

             A26: f2 is_FinSequence_on (( IExec (WH,Q,( Initialize Bt))),m);

            

             A27: (k + 1) < (k + 2) by XREAL_1: 6;

            consider h be FinSequence of INT such that

             A28: ( len h) = ( len f1) and

             A29: for i be Nat st 1 <= i & i <= ( len h) holds (h . i) = (Bt . ( intpos (m + i))) by Th1;

            (k + 1) > k by XREAL_1: 29;

            then

             A30: ( len h) > k by A13, A28, XXREAL_0: 2;

             A31:

            now

              let i be Nat;

              assume that

               A32: i <> (k + 1) & i <> (k + 2) and

               A33: 1 <= i and

               A34: i <= ( len f1);

              

               A35: (m + i) <> ((t . a4) - 1) & (m + i) <> (t . a4) by A8, A9, A32;

              (m + i) >= (m + 1) by A33, XREAL_1: 6;

              then

               A36: (m + i) >= 7 by A16, XXREAL_0: 2;

              

              thus (h . i) = (Bt . ( intpos (m + i))) by A28, A29, A33, A34

              .= (t . ( intpos (m + i))) by A6, A7, A8, A36, A35, Lm7

              .= (f1 . i) by A10, A33, A34;

            end;

            now

              let i,j be Nat;

              assume that

               A37: 1 <= i and

               A38: i <= j and

               A39: j <= k;

              

               A40: j <= ( len f1) by A28, A30, A39, XXREAL_0: 2;

              then

               A41: i <= ( len f1) by A38, XXREAL_0: 2;

              

               A42: k < (k + 1) by XREAL_1: 29;

              then

               A43: j < (k + 1) by A39, XXREAL_0: 2;

              (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

              then

               A44: k < ((k + 1) + 1) by A42, XXREAL_0: 2;

              j >= 1 by A37, A38, XXREAL_0: 2;

              then

               A45: (h . j) = (f1 . j) by A31, A39, A42, A44, A40;

              j < (k + 2) by A39, A44, XXREAL_0: 2;

              then (h . i) = (f1 . i) by A31, A37, A38, A43, A41;

              hence (h . i) <= (h . j) by A14, A37, A38, A43, A45, FINSEQ_6:def 9;

            end;

            then

             A46: h is_non_decreasing_on (1,k) by FINSEQ_6:def 9;

            

             A47: ( len f1) >= ((k + 1) + 1) by A13, INT_1: 7;

            

             A48: 1 <= (k + 1) by NAT_1: 11;

            then

             A49: 1 <= (k + 2) by A27, XXREAL_0: 2;

            then

             A50: (h . (k + 2)) = (t . x) by A23, A21, A25, A28, A29, A47;

            then

             A51: (h . (k + 2)) = (f1 . (k + 1)) by A10, A13, A17, A48;

            

             A52: (((Bt . a4) - (Bt . a6)) - 1) = m by A9, A21, A25;

            

             A53: (h . (k + 1)) = (t . y) by A13, A17, A21, A25, A28, A29, NAT_1: 11;

            then (h . (k + 1)) = (f1 . (k + 2)) by A10, A23, A49, A47;

            then

             A54: (f1,h) are_fiberwise_equipotent by A13, A28, A31, A48, A49, A47, A51, Th3;

            

             A55: h is_FinSequence_on (( Initialize Bt),m)

            proof

              let i be Nat;

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

              then (h . i) = (Bt . ( intpos (m + i))) by A29;

              hence thesis by SCMPDS_5: 15;

            end;

            (h,f2) are_fiberwise_equipotent by A4, A8, A12, A15, A24, A21, A25, A28, A52, A26, A30, A46, A55, A18, A19, A20;

            hence (f1,f2) are_fiberwise_equipotent by A54, CLASSES1: 76;

            

             A56: f2 is_non_decreasing_on (1,(k + 1)) by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A18, A19, A20, A26, A30, A46;

            now

              let i,j be Nat;

              assume that

               A57: 1 <= i and

               A58: i <= j and

               A59: j <= ((k + 1) + 1);

              per cases by A59, NAT_1: 8;

                suppose j <= (k + 1);

                hence (f2 . i) <= (f2 . j) by A56, A57, A58, FINSEQ_6:def 9;

              end;

                suppose

                 A60: j = ((k + 1) + 1);

                hereby

                  per cases ;

                    suppose i = j;

                    hence (f2 . i) <= (f2 . j);

                  end;

                    suppose i <> j;

                    then i < j by A58, XXREAL_0: 1;

                    then i <= (k + 1) by A60, NAT_1: 13;

                    then

                    consider mm be Nat such that

                     A61: 1 <= mm and

                     A62: mm <= (k + 1) and

                     A63: (f2 . i) = (h . mm) by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A57, A18, A19, A20;

                    

                     A64: (f2 . j) = (h . (k + 2)) by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A27, A47, A60, A18, A19, A20;

                    hereby

                      per cases ;

                        suppose mm = (k + 1);

                        hence (f2 . i) <= (f2 . j) by A13, A17, A21, A22, A28, A29, A50, A61, A63, A64;

                      end;

                        suppose

                         A65: mm <> (k + 1);

                        mm < (k + 2) by A27, A62, XXREAL_0: 2;

                        then mm < ( len h) by A28, A47, XXREAL_0: 2;

                        then

                         A66: (h . mm) = (f1 . mm) by A28, A31, A27, A61, A62, A65;

                        (f2 . j) = (f1 . (k + 1)) by A10, A13, A17, A48, A50, A64;

                        hence (f2 . i) <= (f2 . j) by A14, A61, A62, A63, A66, FINSEQ_6:def 9;

                      end;

                    end;

                  end;

                end;

              end;

            end;

            hence f2 is_non_decreasing_on (1,((k + 1) + 1)) by FINSEQ_6:def 9;

            hereby

              let i be Nat;

              assume that

               A67: i > ((k + 1) + 1) and

               A68: i <= ( len f1);

              

               A69: (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

              then

               A70: i > (k + 1) by A67, XXREAL_0: 2;

              1 <= (k + 1) by NAT_1: 11;

              then

               A71: 1 <= i by A70, XXREAL_0: 2;

              

              thus (f2 . i) = (h . i) by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A68, A70, A18, A19, A20

              .= (f1 . i) by A31, A67, A68, A69, A71;

            end;

            hereby

              let i be Nat;

              assume that

               A72: 1 <= i and

               A73: i <= ((k + 1) + 1);

              per cases ;

                suppose

                 A74: i = ((k + 1) + 1);

                reconsider j = (k + 1) as Nat;

                take j;

                thus 1 <= j by NAT_1: 11;

                thus j <= ((k + 1) + 1) by NAT_1: 11;

                thus (f2 . i) = (f1 . j) by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A27, A47, A51, A74, A18, A19, A20;

              end;

                suppose i <> ((k + 1) + 1);

                then i < ((k + 1) + 1) by A73, XXREAL_0: 1;

                then i <= (k + 1) by NAT_1: 13;

                then

                consider mm be Nat such that

                 A75: 1 <= mm and

                 A76: mm <= (k + 1) and

                 A77: (f2 . i) = (h . mm) by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A72, A18, A19, A20;

                hereby

                  

                   A78: (k + 2) = ((k + 1) + 1);

                  per cases ;

                    suppose

                     A79: mm = (k + 1);

                    reconsider j = (k + 2) as Nat;

                    take j;

                    thus 1 <= j by A78, NAT_1: 11;

                    thus j <= ((k + 1) + 1);

                    thus (f2 . i) = (f1 . j) by A10, A23, A49, A47, A53, A77, A79;

                  end;

                    suppose

                     A80: mm <> (k + 1);

                    reconsider mm as Nat;

                    take mm;

                    thus 1 <= mm by A75;

                    thus mm <= ((k + 1) + 1) by A27, A76, XXREAL_0: 2;

                    mm < (k + 2) by A27, A76, XXREAL_0: 2;

                    then mm < ( len f1) by A47, XXREAL_0: 2;

                    hence (f2 . i) = (f1 . mm) by A31, A27, A75, A76, A77, A80;

                  end;

                end;

              end;

            end;

          end;

            suppose

             A81: (t . x) <= (t . y);

             A82:

            now

              let i be Nat;

              assume that

               A83: i >= 1 and

               A84: i <= ( len f1);

              

               A85: (f1 . i) = (t . ( intpos (m + i))) by A10, A83, A84;

              (Bt . ( DataLoc ((Bt . a),6))) = 0 by A15, A22, A81, SCMP_GCD: 1;

              then

               A86: (( Initialize Bt) . ( DataLoc ((Bt . a),6))) = 0 by SCMPDS_5: 15;

              (m + i) >= (m + 1) by A83, XREAL_1: 6;

              then

               A87: (m + i) >= 7 by A16, XXREAL_0: 2;

              

               A88: (( Initialize Bt) . ( intpos (m + i))) = (Bt . ( intpos (m + i))) by SCMPDS_5: 15;

              

               A89: (( Initialize Bt) . ( DataLoc ((( Initialize Bt) . GBP ),6))) <= 0 by A86, SCMPDS_5: 15;

              per cases ;

                suppose

                 A90: (m + i) = ((t . a4) - 1);

                

                hence (f1 . i) = (( IExec (WH,Q,( Initialize Bt))) . x) by A8, A9, A17, A22, A81, A85, A88, A89, SCMPDS_8: 23

                .= (( IExec (WH,Q,( Initialize t))) . x) by A6, A7, A8, Lm14, A5

                .= (f2 . i) by A8, A9, A11, A12, A13, A17, A83, A90, A5;

              end;

                suppose

                 A91: (m + i) = (t . a4);

                

                hence (f1 . i) = (( IExec (WH,Q,( Initialize Bt))) . y) by A8, A9, A23, A22, A81, A85, A88, A89, SCMPDS_8: 23

                .= (( IExec (WH,Q,( Initialize t))) . y) by A6, A7, A8, Lm14, A5

                .= (f2 . i) by A8, A9, A11, A12, A23, A83, A84, A91, A5;

              end;

                suppose (m + i) <> ((t . a4) - 1) & (m + i) <> (t . a4);

                

                hence (f1 . i) = (Bt . ( intpos (m + i))) by A6, A7, A8, A87, A85, Lm7

                .= (( IExec (WH,Q,( Initialize Bt))) . ( intpos (m + i))) by A88, A89, SCMPDS_8: 23

                .= (( IExec (WH,Q,( Initialize t))) . ( intpos (m + i))) by A6, A7, A8, Lm14, A5

                .= (f2 . i) by A11, A12, A83, A84, A5;

              end;

            end;

            then

             A92: f1 = f2 by A12, FINSEQ_1: 14;

            thus (f1,f2) are_fiberwise_equipotent by A12, A82, FINSEQ_1: 14;

            now

              let i,j be Nat;

              assume that

               A93: 1 <= i and

               A94: i <= j and

               A95: j <= ((k + 1) + 1);

              per cases by A95, NAT_1: 8;

                suppose j <= (k + 1);

                hence (f1 . i) <= (f1 . j) by A14, A93, A94, FINSEQ_6:def 9;

              end;

                suppose

                 A96: j = ((k + 1) + 1);

                hereby

                  per cases ;

                    suppose i = j;

                    hence (f1 . i) <= (f1 . j);

                  end;

                    suppose i <> j;

                    then i < j by A94, XXREAL_0: 1;

                    then i <= (k + 1) by A96, NAT_1: 13;

                    then

                     A97: (f1 . i) <= (f1 . (k + 1)) by A14, A93, FINSEQ_6:def 9;

                    1 <= (k + 1) by NAT_1: 11;

                    then

                     A98: (f1 . (k + 1)) = (t . x) by A10, A13, A17;

                    1 <= ((k + 1) + 1) & j <= ( len f1) by A13, A96, INT_1: 7, NAT_1: 11;

                    then (f1 . j) = (t . y) by A10, A23, A96;

                    hence (f1 . i) <= (f1 . j) by A81, A97, A98, XXREAL_0: 2;

                  end;

                end;

              end;

            end;

            hence f2 is_non_decreasing_on (1,((k + 1) + 1)) by A92, FINSEQ_6:def 9;

            thus for i be Nat st i > ((k + 1) + 1) & i <= ( len f1) holds (f1 . i) = (f2 . i) by A12, A82, FINSEQ_1: 14;

            thus for i be Nat st 1 <= i & i <= ((k + 1) + 1) holds ex j be Nat st 1 <= j & j <= ((k + 1) + 1) & (f2 . i) = (f1 . j) by A92;

          end;

        end;

      end;

      

       A99: P[ 0 qua Nat]

      proof

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

        let f1,f2 be FinSequence of INT ;

        

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

        assume that (t . a4) >= (7 + (t . a6)) and

         A101: (t . a) = 0 & 0 = (t . a6) and m = (((t . a4) - (t . a6)) - 1) and

         A102: f1 is_FinSequence_on (t,m) and

         A103: f2 is_FinSequence_on (( IExec (WH,Q,t)),m) and

         A104: ( len f1) = ( len f2) and ( len f1) > 0 and f1 is_non_decreasing_on (1, 0 );

        

         A105: (t . ( DataLoc ((t . a),6))) = 0 by A101, SCMP_GCD: 1;

         A106:

        now

          let i be Nat;

          assume

           A107: 1 <= i & i <= ( len f1);

          

          thus (f1 . i) = (t . ( intpos (m + i))) by A102, A107

          .= (( IExec (WH,Q,( Initialize t))) . ( intpos (m + i))) by A105, A100, SCMPDS_8: 23

          .= (f2 . i) by A103, A104, A107, A100;

        end;

        hence (f1,f2) are_fiberwise_equipotent by A104, FINSEQ_1: 14;

        thus f2 is_non_decreasing_on (1,( 0 + 1)) by FINSEQ_6: 165;

        thus for i be Nat st i > ( 0 + 1) & i <= ( len f1) holds (f1 . i) = (f2 . i) by A106;

        f1 = f2 by A104, A106, FINSEQ_1: 14;

        hence thesis;

      end;

      

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

      assume ( len f) = ( len g) & ( len f) > n & f is_non_decreasing_on (1,n);

      hence thesis by A1, A2, A108;

    end;

    

     Lm15: for s be 0 -started State of SCMPDS , f,g be FinSequence of INT , p0,n be Nat st (s . GBP ) = 0 & (s . a2) = (n - 1) & (s . a3) = (p0 + 1) & (s . a1) = 0 & p0 >= 6 & f is_FinSequence_on (s,p0) & g is_FinSequence_on (( IExec (FR,P,s)),p0) & ( len f) = n & ( len g) = n holds (f,g) are_fiberwise_equipotent & g is_non_decreasing_on (1,n)

    proof

      set a = GBP ;

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

      assume that

       A1: (s . a) = 0 and

       A2: (s . a2) = (n - 1) and

       A3: (s . a3) = (p0 + 1) and

       A4: (s . a1) = 0 and

       A5: p0 >= 6 and

       A6: f is_FinSequence_on (s,p0) & g is_FinSequence_on (( IExec (FR,P,s)),p0) and

       A7: ( len f) = n and

       A8: ( len g) = n;

      per cases ;

        suppose

         A9: n = 0 ;

        then g = {} by A8;

        hence (f,g) are_fiberwise_equipotent by A7, A9;

        thus thesis by A9, FINSEQ_6: 165;

      end;

        suppose n <> 0 ;

        then n >= (1 + 0 ) by INT_1: 7;

        then (n - 1) >= 0 by XREAL_1: 19;

        then

        reconsider n1 = (n - 1) as Element of NAT by INT_1: 3;

        defpred P[ Nat] means for t be 0 -started State of SCMPDS , Q holds for f1,f2 be FinSequence of INT , m be Nat st (t . a) = 0 & ((t . a2) + (t . a1)) = (n - 1) & (t . a2) = $1 & m = (n - (t . a2)) & p0 = (((t . a3) - (t . a1)) - 1) & f1 is_FinSequence_on (t,p0) & f2 is_FinSequence_on (( IExec (FR,Q,t)),p0) & f1 is_non_decreasing_on (1,m) & ( len f1) = n & ( len f2) = n holds (f1,f2) are_fiberwise_equipotent & f2 is_non_decreasing_on (1,n);

        

         A10: ((s . a2) + (s . a1)) = ((n - 1) + 0 ) & 1 = (n - (s . a2)) by A2, A4;

         A11:

        now

          let k be Nat;

          assume

           A12: P[k];

          now

            let t be 0 -started State of SCMPDS , f1,f2 be FinSequence of INT , m be Nat;

            let Q;

            assume that

             A13: (t . a) = 0 and

             A14: ((t . a2) + (t . a1)) = (n - 1) and

             A15: (t . a2) = (k + 1) and

             A16: m = (n - (t . a2)) and

             A17: p0 = (((t . a3) - (t . a1)) - 1) and

             A18: f1 is_FinSequence_on (t,p0) and

             A19: f2 is_FinSequence_on (( IExec (FR,Q,t)),p0) and

             A20: f1 is_non_decreasing_on (1,m) & ( len f1) = n and

             A21: ( len f2) = n;

            set t1 = ( IExec (J4,Q,t)), Bt = ( IExec (B3,Q,t)), Q1 = Q;

            

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

            

             A23: (t1 . a4) = (( Initialize t1) . a4) by SCMPDS_5: 15;

            

             A24: (t1 . a6) = (( Initialize t1) . a6) by SCMPDS_5: 15;

            

             A25: (t1 . a4) = ((t . a3) + 1) by A13, Lm10;

            (p0 + ((t . a1) + 1)) = (t . a3) by A17;

            then (t . a3) >= (6 + ((t . a1) + 1)) by A5, XREAL_1: 6;

            then

             A26: (t . a3) >= ((6 + 1) + (t . a1));

            then

             A27: (Bt . a) = 0 by A13, Lm11;

            

             A28: (Bt . a2) = ((t . a2) - 1) by A13, A26, Lm11;

            then

             A29: (n - (Bt . a2)) = (m + 1) by A16;

            

             A30: (Bt . a1) = ((t . a1) + 1) by A13, A26, Lm11;

            then

             A31: ((Bt . a2) + (Bt . a1)) = (n - 1) by A14, A28;

            (Bt . a3) = ((t . a3) + 1) by A13, A26, Lm11;

            then

             A32: (((Bt . a3) - (Bt . a1)) - 1) = p0 by A17, A30;

            

             A33: (t1 . a6) = ((t . a1) + 1) by A13, Lm10;

            then

             A34: p0 = (((t1 . a4) - (t1 . a6)) - 1) by A17, A25;

            now

              let i be Nat;

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

              

              hence (f2 . i) = (( IExec (FR,Q,t)) . ( intpos (p0 + i))) by A19

              .= (( IExec (FR,Q,( Initialize Bt))) . ( intpos (p0 + i))) by A13, A15, A26, Lm13;

            end;

            then

             A35: f2 is_FinSequence_on (( IExec (FR,Q,( Initialize Bt))),p0);

             A36:

            now

              

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

              let i be Nat;

              assume that

               A38: 1 <= i and

               A39: i <= ( len f1);

              (p0 + 1) <= (p0 + i) by A38, XREAL_1: 6;

              then

               A40: (p0 + i) >= 7 by A37, XXREAL_0: 2;

              

              thus (f1 . i) = (t . ( intpos (p0 + i))) by A18, A38, A39

              .= (t1 . ( intpos (p0 + i))) by A13, A40, Lm10;

            end;

            (t1 . a4) = (p0 + ((t1 . a6) + 1)) by A17, A25, A33;

            then (t1 . a4) >= (6 + ((t1 . a6) + 1)) by A5, XREAL_1: 6;

            then

             A41: (t1 . a4) >= ((6 + 1) + (t1 . a6));

            (m + (k + 1)) = n by A15, A16;

            then

             A42: n > ( 0 + m) by XREAL_1: 6;

            consider h be FinSequence of INT such that

             A43: ( len h) = n and

             A44: for i be Nat st 1 <= i & i <= ( len h) holds (h . i) = (( IExec (WH,Q1,( Initialize t1))) . ( intpos (p0 + i))) by Th1;

            

             A45: h is_FinSequence_on (( IExec (WH,Q1,( Initialize t1))),p0) by A44;

             A46:

            now

              

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

              let i be Nat;

              assume that

               A48: 1 <= i and

               A49: i <= ( len h);

              (p0 + 1) <= (p0 + i) by A48, XREAL_1: 6;

              then (p0 + i) >= 7 by A47, XXREAL_0: 2;

              then

               A50: (p0 + i) > 2 by XXREAL_0: 2;

              

              thus (h . i) = (( IExec (WH,Q1,( Initialize t1))) . ( intpos (p0 + i))) by A44, A48, A49

              .= (Bt . ( intpos (p0 + i))) by A13, A26, A50, Lm11;

            end;

            

             A51: f1 is_FinSequence_on (( Initialize t1),p0)

            proof

              let i be Nat;

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

              then (f1 . i) = (t1 . ( intpos (p0 + i))) by A36;

              hence thesis by SCMPDS_5: 15;

            end;

            

             A52: (t1 . a) = 0 by A13, Lm10;

            then

             A53: (f1,h) are_fiberwise_equipotent by A14, A16, A17, A20, A25, A43, A34, A41, A45, A42, Th16, A23, A24, A22, A51;

            

             A54: h is_non_decreasing_on (1,(m + 1)) by A14, A16, A17, A20, A25, A43, A34, A41, A45, A42, Th16, A23, A24, A22, A51, A52;

            

             A55: (( Initialize Bt) . a) = (Bt . a) by SCMPDS_5: 15;

            

             A56: (( Initialize Bt) . a1) = (Bt . a1) by SCMPDS_5: 15;

            

             A57: (( Initialize Bt) . a2) = (Bt . a2) by SCMPDS_5: 15;

            

             A58: (( Initialize Bt) . a3) = (Bt . a3) by SCMPDS_5: 15;

            

             A59: h is_FinSequence_on (( Initialize Bt),p0)

            proof

              let i be Nat such that

               A60: 1 <= i & i <= ( len h);

              

              thus (h . i) = (Bt . ( intpos (p0 + i))) by A60, A46

              .= (( Initialize Bt) . ( intpos (p0 + i))) by SCMPDS_5: 15;

            end;

            then (h,f2) are_fiberwise_equipotent by A12, A15, A16, A21, A43, A27, A31, A29, A32, A35, A54, A55, A56, A57, A58;

            hence (f1,f2) are_fiberwise_equipotent by A53, CLASSES1: 76;

            thus f2 is_non_decreasing_on (1,n) by A12, A15, A16, A21, A43, A54, A27, A31, A29, A32, A35, A55, A56, A57, A58, A59;

          end;

          hence P[(k + 1)];

        end;

        

         A61: P[ 0 qua Nat]

        proof

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

          let f1,f2 be FinSequence of INT , m be Nat;

          

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

          assume that

           A63: (t . a) = 0 and ((t . a2) + (t . a1)) = (n - 1) and

           A64: (t . a2) = 0 and

           A65: m = (n - (t . a2)) and p0 = (((t . a3) - (t . a1)) - 1) and

           A66: f1 is_FinSequence_on (t,p0) and

           A67: f2 is_FinSequence_on (( IExec (FR,Q,t)),p0) and

           A68: f1 is_non_decreasing_on (1,m) and

           A69: ( len f1) = n & ( len f2) = n;

          

           A70: (t . ( DataLoc ((t . a),2))) = 0 by A63, A64, SCMP_GCD: 1;

           A71:

          now

            let i be Nat;

            assume

             A72: 1 <= i & i <= ( len f2);

            

            thus (f2 . i) = (( IExec (FR,Q,( Initialize t))) . ( intpos (p0 + i))) by A67, A72, A62

            .= (t . ( intpos (p0 + i))) by A70, SCMPDS_7: 47

            .= (f1 . i) by A66, A69, A72;

          end;

          hence (f1,f2) are_fiberwise_equipotent by A69, FINSEQ_1: 14;

          thus thesis by A64, A65, A68, A69, A71, FINSEQ_1: 14;

        end;

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

        then

         A73: P[n1];

        p0 = (((s . a3) - (s . a1)) - 1) & f is_non_decreasing_on (1,1) by A3, A4, FINSEQ_6: 165;

        hence thesis by A1, A6, A7, A8, A10, A73;

      end;

    end;

    theorem :: SCPISORT:17

    for s be 0 -started State of SCMPDS , f,g be FinSequence of INT , p0,n be Nat st p0 >= 6 & ( len f) = n & ( len g) = n & f is_FinSequence_on (s,p0) & g is_FinSequence_on (( IExec (( insert-sort (n,(p0 + 1))),P,s)),p0) holds (f,g) are_fiberwise_equipotent & g is_non_decreasing_on (1,n)

    proof

      set a = GBP ;

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

      assume that

       A1: p0 >= 6 and

       A2: ( len f) = n & ( len g) = n and

       A3: f is_FinSequence_on (s,p0) and

       A4: g is_FinSequence_on (( IExec (( insert-sort (n,(p0 + 1))),P,s)),p0);

      

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

      set i1 = ( GBP := 0 ), i2 = (( GBP ,1) := 0 ), i3 = (( GBP ,2) := (n - 1)), i4 = (( GBP ,3) := (p0 + 1));

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

      

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

      then

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

      

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

      .= 0 by A6, A7, AMI_3: 10, SCMPDS_2: 46;

      then

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

      

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

      .= 0 by A8, A9, AMI_3: 10, SCMPDS_2: 46;

      then

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

       A12:

      now

        let i be Nat;

        assume

         A13: i > 3;

        then

         A14: i > 1 by XXREAL_0: 2;

        

        thus (t3 . ( intpos i)) = (( Exec (i2,t4)) . ( intpos i)) by SCMPDS_5: 42

        .= (t4 . ( intpos i)) by A7, A14, AMI_3: 10, SCMPDS_2: 46

        .= (s . ( intpos i)) by A13, AMI_3: 10, SCMPDS_2: 45;

      end;

       A15:

      now

        let i be Nat;

        assume

         A16: i > 3;

        then

         A17: i > 2 by XXREAL_0: 2;

        

        thus (t2 . ( intpos i)) = (( Exec (i3,t3)) . ( intpos i)) by SCMPDS_5: 41

        .= (t3 . ( intpos i)) by A9, A17, AMI_3: 10, SCMPDS_2: 46

        .= (s . ( intpos i)) by A12, A16;

      end;

      now

        let i be Nat;

        assume that

         A18: 1 <= i and

         A19: i <= ( len f);

        set pi = (p0 + i);

        pi >= (p0 + 1) by A18, XREAL_1: 6;

        then pi >= 7 by A5, XXREAL_0: 2;

        then

         A20: pi > 3 by XXREAL_0: 2;

        

        thus (( Initialize t1) . ( intpos pi)) = (t1 . ( intpos pi)) by SCMPDS_5: 15

        .= (( Exec (i4,t2)) . ( intpos pi)) by SCMPDS_5: 41

        .= (t2 . ( intpos pi)) by A11, A20, AMI_3: 10, SCMPDS_2: 46

        .= (s . ( intpos pi)) by A15, A20

        .= (f . i) by A3, A18, A19;

      end;

      then

       A21: f is_FinSequence_on (( Initialize t1),p0);

      

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

      .= 0 by A7, SCMPDS_2: 46;

      

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

      .= 0 by A22, A9, AMI_3: 10, SCMPDS_2: 46;

      

       A24: I4 is_closed_on (s,P) & I4 is_halting_on (s,P) by SCMPDS_6: 20, SCMPDS_6: 21;

      

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

      .= 0 by A10, A11, AMI_3: 10, SCMPDS_2: 46;

      

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

      .= (n - 1) by A9, SCMPDS_2: 46;

      

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

      .= (p0 + 1) by A11, SCMPDS_2: 46;

      

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

      

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

      

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

      

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

      

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

      .= 0 by A23, A11, AMI_3: 10, SCMPDS_2: 46;

      then (t1 . a3) >= ((t1 . a1) + 7) by A27, A5;

      then FR is_closed_on (( Initialize t1),P) & FR is_halting_on (( Initialize t1),P) by A25, Lm12, A28, A29, A30;

      then

       A33: FR is_closed_on (t1,P) & FR is_halting_on (t1,P) by SCMPDS_6: 125, SCMPDS_6: 126;

      now

        let i be Nat;

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

        

        hence (g . i) = (( IExec ((I4 ';' FR),P,s)) . ( intpos (p0 + i))) by A4

        .= (( IExec (FR,P,( Initialize t1))) . ( intpos (p0 + i))) by A24, A33, SCMPDS_7: 30;

      end;

      then

       A34: g is_FinSequence_on (( IExec (FR,P,( Initialize t1))),p0);

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

      .= (n - 1) by A26, A11, AMI_3: 10, SCMPDS_2: 46;

      hence thesis by A1, A2, A25, A32, A27, A21, A34, Lm15, A28, A29, A30, A31;

    end;