scmbsort.miz



    begin

    reserve p for preProgram of SCM+FSA ,

ic for Instruction of SCM+FSA ,

i,j,k for Nat,

fa,f for FinSeq-Location,

a,b,da,db for Int-Location,

la,lb for Nat;

    reserve p1,p2,q for Instruction-Sequence of SCM+FSA ;

    set SA0 = ( Start-At ( 0 , SCM+FSA ));

    ::$Canceled

    theorem :: SCMBSORT:2

    

     Th1: for s be State of SCM+FSA , f be FinSeq-Location, a,b be Int-Location holds (( Exec ((b := (f,a)),s)) . b) = ((s . f) /. |.(s . a).|)

    proof

      let s be State of SCM+FSA , f be FinSeq-Location, a,b be Int-Location;

      ex k be Nat st (k = |.(s . a).|) & ((( Exec ((b := (f,a)),s)) . b) = ((s . f) /. k)) by SCMFSA_2: 72;

      hence thesis;

    end;

    theorem :: SCMBSORT:3

    

     Th2: for s be State of SCM+FSA , f be FinSeq-Location, a,b be Int-Location holds (( Exec (((f,a) := b),s)) . f) = ((s . f) +* ( |.(s . a).|,(s . b)))

    proof

      let s be State of SCM+FSA , f be FinSeq-Location, a,b be Int-Location;

      ex k be Nat st (k = |.(s . a).|) & ((( Exec (((f,a) := b),s)) . f) = ((s . f) +* (k,(s . b)))) by SCMFSA_2: 73;

      hence thesis;

    end;

    theorem :: SCMBSORT:4

    

     Th3: for s be State of SCM+FSA , f be FinSeq-Location, m,n be Nat, a be Int-Location st m <> (n + 1) holds (( Exec ((( intloc m) := (f,a)),( Initialized s))) . ( intloc (n + 1))) = (s . ( intloc (n + 1)))

    proof

      let s be State of SCM+FSA , f be FinSeq-Location, m,n be Nat, a be Int-Location;

      assume m <> (n + 1);

      then ( intloc m) <> ( intloc (n + 1)) by SCMFSA_2: 101;

      

      hence (( Exec ((( intloc m) := (f,a)),( Initialized s))) . ( intloc (n + 1))) = (( Initialized s) . ( intloc (n + 1))) by SCMFSA_2: 72

      .= (s . ( intloc (n + 1))) by SCMFSA_M: 37;

    end;

    theorem :: SCMBSORT:5

    

     Th4: for s be State of SCM+FSA , m,n be Nat, a be Int-Location st m <> (n + 1) holds (( Exec ((( intloc m) := a),( Initialized s))) . ( intloc (n + 1))) = (s . ( intloc (n + 1)))

    proof

      let s be State of SCM+FSA , m,n be Nat, a be Int-Location;

      assume m <> (n + 1);

      then ( intloc m) <> ( intloc (n + 1)) by SCMFSA_2: 101;

      

      hence (( Exec ((( intloc m) := a),( Initialized s))) . ( intloc (n + 1))) = (( Initialized s) . ( intloc (n + 1))) by SCMFSA_2: 63

      .= (s . ( intloc (n + 1))) by SCMFSA_M: 37;

    end;

    theorem :: SCMBSORT:6

    

     Th5: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA , f be FinSeq-Location, a be read-write Int-Location holds (( IExec (( Stop SCM+FSA ),p,s)) . a) = (s . a) & (( IExec (( Stop SCM+FSA ),p,s)) . f) = (s . f)

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA , f be FinSeq-Location, a be read-write Int-Location;

      

       A1: ( Initialized s) = (s +* ((( intloc 0 ) .--> 1) +* ( Start-At ( 0 , SCM+FSA ))))

      .= ( Initialize (s +* (( intloc 0 ) .--> 1))) by FUNCT_4: 14;

      

       A2: ( IExec (( Stop SCM+FSA ),p,s)) = ( Initialize (s +* (( intloc 0 ) .--> 1))) by A1, SCMFSA8C: 14

      .= ( Initialized s) by A1;

      hence (( IExec (( Stop SCM+FSA ),p,s)) . a) = (s . a) by SCMFSA_M: 37;

      thus thesis by A2, SCMFSA_M: 37;

    end;

    reserve n for Nat;

    theorem :: SCMBSORT:7

    

     Th6: ic in ( rng p) & (ic = (a := b) or ic = ( AddTo (a,b)) or ic = ( SubFrom (a,b)) or ic = ( MultBy (a,b)) or ic = ( Divide (a,b))) implies a in ( UsedILoc p) & b in ( UsedILoc p)

    proof

      assume that

       A1: ic in ( rng p) and

       A2: ic = (a := b) or ic = ( AddTo (a,b)) or ic = ( SubFrom (a,b)) or ic = ( MultBy (a,b)) or ic = ( Divide (a,b));

      

       A3: ( UsedIntLoc ic) = {a, b} by A2, SF_MASTR: 14;

      ( UsedIntLoc ic) c= ( UsedILoc p) by A1, SF_MASTR: 19;

      hence thesis by A3, ZFMISC_1: 32;

    end;

    theorem :: SCMBSORT:8

    

     Th7: ic in ( rng p) & (ic = (a =0_goto la) or ic = (a >0_goto la)) implies a in ( UsedILoc p)

    proof

      assume that

       A1: ic in ( rng p) and

       A2: ic = (a =0_goto la) or ic = (a >0_goto la);

      

       A3: ( UsedIntLoc ic) = {a} by A2, SF_MASTR: 16;

      ( UsedIntLoc ic) c= ( UsedILoc p) by A1, SF_MASTR: 19;

      hence thesis by A3, ZFMISC_1: 31;

    end;

    theorem :: SCMBSORT:9

    

     Th8: ic in ( rng p) & (ic = (b := (fa,a)) or ic = ((fa,a) := b)) implies a in ( UsedILoc p) & b in ( UsedILoc p)

    proof

      assume that

       A1: ic in ( rng p) and

       A2: ic = (b := (fa,a)) or ic = ((fa,a) := b);

      

       A3: ( UsedIntLoc ic) = {a, b} by A2, SF_MASTR: 17;

      ( UsedIntLoc ic) c= ( UsedILoc p) by A1, SF_MASTR: 19;

      hence thesis by A3, ZFMISC_1: 32;

    end;

    theorem :: SCMBSORT:10

    

     Th9: ic in ( rng p) & (ic = (b := (fa,a)) or ic = ((fa,a) := b)) implies fa in ( UsedI*Loc p)

    proof

      assume that

       A1: ic in ( rng p) and

       A2: ic = (b := (fa,a)) or ic = ((fa,a) := b);

      

       A3: ( UsedInt*Loc ic) = {fa} by A2, SF_MASTR: 33;

      ( UsedInt*Loc ic) c= ( UsedI*Loc p) by A1, SF_MASTR: 35;

      hence thesis by A3, ZFMISC_1: 31;

    end;

    theorem :: SCMBSORT:11

    

     Th10: ic in ( rng p) & (ic = (a :=len fa) or ic = (fa :=<0,...,0> a)) implies a in ( UsedILoc p)

    proof

      assume that

       A1: ic in ( rng p) and

       A2: ic = (a :=len fa) or ic = (fa :=<0,...,0> a);

      

       A3: ( UsedIntLoc ic) = {a} by A2, SF_MASTR: 18;

      ( UsedIntLoc ic) c= ( UsedILoc p) by A1, SF_MASTR: 19;

      hence thesis by A3, ZFMISC_1: 31;

    end;

    theorem :: SCMBSORT:12

    

     Th11: ic in ( rng p) & (ic = (a :=len fa) or ic = (fa :=<0,...,0> a)) implies fa in ( UsedI*Loc p)

    proof

      assume that

       A1: ic in ( rng p) and

       A2: ic = (a :=len fa) or ic = (fa :=<0,...,0> a);

      

       A3: ( UsedInt*Loc ic) = {fa} by A2, SF_MASTR: 34;

      ( UsedInt*Loc ic) c= ( UsedI*Loc p) by A1, SF_MASTR: 35;

      hence thesis by A3, ZFMISC_1: 31;

    end;

    theorem :: SCMBSORT:13

    

     Th12: for t be FinPartState of SCM+FSA , p be Program of SCM+FSA , x be set st ( dom t) c= ( Int-Locations \/ FinSeq-Locations ) & x in ((( dom t) \/ ( UsedI*Loc p)) \/ ( UsedILoc p)) holds x is Int-Location or x is FinSeq-Location

    proof

      let t be FinPartState of SCM+FSA , p be Program of SCM+FSA , x be set;

      set D1 = ( UsedI*Loc p);

      set D2 = ( UsedILoc p);

      assume that

       A1: ( dom t) c= ( Int-Locations \/ FinSeq-Locations ) and

       A2: x in ((( dom t) \/ D1) \/ D2);

      x in (( dom t) \/ D1) or x in D2 by A2, XBOOLE_0:def 3;

      then

       A3: x in ( dom t) or x in D1 or x in D2 by XBOOLE_0:def 3;

      per cases by A1, A3, XBOOLE_0:def 3;

        suppose x in Int-Locations ;

        hence thesis by AMI_2:def 16;

      end;

        suppose x in FinSeq-Locations ;

        hence thesis by SCMFSA_2:def 5;

      end;

        suppose x in D1;

        then x in FinSeq-Locations ;

        hence thesis by SCMFSA_2:def 5;

      end;

        suppose x in D2;

        then x in Int-Locations ;

        hence thesis by AMI_2:def 16;

      end;

    end;

    theorem :: SCMBSORT:14

    

     Th13: for i,k be Nat, t be FinPartState of SCM+FSA , p be Program of SCM+FSA , s1,s2 be State of SCM+FSA st k <= i & p c= p1 & p c= p2 & ( dom t) c= ( Int-Locations \/ FinSeq-Locations ) & (for j holds ( IC ( Comput (p1,s1,j))) in ( dom p) & ( IC ( Comput (p2,s2,j))) in ( dom p)) & (( Comput (p1,s1,k)) . ( IC SCM+FSA )) = (( Comput (p2,s2,k)) . ( IC SCM+FSA )) & (( Comput (p1,s1,k)) | ((( dom t) \/ ( UsedI*Loc p)) \/ ( UsedILoc p))) = (( Comput (p2,s2,k)) | ((( dom t) \/ ( UsedI*Loc p)) \/ ( UsedILoc p))) holds (( Comput (p1,s1,i)) . ( IC SCM+FSA )) = (( Comput (p2,s2,i)) . ( IC SCM+FSA )) & (( Comput (p1,s1,i)) | ((( dom t) \/ ( UsedI*Loc p)) \/ ( UsedILoc p))) = (( Comput (p2,s2,i)) | ((( dom t) \/ ( UsedI*Loc p)) \/ ( UsedILoc p)))

    proof

      let i, k;

      let t be FinPartState of SCM+FSA , p be Program of SCM+FSA , s1,s2 be State of SCM+FSA ;

      set Dloc = ((( dom t) \/ ( UsedI*Loc p)) \/ ( UsedILoc p));

      assume that

       A1: k <= i and

       A2: p c= p1 and

       A3: p c= p2 and

       A4: ( dom t) c= ( Int-Locations \/ FinSeq-Locations ) and

       A5: for j holds ( IC ( Comput (p1,s1,j))) in ( dom p) & ( IC ( Comput (p2,s2,j))) in ( dom p) and

       A6: (( Comput (p1,s1,k)) . ( IC SCM+FSA )) = (( Comput (p2,s2,k)) . ( IC SCM+FSA )) and

       A7: (( Comput (p1,s1,k)) | Dloc) = (( Comput (p2,s2,k)) | Dloc);

      consider m be Nat such that

       A8: i = (k + m) by A1, NAT_1: 10;

      reconsider m as Nat;

      

       A9: i = (k + m) by A8;

      

       A10: ( UsedILoc p) c= Dloc by XBOOLE_1: 7;

      Dloc = ((( dom t) \/ ( UsedILoc p)) \/ ( UsedI*Loc p)) by XBOOLE_1: 4;

      then

       A11: ( UsedI*Loc p) c= Dloc by XBOOLE_1: 7;

      defpred P[ Nat] means (( Comput (p1,s1,(k + $1))) . ( IC SCM+FSA )) = (( Comput (p2,s2,(k + $1))) . ( IC SCM+FSA )) & (( Comput (p1,s1,(k + $1))) | Dloc) = (( Comput (p2,s2,(k + $1))) | Dloc);

      

       A12: P[ 0 ] by A6, A7;

       A13:

      now

        let m be Nat;

        assume

         A14: P[m];

        set sk1 = ( Comput (p1,s1,(k + m)));

        set sk11 = ( Comput (p1,s1,(k + (m + 1))));

        set i1 = ( CurInstr (p1,sk1));

        set sk2 = ( Comput (p2,s2,(k + m)));

        set sk12 = ( Comput (p2,s2,(k + (m + 1))));

        set i2 = ( CurInstr (p2,sk2));

        

         A15: ( IC sk1) in ( dom p) by A5;

        

         A16: (p2 /. ( IC sk2)) = (p2 . ( IC sk2)) by PBOOLE: 143;

        

         A17: (p1 /. ( IC sk1)) = (p1 . ( IC sk1)) by PBOOLE: 143;

        i1 = (p . ( IC sk1)) by A2, A15, A17, GRFUNC_1: 2;

        then

         A18: i1 in ( rng p) by A15, FUNCT_1:def 3;

        

         A19: i2 = ((p2 | ( dom p)) . ( IC sk2)) by A16, A5, FUNCT_1: 49

        .= ((p1 | ( dom p)) . ( IC sk1)) by A2, A3, A14, GRFUNC_1: 33

        .= i1 by A17, A5, FUNCT_1: 49;

        

         A20: sk11 = ( Comput (p1,s1,((k + m) + 1)))

        .= ( Following (p1,sk1)) by EXTPRO_1: 3

        .= ( Exec (i1,sk1));

        

         A21: sk12 = ( Comput (p2,s2,((k + m) + 1)))

        .= ( Following (p2,sk2)) by EXTPRO_1: 3

        .= ( Exec (i2,sk2));

        

         A22: ( dom sk11) = the carrier of SCM+FSA by PARTFUN1:def 2

        .= ( dom sk12) by PARTFUN1:def 2;

        ( InsCode i1) = 0 or ... or ( InsCode i1) = 12 by SCMFSA_2: 16;

        per cases ;

          suppose ( InsCode i1) = 0 ;

          then

           A23: i1 = ( halt SCM+FSA ) by SCMFSA_2: 95;

          then sk11 = sk1 by A20, EXTPRO_1:def 3;

          hence P[(m + 1)] by A14, A19, A21, A23, EXTPRO_1:def 3;

        end;

          suppose ( InsCode i1) = 1;

          then

          consider da, db such that

           A24: i1 = (da := db) by SCMFSA_2: 30;

          

           A25: (sk11 . ( IC SCM+FSA )) = (( IC sk1) + 1) by A20, A24, SCMFSA_2: 63

          .= (sk12 . ( IC SCM+FSA )) by A14, A19, A21, A24, SCMFSA_2: 63;

          now

            let x be set;

            assume

             A26: x in Dloc;

            per cases by A4, A26, Th12;

              suppose

               A27: x is Int-Location;

              per cases ;

                suppose

                 A28: x = da;

                then

                 A29: (sk12 . x) = (sk2 . db) by A19, A21, A24, SCMFSA_2: 63;

                

                 A30: db in ( UsedILoc p) by A18, A24, Th6;

                

                then (sk1 . db) = ((sk2 | Dloc) . db) by A10, A14, FUNCT_1: 49

                .= (sk2 . db) by A10, A30, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A24, A28, A29, SCMFSA_2: 63;

              end;

                suppose

                 A31: x <> da;

                then

                 A32: (sk12 . x) = (sk2 . x) by A19, A21, A24, A27, SCMFSA_2: 63;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A26, FUNCT_1: 49

                .= (sk2 . x) by A26, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A24, A27, A31, A32, SCMFSA_2: 63;

              end;

            end;

              suppose

               A33: x is FinSeq-Location;

              then

               A34: (sk12 . x) = (sk2 . x) by A19, A21, A24, SCMFSA_2: 63;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A26, FUNCT_1: 49

              .= (sk2 . x) by A26, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A24, A33, A34, SCMFSA_2: 63;

            end;

          end;

          hence P[(m + 1)] by A22, A25, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 2;

          then

          consider da, db such that

           A35: i1 = ( AddTo (da,db)) by SCMFSA_2: 31;

          

           A36: (sk11 . ( IC SCM+FSA )) = (( IC sk1) + 1) by A20, A35, SCMFSA_2: 64

          .= (sk12 . ( IC SCM+FSA )) by A14, A19, A21, A35, SCMFSA_2: 64;

          now

            let x be set;

            assume

             A37: x in Dloc;

            per cases by A4, A37, Th12;

              suppose

               A38: x is Int-Location;

              per cases ;

                suppose

                 A39: x = da;

                then

                 A40: (sk12 . x) = ((sk2 . da) + (sk2 . db)) by A19, A21, A35, SCMFSA_2: 64;

                

                 A41: da in ( UsedILoc p) by A18, A35, Th6;

                

                then

                 A42: (sk1 . da) = ((sk2 | Dloc) . da) by A10, A14, FUNCT_1: 49

                .= (sk2 . da) by A10, A41, FUNCT_1: 49;

                

                 A43: db in ( UsedILoc p) by A18, A35, Th6;

                

                then (sk1 . db) = ((sk2 | Dloc) . db) by A10, A14, FUNCT_1: 49

                .= (sk2 . db) by A10, A43, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A35, A39, A40, A42, SCMFSA_2: 64;

              end;

                suppose

                 A44: x <> da;

                then

                 A45: (sk12 . x) = (sk2 . x) by A19, A21, A35, A38, SCMFSA_2: 64;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A37, FUNCT_1: 49

                .= (sk2 . x) by A37, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A35, A38, A44, A45, SCMFSA_2: 64;

              end;

            end;

              suppose

               A46: x is FinSeq-Location;

              then

               A47: (sk12 . x) = (sk2 . x) by A19, A21, A35, SCMFSA_2: 64;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A37, FUNCT_1: 49

              .= (sk2 . x) by A37, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A35, A46, A47, SCMFSA_2: 64;

            end;

          end;

          hence P[(m + 1)] by A22, A36, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 3;

          then

          consider da, db such that

           A48: i1 = ( SubFrom (da,db)) by SCMFSA_2: 32;

          

           A49: (sk11 . ( IC SCM+FSA )) = (( IC sk1) + 1) by A20, A48, SCMFSA_2: 65

          .= (sk12 . ( IC SCM+FSA )) by A14, A19, A21, A48, SCMFSA_2: 65;

          now

            let x be set;

            assume

             A50: x in Dloc;

            per cases by A4, A50, Th12;

              suppose

               A51: x is Int-Location;

              per cases ;

                suppose

                 A52: x = da;

                then

                 A53: (sk12 . x) = ((sk2 . da) - (sk2 . db)) by A19, A21, A48, SCMFSA_2: 65;

                

                 A54: da in ( UsedILoc p) by A18, A48, Th6;

                

                then

                 A55: (sk1 . da) = ((sk2 | Dloc) . da) by A10, A14, FUNCT_1: 49

                .= (sk2 . da) by A10, A54, FUNCT_1: 49;

                

                 A56: db in ( UsedILoc p) by A18, A48, Th6;

                

                then (sk1 . db) = ((sk2 | Dloc) . db) by A10, A14, FUNCT_1: 49

                .= (sk2 . db) by A10, A56, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A48, A52, A53, A55, SCMFSA_2: 65;

              end;

                suppose

                 A57: x <> da;

                then

                 A58: (sk12 . x) = (sk2 . x) by A19, A21, A48, A51, SCMFSA_2: 65;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A50, FUNCT_1: 49

                .= (sk2 . x) by A50, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A48, A51, A57, A58, SCMFSA_2: 65;

              end;

            end;

              suppose

               A59: x is FinSeq-Location;

              then

               A60: (sk12 . x) = (sk2 . x) by A19, A21, A48, SCMFSA_2: 65;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A50, FUNCT_1: 49

              .= (sk2 . x) by A50, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A48, A59, A60, SCMFSA_2: 65;

            end;

          end;

          hence P[(m + 1)] by A22, A49, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 4;

          then

          consider da, db such that

           A61: i1 = ( MultBy (da,db)) by SCMFSA_2: 33;

          

           A62: (sk11 . ( IC SCM+FSA )) = (( IC sk1) + 1) by A20, A61, SCMFSA_2: 66

          .= (sk12 . ( IC SCM+FSA )) by A14, A19, A21, A61, SCMFSA_2: 66;

          now

            let x be set;

            assume

             A63: x in Dloc;

            per cases by A4, A63, Th12;

              suppose

               A64: x is Int-Location;

              per cases ;

                suppose

                 A65: x = da;

                then

                 A66: (sk12 . x) = ((sk2 . da) * (sk2 . db)) by A19, A21, A61, SCMFSA_2: 66;

                

                 A67: da in ( UsedILoc p) by A18, A61, Th6;

                

                then

                 A68: (sk1 . da) = ((sk2 | Dloc) . da) by A10, A14, FUNCT_1: 49

                .= (sk2 . da) by A10, A67, FUNCT_1: 49;

                

                 A69: db in ( UsedILoc p) by A18, A61, Th6;

                

                then (sk1 . db) = ((sk2 | Dloc) . db) by A10, A14, FUNCT_1: 49

                .= (sk2 . db) by A10, A69, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A61, A65, A66, A68, SCMFSA_2: 66;

              end;

                suppose

                 A70: x <> da;

                then

                 A71: (sk12 . x) = (sk2 . x) by A19, A21, A61, A64, SCMFSA_2: 66;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A63, FUNCT_1: 49

                .= (sk2 . x) by A63, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A61, A64, A70, A71, SCMFSA_2: 66;

              end;

            end;

              suppose

               A72: x is FinSeq-Location;

              then

               A73: (sk12 . x) = (sk2 . x) by A19, A21, A61, SCMFSA_2: 66;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A63, FUNCT_1: 49

              .= (sk2 . x) by A63, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A61, A72, A73, SCMFSA_2: 66;

            end;

          end;

          hence P[(m + 1)] by A22, A62, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 5;

          then

          consider da, db such that

           A74: i1 = ( Divide (da,db)) by SCMFSA_2: 34;

          

           A75: (sk11 . ( IC SCM+FSA )) = (( IC sk1) + 1) by A20, A74, SCMFSA_2: 67

          .= (sk12 . ( IC SCM+FSA )) by A14, A19, A21, A74, SCMFSA_2: 67;

          now

            let x be set;

            assume

             A76: x in Dloc;

            per cases by A4, A76, Th12;

              suppose

               A77: x is Int-Location;

              

               A78: da in ( UsedILoc p) by A18, A74, Th6;

              

              then

               A79: (sk1 . da) = ((sk2 | Dloc) . da) by A10, A14, FUNCT_1: 49

              .= (sk2 . da) by A10, A78, FUNCT_1: 49;

              

               A80: db in ( UsedILoc p) by A18, A74, Th6;

              

              then

               A81: (sk1 . db) = ((sk2 | Dloc) . db) by A10, A14, FUNCT_1: 49

              .= (sk2 . db) by A10, A80, FUNCT_1: 49;

              

               A82: (sk1 . x) = ((sk2 | Dloc) . x) by A14, A76, FUNCT_1: 49

              .= (sk2 . x) by A76, FUNCT_1: 49;

              now

                per cases ;

                  suppose

                   A83: da <> db;

                  per cases ;

                    suppose

                     A84: x = da;

                    then (sk11 . x) = ((sk1 . da) div (sk1 . db)) by A20, A74, A83, SCMFSA_2: 67;

                    hence (sk11 . x) = (sk12 . x) by A19, A21, A74, A79, A81, A83, A84, SCMFSA_2: 67;

                  end;

                    suppose

                     A85: x = db;

                    then (sk11 . x) = ((sk1 . da) mod (sk1 . db)) by A20, A74, SCMFSA_2: 67;

                    hence (sk11 . x) = (sk12 . x) by A19, A21, A74, A79, A81, A85, SCMFSA_2: 67;

                  end;

                    suppose

                     A86: x <> da & x <> db;

                    then (sk11 . x) = (sk1 . x) by A20, A74, A77, SCMFSA_2: 67;

                    hence (sk11 . x) = (sk12 . x) by A19, A21, A74, A77, A82, A86, SCMFSA_2: 67;

                  end;

                end;

                  suppose

                   A87: da = db;

                  now

                    per cases ;

                      case

                       A88: x = da;

                      then (sk11 . x) = ((sk1 . da) mod (sk1 . da)) by A20, A74, A87, SCMFSA_2: 68;

                      hence (sk11 . x) = (sk12 . x) by A19, A21, A74, A79, A87, A88, SCMFSA_2: 68;

                    end;

                      case

                       A89: x <> da;

                      then (sk11 . x) = (sk1 . x) by A20, A74, A77, A87, SCMFSA_2: 68;

                      hence (sk11 . x) = (sk12 . x) by A19, A21, A74, A77, A82, A87, A89, SCMFSA_2: 68;

                    end;

                  end;

                  hence (sk11 . x) = (sk12 . x);

                end;

              end;

              hence (sk11 . x) = (sk12 . x);

            end;

              suppose

               A90: x is FinSeq-Location;

              then

               A91: (sk12 . x) = (sk2 . x) by A19, A21, A74, SCMFSA_2: 67;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A76, FUNCT_1: 49

              .= (sk2 . x) by A76, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A74, A90, A91, SCMFSA_2: 67;

            end;

          end;

          hence P[(m + 1)] by A22, A75, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 6;

          then

          consider lb such that

           A92: i1 = ( goto lb) by SCMFSA_2: 35;

          

           A93: (sk11 . ( IC SCM+FSA )) = lb by A20, A92, SCMFSA_2: 69

          .= (sk12 . ( IC SCM+FSA )) by A19, A21, A92, SCMFSA_2: 69;

          now

            let x be set;

            assume

             A94: x in Dloc;

            

            then

             A95: (sk1 . x) = ((sk2 | Dloc) . x) by A14, FUNCT_1: 49

            .= (sk2 . x) by A94, FUNCT_1: 49;

            per cases by A4, A94, Th12;

              suppose

               A96: x is Int-Location;

              then (sk11 . x) = (sk1 . x) by A20, A92, SCMFSA_2: 69;

              hence (sk11 . x) = (sk12 . x) by A19, A21, A92, A95, A96, SCMFSA_2: 69;

            end;

              suppose

               A97: x is FinSeq-Location;

              then (sk11 . x) = (sk1 . x) by A20, A92, SCMFSA_2: 69;

              hence (sk11 . x) = (sk12 . x) by A19, A21, A92, A95, A97, SCMFSA_2: 69;

            end;

          end;

          hence P[(m + 1)] by A22, A93, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 7;

          then

          consider lb, da such that

           A98: i1 = (da =0_goto lb) by SCMFSA_2: 36;

          

           A99: da in ( UsedILoc p) by A18, A98, Th7;

          

          then

           A100: (sk1 . da) = ((sk2 | Dloc) . da) by A10, A14, FUNCT_1: 49

          .= (sk2 . da) by A10, A99, FUNCT_1: 49;

           A101:

          now

            per cases ;

              suppose

               A102: (sk1 . da) = 0 ;

              

              hence (sk11 . ( IC SCM+FSA )) = lb by A20, A98, SCMFSA_2: 70

              .= (sk12 . ( IC SCM+FSA )) by A19, A21, A98, A100, A102, SCMFSA_2: 70;

            end;

              suppose

               A103: (sk1 . da) <> 0 ;

              

              hence (sk11 . ( IC SCM+FSA )) = (( IC sk2) + 1) by A14, A20, A98, SCMFSA_2: 70

              .= (sk12 . ( IC SCM+FSA )) by A19, A21, A98, A100, A103, SCMFSA_2: 70;

            end;

          end;

          now

            let x be set;

            assume

             A104: x in Dloc;

            

            then

             A105: (sk1 . x) = ((sk2 | Dloc) . x) by A14, FUNCT_1: 49

            .= (sk2 . x) by A104, FUNCT_1: 49;

            per cases by A4, A104, Th12;

              suppose

               A106: x is Int-Location;

              then (sk11 . x) = (sk1 . x) by A20, A98, SCMFSA_2: 70;

              hence (sk11 . x) = (sk12 . x) by A19, A21, A98, A105, A106, SCMFSA_2: 70;

            end;

              suppose

               A107: x is FinSeq-Location;

              then (sk11 . x) = (sk1 . x) by A20, A98, SCMFSA_2: 70;

              hence (sk11 . x) = (sk12 . x) by A19, A21, A98, A105, A107, SCMFSA_2: 70;

            end;

          end;

          hence P[(m + 1)] by A22, A101, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 8;

          then

          consider lb, da such that

           A108: i1 = (da >0_goto lb) by SCMFSA_2: 37;

          

           A109: da in ( UsedILoc p) by A18, A108, Th7;

          

          then

           A110: (sk1 . da) = ((sk2 | Dloc) . da) by A10, A14, FUNCT_1: 49

          .= (sk2 . da) by A10, A109, FUNCT_1: 49;

           A111:

          now

            per cases ;

              suppose

               A112: (sk1 . da) > 0 ;

              

              hence (sk11 . ( IC SCM+FSA )) = lb by A20, A108, SCMFSA_2: 71

              .= (sk12 . ( IC SCM+FSA )) by A19, A21, A108, A110, A112, SCMFSA_2: 71;

            end;

              suppose

               A113: (sk1 . da) <= 0 ;

              

              hence (sk11 . ( IC SCM+FSA )) = (( IC sk2) + 1) by A14, A20, A108, SCMFSA_2: 71

              .= (sk12 . ( IC SCM+FSA )) by A19, A21, A108, A110, A113, SCMFSA_2: 71;

            end;

          end;

          now

            let x be set;

            assume

             A114: x in Dloc;

            

            then

             A115: (sk1 . x) = ((sk2 | Dloc) . x) by A14, FUNCT_1: 49

            .= (sk2 . x) by A114, FUNCT_1: 49;

            per cases by A4, A114, Th12;

              suppose

               A116: x is Int-Location;

              then (sk11 . x) = (sk1 . x) by A20, A108, SCMFSA_2: 71;

              hence (sk11 . x) = (sk12 . x) by A19, A21, A108, A115, A116, SCMFSA_2: 71;

            end;

              suppose

               A117: x is FinSeq-Location;

              then (sk11 . x) = (sk1 . x) by A20, A108, SCMFSA_2: 71;

              hence (sk11 . x) = (sk12 . x) by A19, A21, A108, A115, A117, SCMFSA_2: 71;

            end;

          end;

          hence P[(m + 1)] by A22, A111, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 9;

          then

          consider a, b, fa such that

           A118: i1 = (b := (fa,a)) by SCMFSA_2: 38;

          

           A119: (sk11 . ( IC SCM+FSA )) = (( IC sk2) + 1) by A14, A20, A118, SCMFSA_2: 72

          .= (sk12 . ( IC SCM+FSA )) by A19, A21, A118, SCMFSA_2: 72;

          now

            let x be set;

            assume

             A120: x in Dloc;

            per cases by A4, A120, Th12;

              suppose

               A121: x is Int-Location;

              per cases ;

                suppose

                 A122: x = b;

                

                 A123: ex k1 be Nat st (k1 = |.(sk1 . a).|) & ((( Exec ((b := (fa,a)),sk1)) . b) = ((sk1 . fa) /. k1)) by SCMFSA_2: 72;

                

                 A124: ex k2 be Nat st (k2 = |.(sk2 . a).|) & ((( Exec ((b := (fa,a)),sk2)) . b) = ((sk2 . fa) /. k2)) by SCMFSA_2: 72;

                

                 A125: a in ( UsedILoc p) by A18, A118, Th8;

                

                then

                 A126: (sk1 . a) = ((sk2 | Dloc) . a) by A10, A14, FUNCT_1: 49

                .= (sk2 . a) by A10, A125, FUNCT_1: 49;

                

                 A127: fa in ( UsedI*Loc p) by A18, A118, Th9;

                

                then (sk1 . fa) = ((sk2 | Dloc) . fa) by A11, A14, FUNCT_1: 49

                .= (sk2 . fa) by A11, A127, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A19, A20, A21, A118, A122, A123, A124, A126;

              end;

                suppose

                 A128: x <> b;

                then

                 A129: (sk12 . x) = (sk2 . x) by A19, A21, A118, A121, SCMFSA_2: 72;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A120, FUNCT_1: 49

                .= (sk2 . x) by A120, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A118, A121, A128, A129, SCMFSA_2: 72;

              end;

            end;

              suppose

               A130: x is FinSeq-Location;

              then

               A131: (sk12 . x) = (sk2 . x) by A19, A21, A118, SCMFSA_2: 72;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A120, FUNCT_1: 49

              .= (sk2 . x) by A120, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A118, A130, A131, SCMFSA_2: 72;

            end;

          end;

          hence P[(m + 1)] by A22, A119, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 10;

          then

          consider a, b, fa such that

           A132: i1 = ((fa,a) := b) by SCMFSA_2: 39;

          

           A133: (sk11 . ( IC SCM+FSA )) = (( IC sk2) + 1) by A14, A20, A132, SCMFSA_2: 73

          .= (sk12 . ( IC SCM+FSA )) by A19, A21, A132, SCMFSA_2: 73;

          now

            let x be set;

            assume

             A134: x in Dloc;

            per cases by A4, A134, Th12;

              suppose

               A135: x is FinSeq-Location;

              per cases ;

                suppose

                 A136: x = fa;

                

                 A137: ex k1 be Nat st (k1 = |.(sk1 . a).|) & ((( Exec (((fa,a) := b),sk1)) . fa) = ((sk1 . fa) +* (k1,(sk1 . b)))) by SCMFSA_2: 73;

                

                 A138: ex k2 be Nat st (k2 = |.(sk2 . a).|) & ((( Exec (((fa,a) := b),sk2)) . fa) = ((sk2 . fa) +* (k2,(sk2 . b)))) by SCMFSA_2: 73;

                

                 A139: a in ( UsedILoc p) by A18, A132, Th8;

                

                then

                 A140: (sk1 . a) = ((sk2 | Dloc) . a) by A10, A14, FUNCT_1: 49

                .= (sk2 . a) by A10, A139, FUNCT_1: 49;

                

                 A141: b in ( UsedILoc p) by A18, A132, Th8;

                

                then

                 A142: (sk1 . b) = ((sk2 | Dloc) . b) by A10, A14, FUNCT_1: 49

                .= (sk2 . b) by A10, A141, FUNCT_1: 49;

                

                 A143: fa in ( UsedI*Loc p) by A18, A132, Th9;

                

                then (sk1 . fa) = ((sk2 | Dloc) . fa) by A11, A14, FUNCT_1: 49

                .= (sk2 . fa) by A11, A143, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A19, A20, A21, A132, A136, A137, A138, A140, A142;

              end;

                suppose

                 A144: x <> fa;

                then

                 A145: (sk12 . x) = (sk2 . x) by A19, A21, A132, A135, SCMFSA_2: 73;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A134, FUNCT_1: 49

                .= (sk2 . x) by A134, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A132, A135, A144, A145, SCMFSA_2: 73;

              end;

            end;

              suppose

               A146: x is Int-Location;

              then

               A147: (sk12 . x) = (sk2 . x) by A19, A21, A132, SCMFSA_2: 73;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A134, FUNCT_1: 49

              .= (sk2 . x) by A134, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A132, A146, A147, SCMFSA_2: 73;

            end;

          end;

          hence P[(m + 1)] by A22, A133, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 11;

          then

          consider a, fa such that

           A148: i1 = (a :=len fa) by SCMFSA_2: 40;

          

           A149: (sk11 . ( IC SCM+FSA )) = (( IC sk2) + 1) by A14, A20, A148, SCMFSA_2: 74

          .= (sk12 . ( IC SCM+FSA )) by A19, A21, A148, SCMFSA_2: 74;

          now

            let x be set;

            assume

             A150: x in Dloc;

            per cases by A4, A150, Th12;

              suppose

               A151: x is Int-Location;

              per cases ;

                suppose

                 A152: x = a;

                then

                 A153: (sk12 . x) = ( len (sk2 . fa)) by A19, A21, A148, SCMFSA_2: 74;

                

                 A154: fa in ( UsedI*Loc p) by A18, A148, Th11;

                

                then (sk1 . fa) = ((sk2 | Dloc) . fa) by A11, A14, FUNCT_1: 49

                .= (sk2 . fa) by A11, A154, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A148, A152, A153, SCMFSA_2: 74;

              end;

                suppose

                 A155: x <> a;

                then

                 A156: (sk12 . x) = (sk2 . x) by A19, A21, A148, A151, SCMFSA_2: 74;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A150, FUNCT_1: 49

                .= (sk2 . x) by A150, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A148, A151, A155, A156, SCMFSA_2: 74;

              end;

            end;

              suppose

               A157: x is FinSeq-Location;

              then

               A158: (sk12 . x) = (sk2 . x) by A19, A21, A148, SCMFSA_2: 74;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A150, FUNCT_1: 49

              .= (sk2 . x) by A150, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A148, A157, A158, SCMFSA_2: 74;

            end;

          end;

          hence P[(m + 1)] by A22, A149, FUNCT_1: 96;

        end;

          suppose ( InsCode i1) = 12;

          then

          consider a, fa such that

           A159: i1 = (fa :=<0,...,0> a) by SCMFSA_2: 41;

          

           A160: (sk11 . ( IC SCM+FSA )) = (( IC sk2) + 1) by A14, A20, A159, SCMFSA_2: 75

          .= (sk12 . ( IC SCM+FSA )) by A19, A21, A159, SCMFSA_2: 75;

          now

            let x be set;

            assume

             A161: x in Dloc;

            per cases by A4, A161, Th12;

              suppose

               A162: x is FinSeq-Location;

              per cases ;

                suppose

                 A163: x = fa;

                

                 A164: ex k1 be Nat st (k1 = |.(sk1 . a).|) & ((( Exec ((fa :=<0,...,0> a),sk1)) . fa) = (k1 |-> 0 )) by SCMFSA_2: 75;

                

                 A165: ex k2 be Nat st (k2 = |.(sk2 . a).|) & ((( Exec ((fa :=<0,...,0> a),sk2)) . fa) = (k2 |-> 0 )) by SCMFSA_2: 75;

                

                 A166: a in ( UsedILoc p) by A18, A159, Th10;

                

                then (sk1 . a) = ((sk2 | Dloc) . a) by A10, A14, FUNCT_1: 49

                .= (sk2 . a) by A10, A166, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A19, A20, A21, A159, A163, A164, A165;

              end;

                suppose

                 A167: x <> fa;

                then

                 A168: (sk12 . x) = (sk2 . x) by A19, A21, A159, A162, SCMFSA_2: 75;

                (sk1 . x) = ((sk2 | Dloc) . x) by A14, A161, FUNCT_1: 49

                .= (sk2 . x) by A161, FUNCT_1: 49;

                hence (sk11 . x) = (sk12 . x) by A20, A159, A162, A167, A168, SCMFSA_2: 75;

              end;

            end;

              suppose

               A169: x is Int-Location;

              then

               A170: (sk12 . x) = (sk2 . x) by A19, A21, A159, SCMFSA_2: 75;

              (sk1 . x) = ((sk2 | Dloc) . x) by A14, A161, FUNCT_1: 49

              .= (sk2 . x) by A161, FUNCT_1: 49;

              hence (sk11 . x) = (sk12 . x) by A20, A159, A169, A170, SCMFSA_2: 75;

            end;

          end;

          hence P[(m + 1)] by A22, A160, FUNCT_1: 96;

        end;

      end;

      for m be Nat holds P[m] from NAT_1:sch 2( A12, A13);

      hence thesis by A9;

    end;

    theorem :: SCMBSORT:15

    

     Th14: for i,k be Nat, p be Program of SCM+FSA , s1,s2 be State of SCM+FSA st k <= i & p c= p1 & p c= p2 & (for j holds ( IC ( Comput (p1,s1,j))) in ( dom p) & ( IC ( Comput (p2,s2,j))) in ( dom p)) & (( Comput (p1,s1,k)) . ( IC SCM+FSA )) = (( Comput (p2,s2,k)) . ( IC SCM+FSA )) & (( Comput (p1,s1,k)) | (( UsedI*Loc p) \/ ( UsedILoc p))) = (( Comput (p2,s2,k)) | (( UsedI*Loc p) \/ ( UsedILoc p))) holds (( Comput (p1,s1,i)) . ( IC SCM+FSA )) = (( Comput (p2,s2,i)) . ( IC SCM+FSA )) & (( Comput (p1,s1,i)) | (( UsedI*Loc p) \/ ( UsedILoc p))) = (( Comput (p2,s2,i)) | (( UsedI*Loc p) \/ ( UsedILoc p)))

    proof

      let i,k be Nat, p be Program of SCM+FSA , s1,s2 be State of SCM+FSA ;

      set D = (( UsedI*Loc p) \/ ( UsedILoc p));

      assume that

       A1: k <= i and

       A2: p c= p1 and

       A3: p c= p2 and

       A4: for j holds ( IC ( Comput (p1,s1,j))) in ( dom p) & ( IC ( Comput (p2,s2,j))) in ( dom p) and

       A5: (( Comput (p1,s1,k)) . ( IC SCM+FSA )) = (( Comput (p2,s2,k)) . ( IC SCM+FSA )) and

       A6: (( Comput (p1,s1,k)) | D) = (( Comput (p2,s2,k)) | D);

      reconsider t = {} as PartState of SCM+FSA by FUNCT_1: 104, RELAT_1: 171;

      set D1 = ((( dom t) \/ ( UsedI*Loc p)) \/ ( UsedILoc p));

      

       A7: ( dom t) c= ( Int-Locations \/ FinSeq-Locations ) by RELAT_1: 38, XBOOLE_1: 2;

      

       A8: D1 = D by RELAT_1: 38;

      hence (( Comput (p1,s1,i)) . ( IC SCM+FSA )) = (( Comput (p2,s2,i)) . ( IC SCM+FSA )) by A1, A2, A3, A4, A5, A6, A7, Th13;

      thus thesis by A1, A2, A3, A4, A5, A6, A7, A8, Th13;

    end;

    ::$Canceled

    theorem :: SCMBSORT:23

    

     Th15: for i1,i2,i3 be Instruction of SCM+FSA holds ( card ((i1 ";" i2) ";" i3)) = 6

    proof

      let i1,i2,i3 be Instruction of SCM+FSA ;

      

      thus ( card ((i1 ";" i2) ";" i3)) = (( card (i1 ";" i2)) + 2) by SCMFSA6A: 34

      .= (4 + 2) by SCMFSA6A: 35

      .= 6;

    end;

    ::$Canceled

    theorem :: SCMBSORT:26

    

     Th16: for I,J be Program of SCM+FSA , k be Nat, i be Instruction of SCM+FSA st k < ( card J) & i = (J . k) holds ((I ";" J) . (( card I) + k)) = ( IncAddr (i,( card I)))

    proof

      let I,J be Program of SCM+FSA , k be Nat, i be Instruction of SCM+FSA such that

       A1: k < ( card J) and

       A2: i = (J . k);

      set m = (( card I) + k);

      

       A3: m < (( card I) + ( card J)) by A1, XREAL_1: 6;

      (m -' ( card I)) = k by NAT_D: 34;

      hence thesis by A2, A3, NAT_1: 11, SCMFSA8C: 2;

    end;

    theorem :: SCMBSORT:27

    

     Th17: for I,J be Program of SCM+FSA , i be ins-loc-free Instruction of SCM+FSA st i <> ( halt SCM+FSA ) holds (((I ";" i) ";" J) . ( card I)) = i

    proof

      let I,J be Program of SCM+FSA , i be ins-loc-free Instruction of SCM+FSA ;

      assume that

       A1: i <> ( halt SCM+FSA );

      set x1 = ( card I);

      

       A2: ( card (I ";" i)) = (( card I) + 2) by SCMFSA6A: 34;

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

      then

       A3: x1 in ( dom (I ";" i)) by A2, AFINSQ_1: 66;

      

       A4: (( Macro i) . 0 ) = i by COMPOS_1: 58;

      

       A5: ( card ( Macro i)) = 2 by COMPOS_1: 56;

      

       A6: ((I ";" i) . x1) = ((I ";" ( Macro i)) . (( card I) + 0 )) by SCMFSA6A:def 6

      .= ( IncAddr (i,( card I))) by A4, A5, Th16

      .= i by COMPOS_0: 4;

      

      thus (((I ";" i) ";" J) . x1) = (( Directed (I ";" i)) . x1) by A3, SCMFSA8A: 14

      .= i by A1, A3, A6, SCMFSA8A: 16;

    end;

    theorem :: SCMBSORT:28

    

     Th18: for I,J be Program of SCM+FSA , i be Instruction of SCM+FSA holds (((I ";" i) ";" J) . (( card I) + 1)) = ( goto (( card I) + 2))

    proof

      let I,J be Program of SCM+FSA , i be Instruction of SCM+FSA ;

      set x1 = ( card I);

      

       A1: ( card (I ";" i)) = (( card I) + 2) by SCMFSA6A: 34;

      

       A2: ( card ( Macro i)) = 2 by COMPOS_1: 56;

      set x2 = (( card I) + 1);

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

      then

       A3: x2 in ( dom (I ";" i)) by A1, AFINSQ_1: 66;

      (( Macro i) . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

      then ((I ";" ( Macro i)) . x2) = ( IncAddr (( halt SCM+FSA ),( card I))) by A2, Th16;

      

      then

       A4: ((I ";" i) . x2) = ( IncAddr (( halt SCM+FSA ),( card I))) by SCMFSA6A:def 6

      .= ( halt SCM+FSA ) by COMPOS_0: 4;

      

      thus (((I ";" i) ";" J) . x2) = (( Directed (I ";" i)) . x2) by A3, SCMFSA8A: 14

      .= ( goto (( card I) + 2)) by A1, A3, A4, SCMFSA8A: 16;

    end;

    ::$Canceled

    theorem :: SCMBSORT:32

    

     Th19: for p be Program of SCM+FSA , s be State of SCM+FSA holds (( UsedI*Loc p) \/ ( UsedILoc p)) c= ( dom s)

    proof

      let p be Program of SCM+FSA , s be State of SCM+FSA ;

       Int-Locations c= ( dom s) by SCMFSA_2: 45;

      then

       A1: ( UsedILoc p) c= ( dom s) by XBOOLE_1: 1;

       FinSeq-Locations c= ( dom s) by SCMFSA_2: 46;

      then ( UsedI*Loc p) c= ( dom s) by XBOOLE_1: 1;

      hence thesis by A1, XBOOLE_1: 8;

    end;

    theorem :: SCMBSORT:33

    

     Th20: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA , I be Program of SCM+FSA , f be FinSeq-Location holds (( Result ((p +* I),( Initialized s))) . f) = (( IExec (I,p,s)) . f)

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA , I be Program of SCM+FSA , f be FinSeq-Location;

      set D = ( Int-Locations \/ FinSeq-Locations );

      f in FinSeq-Locations by SCMFSA_2:def 5;

      then

       A1: f in D by XBOOLE_0:def 3;

      

      hence (( Result ((p +* I),( Initialized s))) . f) = (( DataPart ( Result ((p +* I),( Initialized s)))) . f) by FUNCT_1: 49, SCMFSA_2: 100

      .= (( DataPart ( IExec (I,p,s))) . f) by SCMFSA8B: 32

      .= (( IExec (I,p,s)) . f) by A1, FUNCT_1: 49, SCMFSA_2: 100;

    end;

    set a0 = ( intloc 0 );

    set a1 = ( intloc 1);

    set a2 = ( intloc 2);

    set a3 = ( intloc 3);

    set a4 = ( intloc 4);

    set a5 = ( intloc 5);

    set a6 = ( intloc 6);

    

     Lm1: a0 <> a2 by SCMFSA_2: 101;

    

     Lm2: a0 <> a4 by SCMFSA_2: 101;

    

     Lm3: a0 <> a5 by SCMFSA_2: 101;

    

     Lm4: a0 <> a6 by SCMFSA_2: 101;

    

     Lm5: a1 <> a2 by SCMFSA_2: 101;

    

     Lm6: a1 <> a3 by SCMFSA_2: 101;

    

     Lm7: a1 <> a4 by SCMFSA_2: 101;

    

     Lm8: a1 <> a5 by SCMFSA_2: 101;

    

     Lm9: a1 <> a6 by SCMFSA_2: 101;

    

     Lm10: a2 <> a3 by SCMFSA_2: 101;

    

     Lm11: a2 <> a4 by SCMFSA_2: 101;

    

     Lm12: a2 <> a5 by SCMFSA_2: 101;

    

     Lm13: a2 <> a6 by SCMFSA_2: 101;

    

     Lm14: a3 <> a4 by SCMFSA_2: 101;

    

     Lm15: a3 <> a5 by SCMFSA_2: 101;

    

     Lm16: a3 <> a6 by SCMFSA_2: 101;

    

     Lm17: a4 <> a5 by SCMFSA_2: 101;

    

     Lm18: a4 <> a6 by SCMFSA_2: 101;

    

     Lm19: a5 <> a6 by SCMFSA_2: 101;

    set initializeWorkMem = (((((a2 := a0) ";" (a3 := a0)) ";" (a4 := a0)) ";" (a5 := a0)) ";" (a6 := a0));

    definition

      let f be FinSeq-Location;

      :: SCMBSORT:def1

      func bubble-sort f -> Program of SCM+FSA equals (((((((( intloc 2) := ( intloc 0 )) ";" (( intloc 3) := ( intloc 0 ))) ";" (( intloc 4) := ( intloc 0 ))) ";" (( intloc 5) := ( intloc 0 ))) ";" (( intloc 6) := ( intloc 0 ))) ";" (( intloc 1) :=len f)) ";" ( Times (( intloc 1),((((( intloc 2) := ( intloc 1)) ";" ( SubFrom (( intloc 2),( intloc 0 )))) ";" (( intloc 3) :=len f)) ";" ( Times (( intloc 2),((((((( intloc 4) := ( intloc 3)) ";" ( SubFrom (( intloc 3),( intloc 0 )))) ";" (( intloc 5) := (f,( intloc 3)))) ";" (( intloc 6) := (f,( intloc 4)))) ";" ( SubFrom (( intloc 6),( intloc 5)))) ";" ( if>0 (( intloc 6),(((( intloc 6) := (f,( intloc 4))) ";" ((f,( intloc 3)) := ( intloc 6))) ";" ((f,( intloc 4)) := ( intloc 5))),( Stop SCM+FSA ))))))))));

      correctness ;

    end

    definition

      :: SCMBSORT:def2

      func Bubble-Sort-Algorithm -> Program of SCM+FSA equals ( bubble-sort ( fsloc 0 ));

      coherence ;

    end

    set b1 = ( intloc ( 0 + 1)), b2 = ( intloc (1 + 1)), b3 = ( intloc (2 + 1)), b4 = ( intloc (3 + 1)), b5 = ( intloc (4 + 1)), b6 = ( intloc (5 + 1));

    set f0 = ( fsloc 0 ), i1 = (b4 := b3), i2 = ( SubFrom (b3,a0)), i3 = (b5 := (f0,b3)), i4 = (b6 := (f0,b4)), i5 = ( SubFrom (b6,b5)), i6 = ((f0,b3) := b6), i7 = ((f0,b4) := b5), SS = ( Stop SCM+FSA ), ifc = ( if>0 (b6,((i4 ";" i6) ";" i7),SS)), body2 = (((((i1 ";" i2) ";" i3) ";" i4) ";" i5) ";" ifc), T2 = ( Times (b2,body2)), j1 = (b2 := b1), j2 = ( SubFrom (b2,a0)), j3 = (b3 :=len f0), Sb = ((j1 ";" j2) ";" j3), body1 = (Sb ";" T2), T1 = ( Times (b1,body1)), w2 = (b2 := a0), w3 = (b3 := a0), w4 = (b4 := a0), w5 = (b5 := a0), w6 = (b6 := a0), w7 = (b1 :=len f0);

    theorem :: SCMBSORT:34

    

     Th21: for f be FinSeq-Location holds ( UsedILoc ( bubble-sort f)) = {( intloc 0 ), ( intloc 1), ( intloc 2), ( intloc 3), ( intloc 4), ( intloc 5), ( intloc 6)}

    proof

      let f be FinSeq-Location;

      set i1 = (a4 := a3), i2 = ( SubFrom (a3,a0)), i3 = (a5 := (f,a3)), i4 = (a6 := (f,a4)), i5 = ( SubFrom (a6,a5)), i6 = ((f,a3) := a6), i7 = ((f,a4) := a5), ifc = ( if>0 (a6,((i4 ";" i6) ";" i7),( Stop SCM+FSA ))), Sif = ( UsedILoc ifc), body2 = (((((i1 ";" i2) ";" i3) ";" i4) ";" i5) ";" ifc);

      

       A1: Sif = (( {a6} \/ ( UsedILoc ((i4 ";" i6) ";" i7))) \/ {} ) by SCMFSA9A: 3, SCMFSA9A: 43

      .= ( {a6} \/ (( UsedILoc (i4 ";" i6)) \/ ( UsedIntLoc i7))) by SF_MASTR: 30

      .= ( {a6} \/ (( UsedILoc (i4 ";" i6)) \/ {a4, a5})) by SF_MASTR: 17

      .= ( {a6} \/ ((( UsedIntLoc i4) \/ ( UsedIntLoc i6)) \/ {a4, a5})) by SF_MASTR: 31

      .= ( {a6} \/ ((( UsedIntLoc i4) \/ {a3, a6}) \/ {a4, a5})) by SF_MASTR: 17

      .= ( {a6} \/ (( {a4, a6} \/ {a3, a6}) \/ {a4, a5})) by SF_MASTR: 17

      .= ( {a6} \/ ( {a4, a6, a3, a6} \/ {a4, a5})) by ENUMSET1: 5

      .= ( {a6} \/ ( {a6, a6, a3, a4} \/ {a4, a5})) by ENUMSET1: 75

      .= (( {a6} \/ {a6, a6, a3, a4}) \/ {a4, a5}) by XBOOLE_1: 4

      .= ( {a6, a6, a6, a3, a4} \/ {a4, a5}) by ENUMSET1: 7

      .= ( {a6, a3, a4} \/ {a4, a5}) by ENUMSET1: 38

      .= (( {a6, a3} \/ {a4}) \/ {a4, a5}) by ENUMSET1: 3

      .= ( {a6, a3} \/ ( {a4} \/ {a4, a5})) by XBOOLE_1: 4

      .= ( {a6, a3} \/ {a4, a4, a5}) by ENUMSET1: 2

      .= ( {a4, a5} \/ {a6, a3}) by ENUMSET1: 30

      .= {a4, a5, a6, a3} by ENUMSET1: 5

      .= {a4, a3, a6, a5} by ENUMSET1: 64;

      set ui12 = ( UsedILoc (i1 ";" i2));

      

       A2: ( UsedILoc body2) = (( UsedILoc ((((i1 ";" i2) ";" i3) ";" i4) ";" i5)) \/ Sif) by SF_MASTR: 27

      .= ((( UsedILoc (((i1 ";" i2) ";" i3) ";" i4)) \/ ( UsedIntLoc i5)) \/ Sif) by SF_MASTR: 30

      .= ((( UsedILoc (((i1 ";" i2) ";" i3) ";" i4)) \/ {a6, a5}) \/ Sif) by SF_MASTR: 14

      .= (((( UsedILoc ((i1 ";" i2) ";" i3)) \/ ( UsedIntLoc i4)) \/ {a6, a5}) \/ Sif) by SF_MASTR: 30

      .= (((( UsedILoc ((i1 ";" i2) ";" i3)) \/ {a6, a4}) \/ {a6, a5}) \/ Sif) by SF_MASTR: 17

      .= ((((ui12 \/ ( UsedIntLoc i3)) \/ {a6, a4}) \/ {a6, a5}) \/ Sif) by SF_MASTR: 30

      .= ((((ui12 \/ {a5, a3}) \/ {a6, a4}) \/ {a6, a5}) \/ Sif) by SF_MASTR: 17

      .= (((ui12 \/ ( {a5, a3} \/ {a6, a4})) \/ {a6, a5}) \/ Sif) by XBOOLE_1: 4

      .= (((ui12 \/ {a5, a3, a6, a4}) \/ {a6, a5}) \/ Sif) by ENUMSET1: 5

      .= (((ui12 \/ {a4, a3, a6, a5}) \/ {a6, a5}) \/ Sif) by ENUMSET1: 75

      .= (((ui12 \/ ( {a4, a3} \/ {a6, a5})) \/ {a6, a5}) \/ Sif) by ENUMSET1: 5

      .= ((((ui12 \/ {a4, a3}) \/ {a6, a5}) \/ {a6, a5}) \/ Sif) by XBOOLE_1: 4

      .= (((ui12 \/ {a4, a3}) \/ ( {a6, a5} \/ {a6, a5})) \/ Sif) by XBOOLE_1: 4

      .= ((ui12 \/ ( {a4, a3} \/ {a6, a5})) \/ Sif) by XBOOLE_1: 4

      .= ((ui12 \/ {a4, a3, a6, a5}) \/ Sif) by ENUMSET1: 5

      .= (ui12 \/ ( {a4, a3, a6, a5} \/ Sif)) by XBOOLE_1: 4

      .= ((( UsedIntLoc i1) \/ ( UsedIntLoc i2)) \/ {a4, a3, a6, a5}) by A1, SF_MASTR: 31

      .= ((( UsedIntLoc i1) \/ {a3, a0}) \/ {a4, a3, a6, a5}) by SF_MASTR: 14

      .= (( {a3, a4} \/ {a3, a0}) \/ {a4, a3, a6, a5}) by SF_MASTR: 14

      .= ( {a3, a4, a3, a0} \/ {a4, a3, a6, a5}) by ENUMSET1: 5

      .= ( {a3, a3, a4, a0} \/ {a4, a3, a6, a5}) by ENUMSET1: 62

      .= ( {a3, a4, a0} \/ {a4, a3, a6, a5}) by ENUMSET1: 31

      .= ( {a0, a4, a3} \/ {a4, a3, a6, a5}) by ENUMSET1: 60

      .= (( {a0} \/ {a4, a3}) \/ {a4, a3, a6, a5}) by ENUMSET1: 2

      .= (( {a0} \/ {a4, a3}) \/ ( {a4, a3} \/ {a6, a5})) by ENUMSET1: 5

      .= ((( {a0} \/ {a4, a3}) \/ {a4, a3}) \/ {a6, a5}) by XBOOLE_1: 4

      .= (( {a0} \/ ( {a4, a3} \/ {a4, a3})) \/ {a6, a5}) by XBOOLE_1: 4

      .= ( {a0} \/ ( {a4, a3} \/ {a6, a5})) by XBOOLE_1: 4

      .= ( {a0} \/ {a4, a3, a6, a5}) by ENUMSET1: 5;

      set j1 = (a2 := a1), j2 = ( SubFrom (a2,a0)), j3 = (a3 :=len f), Sfor = ( UsedILoc ( Times (a2,body2))), body1 = (((j1 ";" j2) ";" j3) ";" ( Times (a2,body2)));

      

       A3: Sfor = (( {a4, a3, a6, a5} \/ {a0}) \/ {a2, a0}) by A2, SCMFSA9A: 44

      .= ( {a4, a3, a6, a5} \/ ( {a0} \/ {a2, a0})) by XBOOLE_1: 4

      .= ( {a4, a3, a6, a5} \/ {a0, a0, a2}) by ENUMSET1: 2

      .= ( {a4, a3, a6, a5} \/ {a0, a2}) by ENUMSET1: 30

      .= ( {a4, a5, a6, a3} \/ {a0, a2}) by ENUMSET1: 64

      .= (( {a4, a5, a6} \/ {a3}) \/ {a0, a2}) by ENUMSET1: 6

      .= ( {a4, a5, a6} \/ ( {a3} \/ {a0, a2})) by XBOOLE_1: 4

      .= ( {a4, a5, a6} \/ {a0, a2, a3}) by ENUMSET1: 3;

      

       A4: ( UsedILoc body1) = (( UsedILoc ((j1 ";" j2) ";" j3)) \/ Sfor) by SF_MASTR: 27

      .= ((( UsedILoc (j1 ";" j2)) \/ ( UsedIntLoc j3)) \/ Sfor) by SF_MASTR: 30

      .= ((( UsedILoc (j1 ";" j2)) \/ {a3}) \/ Sfor) by SF_MASTR: 18

      .= (((( UsedIntLoc j1) \/ ( UsedIntLoc j2)) \/ {a3}) \/ Sfor) by SF_MASTR: 31

      .= (((( UsedIntLoc j1) \/ {a2, a0}) \/ {a3}) \/ Sfor) by SF_MASTR: 14

      .= ((( {a2, a1} \/ {a2, a0}) \/ {a3}) \/ Sfor) by SF_MASTR: 14

      .= (( {a2, a1} \/ ( {a0, a2} \/ {a3})) \/ Sfor) by XBOOLE_1: 4

      .= (( {a2, a1} \/ {a0, a2, a3}) \/ Sfor) by ENUMSET1: 3

      .= ((( {a2, a1} \/ {a0, a2, a3}) \/ {a0, a2, a3}) \/ {a4, a5, a6}) by A3, XBOOLE_1: 4

      .= (( {a2, a1} \/ ( {a0, a2, a3} \/ {a0, a2, a3})) \/ {a4, a5, a6}) by XBOOLE_1: 4

      .= (( {a2, a1} \/ ( {a0, a2} \/ {a3})) \/ {a4, a5, a6}) by ENUMSET1: 3

      .= ((( {a2, a1} \/ {a0, a2}) \/ {a3}) \/ {a4, a5, a6}) by XBOOLE_1: 4

      .= (( {a2, a1, a0, a2} \/ {a3}) \/ {a4, a5, a6}) by ENUMSET1: 5

      .= (( {a2, a2, a0, a1} \/ {a3}) \/ {a4, a5, a6}) by ENUMSET1: 64

      .= (( {a2, a0, a1} \/ {a3}) \/ {a4, a5, a6}) by ENUMSET1: 31

      .= (( {a0, a1, a2} \/ {a3}) \/ {a4, a5, a6}) by ENUMSET1: 59

      .= ( {a0, a1, a2, a3} \/ {a4, a5, a6}) by ENUMSET1: 6

      .= {a0, a1, a2, a3, a4, a5, a6} by ENUMSET1: 19;

      set k2 = (a2 := a0), k3 = (a3 := a0), k4 = (a4 := a0), k5 = (a5 := a0);

      

       A5: ( UsedILoc initializeWorkMem) = (( UsedILoc (((k2 ";" k3) ";" k4) ";" k5)) \/ ( UsedIntLoc (a6 := a0))) by SF_MASTR: 30

      .= (( UsedILoc (((k2 ";" k3) ";" k4) ";" k5)) \/ {a6, a0}) by SF_MASTR: 14

      .= ((( UsedILoc ((k2 ";" k3) ";" k4)) \/ ( UsedIntLoc k5)) \/ {a6, a0}) by SF_MASTR: 30

      .= ((( UsedILoc ((k2 ";" k3) ";" k4)) \/ {a5, a0}) \/ {a6, a0}) by SF_MASTR: 14

      .= (((( UsedILoc (k2 ";" k3)) \/ ( UsedIntLoc k4)) \/ {a5, a0}) \/ {a6, a0}) by SF_MASTR: 30

      .= (((( UsedILoc (k2 ";" k3)) \/ {a4, a0}) \/ {a5, a0}) \/ {a6, a0}) by SF_MASTR: 14

      .= ((((( UsedIntLoc k2) \/ ( UsedIntLoc k3)) \/ {a4, a0}) \/ {a5, a0}) \/ {a6, a0}) by SF_MASTR: 31

      .= ((((( UsedIntLoc k2) \/ {a3, a0}) \/ {a4, a0}) \/ {a5, a0}) \/ {a6, a0}) by SF_MASTR: 14

      .= (((( {a2, a0} \/ {a3, a0}) \/ {a4, a0}) \/ {a5, a0}) \/ {a6, a0}) by SF_MASTR: 14

      .= ((( {a2, a0} \/ {a3, a0}) \/ {a4, a0}) \/ ( {a5, a0} \/ {a6, a0})) by XBOOLE_1: 4

      .= ((( {a2, a0} \/ {a3, a0}) \/ {a4, a0}) \/ {a0, a5, a6}) by ENUMSET1: 87

      .= (( {a0, a2, a3} \/ {a4, a0}) \/ {a0, a5, a6}) by ENUMSET1: 87

      .= (( {a0, a2, a3} \/ {a4, a0}) \/ ( {a0} \/ {a5, a6})) by ENUMSET1: 2

      .= ((( {a0, a2, a3} \/ {a4, a0}) \/ {a0}) \/ {a5, a6}) by XBOOLE_1: 4

      .= (( {a0, a2, a3} \/ ( {a4, a0} \/ {a0})) \/ {a5, a6}) by XBOOLE_1: 4

      .= (( {a0, a2, a3} \/ {a4, a0, a0}) \/ {a5, a6}) by ENUMSET1: 3

      .= (( {a0, a2, a3} \/ ( {a0, a0} \/ {a4})) \/ {a5, a6}) by ENUMSET1: 2

      .= ((( {a0, a2, a3} \/ {a0, a0}) \/ {a4}) \/ {a5, a6}) by XBOOLE_1: 4

      .= (( {a0, a0, a0, a2, a3} \/ {a4}) \/ {a5, a6}) by ENUMSET1: 8

      .= (( {a0, a2, a3} \/ {a4}) \/ {a5, a6}) by ENUMSET1: 38

      .= ( {a0, a2, a3, a4} \/ {a5, a6}) by ENUMSET1: 6

      .= {a0, a2, a3, a4, a5, a6} by ENUMSET1: 14

      .= ( {a0} \/ {a2, a3, a4, a5, a6}) by ENUMSET1: 11;

      set k7 = (a1 :=len f), Ut = ( UsedILoc ( Times (a1,body1)));

      

      thus ( UsedILoc ( bubble-sort f)) = (( UsedILoc (initializeWorkMem ";" k7)) \/ Ut) by SF_MASTR: 27

      .= ((( UsedILoc initializeWorkMem) \/ ( UsedIntLoc k7)) \/ Ut) by SF_MASTR: 30

      .= ((( {a0} \/ {a2, a3, a4, a5, a6}) \/ {a1}) \/ Ut) by A5, SF_MASTR: 18

      .= ((( {a0} \/ {a1}) \/ {a2, a3, a4, a5, a6}) \/ Ut) by XBOOLE_1: 4

      .= (( {a0, a1} \/ {a2, a3, a4, a5, a6}) \/ Ut) by ENUMSET1: 1

      .= ( {a0, a1, a2, a3, a4, a5, a6} \/ Ut) by ENUMSET1: 17

      .= ( {a0, a1, a2, a3, a4, a5, a6} \/ ( {a1, a0} \/ {a0, a1, a2, a3, a4, a5, a6})) by A4, SCMFSA9A: 44

      .= (( {a0, a1, a2, a3, a4, a5, a6} \/ {a0, a1, a2, a3, a4, a5, a6}) \/ {a1, a0}) by XBOOLE_1: 4

      .= (( {a2, a3, a4, a5, a6} \/ {a0, a1}) \/ {a0, a1}) by ENUMSET1: 17

      .= ( {a2, a3, a4, a5, a6} \/ ( {a0, a1} \/ {a0, a1})) by XBOOLE_1: 4

      .= {a0, a1, a2, a3, a4, a5, a6} by ENUMSET1: 17;

    end;

    theorem :: SCMBSORT:35

    

     Th22: for f be FinSeq-Location holds ( UsedI*Loc ( bubble-sort f)) = {f}

    proof

      let f be FinSeq-Location;

      set i1 = (a4 := a3), i2 = ( SubFrom (a3,a0)), i3 = (a5 := (f,a3)), i4 = (a6 := (f,a4)), i5 = ( SubFrom (a6,a5)), i6 = ((f,a3) := a6), i7 = ((f,a4) := a5), ifc = ( if>0 (a6,((i4 ";" i6) ";" i7),( Stop SCM+FSA ))), Sif = ( UsedI*Loc ifc), body2 = (((((i1 ";" i2) ";" i3) ";" i4) ";" i5) ";" ifc);

      

       A1: Sif = (( UsedI*Loc ((i4 ";" i6) ";" i7)) \/ {} ) by SCMFSA9A: 4, SCMFSA9A: 10

      .= (( UsedI*Loc (i4 ";" i6)) \/ ( UsedInt*Loc i7)) by SF_MASTR: 46

      .= (( UsedI*Loc (i4 ";" i6)) \/ {f}) by SF_MASTR: 33

      .= ((( UsedInt*Loc i4) \/ ( UsedInt*Loc i6)) \/ {f}) by SF_MASTR: 47

      .= ((( UsedInt*Loc i4) \/ {f}) \/ {f}) by SF_MASTR: 33

      .= (( {f} \/ {f}) \/ {f}) by SF_MASTR: 33

      .= {f};

      

       A2: ( UsedI*Loc body2) = (( UsedI*Loc ((((i1 ";" i2) ";" i3) ";" i4) ";" i5)) \/ Sif) by SF_MASTR: 43

      .= ((( UsedI*Loc (((i1 ";" i2) ";" i3) ";" i4)) \/ ( UsedInt*Loc i5)) \/ Sif) by SF_MASTR: 46

      .= ((( UsedI*Loc (((i1 ";" i2) ";" i3) ";" i4)) \/ {} ) \/ Sif) by SF_MASTR: 32

      .= ((( UsedI*Loc ((i1 ";" i2) ";" i3)) \/ ( UsedInt*Loc i4)) \/ Sif) by SF_MASTR: 46

      .= ((( UsedI*Loc ((i1 ";" i2) ";" i3)) \/ {f}) \/ Sif) by SF_MASTR: 33

      .= (( UsedI*Loc ((i1 ";" i2) ";" i3)) \/ ( {f} \/ {f})) by A1, XBOOLE_1: 4

      .= ((( UsedI*Loc (i1 ";" i2)) \/ ( UsedInt*Loc i3)) \/ {f}) by SF_MASTR: 46

      .= ((( UsedI*Loc (i1 ";" i2)) \/ {f}) \/ {f}) by SF_MASTR: 33

      .= (((( UsedInt*Loc i1) \/ ( UsedInt*Loc i2)) \/ {f}) \/ {f}) by SF_MASTR: 47

      .= (((( UsedInt*Loc i1) \/ {} ) \/ {f}) \/ {f}) by SF_MASTR: 32

      .= ((( {} \/ {} ) \/ {f}) \/ {f}) by SF_MASTR: 32

      .= {f};

      set j1 = (a2 := a1), j2 = ( SubFrom (a2,a0)), j3 = (a3 :=len f), Sfor = ( UsedI*Loc ( Times (a2,body2))), body1 = (((j1 ";" j2) ";" j3) ";" ( Times (a2,body2)));

      

       A3: Sfor = {f} by A2, SCMFSA9A: 45;

      

       A4: ( UsedI*Loc body1) = (( UsedI*Loc ((j1 ";" j2) ";" j3)) \/ Sfor) by SF_MASTR: 43

      .= ((( UsedI*Loc (j1 ";" j2)) \/ ( UsedInt*Loc j3)) \/ Sfor) by SF_MASTR: 46

      .= ((( UsedI*Loc (j1 ";" j2)) \/ {f}) \/ Sfor) by SF_MASTR: 34

      .= (((( UsedInt*Loc j1) \/ ( UsedInt*Loc j2)) \/ {f}) \/ Sfor) by SF_MASTR: 47

      .= ((( {} \/ ( UsedInt*Loc j2)) \/ {f}) \/ Sfor) by SF_MASTR: 32

      .= ((( {} \/ {} ) \/ {f}) \/ Sfor) by SF_MASTR: 32

      .= {f} by A3;

      set k2 = (a2 := a0), k3 = (a3 := a0), k4 = (a4 := a0), k5 = (a5 := a0);

      

       A5: ( UsedI*Loc initializeWorkMem) = (( UsedI*Loc (((k2 ";" k3) ";" k4) ";" k5)) \/ ( UsedInt*Loc (a6 := a0))) by SF_MASTR: 46

      .= (( UsedI*Loc (((k2 ";" k3) ";" k4) ";" k5)) \/ {} ) by SF_MASTR: 32

      .= (( UsedI*Loc ((k2 ";" k3) ";" k4)) \/ ( UsedInt*Loc k5)) by SF_MASTR: 46

      .= (( UsedI*Loc ((k2 ";" k3) ";" k4)) \/ {} ) by SF_MASTR: 32

      .= (( UsedI*Loc (k2 ";" k3)) \/ ( UsedInt*Loc k4)) by SF_MASTR: 46

      .= (( UsedI*Loc (k2 ";" k3)) \/ {} ) by SF_MASTR: 32

      .= (( UsedInt*Loc k2) \/ ( UsedInt*Loc k3)) by SF_MASTR: 47

      .= (( UsedInt*Loc k2) \/ {} ) by SF_MASTR: 32

      .= {} by SF_MASTR: 32;

      set k7 = (a1 :=len f), Ut = ( UsedI*Loc ( Times (a1,body1)));

      

      thus ( UsedI*Loc ( bubble-sort f)) = (( UsedI*Loc (initializeWorkMem ";" k7)) \/ Ut) by SF_MASTR: 43

      .= ((( UsedI*Loc initializeWorkMem) \/ ( UsedInt*Loc k7)) \/ Ut) by SF_MASTR: 46

      .= ( {f} \/ Ut) by A5, SF_MASTR: 34

      .= ( {f} \/ {f}) by A4, SCMFSA9A: 45

      .= {f};

    end;

    ::$Canceled

    theorem :: SCMBSORT:38

    

     Th23: for f be FinSeq-Location holds ( card ( bubble-sort f)) = 53

    proof

      let f be FinSeq-Location;

      set i1 = (a4 := a3), i2 = ( SubFrom (a3,a0)), i3 = (a5 := (f,a3)), i4 = (a6 := (f,a4)), i5 = ( SubFrom (a6,a5)), i6 = ((f,a3) := a6), i7 = ((f,a4) := a5), ifc = ( if>0 (a6,((i4 ";" i6) ";" i7),( Stop SCM+FSA ))), Cif = ( card ifc), body2 = (((((i1 ";" i2) ";" i3) ";" i4) ";" i5) ";" ifc);

      ( card ( Stop SCM+FSA )) = 1 by COMPOS_1: 4;

      

      then

       A1: Cif = ((( card ((i4 ";" i6) ";" i7)) + 1) + 4) by SCMFSA8B: 12

      .= ((6 + 1) + 4) by Th15

      .= 11;

      

       A2: ( card body2) = (( card ((((i1 ";" i2) ";" i3) ";" i4) ";" i5)) + Cif) by SCMFSA6A: 21

      .= (( card (((i1 ";" i2) ";" i3) ";" (i4 ";" i5))) + Cif) by SCMFSA6A: 28

      .= ((( card ((i1 ";" i2) ";" i3)) + ( card (i4 ";" i5))) + Cif) by SCMFSA6A: 21

      .= ((6 + ( card (i4 ";" i5))) + Cif) by Th15

      .= ((6 + 4) + Cif) by SCMFSA6A: 35

      .= 21 by A1;

      set j1 = (a2 := a1), j2 = ( SubFrom (a2,a0)), j3 = (a3 :=len f), body1 = (((j1 ";" j2) ";" j3) ";" ( Times (a2,body2)));

      

       A3: ( card body1) = (( card ((j1 ";" j2) ";" j3)) + ( card ( Times (a2,body2)))) by SCMFSA6A: 21

      .= (6 + ( card ( Times (a2,body2)))) by Th15

      .= (6 + (21 + 7)) by A2, SCMFSA8C: 94

      .= 34;

      set k2 = (a2 := a0), k3 = (a3 := a0), k4 = (a4 := a0), k5 = (a5 := a0), k6 = (a6 := a0);

      

       A4: ( card initializeWorkMem) = (( card (((k2 ";" k3) ";" k4) ";" k5)) + 2) by SCMFSA6A: 34

      .= ((( card ((k2 ";" k3) ";" k4)) + 2) + 2) by SCMFSA6A: 34

      .= (( card ((k2 ";" k3) ";" k4)) + 4)

      .= (6 + 4) by Th15

      .= 10;

      set k7 = (a1 :=len f), Ct = ( card ( Times (a1,body1)));

      

       A5: Ct = (34 + 7) by A3, SCMFSA8C: 94;

      

      thus ( card ( bubble-sort f)) = (( card (initializeWorkMem ";" k7)) + Ct) by SCMFSA6A: 21

      .= ((10 + 2) + Ct) by A4, SCMFSA6A: 34

      .= 53 by A5;

    end;

    theorem :: SCMBSORT:39

    

     Th24: for P be Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds for f be FinSeq-Location, k be Nat st k < 53 holds ( Bubble-Sort-Algorithm . k) = (P . k)

    proof

      let P be Instruction-Sequence of SCM+FSA such that

       A1: Bubble-Sort-Algorithm c= P;

      let f be FinSeq-Location, k be Nat;

      assume

       A2: k < 53;

      ( card ( bubble-sort f0)) = 53 by Th23;

      then k in ( dom Bubble-Sort-Algorithm ) by A2, AFINSQ_1: 66;

      hence ( Bubble-Sort-Algorithm . k) = (P . k) by A1, GRFUNC_1: 2;

    end;

    

     Lm20: for P be Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds (P . 0 ) = (a2 := a0) & (P . 1) = ( goto 2) & (P . 2) = (a3 := a0) & (P . 3) = ( goto 4) & (P . 4) = (a4 := a0) & (P . 5) = ( goto 6) & (P . 6) = (a5 := a0) & (P . 7) = ( goto 8) & (P . 8) = (a6 := a0) & (P . 9) = ( goto 10) & (P . 10) = (a1 :=len ( fsloc 0 )) & (P . 11) = ( goto 12)

    proof

      set f0 = ( fsloc 0 ), TT = ( Times (a1,((((a2 := a1) ";" ( SubFrom (a2,a0))) ";" (a3 :=len f0)) ";" ( Times (a2,((((((a4 := a3) ";" ( SubFrom (a3,a0))) ";" (a5 := (f0,a3))) ";" (a6 := (f0,a4))) ";" ( SubFrom (a6,a5))) ";" ( if>0 (a6,(((a6 := (f0,a4)) ";" ((f0,a3) := a6)) ";" ((f0,a4) := a5)),( Stop SCM+FSA )))))))));

      set q = Bubble-Sort-Algorithm ;

      let P be Instruction-Sequence of SCM+FSA such that

       A1: q c= P;

      set W2 = (a2 := a0), W3 = (a3 := a0), W4 = (a4 := a0), W5 = (a5 := a0), W6 = (a6 := a0), W7 = (a1 :=len f0), T7 = (W7 ";" TT), T6 = (W6 ";" T7), T5 = (W5 ";" T6), T4 = (W4 ";" T5), T3 = (W3 ";" T4), X3 = (W2 ";" W3), X4 = (X3 ";" W4), X5 = (X4 ";" W5), X6 = (X5 ";" W6);

      

       A2: q = ((X5 ";" W6) ";" T7) by SCMFSA6A: 27;

      then

       A3: q = ((X4 ";" W5) ";" T6) by SCMFSA6A: 27;

      then

       A4: q = ((X3 ";" W4) ";" T5) by SCMFSA6A: 27;

      then q = ((W2 ";" W3) ";" T4) by SCMFSA6A: 27;

      then q = (W2 ";" T3) by SCMFSA6A: 31;

      then

       A5: q = (( Macro W2) ";" T3) by SCMFSA6A:def 5;

      

       A6: q = ((( Macro W2) ";" W3) ";" T4) by A5, SCMFSA6A: 27;

      

       A7: ( dom ( Macro W2)) = { 0 , 1} by COMPOS_1: 61;

      then

       A8: 0 in ( dom ( Macro W2)) by TARSKI:def 2;

      

       A9: 1 in ( dom ( Macro W2)) by A7, TARSKI:def 2;

      

      thus (P . 0 ) = (q . 0 ) by A1, Th24

      .= (( Directed ( Macro W2)) . 0 ) by A8, A5, SCMFSA8A: 14

      .= W2 by SCMFSA7B: 1;

      

      thus (P . 1) = (q . 1) by A1, Th24

      .= (( Directed ( Macro W2)) . 1) by A9, A5, SCMFSA8A: 14

      .= ( goto 2) by SCMFSA7B: 2;

      

       A10: ( card ( Macro W2)) = 2 by COMPOS_1: 56;

      

      thus (P . 2) = (q . 2) by A1, Th24

      .= W3 by A6, A10, Th17;

      

      thus (P . 3) = (q . (2 + 1)) by A1, Th24

      .= ( goto (2 + 2)) by A6, A10, Th18

      .= ( goto 4);

      

       A11: ( card X3) = 4 by SCMFSA6A: 35;

      

      thus (P . 4) = (q . 4) by A1, Th24

      .= W4 by A4, A11, Th17;

      

      thus (P . 5) = (q . (4 + 1)) by A1, Th24

      .= ( goto (4 + 2)) by A4, A11, Th18

      .= ( goto 6);

      

       A12: ( card X4) = 6 by Th15;

      

      thus (P . 6) = (q . 6) by A1, Th24

      .= W5 by A3, A12, Th17;

      

      thus (P . 7) = (q . (6 + 1)) by A1, Th24

      .= ( goto (6 + 2)) by A3, A12, Th18

      .= ( goto 8);

      

       A13: ( card X5) = (6 + 2) by A12, SCMFSA6A: 34;

      

      thus (P . 8) = (q . 8) by A1, Th24

      .= W6 by A2, A13, Th17;

      

      thus (P . 9) = (q . (8 + 1)) by A1, Th24

      .= ( goto (8 + 2)) by A2, A13, Th18

      .= ( goto 10);

      

       A14: ( card X6) = (8 + 2) by A13, SCMFSA6A: 34;

      

      thus (P . 10) = (q . 10) by A1, Th24

      .= W7 by A14, Th17;

      

      thus (P . 11) = (q . (10 + 1)) by A1, Th24

      .= ( goto (10 + 2)) by A14, Th18

      .= ( goto 12);

    end;

    

     Lm21: for s be 0 -started State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds (( Comput (P,s,1)) . ( IC SCM+FSA )) = 1 & (( Comput (P,s,1)) . a0) = (s . a0) & (( Comput (P,s,1)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,2)) . ( IC SCM+FSA )) = 2 & (( Comput (P,s,2)) . a0) = (s . a0) & (( Comput (P,s,2)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,3)) . ( IC SCM+FSA )) = 3 & (( Comput (P,s,3)) . a0) = (s . a0) & (( Comput (P,s,3)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,4)) . ( IC SCM+FSA )) = 4 & (( Comput (P,s,4)) . a0) = (s . a0) & (( Comput (P,s,4)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,5)) . ( IC SCM+FSA )) = 5 & (( Comput (P,s,5)) . a0) = (s . a0) & (( Comput (P,s,5)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,6)) . ( IC SCM+FSA )) = 6 & (( Comput (P,s,6)) . a0) = (s . a0) & (( Comput (P,s,6)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,7)) . ( IC SCM+FSA )) = 7 & (( Comput (P,s,7)) . a0) = (s . a0) & (( Comput (P,s,7)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,8)) . ( IC SCM+FSA )) = 8 & (( Comput (P,s,8)) . a0) = (s . a0) & (( Comput (P,s,8)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,9)) . ( IC SCM+FSA )) = 9 & (( Comput (P,s,9)) . a0) = (s . a0) & (( Comput (P,s,9)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,10)) . ( IC SCM+FSA )) = 10 & (( Comput (P,s,10)) . a0) = (s . a0) & (( Comput (P,s,10)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,11)) . ( IC SCM+FSA )) = 11 & (( Comput (P,s,11)) . a0) = (s . a0) & (( Comput (P,s,11)) . ( fsloc 0 )) = (s . ( fsloc 0 )) & (( Comput (P,s,11)) . a1) = ( len (s . ( fsloc 0 ))) & (( Comput (P,s,11)) . a2) = (s . a0) & (( Comput (P,s,11)) . a3) = (s . a0) & (( Comput (P,s,11)) . a4) = (s . a0) & (( Comput (P,s,11)) . a5) = (s . a0) & (( Comput (P,s,11)) . a6) = (s . a0)

    proof

      let s be 0 -started State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA such that

       A1: Bubble-Sort-Algorithm c= P;

      

       A2: ( IC ( Comput (P,s, 0 ))) = 0 by MEMSTR_0:def 11;

      

      then

       A3: ( Comput (P,s,( 0 + 1))) = ( Exec ((P . 0 ),( Comput (P,s, 0 )))) by EXTPRO_1: 6

      .= ( Exec ((a2 := a0),( Comput (P,s, 0 )))) by A1, Lm20;

      

      hence (( Comput (P,s,1)) . ( IC SCM+FSA )) = (( IC ( Comput (P,s, 0 ))) + 1) by SCMFSA_2: 63

      .= 1 by A2;

      then

       A4: ( IC ( Comput (P,s,1))) = 1;

      

       A5: (( Comput (P,s,1)) . a2) = (s . a0) by A3, SCMFSA_2: 63;

      thus

       A6: (( Comput (P,s,1)) . a0) = (s . a0) by A3, Lm1, SCMFSA_2: 63;

      thus

       A7: (( Comput (P,s,1)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A3, SCMFSA_2: 63;

      

       A8: ( Comput (P,s,(1 + 1))) = ( Exec ((P . 1),( Comput (P,s,1)))) by A4, EXTPRO_1: 6

      .= ( Exec (( goto 2),( Comput (P,s,1)))) by A1, Lm20;

      hence

       A9: (( Comput (P,s,2)) . ( IC SCM+FSA )) = 2 by SCMFSA_2: 69;

      

       A10: ( IC ( Comput (P,s,2))) = 2 by A8, SCMFSA_2: 69;

      thus

       A11: (( Comput (P,s,2)) . a0) = (s . a0) by A6, A8, SCMFSA_2: 69;

      thus

       A12: (( Comput (P,s,2)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A7, A8, SCMFSA_2: 69;

      

       A13: (( Comput (P,s,2)) . a2) = (s . a0) by A5, A8, SCMFSA_2: 69;

      

       A14: ( Comput (P,s,(2 + 1))) = ( Exec ((P . 2),( Comput (P,s,2)))) by A10, EXTPRO_1: 6

      .= ( Exec ((a3 := a0),( Comput (P,s,2)))) by A1, Lm20;

      

      hence (( Comput (P,s,3)) . ( IC SCM+FSA )) = (( IC ( Comput (P,s,2))) + 1) by SCMFSA_2: 63

      .= 3 by A9;

      then

       A15: ( IC ( Comput (P,s,3))) = 3;

      

       A16: (( Comput (P,s,3)) . a3) = (s . a0) by A11, A14, SCMFSA_2: 63;

      thus

       A17: (( Comput (P,s,3)) . a0) = (s . a0) by A11, A14, SCMFSA_2: 63;

      thus

       A18: (( Comput (P,s,3)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A12, A14, SCMFSA_2: 63;

      

       A19: (( Comput (P,s,3)) . a2) = (s . a0) by A13, A14, Lm10, SCMFSA_2: 63;

      

       A20: ( Comput (P,s,(3 + 1))) = ( Exec ((P . 3),( Comput (P,s,3)))) by A15, EXTPRO_1: 6

      .= ( Exec (( goto 4),( Comput (P,s,3)))) by A1, Lm20;

      hence

       A21: (( Comput (P,s,4)) . ( IC SCM+FSA )) = 4 by SCMFSA_2: 69;

      

       A22: ( IC ( Comput (P,s,4))) = 4 by A20, SCMFSA_2: 69;

      thus

       A23: (( Comput (P,s,4)) . a0) = (s . a0) by A17, A20, SCMFSA_2: 69;

      thus

       A24: (( Comput (P,s,4)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A18, A20, SCMFSA_2: 69;

      

       A25: (( Comput (P,s,4)) . a2) = (s . a0) by A19, A20, SCMFSA_2: 69;

      

       A26: (( Comput (P,s,4)) . a3) = (s . a0) by A16, A20, SCMFSA_2: 69;

      

       A27: ( Comput (P,s,(4 + 1))) = ( Exec ((P . 4),( Comput (P,s,4)))) by A22, EXTPRO_1: 6

      .= ( Exec ((a4 := a0),( Comput (P,s,4)))) by A1, Lm20;

      

      hence (( Comput (P,s,5)) . ( IC SCM+FSA )) = (( IC ( Comput (P,s,4))) + 1) by SCMFSA_2: 63

      .= 5 by A21;

      then

       A28: ( IC ( Comput (P,s,5))) = 5;

      

       A29: (( Comput (P,s,5)) . a4) = (s . a0) by A23, A27, SCMFSA_2: 63;

      thus

       A30: (( Comput (P,s,5)) . a0) = (s . a0) by A23, A27, Lm2, SCMFSA_2: 63;

      thus

       A31: (( Comput (P,s,5)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A24, A27, SCMFSA_2: 63;

      

       A32: (( Comput (P,s,5)) . a2) = (s . a0) by A25, A27, Lm11, SCMFSA_2: 63;

      

       A33: (( Comput (P,s,5)) . a3) = (s . a0) by A26, A27, Lm14, SCMFSA_2: 63;

      

       A34: ( Comput (P,s,(5 + 1))) = ( Exec ((P . 5),( Comput (P,s,5)))) by A28, EXTPRO_1: 6

      .= ( Exec (( goto 6),( Comput (P,s,5)))) by A1, Lm20;

      hence

       A35: (( Comput (P,s,6)) . ( IC SCM+FSA )) = 6 by SCMFSA_2: 69;

      

       A36: ( IC ( Comput (P,s,6))) = 6 by A34, SCMFSA_2: 69;

      thus

       A37: (( Comput (P,s,6)) . a0) = (s . a0) by A30, A34, SCMFSA_2: 69;

      thus

       A38: (( Comput (P,s,6)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A31, A34, SCMFSA_2: 69;

      

       A39: (( Comput (P,s,6)) . a2) = (s . a0) by A32, A34, SCMFSA_2: 69;

      

       A40: (( Comput (P,s,6)) . a3) = (s . a0) by A33, A34, SCMFSA_2: 69;

      

       A41: (( Comput (P,s,6)) . a4) = (s . a0) by A29, A34, SCMFSA_2: 69;

      

       A42: ( Comput (P,s,(6 + 1))) = ( Exec ((P . 6),( Comput (P,s,6)))) by A36, EXTPRO_1: 6

      .= ( Exec ((a5 := a0),( Comput (P,s,6)))) by A1, Lm20;

      

      hence (( Comput (P,s,7)) . ( IC SCM+FSA )) = (( IC ( Comput (P,s,6))) + 1) by SCMFSA_2: 63

      .= 7 by A35;

      then

       A43: ( IC ( Comput (P,s,7))) = 7;

      

       A44: (( Comput (P,s,7)) . a5) = (s . a0) by A37, A42, SCMFSA_2: 63;

      thus

       A45: (( Comput (P,s,7)) . a0) = (s . a0) by A37, A42, Lm3, SCMFSA_2: 63;

      thus

       A46: (( Comput (P,s,7)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A38, A42, SCMFSA_2: 63;

      

       A47: (( Comput (P,s,7)) . a2) = (s . a0) by A39, A42, Lm12, SCMFSA_2: 63;

      

       A48: (( Comput (P,s,7)) . a3) = (s . a0) by A40, A42, Lm15, SCMFSA_2: 63;

      

       A49: (( Comput (P,s,7)) . a4) = (s . a0) by A41, A42, Lm17, SCMFSA_2: 63;

      

       A50: ( Comput (P,s,(7 + 1))) = ( Exec ((P . 7),( Comput (P,s,7)))) by A43, EXTPRO_1: 6

      .= ( Exec (( goto 8),( Comput (P,s,7)))) by A1, Lm20;

      hence

       A51: (( Comput (P,s,8)) . ( IC SCM+FSA )) = 8 by SCMFSA_2: 69;

      

       A52: ( IC ( Comput (P,s,8))) = 8 by A50, SCMFSA_2: 69;

      thus

       A53: (( Comput (P,s,8)) . a0) = (s . a0) by A45, A50, SCMFSA_2: 69;

      thus

       A54: (( Comput (P,s,8)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A46, A50, SCMFSA_2: 69;

      

       A55: (( Comput (P,s,8)) . a2) = (s . a0) by A47, A50, SCMFSA_2: 69;

      

       A56: (( Comput (P,s,8)) . a3) = (s . a0) by A48, A50, SCMFSA_2: 69;

      

       A57: (( Comput (P,s,8)) . a4) = (s . a0) by A49, A50, SCMFSA_2: 69;

      

       A58: (( Comput (P,s,8)) . a5) = (s . a0) by A44, A50, SCMFSA_2: 69;

      

       A59: ( Comput (P,s,(8 + 1))) = ( Exec ((P . 8),( Comput (P,s,8)))) by A52, EXTPRO_1: 6

      .= ( Exec ((a6 := a0),( Comput (P,s,8)))) by A1, Lm20;

      

      hence (( Comput (P,s,9)) . ( IC SCM+FSA )) = (( IC ( Comput (P,s,8))) + 1) by SCMFSA_2: 63

      .= 9 by A51;

      then

       A60: ( IC ( Comput (P,s,9))) = 9;

      

       A61: (( Comput (P,s,9)) . a6) = (s . a0) by A53, A59, SCMFSA_2: 63;

      thus

       A62: (( Comput (P,s,9)) . a0) = (s . a0) by A53, A59, Lm4, SCMFSA_2: 63;

      thus

       A63: (( Comput (P,s,9)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A54, A59, SCMFSA_2: 63;

      

       A64: (( Comput (P,s,9)) . a2) = (s . a0) by A55, A59, Lm13, SCMFSA_2: 63;

      

       A65: (( Comput (P,s,9)) . a3) = (s . a0) by A56, A59, Lm16, SCMFSA_2: 63;

      

       A66: (( Comput (P,s,9)) . a4) = (s . a0) by A57, A59, Lm18, SCMFSA_2: 63;

      

       A67: (( Comput (P,s,9)) . a5) = (s . a0) by A58, A59, Lm19, SCMFSA_2: 63;

      

       A68: ( Comput (P,s,(9 + 1))) = ( Exec ((P . 9),( Comput (P,s,9)))) by A60, EXTPRO_1: 6

      .= ( Exec (( goto 10),( Comput (P,s,9)))) by A1, Lm20;

      hence

       A69: (( Comput (P,s,10)) . ( IC SCM+FSA )) = 10 by SCMFSA_2: 69;

      

       A70: ( IC ( Comput (P,s,10))) = 10 by A68, SCMFSA_2: 69;

      thus

       A71: (( Comput (P,s,10)) . a0) = (s . a0) by A62, A68, SCMFSA_2: 69;

      thus

       A72: (( Comput (P,s,10)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A63, A68, SCMFSA_2: 69;

      

       A73: (( Comput (P,s,10)) . a2) = (s . a0) by A64, A68, SCMFSA_2: 69;

      

       A74: (( Comput (P,s,10)) . a3) = (s . a0) by A65, A68, SCMFSA_2: 69;

      

       A75: (( Comput (P,s,10)) . a4) = (s . a0) by A66, A68, SCMFSA_2: 69;

      

       A76: (( Comput (P,s,10)) . a5) = (s . a0) by A67, A68, SCMFSA_2: 69;

      

       A77: (( Comput (P,s,10)) . a6) = (s . a0) by A61, A68, SCMFSA_2: 69;

      

       A78: ( Comput (P,s,(10 + 1))) = ( Exec ((P . 10),( Comput (P,s,10)))) by A70, EXTPRO_1: 6

      .= ( Exec ((a1 :=len ( fsloc 0 )),( Comput (P,s,10)))) by A1, Lm20;

      

      hence (( Comput (P,s,11)) . ( IC SCM+FSA )) = (( IC ( Comput (P,s,10))) + 1) by SCMFSA_2: 74

      .= 11 by A69;

      thus (( Comput (P,s,11)) . a0) = (s . a0) by A71, A78, SCMFSA_2: 74;

      thus (( Comput (P,s,11)) . ( fsloc 0 )) = (s . ( fsloc 0 )) by A72, A78, SCMFSA_2: 74;

      thus (( Comput (P,s,11)) . a1) = ( len (s . ( fsloc 0 ))) by A72, A78, SCMFSA_2: 74;

      thus (( Comput (P,s,11)) . a2) = (s . a0) by A73, A78, Lm5, SCMFSA_2: 74;

      thus (( Comput (P,s,11)) . a3) = (s . a0) by A74, A78, Lm6, SCMFSA_2: 74;

      thus (( Comput (P,s,11)) . a4) = (s . a0) by A75, A78, Lm7, SCMFSA_2: 74;

      thus (( Comput (P,s,11)) . a5) = (s . a0) by A76, A78, Lm8, SCMFSA_2: 74;

      thus thesis by A77, A78, Lm9, SCMFSA_2: 74;

    end;

    

     Lm22: not body2 destroys b2

    proof

      

       A1: not i1 destroys b2 by SCMFSA7B: 6, SCMFSA_2: 101;

      

       A2: not i2 destroys b2 by SCMFSA7B: 8, SCMFSA_2: 101;

      

       A3: not i3 destroys b2 by SCMFSA7B: 14, SCMFSA_2: 101;

      

       A4: not i4 destroys b2 by SCMFSA7B: 14, SCMFSA_2: 101;

      

       A5: not i6 destroys b2 by SCMFSA7B: 15;

      

       A6: not i7 destroys b2 by SCMFSA7B: 15;

      

       A7: not SS destroys b2 by SCMFSA8C: 56;

       not ((i4 ";" i6) ";" i7) destroys b2 by A4, A5, A6, SCMFSA8C: 54, SCMFSA8C: 55;

      then

       A8: not ifc destroys b2 by A7, SCMFSA8C: 88;

       not ((i1 ";" i2) ";" i3) destroys b2 by A1, A2, A3, SCMFSA8C: 54, SCMFSA8C: 55;

      then not (((i1 ";" i2) ";" i3) ";" i4) destroys b2 by Lm13, SCMFSA7B: 14, SCMFSA8C: 54;

      then not ((((i1 ";" i2) ";" i3) ";" i4) ";" i5) destroys b2 by Lm13, SCMFSA7B: 8, SCMFSA8C: 54;

      hence thesis by A8, SCMFSA8C: 52;

    end;

    

     Lm23: ( Times (b2,body2)) is good InitHalting

    proof

      thus ( Times (b2,body2)) is good;

      let s be State of SCM+FSA such that

       A1: ( Initialize (( intloc 0 ) .--> 1)) c= s;

      let P be Instruction-Sequence of SCM+FSA such that

       A2: ( Times (b2,body2)) c= P;

      

       A3: (P +* ( Times (b2,body2))) = P by A2, FUNCT_4: 98;

      

       A5: ( dom (( intloc 0 ) .--> 1)) misses {( IC SCM+FSA )} by SCMFSA_2: 56, ZFMISC_1: 11;

      ( Start-At ( 0 , SCM+FSA )) c= ( Initialize (( intloc 0 ) .--> 1)) by FUNCT_4: 25;

      then

       A6: s = ( Initialize s) by A1, FUNCT_4: 98, XBOOLE_1: 1;

      

       A7: ( intloc 0 ) in ( dom (( intloc 0 ) .--> 1)) by TARSKI:def 1;

      ( dom (( intloc 0 ) .--> 1)) misses ( dom ( Start-At ( 0 , SCM+FSA ))) by A5;

      then (( intloc 0 ) .--> 1) c= ( Initialize (( intloc 0 ) .--> 1)) by FUNCT_4: 32;

      then (( intloc 0 ) .--> 1) c= s by A1, XBOOLE_1: 1;

      

      then

       A8: (s . ( intloc 0 )) = ((( intloc 0 ) .--> 1) . ( intloc 0 )) by A7, GRFUNC_1: 2

      .= 1 by FUNCOP_1: 72;

      ( Times (b2,body2)) is_halting_on (s,P) by Lm22, A8, SCM_HALT: 62, A6;

      hence P halts_on s by A6, A3, SCMFSA7B:def 7;

    end;

    

     Lm24: not body2 destroys b1

    proof

      

       A1: not i1 destroys b1 by SCMFSA7B: 6, SCMFSA_2: 101;

      

       A2: not i2 destroys b1 by SCMFSA7B: 8, SCMFSA_2: 101;

      

       A3: not i3 destroys b1 by SCMFSA7B: 14, SCMFSA_2: 101;

      

       A4: not i4 destroys b1 by SCMFSA7B: 14, SCMFSA_2: 101;

      

       A5: not i6 destroys b1 by SCMFSA7B: 15;

      

       A6: not i7 destroys b1 by SCMFSA7B: 15;

      

       A7: not SS destroys b1 by SCMFSA8C: 56;

       not ((i4 ";" i6) ";" i7) destroys b1 by A4, A5, A6, SCMFSA8C: 54, SCMFSA8C: 55;

      then

       A8: not ifc destroys b1 by A7, SCMFSA8C: 88;

       not ((i1 ";" i2) ";" i3) destroys b1 by A1, A2, A3, SCMFSA8C: 54, SCMFSA8C: 55;

      then not (((i1 ";" i2) ";" i3) ";" i4) destroys b1 by Lm9, SCMFSA7B: 14, SCMFSA8C: 54;

      then not ((((i1 ";" i2) ";" i3) ";" i4) ";" i5) destroys b1 by Lm9, SCMFSA7B: 8, SCMFSA8C: 54;

      hence thesis by A8, SCMFSA8C: 52;

    end;

    

     Lm25: not body1 destroys b1

    proof

      

       A1: not j1 destroys b1 by SCMFSA7B: 6, SCMFSA_2: 101;

      

       A2: not j2 destroys b1 by SCMFSA7B: 8, SCMFSA_2: 101;

      

       A3: not j3 destroys b1 by SCMFSA7B: 16, SCMFSA_2: 101;

      

       A4: not T2 destroys b1 by Lm24, SCMFSA8C: 93, SCMFSA_2: 101;

       not ((j1 ";" j2) ";" j3) destroys b1 by A1, A2, A3, SCMFSA8C: 54, SCMFSA8C: 55;

      hence thesis by A4, SCMFSA8C: 52;

    end;

    

     Lm26: ( Times (b1,body1)) is good InitHalting

    proof

      thus ( Times (b1,body1)) is good;

      let s be State of SCM+FSA such that

       A1: ( Initialize (( intloc 0 ) .--> 1)) c= s;

      let P be Instruction-Sequence of SCM+FSA such that

       A2: ( Times (b1,body1)) c= P;

      

       A3: (P +* ( Times (b1,body1))) = P by A2, FUNCT_4: 98;

      

       A5: ( dom (( intloc 0 ) .--> 1)) misses {( IC SCM+FSA )} by SCMFSA_2: 56, ZFMISC_1: 11;

      ( Start-At ( 0 , SCM+FSA )) c= ( Initialize (( intloc 0 ) .--> 1)) by FUNCT_4: 25;

      then

       A6: s = ( Initialize s) by A1, FUNCT_4: 98, XBOOLE_1: 1;

      

       A7: ( intloc 0 ) in ( dom (( intloc 0 ) .--> 1)) by TARSKI:def 1;

      ( dom (( intloc 0 ) .--> 1)) misses ( dom ( Start-At ( 0 , SCM+FSA ))) by A5;

      then (( intloc 0 ) .--> 1) c= ( Initialize (( intloc 0 ) .--> 1)) by FUNCT_4: 32;

      then (( intloc 0 ) .--> 1) c= s by A1, XBOOLE_1: 1;

      

      then

       A8: (s . ( intloc 0 )) = ((( intloc 0 ) .--> 1) . ( intloc 0 )) by A7, GRFUNC_1: 2

      .= 1 by FUNCOP_1: 72;

      reconsider TT = T2 as good InitHalting Program of SCM+FSA by Lm23;

      body1 = (((j1 ";" j2) ";" j3) ";" TT);

      then ( Times (b1,body1)) is_halting_on (s,P) by Lm25, A8, SCM_HALT: 62, A6;

      hence P halts_on s by A6, A3, SCMFSA7B:def 7;

    end;

    theorem :: SCMBSORT:40

    ( bubble-sort ( fsloc 0 )) is keepInt0_1 InitHalting by Lm26;

    

     Lm27: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA holds ((s . b6) > 0 implies (( IExec (ifc,p,s)) . f0) = (((s . f0) +* ( |.(s . b3).|,((s . f0) /. |.(s . b4).|))) +* ( |.(s . b4).|,(s . b5)))) & ((s . b6) <= 0 implies (( IExec (ifc,p,s)) . f0) = (s . f0))

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      set s0 = ( Initialized s), s1 = ( Exec (i4,s0)), s2 = ( IExec ((i4 ";" i6),p,s));

      

       A1: (s0 . f0) = (s . f0) by SCMFSA_M: 37;

      (s0 . b4) = (s . b4) by SCMFSA_M: 37;

      then

       A2: (s1 . b6) = ((s . f0) /. |.(s . b4).|) by A1, Th1;

      

       A3: (s1 . f0) = (s . f0) by A1, SCMFSA_2: 72;

      

       A4: (s1 . b3) = (s . b3) by Th3;

      

       A5: (s1 . b4) = (s . b4) by Th3;

      

       A6: (s1 . b5) = (s . b5) by Th3;

      

       A7: (s2 . f0) = (( Exec (i6,s1)) . f0) by SCMFSA6C: 9

      .= ((s . f0) +* ( |.(s . b3).|,((s . f0) /. |.(s . b4).|))) by A2, A3, A4, Th2;

      

       A8: (s2 . b4) = (( Exec (i6,s1)) . b4) by SCMFSA6C: 8

      .= (s . b4) by A5, SCMFSA_2: 73;

      

       A9: (s2 . b5) = (( Exec (i6,s1)) . b5) by SCMFSA6C: 8

      .= (s . b5) by A6, SCMFSA_2: 73;

      set I = ((i4 ";" i6) ";" i7), J = ( Stop SCM+FSA );

      hereby

        assume (s . b6) > 0 ;

        

        hence (( IExec (( if>0 (b6,I,J)),p,s)) . f0) = (( IExec (I,p,s)) . f0) by SCM_HALT: 44

        .= (( Exec (i7,s2)) . f0) by SCMFSA6C: 7

        .= (((s . f0) +* ( |.(s . b3).|,((s . f0) /. |.(s . b4).|))) +* ( |.(s . b4).|,(s . b5))) by A7, A8, A9, Th2;

      end;

      assume (s . b6) <= 0 ;

      

      hence (( IExec (( if>0 (b6,I,J)),p,s)) . f0) = (( IExec (J,p,s)) . f0) by SCM_HALT: 44

      .= (s . f0) by Th5;

    end;

    

     Lm28: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA holds (( IExec (ifc,p,s)) . b3) = (s . b3)

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      set s1 = ( Exec (i4,( Initialized s))), s2 = ( IExec ((i4 ";" i6),p,s));

      

       A1: (s1 . b3) = (s . b3) by Th3;

      

       A2: (s2 . b3) = (( Exec (i6,s1)) . b3) by SCMFSA6C: 8

      .= (s . b3) by A1, SCMFSA_2: 73;

      per cases ;

        suppose (s . b6) > 0 ;

        

        hence (( IExec (ifc,p,s)) . b3) = (( IExec (((i4 ";" i6) ";" i7),p,s)) . b3) by SCM_HALT: 44

        .= (( Exec (i7,s2)) . b3) by SCMFSA6C: 6

        .= (s . b3) by A2, SCMFSA_2: 73;

      end;

        suppose (s . b6) <= 0 ;

        

        hence (( IExec (ifc,p,s)) . b3) = (( IExec (( Stop SCM+FSA ),p,s)) . b3) by SCM_HALT: 44

        .= (s . b3) by Th5;

      end;

    end;

    

     Lm29: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA st (s . b3) <= ( len (s . f0)) & (s . b3) >= 2 holds (( IExec (body2,p,s)) . b3) = ((s . b3) - 1) & ((s . f0),(( IExec (body2,p,s)) . f0)) are_fiberwise_equipotent & (((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) or ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1))) & (((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) or ((s . f0) . ((s . b3) - 1)) = ((( IExec (body2,p,s)) . f0) . (s . b3))) & (((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) or ((s . f0) . ((s . b3) - 1)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1))) & (for k be set st k <> ((s . b3) - 1) & k <> (s . b3) & k in ( dom (s . f0)) holds ((s . f0) . k) = ((( IExec (body2,p,s)) . f0) . k)) & ex x1,x2 be Integer st x1 = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) & x2 = ((( IExec (body2,p,s)) . f0) . (s . b3)) & x1 >= x2

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      assume that

       A1: (s . b3) <= ( len (s . f0)) and

       A2: (s . b3) >= 2;

      

       A3: ((s . b3) - 1) >= (2 - 1) by A2, XREAL_1: 9;

      then

       A4: |.((s . b3) - 1).| = ((s . b3) - 1) by ABSVALUE:def 1;

      

       A5: ((s . b3) - 1) <= ( len (s . f0)) by A1, XREAL_1: 146, XXREAL_0: 2;

      

       A6: (s . b3) >= 1 by A2, XXREAL_0: 2;

      

       A7: |.(s . b3).| = (s . b3) by A2, ABSVALUE:def 1;

      reconsider k1 = ((s . b3) - 1) as Element of NAT by A3, INT_1: 3;

      reconsider k2 = (s . b3) as Element of NAT by A2, INT_1: 3;

      

       A8: k1 in ( dom (s . f0)) by A3, A5, FINSEQ_3: 25;

      reconsider n1 = ((s . f0) . k1) as Integer;

      

       A9: k2 in ( dom (s . f0)) by A1, A6, FINSEQ_3: 25;

      reconsider n2 = ((s . f0) . k2) as Integer;

      set s0 = ( Initialized s), s1 = ( Exec (i1,s0)), s2 = ( IExec ((i1 ";" i2),p,s)), s3 = ( IExec (((i1 ";" i2) ";" i3),p,s)), s4 = ( IExec ((((i1 ";" i2) ";" i3) ";" i4),p,s)), s5 = ( IExec (((((i1 ";" i2) ";" i3) ";" i4) ";" i5),p,s)), s6 = ( IExec (body2,p,s));

      

       A10: (s1 . b4) = (s0 . b3) by SCMFSA_2: 63

      .= (s . b3) by SCMFSA_M: 37;

      

       A11: (s1 . f0) = (s0 . f0) by SCMFSA_2: 63

      .= (s . f0) by SCMFSA_M: 37;

      

       A12: (s1 . b3) = (s . b3) by Th4;

      

       A13: (s1 . a0) = (s0 . a0) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      

       A14: (s2 . f0) = (( Exec (i2,s1)) . f0) by SCMFSA6C: 9

      .= (s . f0) by A11, SCMFSA_2: 65;

      

       A15: (s2 . b3) = (( Exec (i2,s1)) . b3) by SCMFSA6C: 8

      .= ((s . b3) - 1) by A12, A13, SCMFSA_2: 65;

      

       A16: (s2 . b4) = (( Exec (i2,s1)) . b4) by SCMFSA6C: 8

      .= (s . b3) by A10, Lm14, SCMFSA_2: 65;

      

       A17: (s3 . f0) = (( Exec (i3,s2)) . f0) by SCMFSA6C: 7

      .= (s . f0) by A14, SCMFSA_2: 72;

      

       A18: ((s . f0) /. k1) = n1 by A3, A5, FINSEQ_4: 15;

      

       A19: (s3 . b5) = (( Exec (i3,s2)) . b5) by SCMFSA6C: 6

      .= n1 by A4, A14, A15, A18, Th1;

      

       A20: (s3 . b4) = (( Exec (i3,s2)) . b4) by SCMFSA6C: 6

      .= (s . b3) by A16, Lm17, SCMFSA_2: 72;

      

       A21: (s3 . b3) = (( Exec (i3,s2)) . b3) by SCMFSA6C: 6

      .= ((s . b3) - 1) by A15, Lm15, SCMFSA_2: 72;

      

       A22: (s4 . f0) = (( Exec (i4,s3)) . f0) by SCMFSA6C: 7

      .= (s . f0) by A17, SCMFSA_2: 72;

      

       A23: ((s . f0) /. k2) = n2 by A1, A6, FINSEQ_4: 15;

      

       A24: (s4 . b6) = (( Exec (i4,s3)) . b6) by SCMFSA6C: 6

      .= n2 by A7, A17, A20, A23, Th1;

      

       A25: (s4 . b3) = (( Exec (i4,s3)) . b3) by SCMFSA6C: 6

      .= ((s . b3) - 1) by A21, Lm16, SCMFSA_2: 72;

      

       A26: (s4 . b4) = (( Exec (i4,s3)) . b4) by SCMFSA6C: 6

      .= (s . b3) by A20, Lm18, SCMFSA_2: 72;

      

       A27: (s4 . b5) = (( Exec (i4,s3)) . b5) by SCMFSA6C: 6

      .= ((s . f0) . ((s . b3) - 1)) by A19, Lm19, SCMFSA_2: 72;

      

       A28: (s5 . f0) = (( Exec (i5,s4)) . f0) by SCMFSA6C: 7

      .= (s . f0) by A22, SCMFSA_2: 65;

      

       A29: (s5 . b3) = (( Exec (i5,s4)) . b3) by SCMFSA6C: 6

      .= ((s . b3) - 1) by A25, Lm16, SCMFSA_2: 65;

      

       A30: (s5 . b4) = (( Exec (i5,s4)) . b4) by SCMFSA6C: 6

      .= (s . b3) by A26, Lm18, SCMFSA_2: 65;

      

       A31: (s5 . b5) = (( Exec (i5,s4)) . b5) by SCMFSA6C: 6

      .= n1 by A27, Lm19, SCMFSA_2: 65;

      

       A32: (s5 . b6) = (( Exec (i5,s4)) . b6) by SCMFSA6C: 6

      .= (n2 - n1) by A24, A27, SCMFSA_2: 65;

      

       A33: (s6 . f0) = (( IExec (ifc,p,s5)) . f0) by SCMFSA6C: 2;

      

      thus (s6 . b3) = (( IExec (ifc,p,s5)) . b3) by SCMFSA6C: 1

      .= ((s . b3) - 1) by A29, Lm28;

      per cases ;

        suppose

         A34: (s5 . b6) > 0 ;

        then

         A35: (s6 . f0) = (((s . f0) +* (k1,n2)) +* (k2,n1)) by A4, A7, A23, A28, A29, A30, A31, A33, Lm27;

        

         A36: ( dom ((s . f0) +* (k1,n2))) = ( dom (s . f0)) by FUNCT_7: 30;

        then

         A37: ( dom (s6 . f0)) = ( dom (s . f0)) by A35, FUNCT_7: 30;

        

         A38: k2 in ( dom ((s . f0) +* (k1,n2))) by A1, A6, A36, FINSEQ_3: 25;

        

         A39: ((s6 . f0) . k2) = ((s . f0) . k1) by A9, A35, A36, FUNCT_7: 31;

         A40:

        now

          per cases ;

            suppose k1 = k2;

            hence ((s6 . f0) . k1) = ((s . f0) . k2);

          end;

            suppose k1 <> k2;

            

            hence ((s6 . f0) . k1) = (((s . f0) +* (k1,n2)) . k1) by A35, FUNCT_7: 32

            .= ((s . f0) . k2) by A8, FUNCT_7: 31;

          end;

        end;

         A41:

        now

          let k be set;

          assume that

           A42: k <> k1 and

           A43: k <> k2 and k in ( dom (s . f0));

          

          thus ((s6 . f0) . k) = (((s . f0) +* (k1,n2)) . k) by A35, A43, FUNCT_7: 32

          .= ((s . f0) . k) by A42, FUNCT_7: 32;

        end;

        hence ((s . f0),(s6 . f0)) are_fiberwise_equipotent by A8, A9, A37, A39, A40, RFINSEQ: 28;

        thus ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) or ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) by A40;

        thus ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) or ((s . f0) . ((s . b3) - 1)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) by A35, A38, FUNCT_7: 31;

        thus ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) or ((s . f0) . ((s . b3) - 1)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) by A40;

        thus for k be set st k <> ((s . b3) - 1) & k <> (s . b3) & k in ( dom (s . f0)) holds ((s . f0) . k) = ((s6 . f0) . k) by A41;

        

         A44: ((n2 - n1) + n1) > ( 0 + n1) by A32, A34, XREAL_1: 6;

        take n2, n1;

        thus thesis by A9, A35, A36, A40, A44, FUNCT_7: 31;

      end;

        suppose

         A45: (s5 . b6) <= 0 ;

        hence ((s . f0),(s6 . f0)) are_fiberwise_equipotent by A28, A33, Lm27;

        thus ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) or ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) by A28, A33, A45, Lm27;

        thus ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) or ((s . f0) . ((s . b3) - 1)) = ((( IExec (body2,p,s)) . f0) . (s . b3)) by A28, A33, A45, Lm27;

        thus ((s . f0) . (s . b3)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) or ((s . f0) . ((s . b3) - 1)) = ((( IExec (body2,p,s)) . f0) . ((s . b3) - 1)) by A28, A33, A45, Lm27;

        thus for k be set st k <> ((s . b3) - 1) & k <> (s . b3) & k in ( dom (s . f0)) holds ((s . f0) . k) = ((s6 . f0) . k) by A28, A33, A45, Lm27;

        

         A46: ((n2 - n1) + n1) <= ( 0 + n1) by A32, A45, XREAL_1: 6;

        take n1, n2;

        thus thesis by A28, A33, A45, A46, Lm27;

      end;

    end;

    

     Lm30: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA st (s . b2) >= 0 & (s . b2) < (s . b3) & (s . b3) <= ( len (s . f0)) holds ex k be Nat st k <= (s . b3) & k >= ((s . b3) - (s . b2)) & ((( IExec (T2,p,s)) . f0) . k) = ((s . f0) . (s . b3))

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      assume that

       A1: (s . b2) >= 0 and

       A2: (s . b2) < (s . b3) and

       A3: (s . b3) <= ( len (s . f0));

      defpred P[ Nat] means for t be State of SCM+FSA , q st (t . b2) = $1 & (t . b2) < (t . b3) & (t . b3) <= ( len (t . f0)) holds (for m be Nat st m > (t . b3) & m <= ( len (t . f0)) holds ((t . f0) . m) = ((( IExec (T2,q,t)) . f0) . m)) & ex n be Nat st n <= (t . b3) & n >= ((t . b3) - $1) & ((( IExec (T2,q,t)) . f0) . n) = ((t . f0) . (t . b3));

      

       A4: P[ 0 ]

      proof

        let t be State of SCM+FSA , q;

        assume that

         A5: (t . b2) = 0 and

         A6: (t . b2) < (t . b3) and (t . b3) <= ( len (t . f0));

        set If0 = (( IExec (T2,q,t)) . f0);

        thus for m be Nat st m > (t . b3) & m <= ( len (t . f0)) holds ((t . f0) . m) = (If0 . m) by A5, SCM_HALT: 67;

        reconsider n = (t . b3) as Element of NAT by A5, A6, INT_1: 3;

        take n;

        thus n <= (t . b3);

        thus n >= ((t . b3) - 0 );

        thus thesis by A5, SCM_HALT: 67;

      end;

      set sb2 = ( SubFrom (b2,a0));

       A7:

      now

        let k be Nat;

        assume

         A8: P[k];

        now

          let t be State of SCM+FSA , q;

          assume that

           A9: (t . b2) = (k + 1) and

           A10: (t . b2) < (t . b3) and

           A11: (t . b3) <= ( len (t . f0));

          set t1 = ( IExec ((body2 ";" sb2),q,t)), IB = ( IExec (body2,q,t)), t2 = ( IExec (T2,q,t1));

          

           A12: (t1 . b2) = (( Exec (sb2,IB)) . b2) by SCM_HALT: 23

          .= ((IB . b2) - (IB . a0)) by SCMFSA_2: 65

          .= ((IB . b2) - 1) by SCM_HALT: 9

          .= ((( Initialized t) . b2) - 1) by Lm22, SCM_HALT: 53

          .= ((t . b2) - 1) by SCMFSA_M: 37;

          

           A13: 2 <= (k + 2) by NAT_1: 11;

          ((k + 1) + 1) <= (t . b3) by A9, A10, INT_1: 7;

          then

           A14: 2 <= (t . b3) by A13, XXREAL_0: 2;

          

           A15: (t1 . b3) = (( Exec (sb2,IB)) . b3) by SCM_HALT: 23

          .= (IB . b3) by Lm10, SCMFSA_2: 65

          .= ((t . b3) - 1) by A11, A14, Lm29;

          

           A16: ((t . b2) - 1) < ((t . b3) - 1) by A10, XREAL_1: 9;

          

           A17: (t1 . b2) < (t1 . b3) by A10, A12, A15, XREAL_1: 9;

          

           A18: (t1 . f0) = (( Exec (sb2,IB)) . f0) by SCM_HALT: 24

          .= (IB . f0) by SCMFSA_2: 65;

          

           A19: ((t . f0),(IB . f0)) are_fiberwise_equipotent by A11, A14, Lm29;

          then

           A20: ( len (t . f0)) = ( len (t1 . f0)) by A18, RFINSEQ: 3;

          then

           A21: (t1 . b3) <= ( len (t1 . f0)) by A11, A15, XREAL_1: 146, XXREAL_0: 2;

          

           A22: (( IExec (T2,q,t)) . f0) = (t2 . f0) by A9, Lm22, SCM_HALT: 69;

          

           A23: (IB . f0) = (( Exec (sb2,IB)) . f0) by SCMFSA_2: 65

          .= (t1 . f0) by SCM_HALT: 24;

          thus for m be Nat st m > (t . b3) & m <= ( len (t . f0)) holds ((t . f0) . m) = ((( IExec (T2,q,t)) . f0) . m)

          proof

            let m be Nat;

            assume that

             A24: m > (t . b3) and

             A25: m <= ( len (t . f0));

            

             A26: (t . b3) > ((t . b3) - 1) by XREAL_1: 146;

            

             A27: m > (t1 . b3) by A15, A24, XREAL_1: 146, XXREAL_0: 2;

            

             A28: m <= ( len (t1 . f0)) by A18, A19, A25, RFINSEQ: 3;

            m >= 2 by A14, A24, XXREAL_0: 2;

            then m >= 1 by XXREAL_0: 2;

            then m in ( dom (t . f0)) by A25, FINSEQ_3: 25;

            

            hence ((t . f0) . m) = ((t1 . f0) . m) by A11, A14, A23, A24, A26, Lm29

            .= ((( IExec (T2,q,t)) . f0) . m) by A8, A9, A12, A17, A21, A22, A27, A28;

          end;

          hereby

            reconsider n = (t . b3) as Element of NAT by A9, A10, INT_1: 3;

            reconsider n as Nat;

            per cases by A11, A14, Lm29;

              suppose

               A29: ((t . f0) . (t . b3)) = ((( IExec (body2,q,t)) . f0) . (t . b3));

              take n;

              thus n <= (t . b3);

              n <= (n + (k + 1)) by NAT_1: 11;

              hence n >= ((t . b3) - (k + 1)) by XREAL_1: 20;

              thus ((( IExec (T2,q,t)) . f0) . n) = ((t . f0) . (t . b3)) by A8, A9, A11, A12, A15, A16, A20, A21, A22, A23, A29, XREAL_1: 146;

            end;

              suppose

               A30: ((t . f0) . (t . b3)) = ((( IExec (body2,q,t)) . f0) . ((t . b3) - 1));

              consider m be Nat such that

               A31: m <= (t1 . b3) and

               A32: m >= ((t1 . b3) - k) and

               A33: ((( IExec (T2,q,t1)) . f0) . m) = ((t1 . f0) . (t1 . b3)) by A8, A9, A12, A17, A21;

              take m;

              thus m <= (t . b3) by A15, A31, XREAL_1: 146, XXREAL_0: 2;

              thus m >= ((t . b3) - (k + 1)) by A15, A32;

              thus ((( IExec (T2,q,t)) . f0) . m) = ((t . f0) . (t . b3)) by A9, A15, A23, A30, A33, Lm22, SCM_HALT: 69;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

      

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

      reconsider i = (s . b2) as Element of NAT by A1, INT_1: 3;

       P[i] by A34;

      hence thesis by A2, A3;

    end;

    

     Lm31: for k be Nat holds for t be State of SCM+FSA , q st k = (t . b2) & k < (t . b3) & (t . b3) <= ( len (t . f0)) holds ((t . f0),(( IExec (T2,q,t)) . f0)) are_fiberwise_equipotent & (for m be Nat st m < ((t . b3) - k) & m >= 1 or (m > (t . b3) & m in ( dom (t . f0))) holds ((t . f0) . m) = ((( IExec (T2,q,t)) . f0) . m)) & (for m be Nat st m >= ((t . b3) - k) & m <= (t . b3) holds (ex x1,x2 be Integer st x1 = ((( IExec (T2,q,t)) . f0) . ((t . b3) - k)) & x2 = ((( IExec (T2,q,t)) . f0) . m) & x1 >= x2)) & for i be Nat st i >= ((t . b3) - k) & i <= (t . b3) holds ex n be Nat st n >= ((t . b3) - k) & n <= (t . b3) & ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n)

    proof

      defpred P[ Nat] means for t be State of SCM+FSA st $1 = (t . b2) & $1 < (t . b3) & (t . b3) <= ( len (t . f0)) holds (((t . f0),(( IExec (T2,q,t)) . f0)) are_fiberwise_equipotent ) & (for m be Nat st m < ((t . b3) - $1) & m >= 1 or (m > (t . b3) & m in ( dom (t . f0))) holds ((t . f0) . m) = ((( IExec (T2,q,t)) . f0) . m)) & (for m be Nat st m >= ((t . b3) - $1) & m <= (t . b3) holds (ex x1,x2 be Integer st x1 = ((( IExec (T2,q,t)) . f0) . ((t . b3) - $1)) & x2 = ((( IExec (T2,q,t)) . f0) . m) & x1 >= x2)) & for i be Nat st i >= ((t . b3) - $1) & i <= (t . b3) holds ex n be Nat st n >= ((t . b3) - $1) & n <= (t . b3) & ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n);

      now

        let t be State of SCM+FSA , q;

        assume that

         A1: 0 = (t . b2) and 0 < (t . b3) and (t . b3) <= ( len (t . f0));

        set If0 = (( IExec (T2,q,t)) . f0);

        thus ((t . f0),If0) are_fiberwise_equipotent by A1, SCM_HALT: 67;

        thus for m be Nat st m < ((t . b3) - 0 ) & m >= 1 or m > (t . b3) & m in ( dom (t . f0)) holds ((t . f0) . m) = ((( IExec (T2,q,t)) . f0) . m) by A1, SCM_HALT: 67;

        hereby

          let m be Nat;

          assume that

           A2: m >= ((t . b3) - 0 ) and

           A3: m <= (t . b3);

          

           A4: m = (t . b3) by A2, A3, XXREAL_0: 1;

          reconsider n1 = ((t . f0) . m) as Integer;

          take x1 = n1, x2 = n1;

          thus x1 = ((( IExec (T2,q,t)) . f0) . ((t . b3) - 0 )) by A1, A4, SCM_HALT: 67;

          thus x2 = (If0 . m) by A1, SCM_HALT: 67;

          thus x1 >= x2;

        end;

        let i be Nat;

        assume that

         A5: i >= ((t . b3) - 0 ) and

         A6: i <= (t . b3);

        take n = i;

        thus n >= ((t . b3) - 0 ) & n <= (t . b3) by A5, A6;

        thus ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n) by A1, SCM_HALT: 67;

      end;

      then

       A7: P[ 0 ];

      set sb2 = ( SubFrom (b2,a0));

       A8:

      now

        let k be Nat;

        assume

         A9: P[k];

        now

          let t be State of SCM+FSA , q;

          set t1 = ( IExec ((body2 ";" sb2),q,t)), IB = ( IExec (body2,q,t)), t2 = ( IExec (T2,q,t1));

          assume that

           A10: (k + 1) = (t . b2) and

           A11: (k + 1) < (t . b3) and

           A12: (t . b3) <= ( len (t . f0));

          

           A13: (t1 . b2) = (( Exec (sb2,IB)) . b2) by SCM_HALT: 23

          .= ((IB . b2) - (IB . a0)) by SCMFSA_2: 65

          .= ((IB . b2) - 1) by SCM_HALT: 9

          .= ((( Initialized t) . b2) - 1) by Lm22, SCM_HALT: 53

          .= ((k + 1) - 1) by A10, SCMFSA_M: 37

          .= k;

          

           A14: 2 <= (k + 2) by NAT_1: 11;

          ((k + 1) + 1) <= (t . b3) by A11, INT_1: 7;

          then

           A15: 2 <= (t . b3) by A14, XXREAL_0: 2;

          

           A16: (t1 . b3) = (( Exec (sb2,IB)) . b3) by SCM_HALT: 23

          .= (IB . b3) by Lm10, SCMFSA_2: 65

          .= ((t . b3) - 1) by A12, A15, Lm29;

          

           A17: ((k + 1) - 1) < ((t . b3) - 1) by A11, XREAL_1: 9;

          

           A18: (t1 . f0) = (( Exec (sb2,IB)) . f0) by SCM_HALT: 24

          .= (IB . f0) by SCMFSA_2: 65;

          

           A19: ((t . f0),(IB . f0)) are_fiberwise_equipotent by A12, A15, Lm29;

          then

           A20: ( len (t . f0)) = ( len (t1 . f0)) by A18, RFINSEQ: 3;

          

           A21: (t . b3) <= ( len (t1 . f0)) by A12, A18, A19, RFINSEQ: 3;

          

           A22: (t1 . b3) <= ( len (t1 . f0)) by A12, A16, A20, XREAL_1: 146, XXREAL_0: 2;

          

           A23: (t . b3) = ((t1 . b3) + 1) by A16;

          

           A24: ((t1 . f0),(t2 . f0)) are_fiberwise_equipotent by A9, A13, A16, A17, A22;

          

           A25: (( IExec (T2,q,t)) . f0) = (t2 . f0) by A10, Lm22, SCM_HALT: 69;

          ((t1 . f0),(( IExec (T2,q,t)) . f0)) are_fiberwise_equipotent by A10, A24, Lm22, SCM_HALT: 69;

          hence ((t . f0),(( IExec (T2,q,t)) . f0)) are_fiberwise_equipotent by A18, A19, CLASSES1: 76;

          

           A26: ((t . b3) - (k + 1)) = ((t1 . b3) - k) by A16;

          consider n1,n2 be Integer such that

           A27: n1 = ((IB . f0) . ((t . b3) - 1)) and

           A28: n2 = ((IB . f0) . (t . b3)) and

           A29: n1 >= n2 by A12, A15, Lm29;

          

           A30: (IB . f0) = (( Exec (sb2,IB)) . f0) by SCMFSA_2: 65

          .= (t1 . f0) by SCM_HALT: 24;

          

           A31: (t . b3) in NAT by A11, INT_1: 3;

          

           A32: (t . b3) >= 1 by A15, XXREAL_0: 2;

          then

           A33: (t . b3) in ( dom (t1 . f0)) by A12, A20, A31, FINSEQ_3: 25;

          hereby

            let m be Nat;

            assume that

             A34: m < ((t . b3) - (k + 1)) & m >= 1 or m > (t . b3) & m in ( dom (t . f0));

            per cases by A34;

              suppose

               A35: m < ((t . b3) - (k + 1)) & m >= 1;

              

               A36: (((t . b3) - (k + 1)) + (k + 1)) = (t . b3);

              

               A37: (m + (k + 1)) < (((t . b3) - (k + 1)) + (k + 1)) by A35, XREAL_1: 6;

              

               A38: (m + (k + 1)) < (t . b3) by A35, A36, XREAL_1: 6;

              m <= (m + (k + 1)) by NAT_1: 11;

              then m <= (t . b3) by A37, XXREAL_0: 2;

              then m <= ( len (t1 . f0)) by A12, A20, XXREAL_0: 2;

              then

               A39: m in ( dom (t . f0)) by A20, A35, FINSEQ_3: 25;

              

               A40: m <> (t . b3) by A35, A36, XREAL_1: 29;

              m <> ((t . b3) - 1)

              proof

                assume

                 A41: m = ((t . b3) - 1);

                (m + (k + 1)) = ((m + 1) + k);

                hence contradiction by A38, A41, NAT_1: 11;

              end;

              

              hence ((t . f0) . m) = ((t1 . f0) . m) by A12, A15, A30, A39, A40, Lm29

              .= ((( IExec (T2,q,t)) . f0) . m) by A9, A13, A17, A22, A25, A26, A35;

            end;

              suppose

               A42: m > (t . b3) & m in ( dom (t . f0));

              then

               A43: m in ( dom (t1 . f0)) by A18, A19, RFINSEQ: 3;

              

               A44: (t . b3) > ((t . b3) - 1) by XREAL_1: 146;

              

               A45: m > (t1 . b3) by A16, A42, XREAL_1: 146, XXREAL_0: 2;

              

              thus ((t . f0) . m) = ((t1 . f0) . m) by A12, A15, A30, A42, A44, Lm29

              .= ((( IExec (T2,q,t)) . f0) . m) by A9, A13, A16, A17, A22, A25, A43, A45;

            end;

          end;

          hereby

            let m be Nat;

            assume that

             A46: m >= ((t . b3) - (k + 1)) and

             A47: m <= (t . b3);

            consider nn be Nat such that

             A48: nn <= (t1 . b3) and

             A49: nn >= ((t1 . b3) - (t1 . b2)) and

             A50: ((t2 . f0) . nn) = ((t1 . f0) . (t1 . b3)) by A13, A16, A17, A22, Lm30;

            consider y1,y2 be Integer such that

             A51: y1 = ((t2 . f0) . ((t1 . b3) - k)) and

             A52: y2 = ((t2 . f0) . nn) and

             A53: y1 >= y2 by A9, A13, A16, A17, A22, A48, A49;

            per cases ;

              suppose

               A54: m > (t1 . b3);

              then m >= ((t1 . b3) + 1) by INT_1: 7;

              then

               A55: m = (t . b3) by A16, A47, XXREAL_0: 1;

              take y1, n2;

              thus y1 = ((( IExec (T2,q,t)) . f0) . ((t . b3) - (k + 1))) by A10, A16, A51, Lm22, SCM_HALT: 69;

              thus n2 = ((( IExec (T2,q,t)) . f0) . m) by A9, A13, A16, A17, A22, A25, A28, A30, A33, A54, A55;

              thus y1 >= n2 by A16, A27, A29, A30, A50, A52, A53, XXREAL_0: 2;

            end;

              suppose m <= (t1 . b3);

              then

              consider y1,y2 be Integer such that

               A56: y1 = ((t2 . f0) . ((t1 . b3) - k)) and

               A57: y2 = ((t2 . f0) . m) and

               A58: y1 >= y2 by A9, A13, A16, A17, A22, A46;

              take y1, y2;

              thus y1 = ((( IExec (T2,q,t)) . f0) . ((t . b3) - (k + 1))) by A10, A16, A56, Lm22, SCM_HALT: 69;

              thus y2 = ((( IExec (T2,q,t)) . f0) . m) by A10, A57, Lm22, SCM_HALT: 69;

              thus y1 >= y2 by A58;

            end;

          end;

          thus for i be Nat st i >= ((t . b3) - (k + 1)) & i <= (t . b3) holds ex n be Nat st n >= ((t . b3) - (k + 1)) & n <= (t . b3) & ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n)

          proof

            let i be Nat;

            assume that

             A59: i >= ((t . b3) - (k + 1)) and

             A60: i <= (t . b3);

            per cases ;

              suppose

               A61: i = (t . b3);

              then

               A62: i > (t1 . b3) by A23, XREAL_1: 29;

              

               A63: i in ( dom (t1 . f0)) by A21, A32, A61, FINSEQ_3: 25;

              per cases by A12, A15, Lm29;

                suppose

                 A64: ((t . f0) . (t . b3)) = ((( IExec (body2,q,t)) . f0) . (t . b3));

                reconsider n = (t . b3) as Element of NAT by A11, INT_1: 3;

                take n;

                thus n >= ((t . b3) - (k + 1)) & n <= (t . b3) by A59, A61;

                thus ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n) by A9, A13, A16, A17, A22, A25, A30, A61, A62, A63, A64;

              end;

                suppose

                 A65: ((t . f0) . ((t . b3) - 1)) = ((( IExec (body2,q,t)) . f0) . (t . b3));

                ((t . b3) - 1) >= (1 - 1) by A32, XREAL_1: 9;

                then

                reconsider n = ((t . b3) - 1) as Element of NAT by INT_1: 3;

                take n;

                n <= (n + k) by NAT_1: 11;

                hence n >= ((t . b3) - (k + 1)) by A26, XREAL_1: 20;

                thus n <= (t . b3) by XREAL_1: 146;

                thus ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n) by A9, A13, A16, A17, A22, A25, A30, A61, A62, A63, A65;

              end;

            end;

              suppose i <> (t . b3);

              then i < (t . b3) by A60, XXREAL_0: 1;

              then (i + 1) <= (t . b3) by INT_1: 7;

              then i <= (t1 . b3) by A16, XREAL_1: 19;

              then

              consider n be Nat such that

               A66: n >= ((t1 . b3) - k) and

               A67: n <= (t1 . b3) and

               A68: ((t2 . f0) . i) = ((t1 . f0) . n) by A9, A13, A16, A17, A22, A59;

              thus ex n be Nat st n >= ((t . b3) - (k + 1)) & n <= (t . b3) & ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n)

              proof

                per cases ;

                  suppose

                   A69: n = (t1 . b3);

                  per cases by A12, A15, Lm29;

                    suppose

                     A70: ((t . f0) . (t . b3)) = ((( IExec (body2,q,t)) . f0) . ((t . b3) - 1));

                    reconsider m = (t . b3) as Element of NAT by A11, INT_1: 3;

                    take m;

                    m <= (m + (k + 1)) by NAT_1: 11;

                    hence m >= ((t . b3) - (k + 1)) by XREAL_1: 20;

                    thus m <= (t . b3);

                    thus ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . m) by A10, A16, A30, A68, A69, A70, Lm22, SCM_HALT: 69;

                  end;

                    suppose

                     A71: ((t . f0) . ((t . b3) - 1)) = ((( IExec (body2,q,t)) . f0) . ((t . b3) - 1));

                    take n;

                    thus n >= ((t . b3) - (k + 1)) by A16, A66;

                    thus n <= (t . b3) by A16, A69, XREAL_1: 146;

                    thus ((( IExec (T2,q,t)) . f0) . i) = ((t . f0) . n) by A10, A16, A30, A68, A69, A71, Lm22, SCM_HALT: 69;

                  end;

                end;

                  suppose

                   A72: n <> (t1 . b3);

                  

                   A73: (t1 . b3) < (t . b3) by A16, XREAL_1: 146;

                  

                   A74: n < (t . b3) by A16, A67, XREAL_1: 146, XXREAL_0: 2;

                  (k - k) < ((t1 . b3) - k) by A16, A17, XREAL_1: 9;

                  then

                   A75: n >= ( 0 + 1) by A66, INT_1: 7;

                  n <= ( len (t1 . f0)) by A12, A20, A74, XXREAL_0: 2;

                  then

                   A76: n in ( dom (t . f0)) by A20, A75, FINSEQ_3: 25;

                  take n;

                  thus n >= ((t . b3) - (k + 1)) by A16, A66;

                  thus n <= (t . b3) by A16, A67, XREAL_1: 146, XXREAL_0: 2;

                  thus thesis by A12, A15, A16, A25, A30, A67, A68, A72, A73, A76, Lm29;

                end;

              end;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

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

      hence thesis;

    end;

    

     Lm32: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA holds (( IExec (Sb,p,s)) . b2) = ((s . b1) - 1) & (( IExec (Sb,p,s)) . b3) = ( len (s . f0)) & (( IExec (Sb,p,s)) . f0) = (s . f0)

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      set s0 = ( Initialized s), s1 = ( Exec (j1,s0)), s2 = ( IExec ((j1 ";" j2),p,s)), s3 = ( IExec (((j1 ";" j2) ";" j3),p,s));

      

       A1: (s1 . b2) = (s0 . b1) by SCMFSA_2: 63

      .= (s . b1) by SCMFSA_M: 37;

      

       A2: (s1 . f0) = (s0 . f0) by SCMFSA_2: 63

      .= (s . f0) by SCMFSA_M: 37;

      

       A3: (s1 . a0) = (s0 . a0) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      

       A4: (s2 . f0) = (( Exec (j2,s1)) . f0) by SCMFSA6C: 9

      .= (s . f0) by A2, SCMFSA_2: 65;

      

       A5: (s2 . b2) = (( Exec (j2,s1)) . b2) by SCMFSA6C: 8

      .= ((s . b1) - 1) by A1, A3, SCMFSA_2: 65;

      

      thus (s3 . b2) = (( Exec (j3,s2)) . b2) by SCMFSA6C: 6

      .= ((s . b1) - 1) by A5, Lm10, SCMFSA_2: 74;

      

      thus (s3 . b3) = (( Exec (j3,s2)) . b3) by SCMFSA6C: 6

      .= ( len (s . f0)) by A4, SCMFSA_2: 74;

      

      thus (s3 . f0) = (( Exec (j3,s2)) . f0) by SCMFSA6C: 7

      .= (s . f0) by A4, SCMFSA_2: 74;

    end;

    

     Lm33: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA st (s . b1) = ( len (s . f0)) holds ((s . f0),(( IExec (T1,p,s)) . f0)) are_fiberwise_equipotent & for i,j be Nat st i >= 1 & j <= ( len (s . f0)) & i < j holds for x1,x2 be Integer st x1 = ((( IExec (T1,p,s)) . f0) . i) & x2 = ((( IExec (T1,p,s)) . f0) . j) holds x1 >= x2

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      assume

       A1: (s . b1) = ( len (s . f0));

      per cases ;

        suppose

         A2: ( len (s . f0)) = 0 ;

        hence ((s . f0),(( IExec (T1,p,s)) . f0)) are_fiberwise_equipotent by A1, Lm23, SCM_HALT: 67;

        thus thesis by A2;

      end;

        suppose

         A3: ( len (s . f0)) <> 0 ;

        defpred P[ Nat] means for t be State of SCM+FSA , q st (t . b1) = ($1 + 1) & (t . b1) <= ( len (t . f0)) holds (((t . f0),(( IExec (T1,q,t)) . f0)) are_fiberwise_equipotent ) & (for i,j be Nat st i >= (( len (t . f0)) - $1) & j <= ( len (t . f0)) & i < j holds for x1,x2 be Integer st x1 = ((( IExec (T1,q,t)) . f0) . i) & x2 = ((( IExec (T1,q,t)) . f0) . j) holds x1 >= x2) & (for i be Nat st i < (( len (t . f0)) - $1) & i >= 1 holds ((( IExec (T1,q,t)) . f0) . i) = ((t . f0) . i)) & (for i be Nat st i >= (( len (t . f0)) - $1) & i <= ( len (t . f0)) holds ex n be Nat st n >= (( len (t . f0)) - $1) & n <= ( len (t . f0)) & ((( IExec (T1,q,t)) . f0) . i) = ((t . f0) . n));

        set B11 = ( SubFrom (b1,a0));

        

         A4: P[ 0 ]

        proof

          let t be State of SCM+FSA , q;

          assume that

           A5: (t . b1) = ( 0 + 1) and (t . b1) <= ( len (t . f0));

          set IB = ( IExec ((body1 ";" B11),q,t));

          

           A6: (IB . b1) = (1 - 1) by A5, Lm23, Lm25, SCM_HALT: 66;

          

           A7: (( IExec (Sb,q,t)) . b2) = (1 - 1) by A5, Lm32;

          

           A8: (( IExec (T1,q,t)) . f0) = (( IExec (T1,q,IB)) . f0) by A5, Lm23, Lm25, SCM_HALT: 69

          .= (IB . f0) by A6, Lm23, SCM_HALT: 67

          .= (( Exec (B11,( IExec (body1,q,t)))) . f0) by Lm23, SCM_HALT: 24

          .= (( IExec (body1,q,t)) . f0) by SCMFSA_2: 65

          .= (( IExec (T2,q,( IExec (Sb,q,t)))) . f0) by Lm23, SCM_HALT: 21

          .= (( IExec (Sb,q,t)) . f0) by A7, SCM_HALT: 67

          .= (t . f0) by Lm32;

          hence ((t . f0),(( IExec (T1,q,t)) . f0)) are_fiberwise_equipotent ;

          thus for i,j be Nat st i >= (( len (t . f0)) - 0 ) & j <= ( len (t . f0)) & i < j holds for x1,x2 be Integer st x1 = ((( IExec (T1,q,t)) . f0) . i) & x2 = ((( IExec (T1,q,t)) . f0) . j) holds x1 >= x2 by XXREAL_0: 2;

          thus for i be Nat st i < (( len (t . f0)) - 0 ) & i >= 1 holds ((( IExec (T1,q,t)) . f0) . i) = ((t . f0) . i) by A8;

          let i be Nat;

          assume that

           A9: i >= (( len (t . f0)) - 0 ) and

           A10: i <= ( len (t . f0));

          take n = i;

          thus n >= (( len (t . f0)) - 0 ) & n <= ( len (t . f0)) by A9, A10;

          thus thesis by A8;

        end;

         A11:

        now

          let k be Nat;

          assume

           A12: P[k];

          now

            let t be State of SCM+FSA , q;

            set t1 = ( IExec ((body1 ";" B11),q,t)), IB = ( IExec (body1,q,t)), t2 = ( IExec (T1,q,t1));

            assume that

             A13: (t . b1) = ((k + 1) + 1) and

             A14: (t . b1) <= ( len (t . f0));

            

             A15: (t1 . b1) = (( Exec (B11,IB)) . b1) by Lm23, SCM_HALT: 23

            .= ((IB . b1) - (IB . a0)) by SCMFSA_2: 65

            .= ((IB . b1) - 1) by Lm23, SCM_HALT: 9

            .= ((( Initialized t) . b1) - 1) by Lm23, Lm25, SCM_HALT: 53

            .= (((k + 1) + 1) - 1) by A13, SCMFSA_M: 37

            .= (k + 1);

            then (t1 . b1) < (t . b1) by A13, XREAL_1: 29;

            then

             A16: (t1 . b1) <= ( len (t . f0)) by A14, XXREAL_0: 2;

            set Ts = ( IExec (Sb,q,t));

            

             A17: (Ts . b2) = (((k + 1) + 1) - 1) by A13, Lm32

            .= (k + 1);

            

             A18: (Ts . b3) = ( len (t . f0)) by Lm32;

            then

             A19: (Ts . b3) = ( len (Ts . f0)) by Lm32;

            

             A20: (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

            

             A21: (k + 1) < (t . b1) by A13, XREAL_1: 29;

            

             A22: (k + 1) < ( len (t . f0)) by A13, A14, A20, XXREAL_0: 2;

            

             A23: (k + 1) < (Ts . b3) by A14, A18, A21, XXREAL_0: 2;

            

             A24: ((Ts . f0),(( IExec (T2,q,Ts)) . f0)) are_fiberwise_equipotent by A17, A18, A19, A22, Lm31;

            

             A25: (Ts . f0) = (t . f0) by Lm32;

            

             A26: (t1 . f0) = (( Exec (B11,IB)) . f0) by Lm23, SCM_HALT: 24

            .= (IB . f0) by SCMFSA_2: 65

            .= (( IExec (T2,q,Ts)) . f0) by Lm23, SCM_HALT: 21;

            then

             A27: ((t . f0),(t1 . f0)) are_fiberwise_equipotent by A17, A18, A23, A25, Lm31;

            

             A28: ( len (t . f0)) = ( len (t1 . f0)) by A24, A25, A26, RFINSEQ: 3;

            

             A29: (t1 . b1) <= ( len (t1 . f0)) by A16, A27, RFINSEQ: 3;

            

             A30: ((t1 . f0),(( IExec (T1,q,t1)) . f0)) are_fiberwise_equipotent by A12, A15, A16, A28;

            

             A31: (( IExec (T1,q,t)) . f0) = (t2 . f0) by A13, Lm23, Lm25, SCM_HALT: 69;

            hence ((t . f0),(( IExec (T1,q,t)) . f0)) are_fiberwise_equipotent by A27, A30, CLASSES1: 76;

            set lk = (( len (t . f0)) - (k + 1));

            

             A32: (lk + 1) = (( len (t1 . f0)) - k) by A28;

            thus for i,j be Nat st i >= (( len (t . f0)) - (k + 1)) & j <= ( len (t . f0)) & i < j holds for x1,x2 be Integer st x1 = ((( IExec (T1,q,t)) . f0) . i) & x2 = ((( IExec (T1,q,t)) . f0) . j) holds x1 >= x2

            proof

              let i,j be Nat;

              assume that

               A33: i >= lk and

               A34: j <= ( len (t . f0)) and

               A35: i < j;

              j > lk by A33, A35, XXREAL_0: 2;

              then j >= (( len (t1 . f0)) - k) by A32, INT_1: 7;

              then

              consider n be Nat such that

               A36: n >= (( len (t1 . f0)) - k) and

               A37: n <= ( len (t1 . f0)) and

               A38: ((( IExec (T1,q,t1)) . f0) . j) = ((t1 . f0) . n) by A12, A15, A16, A28, A34;

              lk < (lk + 1) by XREAL_1: 29;

              then

               A39: n >= ((Ts . b3) - (k + 1)) by A18, A28, A36, XXREAL_0: 2;

              

               A40: n <= (Ts . b3) by A28, A37, Lm32;

              hereby

                let x1,x2 be Integer;

                assume that

                 A41: x1 = ((( IExec (T1,q,t)) . f0) . i) and

                 A42: x2 = ((( IExec (T1,q,t)) . f0) . j);

                per cases ;

                  suppose

                   A43: i = lk;

                  

                   A44: ex y1,y2 be Integer st (y1 = ((( IExec (T2,q,Ts)) . f0) . ((Ts . b3) - (k + 1)))) & (y2 = ((( IExec (T2,q,Ts)) . f0) . n)) & (y1 >= y2) by A17, A19, A23, A39, A40, Lm31;

                  

                   A45: i < (( len (t1 . f0)) - k) by A32, A43, XREAL_1: 29;

                  

                   A46: 1 <= i by A13, A14, A43, XREAL_1: 19;

                  i = ((Ts . b3) - (k + 1)) by A43, Lm32;

                  hence x1 >= x2 by A12, A15, A16, A26, A28, A31, A38, A41, A42, A44, A45, A46;

                end;

                  suppose i <> lk;

                  then i > lk by A33, XXREAL_0: 1;

                  then i >= (( len (t1 . f0)) - k) by A32, INT_1: 7;

                  hence x1 >= x2 by A12, A15, A16, A28, A31, A34, A35, A41, A42;

                end;

              end;

            end;

            thus for i be Nat st i < (( len (t . f0)) - (k + 1)) & i >= 1 holds ((( IExec (T1,q,t)) . f0) . i) = ((t . f0) . i)

            proof

              let i be Nat;

              assume that

               A47: i < lk and

               A48: i >= 1;

              lk < (lk + 1) by XREAL_1: 29;

              then i < (( len (t1 . f0)) - k) by A28, A47, XXREAL_0: 2;

              

              hence ((( IExec (T1,q,t)) . f0) . i) = ((t1 . f0) . i) by A12, A15, A29, A31, A48

              .= ((t . f0) . i) by A17, A18, A23, A25, A26, A47, A48, Lm31;

            end;

            thus for i be Nat st i >= (( len (t . f0)) - (k + 1)) & i <= ( len (t . f0)) holds ex n be Nat st n >= (( len (t . f0)) - (k + 1)) & n <= ( len (t . f0)) & ((( IExec (T1,q,t)) . f0) . i) = ((t . f0) . n)

            proof

              let i be Nat;

              assume that

               A49: i >= (( len (t . f0)) - (k + 1)) and

               A50: i <= ( len (t . f0));

              per cases ;

                suppose

                 A51: i = lk;

                then

                 A52: i < (( len (t1 . f0)) - k) by A32, XREAL_1: 29;

                

                 A53: i >= 1 by A13, A14, A51, XREAL_1: 19;

                consider n be Nat such that

                 A54: n >= ((Ts . b3) - (k + 1)) and

                 A55: n <= (Ts . b3) and

                 A56: ((( IExec (T2,q,Ts)) . f0) . i) = ((Ts . f0) . n) by A17, A18, A19, A22, A49, A50, Lm31;

                take n;

                thus n >= (( len (t . f0)) - (k + 1)) by A54, Lm32;

                thus n <= ( len (t . f0)) by A55, Lm32;

                thus thesis by A12, A15, A25, A26, A29, A31, A52, A53, A56;

              end;

                suppose i <> lk;

                then i > lk by A49, XXREAL_0: 1;

                then i >= (( len (t1 . f0)) - k) by A32, INT_1: 7;

                then

                consider m be Nat such that

                 A57: m >= (( len (t1 . f0)) - k) and

                 A58: m <= ( len (t1 . f0)) and

                 A59: ((( IExec (T1,q,t1)) . f0) . i) = ((t1 . f0) . m) by A12, A15, A16, A28, A50;

                (lk + 1) > lk by XREAL_1: 29;

                then m > ((Ts . b3) - (k + 1)) by A18, A28, A57, XXREAL_0: 2;

                then

                consider n be Nat such that

                 A60: n >= ((Ts . b3) - (k + 1)) and

                 A61: n <= (Ts . b3) and

                 A62: ((( IExec (T2,q,Ts)) . f0) . m) = ((Ts . f0) . n) by A17, A18, A19, A22, A28, A58, Lm31;

                take n;

                thus n >= (( len (t . f0)) - (k + 1)) by A60, Lm32;

                thus n <= ( len (t . f0)) by A61, Lm32;

                thus thesis by A26, A31, A59, A62, Lm32;

              end;

            end;

          end;

          hence P[(k + 1)];

        end;

        

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

        (s . b1) >= (1 + 0 ) by A1, A3, INT_1: 7;

        then

        reconsider m = ((s . b1) - 1) as Element of NAT by INT_1: 5;

        

         A64: (m + 1) = (s . b1);

        hence ((s . f0),(( IExec (T1,p,s)) . f0)) are_fiberwise_equipotent by A1, A63;

        (( len (s . f0)) - m) = 1 by A1;

        hence thesis by A63, A64;

      end;

    end;

    theorem :: SCMBSORT:41

    

     Th26: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA holds ((s . ( fsloc 0 )),(( IExec (( bubble-sort ( fsloc 0 )),p,s)) . ( fsloc 0 ))) are_fiberwise_equipotent & for i,j be Nat st i >= 1 & j <= ( len (s . ( fsloc 0 ))) & i < j holds for x1,x2 be Integer st x1 = ((( IExec (( bubble-sort ( fsloc 0 )),p,s)) . ( fsloc 0 )) . i) & x2 = ((( IExec (( bubble-sort ( fsloc 0 )),p,s)) . ( fsloc 0 )) . j) holds x1 >= x2

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      set W27 = (((((w2 ";" w3) ";" w4) ";" w5) ";" w6) ";" w7), s0 = ( Initialized s), s1 = ( Exec (w2,s0)), s2 = ( IExec ((w2 ";" w3),p,s)), s3 = ( IExec (((w2 ";" w3) ";" w4),p,s)), s4 = ( IExec ((((w2 ";" w3) ";" w4) ";" w5),p,s)), s5 = ( IExec (((((w2 ";" w3) ";" w4) ";" w5) ";" w6),p,s)), s6 = ( IExec (W27,p,s));

      

       A1: (s5 . f0) = (( Exec (w6,s4)) . f0) by SCMFSA6C: 7

      .= (s4 . f0) by SCMFSA_2: 63

      .= (( Exec (w5,s3)) . f0) by SCMFSA6C: 7

      .= (s3 . f0) by SCMFSA_2: 63

      .= (( Exec (w4,s2)) . f0) by SCMFSA6C: 7

      .= (s2 . f0) by SCMFSA_2: 63

      .= (( Exec (w3,s1)) . f0) by SCMFSA6C: 9

      .= (s1 . f0) by SCMFSA_2: 63

      .= (s0 . f0) by SCMFSA_2: 63

      .= (s . f0) by SCMFSA_M: 37;

      

       A2: (s6 . f0) = (( Exec (w7,s5)) . f0) by SCMFSA6C: 7

      .= (s . f0) by A1, SCMFSA_2: 74;

      

       A3: (s6 . b1) = (( Exec (w7,s5)) . b1) by SCMFSA6C: 6

      .= ( len (s6 . f0)) by A1, A2, SCMFSA_2: 74;

      

       A4: (( IExec (( bubble-sort f0),p,s)) . f0) = (( IExec (T1,p,s6)) . f0) by Lm26, SCM_HALT: 21;

      hence ((s . f0),(( IExec (( bubble-sort f0),p,s)) . f0)) are_fiberwise_equipotent by A2, A3, Lm33;

      let i,j be Nat;

      assume that

       A5: i >= 1 and

       A6: j <= ( len (s . f0)) and

       A7: i < j;

      thus thesis by A2, A3, A4, A5, A6, A7, Lm33;

    end;

    theorem :: SCMBSORT:42

    

     Th27: for i be Nat, s be State of SCM+FSA , P be Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds for w be FinSequence of INT st ( Initialized (( fsloc 0 ) .--> w)) c= s holds ( IC ( Comput (P,s,i))) in ( dom Bubble-Sort-Algorithm )

    proof

      set Ba = Bubble-Sort-Algorithm , Ib = ((( intloc 0 ) .--> 1) +* ( Start-At ( 0 , SCM+FSA )));

      let i be Nat, s be State of SCM+FSA , P be Instruction-Sequence of SCM+FSA such that

       A1: Bubble-Sort-Algorithm c= P;

      let w be FinSequence of INT ;

      set x = (( fsloc 0 ) .--> w);

      assume

       A2: ( Initialized x) c= s;

      set BSA = Bubble-Sort-Algorithm ;

      ( Initialize (( intloc 0 ) .--> 1)) c= ( Initialized x) by FUNCT_4: 25;

      then ( Initialize (( intloc 0 ) .--> 1)) c= s by A2, XBOOLE_1: 1;

      then ( IC s) = 0 by MEMSTR_0: 47;

      then ( IC s) in ( dom Bubble-Sort-Algorithm ) by AFINSQ_1: 65;

      hence thesis by A1, AMISTD_1: 21;

    end;

    theorem :: SCMBSORT:43

    

     Th28: for p be Instruction-Sequence of SCM+FSA holds for s be State of SCM+FSA , t be FinSequence of INT st (( Initialize (( intloc 0 ) .--> 1)) +* (( fsloc 0 ) .--> t)) c= s & Bubble-Sort-Algorithm c= p holds ex u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (( Result (p,s)) . ( fsloc 0 )) = u

    proof

      let p be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA , t be FinSequence of INT ;

      set Ba = Bubble-Sort-Algorithm , pp = ( Initialize (( intloc 0 ) .--> 1)), x = (( fsloc 0 ) .--> t), z = (( IExec (( bubble-sort f0),p,s)) . f0);

      assume that

       A1: (pp +* x) c= s and

       A2: Ba c= p;

      

       A3: (p +* Ba) = p by A2, FUNCT_4: 98;

      

       A4: f0 in ( dom x) by TARSKI:def 1;

      then f0 in ( dom (pp +* x)) by FUNCT_4: 12;

      

      then

       A5: (s . f0) = ((pp +* x) . f0) by A1, GRFUNC_1: 2

      .= (x . f0) by A4, FUNCT_4: 13

      .= t by FUNCOP_1: 72;

      

       A6: ((s . f0),z) are_fiberwise_equipotent by Th26;

      reconsider u = z as FinSequence of REAL by FINSEQ_3: 117;

      take u;

      thus (t,u) are_fiberwise_equipotent by A5, Th26;

      

       A7: ( dom (s . f0)) = ( dom u) by A6, RFINSEQ: 3;

      now

        let i,j be Nat;

        assume that

         A8: i in ( dom u) and

         A9: j in ( dom u) and

         A10: i < j;

        

         A11: i >= 1 by A8, FINSEQ_3: 25;

        

         A12: j <= ( len (s . f0)) by A7, A9, FINSEQ_3: 25;

        reconsider y1 = (z . i) as Integer;

        reconsider y2 = (z . j) as Integer;

        thus (u . i) >= (u . j) by A10, A11, A12, Th26;

      end;

      hence u is non-increasing by RFINSEQ: 19;

      thus u is FinSequence of INT ;

      ( dom pp) misses ( dom x) by SCMFSA_M: 32;

      then pp c= (pp +* x) by FUNCT_4: 32;

      then s = (s +* pp) by A1, FUNCT_4: 98, XBOOLE_1: 1;

      then s = ( Initialized s);

      hence thesis by Th20, A3;

    end;

    theorem :: SCMBSORT:44

    

     Th29: for w be FinSequence of INT holds ( Initialized (( fsloc 0 ) .--> w)) is Bubble-Sort-Algorithm -autonomic

    proof

      let w be FinSequence of INT ;

      set p = ( Initialized (( fsloc 0 ) .--> w)), q = Bubble-Sort-Algorithm ;

      

       A1: for P,Q be Instruction-Sequence of SCM+FSA st q c= P & q c= Q holds for s1,s2 be State of SCM+FSA , i st p c= s1 & p c= s2 & i <= 10 holds (( Comput (P,s1,i)) . ( intloc 0 )) = (( Comput (Q,s2,i)) . ( intloc 0 )) & (( Comput (P,s1,i)) . ( IC SCM+FSA )) = (( Comput (Q,s2,i)) . ( IC SCM+FSA )) & (( Comput (P,s1,i)) . ( fsloc 0 )) = (( Comput (Q,s2,i)) . ( fsloc 0 ))

      proof

        let P,Q be Instruction-Sequence of SCM+FSA such that

         A2: q c= P & q c= Q;

        let s1,s2 be State of SCM+FSA , i;

        assume that

         A3: p c= s1 and

         A4: p c= s2 and

         A5: i <= 10;

        

         A6: q c= P by A2;

        

         A7: q c= Q by A2;

        

         A8: s1 is 0 -started by A3, MEMSTR_0: 17;

        

         A9: s2 is 0 -started by A4, MEMSTR_0: 17;

        

         A10: (s1 . ( intloc 0 )) = 1 by A3, SCMFSA_M: 33

        .= (s2 . ( intloc 0 )) by A4, SCMFSA_M: 33;

        

         A11: (s1 . ( fsloc 0 )) = w by A3, SCMFSA_M: 33

        .= (s2 . ( fsloc 0 )) by A4, SCMFSA_M: 33;

        

         A12: ( IC s1) = 0 by A8

        .= ( IC s2) by A9;

        i = 0 or ... or i = 10 by A5;

        per cases ;

          suppose

           A13: i = 0 ;

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (( Comput (Q,s2,i)) . ( intloc 0 )) by A10;

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A12, A13;

          thus thesis by A11, A13;

        end;

          suppose

           A14: i = 1;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A2, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A14, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 1 by A2, A8, A14, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A7, A9, A14, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A6, A8, A14, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A14, Lm21;

        end;

          suppose

           A15: i = 2;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A6, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A15, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 2 by A2, A8, A15, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A15, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A15, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A15, Lm21;

        end;

          suppose

           A16: i = 3;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A2, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A16, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 3 by A2, A8, A16, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A16, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A6, A8, A16, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A16, Lm21;

        end;

          suppose

           A17: i = 4;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A6, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A17, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 4 by A2, A8, A17, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A17, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A17, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A17, Lm21;

        end;

          suppose

           A18: i = 5;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A6, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A18, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 5 by A2, A8, A18, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A18, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A18, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A18, Lm21;

        end;

          suppose

           A19: i = 6;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A2, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A19, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 6 by A2, A8, A19, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A19, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A19, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A19, Lm21;

        end;

          suppose

           A20: i = 7;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A6, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A20, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 7 by A2, A8, A20, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A20, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A20, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A20, Lm21;

        end;

          suppose

           A21: i = 8;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A2, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A21, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 8 by A2, A8, A21, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A21, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A21, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A21, Lm21;

        end;

          suppose

           A22: i = 9;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A2, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A22, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 9 by A2, A8, A22, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A22, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A22, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A22, Lm21;

        end;

          suppose

           A23: i = 10;

          

          hence (( Comput (P,s1,i)) . ( intloc 0 )) = (s1 . ( intloc 0 )) by A2, A8, Lm21

          .= (( Comput (Q,s2,i)) . ( intloc 0 )) by A2, A9, A10, A23, Lm21;

          

          thus (( Comput (P,s1,i)) . ( IC SCM+FSA )) = 10 by A2, A8, A23, Lm21

          .= (( Comput (Q,s2,i)) . ( IC SCM+FSA )) by A2, A9, A23, Lm21;

          

          thus (( Comput (P,s1,i)) . ( fsloc 0 )) = (s1 . ( fsloc 0 )) by A2, A8, A23, Lm21

          .= (( Comput (Q,s2,i)) . ( fsloc 0 )) by A2, A9, A11, A23, Lm21;

        end;

      end;

      set UD = {( fsloc 0 ), a0, a1, a2, a3, a4, a5, a6}, Us = (( UsedI*Loc q) \/ ( UsedILoc q));

      

       A24: ( UsedI*Loc q) = {( fsloc 0 )} by Th22;

      

       A25: ( UsedILoc q) = {a0, a1, a2, a3, a4, a5, a6} by Th21;

      then

       A26: Us = UD by A24, ENUMSET1: 22;

      

       A27: for P,Q be Instruction-Sequence of SCM+FSA st q c= P & q c= Q holds for i be Nat, s1,s2 be State of SCM+FSA st 11 <= i & p c= s1 & p c= s2 holds (( Comput (P,s1,i)) | Us) = (( Comput (Q,s2,i)) | Us) & (( Comput (P,s1,i)) . ( IC SCM+FSA )) = (( Comput (Q,s2,i)) . ( IC SCM+FSA ))

      proof

        let P,Q be Instruction-Sequence of SCM+FSA such that

         A28: q c= P & q c= Q;

        let i be Nat, s1,s2 be State of SCM+FSA such that

         A29: 11 <= i and

         A30: p c= s1 and

         A31: p c= s2;

        set Cs11 = ( Comput (P,s1,11)), Cs21 = ( Comput (Q,s2,11));

        

         A32: s1 is 0 -started by A30, MEMSTR_0: 17;

        

         A33: s2 is 0 -started by A31, MEMSTR_0: 17;

        

         A34: (s1 . ( intloc 0 )) = 1 by A30, SCMFSA_M: 33

        .= (s2 . ( intloc 0 )) by A31, SCMFSA_M: 33;

        

         A35: (s1 . ( fsloc 0 )) = w by A30, SCMFSA_M: 33

        .= (s2 . ( fsloc 0 )) by A31, SCMFSA_M: 33;

        

         A36: Us c= ( dom Cs11) by Th19;

        

         A37: Us c= ( dom Cs21) by Th19;

        now

          let x be set;

          assume x in Us;

          then

           A38: x in UD by A24, A25, ENUMSET1: 22;

          per cases by A38, ENUMSET1:def 6;

            suppose

             A39: x = ( fsloc 0 );

            

            hence (Cs11 . x) = (s1 . ( fsloc 0 )) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A35, A39, Lm21;

          end;

            suppose

             A40: x = a0;

            

            hence (Cs11 . x) = (s1 . a0) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A34, A40, Lm21;

          end;

            suppose

             A41: x = a1;

            

            hence (Cs11 . x) = ( len (s1 . ( fsloc 0 ))) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A35, A41, Lm21;

          end;

            suppose

             A42: x = a2;

            

            hence (Cs11 . x) = (s1 . a0) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A34, A42, Lm21;

          end;

            suppose

             A43: x = a3;

            

            hence (Cs11 . x) = (s1 . a0) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A34, A43, Lm21;

          end;

            suppose

             A44: x = a4;

            

            hence (Cs11 . x) = (s1 . a0) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A34, A44, Lm21;

          end;

            suppose

             A45: x = a5;

            

            hence (Cs11 . x) = (s1 . a0) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A34, A45, Lm21;

          end;

            suppose

             A46: x = a6;

            

            hence (Cs11 . x) = (s1 . a0) by A32, A28, Lm21

            .= (Cs21 . x) by A33, A28, A34, A46, Lm21;

          end;

        end;

        then

         A47: (Cs11 | Us) = (Cs21 | Us) by A36, A37, FUNCT_1: 95;

        

         A48: (Cs11 . ( IC SCM+FSA )) = 11 by A32, A28, Lm21

        .= (Cs21 . ( IC SCM+FSA )) by A33, A28, Lm21;

        

         A49: for i holds ( IC ( Comput (P,s1,i))) in ( dom q) by A30, Th27, A28;

        for i holds ( IC ( Comput (Q,s2,i))) in ( dom q) by A31, Th27, A28;

        hence thesis by A29, A47, A48, A49, Th14, A28;

      end;

      set DD = {( intloc 0 ), ( IC SCM+FSA ), ( fsloc 0 )};

      let P,Q be Instruction-Sequence of SCM+FSA such that

       A50: q c= P & q c= Q;

      let s1,s2 be State of SCM+FSA ;

      assume that

       A51: p c= s1 and

       A52: p c= s2;

      let i be Nat;

      reconsider i as Nat;

      set Cs1i = ( Comput (P,s1,i)), Cs2i = ( Comput (Q,s2,i));

      

       A53: ( dom p) = DD by SCMFSA_M: 31;

      

       A54: DD c= ( dom Cs1i) by SCMFSA_M: 34;

      

       A55: DD c= ( dom Cs2i) by SCMFSA_M: 34;

      

       A56: ( intloc 0 ) in Us by A26, ENUMSET1:def 6;

      

       A57: ( fsloc 0 ) in Us by A26, ENUMSET1:def 6;

      

       A58: Us c= ( dom Cs1i) by Th19;

      

       A59: Us c= ( dom Cs2i) by Th19;

      

       A60: i > 10 implies (10 + 1) < (i + 1) by XREAL_1: 6;

      now

        let x be set;

        assume

         A61: x in DD;

        per cases by A61, ENUMSET1:def 1;

          suppose

           A62: x = ( intloc 0 );

          per cases ;

            suppose i <= 10;

            hence (Cs1i . x) = (Cs2i . x) by A1, A51, A52, A62, A50;

          end;

            suppose i > 10;

            then 11 <= i by A60, NAT_1: 13;

            then (Cs1i | Us) = (Cs2i | Us) by A27, A51, A52, A50;

            hence (Cs1i . x) = (Cs2i . x) by A56, A58, A59, A62, FUNCT_1: 95;

          end;

        end;

          suppose

           A63: x = ( IC SCM+FSA );

          per cases ;

            suppose i <= 10;

            hence (Cs1i . x) = (Cs2i . x) by A1, A51, A52, A63, A50;

          end;

            suppose i > 10;

            then 11 <= i by A60, NAT_1: 13;

            hence (Cs1i . x) = (Cs2i . x) by A27, A51, A52, A63, A50;

          end;

        end;

          suppose

           A64: x = ( fsloc 0 );

          per cases ;

            suppose i <= 10;

            hence (Cs1i . x) = (Cs2i . x) by A1, A51, A52, A64, A50;

          end;

            suppose i > 10;

            then 11 <= i by A60, NAT_1: 13;

            then (Cs1i | Us) = (Cs2i | Us) by A27, A51, A52, A50;

            hence (Cs1i . x) = (Cs2i . x) by A57, A58, A59, A64, FUNCT_1: 95;

          end;

        end;

      end;

      hence thesis by A53, A54, A55, FUNCT_1: 95;

    end;

    registration

      cluster Bubble-Sort-Algorithm -> halt-ending;

      coherence ;

    end

    theorem :: SCMBSORT:45

    ( Bubble-Sort-Algorithm ,( Initialize (( intloc 0 ) .--> 1))) computes Sorting-Function

    proof

      let x be set;

      assume x in ( dom Sorting-Function );

      then

      consider w be FinSequence of INT such that

       A1: x = (( fsloc 0 ) .--> w) by SCMFSA_M: 35;

      reconsider d = x as FinPartState of SCM+FSA by A1;

      set q = Bubble-Sort-Algorithm , p = ( Initialize (( intloc 0 ) .--> 1));

      

       A2: ( dom d) = {( fsloc 0 )} by A1;

      take d;

      thus x = d;

      

       A3: ( dom d) misses {( IC SCM+FSA )} by A2, SCMFSA_2: 57, ZFMISC_1: 11;

      

       A4: ( dom d) misses {( intloc 0 )} by A2, SCMFSA_2: 58, ZFMISC_1: 11;

      ( dom p) = (( dom (( intloc 0 ) .--> 1)) \/ {( IC SCM+FSA )}) by MEMSTR_0: 42

      .= ( {( IC SCM+FSA )} \/ {( intloc 0 )});

      then

       A5: ( dom d) misses ( dom p) by A3, A4, XBOOLE_1: 70;

      

       A6: (d +* p) = (p +* d) by A5, FUNCT_4: 35;

      ( Initialized d) = (d +* p)

      .= (p +* d) by A5, FUNCT_4: 35

      .= (p +* d)

      .= (p +* d);

      then

       A7: (p +* d) is q -autonomic by A1, Th29;

      now

        let t be State of SCM+FSA ;

        assume

         A8: (p +* d) c= t;

        let P be Instruction-Sequence of SCM+FSA such that

         A9: q c= P;

        set bf = ( bubble-sort ( fsloc 0 ));

        ( Initialize (( intloc 0 ) .--> 1)) c= (p +* d) by A6, FUNCT_4: 25;

        then ( Initialize (( intloc 0 ) .--> 1)) c= t by A8, XBOOLE_1: 1;

        hence P halts_on t by Lm26, A9, SCM_HALT:def 2;

      end;

      then

       A10: (p +* d) is q -halted;

      thus

       A11: (p +* d) is Autonomy of q by A10, A7, EXTPRO_1:def 12;

      consider z be FinSequence of REAL such that

       A12: (w,z) are_fiberwise_equipotent and

       A13: z is non-increasing and z is FinSequence of INT and

       A14: ( Sorting-Function . d) = (( fsloc 0 ) .--> z) by A1, SCMFSA_M: 36;

      consider t be State of SCM+FSA such that

       A15: (p +* d) c= t by PBOOLE: 141;

      consider T be Instruction-Sequence of SCM+FSA such that

       A16: q c= T by PBOOLE: 145;

      consider u be FinSequence of REAL such that

       A17: (w,u) are_fiberwise_equipotent and

       A18: u is non-increasing and u is FinSequence of INT and

       A19: (( Result (T,t)) . ( fsloc 0 )) = u by Th28, A1, A15, A16;

      

       A20: u = z by A12, A13, A17, A18, CLASSES1: 76, RFINSEQ: 23;

      ( fsloc 0 ) in the carrier of SCM+FSA ;

      then

       A21: ( fsloc 0 ) in ( dom ( Result (T,t))) by PARTFUN1:def 2;

      d c= (p +* d) by FUNCT_4: 25;

      then

       A22: ( dom d) c= ( dom (p +* d)) by RELAT_1: 11;

      

       A23: ( dom (( fsloc 0 ) .--> z)) = {( fsloc 0 )};

      ( Result (q,(p +* d))) = (( Result (T,t)) | ( dom (p +* d))) by A11, A15, A16, EXTPRO_1:def 13;

      hence ( Sorting-Function . d) c= ( Result (q,(p +* d))) by A2, A14, A19, A20, A21, A23, A22, FUNCT_4: 85, RELAT_1: 151;

    end;