scmfsa_4.miz



    begin

    reserve L,j,k,l,m,n,p,q for Nat,

A for Data-Location,

I for Instruction of SCM ;

    registration

      let a,b be Int-Location;

      cluster (a := b) -> ins-loc-free;

      coherence

      proof

        (a := b) = [1, {} , <*a, b*>] by SCMFSA10: 2;

        hence ( JumpPart (a := b)) is empty;

      end;

      cluster ( AddTo (a,b)) -> ins-loc-free;

      coherence

      proof

        ( AddTo (a,b)) = [2, {} , <*a, b*>] by SCMFSA10: 3;

        hence ( JumpPart ( AddTo (a,b))) is empty;

      end;

      cluster ( SubFrom (a,b)) -> ins-loc-free;

      coherence

      proof

        ( SubFrom (a,b)) = [3, {} , <*a, b*>] by SCMFSA10: 4;

        hence ( JumpPart ( SubFrom (a,b))) is empty;

      end;

      cluster ( MultBy (a,b)) -> ins-loc-free;

      coherence

      proof

        ( MultBy (a,b)) = [4, {} , <*a, b*>] by SCMFSA10: 5;

        hence ( JumpPart ( MultBy (a,b))) is empty;

      end;

      cluster ( Divide (a,b)) -> ins-loc-free;

      coherence

      proof

        ( Divide (a,b)) = [5, {} , <*a, b*>] by SCMFSA10: 6;

        hence ( JumpPart ( Divide (a,b))) is empty;

      end;

    end

    theorem :: SCMFSA_4:1

    

     Th1: for k,loc be Nat holds ( IncAddr (( goto loc),k)) = ( goto (loc + k)) by SCMFSA10: 41;

    theorem :: SCMFSA_4:2

    

     Th2: for k,loc be Nat, a be Int-Location holds ( IncAddr ((a =0_goto loc),k)) = (a =0_goto (loc + k))

    proof

      let k,loc be Nat, a be Int-Location;

      

       A1: (a =0_goto loc) = [7, <*loc*>, <*a*>] by SCMFSA10: 7;

      

       A2: (a =0_goto (loc + k)) = [7, <*(loc + k)*>, <*a*>] by SCMFSA10: 7;

      

       A3: ( InsCode ( IncAddr ((a =0_goto loc),k))) = ( InsCode (a =0_goto loc)) by COMPOS_0:def 9

      .= 7 by A1

      .= ( InsCode (a =0_goto (loc + k))) by A2;

      

       A4: ( AddressPart ( IncAddr ((a =0_goto loc),k))) = ( AddressPart (a =0_goto loc)) by COMPOS_0:def 9

      .= <*a*> by A1

      .= ( AddressPart (a =0_goto (loc + k))) by A2;

      

       A5: ( JumpPart ( IncAddr ((a =0_goto loc),k))) = (k + ( JumpPart (a =0_goto loc))) by COMPOS_0:def 9;

      ( JumpPart ( IncAddr ((a =0_goto loc),k))) = ( JumpPart (a =0_goto (loc + k)))

      proof

        thus

         A6: ( dom ( JumpPart ( IncAddr ((a =0_goto loc),k)))) = ( dom ( JumpPart (a =0_goto (loc + k)))) by A3, COMPOS_0:def 5;

        

         A7: ( JumpPart (a =0_goto loc)) = <*loc*> by A1;

        

         A8: ( JumpPart (a =0_goto (loc + k))) = <*(loc + k)*> by A2;

        let x be object;

        assume

         A9: x in ( dom ( JumpPart ( IncAddr ((a =0_goto loc),k))));

        ( dom <*(loc + k)*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A10: x = 1 by A9, A6, A8, TARSKI:def 1;

        

        thus (( JumpPart ( IncAddr ((a =0_goto loc),k))) . x) = (k + (( JumpPart (a =0_goto loc)) . x)) by A5, A9, VALUED_1:def 2

        .= (loc + k) by A7, A10, FINSEQ_1: 40

        .= (( JumpPart (a =0_goto (loc + k))) . x) by A8, A10, FINSEQ_1: 40;

      end;

      hence thesis by A3, A4, COMPOS_0: 1;

    end;

    theorem :: SCMFSA_4:3

    

     Th3: for k,loc be Nat, a be Int-Location holds ( IncAddr ((a >0_goto loc),k)) = (a >0_goto (loc + k))

    proof

      let k,loc be Nat, a be Int-Location;

      

       A1: (a >0_goto loc) = [8, <*loc*>, <*a*>] by SCMFSA10: 8;

      

       A2: (a >0_goto (loc + k)) = [8, <*(loc + k)*>, <*a*>] by SCMFSA10: 8;

      

       A3: ( InsCode ( IncAddr ((a >0_goto loc),k))) = ( InsCode (a >0_goto loc)) by COMPOS_0:def 9

      .= 8 by A1

      .= ( InsCode (a >0_goto (loc + k))) by A2;

      

       A4: ( AddressPart ( IncAddr ((a >0_goto loc),k))) = ( AddressPart (a >0_goto loc)) by COMPOS_0:def 9

      .= <*a*> by A1

      .= ( AddressPart (a >0_goto (loc + k))) by A2;

      

       A5: ( JumpPart ( IncAddr ((a >0_goto loc),k))) = (k + ( JumpPart (a >0_goto loc))) by COMPOS_0:def 9;

      ( JumpPart ( IncAddr ((a >0_goto loc),k))) = ( JumpPart (a >0_goto (loc + k)))

      proof

        thus

         A6: ( dom ( JumpPart ( IncAddr ((a >0_goto loc),k)))) = ( dom ( JumpPart (a >0_goto (loc + k)))) by A3, COMPOS_0:def 5;

        

         A7: ( JumpPart (a >0_goto loc)) = <*loc*> by A1;

        

         A8: ( JumpPart (a >0_goto (loc + k))) = <*(loc + k)*> by A2;

        let x be object;

        assume

         A9: x in ( dom ( JumpPart ( IncAddr ((a >0_goto loc),k))));

        ( dom <*(loc + k)*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A10: x = 1 by A9, A6, A8, TARSKI:def 1;

        

        thus (( JumpPart ( IncAddr ((a >0_goto loc),k))) . x) = (k + (( JumpPart (a >0_goto loc)) . x)) by A5, A9, VALUED_1:def 2

        .= (loc + k) by A7, A10, FINSEQ_1: 40

        .= (( JumpPart (a >0_goto (loc + k))) . x) by A8, A10, FINSEQ_1: 40;

      end;

      hence thesis by A3, A4, COMPOS_0: 1;

    end;

    registration

      let a,b be Int-Location;

      let f be FinSeq-Location;

      cluster (b := (f,a)) -> ins-loc-free;

      coherence ;

      cluster ((f,a) := b) -> ins-loc-free;

      coherence ;

    end

    registration

      let a be Int-Location;

      let f be FinSeq-Location;

      cluster (a :=len f) -> ins-loc-free;

      coherence ;

      cluster (f :=<0,...,0> a) -> ins-loc-free;

      coherence ;

    end

    reserve i for Instruction of SCM+FSA ;

    begin

    registration

      cluster SCM+FSA -> relocable;

      coherence

      proof

        let INS be Instruction of SCM+FSA , j,k be Nat;

        let s be State of SCM+FSA ;

        

         A1: ( IC ( IncIC (( Exec (( IncAddr (INS,j)),s)),k))) = (( IC ( Exec (( IncAddr (INS,j)),s))) + k) by MEMSTR_0: 53

        .= ( IC ( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k))))) by AMISTD_2:def 3;

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

        per cases ;

          suppose ( InsCode INS) = 0 ;

          then

           A2: INS = ( halt SCM+FSA ) by SCMFSA_2: 95;

          then

           A3: ( IncAddr (INS,j)) = ( halt SCM+FSA ) by COMPOS_0: 4;

          ( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) = ( Exec (INS,( IncIC (s,k)))) by A2, COMPOS_0: 4

          .= ( IncIC (s,k)) by A2, EXTPRO_1:def 3

          .= ( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) by A3, EXTPRO_1:def 3;

          hence thesis;

        end;

          suppose ( InsCode INS) = 1;

          then

          consider da,db be Int-Location such that

           A4: INS = (da := db) by SCMFSA_2: 30;

           A5:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( Exec (INS,( IncIC (s,k)))) . f) by A4, COMPOS_0: 4

            .= (( IncIC (s,k)) . f) by A4, SCMFSA_2: 63

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (INS,s)) . f) by A4, SCMFSA_2: 63

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A4, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            per cases ;

              suppose

               A6: da = d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A4, COMPOS_0: 4

              .= (( IncIC (s,k)) . db) by A4, A6, SCMFSA_2: 63

              .= (s . db) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A4, A6, SCMFSA_2: 63

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A4, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

              suppose

               A7: da <> d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A4, COMPOS_0: 4

              .= (( IncIC (s,k)) . d) by A4, A7, SCMFSA_2: 63

              .= (s . d) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A4, A7, SCMFSA_2: 63

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A4, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

          end;

          hence thesis by A5, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 2;

          then

          consider da,db be Int-Location such that

           A8: INS = ( AddTo (da,db)) by SCMFSA_2: 31;

           A9:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( Exec (INS,( IncIC (s,k)))) . f) by A8, COMPOS_0: 4

            .= (( IncIC (s,k)) . f) by A8, SCMFSA_2: 64

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (INS,s)) . f) by A8, SCMFSA_2: 64

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A8, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            per cases ;

              suppose

               A10: da = d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A8, COMPOS_0: 4

              .= ((( IncIC (s,k)) . da) + (( IncIC (s,k)) . db)) by A10, A8, SCMFSA_2: 64

              .= ((s . da) + (( IncIC (s,k)) . db)) by SCMFSA_3: 3

              .= ((s . da) + (s . db)) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A8, A10, SCMFSA_2: 64

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A8, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

              suppose

               A11: da <> d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A8, COMPOS_0: 4

              .= (( IncIC (s,k)) . d) by A8, A11, SCMFSA_2: 64

              .= (s . d) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A8, A11, SCMFSA_2: 64

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A8, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

          end;

          hence thesis by A9, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 3;

          then

          consider da,db be Int-Location such that

           A12: INS = ( SubFrom (da,db)) by SCMFSA_2: 32;

           A13:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( Exec (INS,( IncIC (s,k)))) . f) by A12, COMPOS_0: 4

            .= (( IncIC (s,k)) . f) by A12, SCMFSA_2: 65

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (INS,s)) . f) by A12, SCMFSA_2: 65

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A12, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            per cases ;

              suppose

               A14: da = d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A12, COMPOS_0: 4

              .= ((( IncIC (s,k)) . da) - (( IncIC (s,k)) . db)) by A14, A12, SCMFSA_2: 65

              .= ((s . da) - (( IncIC (s,k)) . db)) by SCMFSA_3: 3

              .= ((s . da) - (s . db)) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A12, A14, SCMFSA_2: 65

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A12, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

              suppose

               A15: da <> d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A12, COMPOS_0: 4

              .= (( IncIC (s,k)) . d) by A12, A15, SCMFSA_2: 65

              .= (s . d) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A12, A15, SCMFSA_2: 65

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A12, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

          end;

          hence thesis by A13, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 4;

          then

          consider da,db be Int-Location such that

           A16: INS = ( MultBy (da,db)) by SCMFSA_2: 33;

           A17:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( Exec (INS,( IncIC (s,k)))) . f) by A16, COMPOS_0: 4

            .= (( IncIC (s,k)) . f) by A16, SCMFSA_2: 66

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (INS,s)) . f) by A16, SCMFSA_2: 66

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A16, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            per cases ;

              suppose

               A18: da = d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A16, COMPOS_0: 4

              .= ((( IncIC (s,k)) . da) * (( IncIC (s,k)) . db)) by A18, A16, SCMFSA_2: 66

              .= ((s . da) * (( IncIC (s,k)) . db)) by SCMFSA_3: 3

              .= ((s . da) * (s . db)) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A16, A18, SCMFSA_2: 66

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A16, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

              suppose

               A19: da <> d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A16, COMPOS_0: 4

              .= (( IncIC (s,k)) . d) by A16, A19, SCMFSA_2: 66

              .= (s . d) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A16, A19, SCMFSA_2: 66

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A16, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

          end;

          hence thesis by A17, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 5;

          then

          consider da,db be Int-Location such that

           A20: INS = ( Divide (da,db)) by SCMFSA_2: 34;

           A21:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( Exec (INS,( IncIC (s,k)))) . f) by A20, COMPOS_0: 4

            .= (( IncIC (s,k)) . f) by A20, SCMFSA_2: 67

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (INS,s)) . f) by A20, SCMFSA_2: 67

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A20, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            per cases ;

              suppose

               A22: da <> db;

              hereby

                per cases ;

                  suppose

                   A23: da = d;

                  

                  thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A20, COMPOS_0: 4

                  .= ((( IncIC (s,k)) . da) div (( IncIC (s,k)) . db)) by A22, A23, A20, SCMFSA_2: 67

                  .= ((s . da) div (( IncIC (s,k)) . db)) by SCMFSA_3: 3

                  .= ((s . da) div (s . db)) by SCMFSA_3: 3

                  .= (( Exec (INS,s)) . d) by A20, A22, A23, SCMFSA_2: 67

                  .= (( Exec (( IncAddr (INS,j)),s)) . d) by A20, COMPOS_0: 4

                  .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

                end;

                  suppose

                   A24: db = d;

                  

                  thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A20, COMPOS_0: 4

                  .= ((( IncIC (s,k)) . da) mod (( IncIC (s,k)) . db)) by A24, A20, SCMFSA_2: 67

                  .= ((s . da) mod (( IncIC (s,k)) . db)) by SCMFSA_3: 3

                  .= ((s . da) mod (s . db)) by SCMFSA_3: 3

                  .= (( Exec (INS,s)) . d) by A20, A24, SCMFSA_2: 67

                  .= (( Exec (( IncAddr (INS,j)),s)) . d) by A20, COMPOS_0: 4

                  .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

                end;

                  suppose

                   A25: da <> d & db <> d;

                  

                  thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A20, COMPOS_0: 4

                  .= (( IncIC (s,k)) . d) by A20, A25, SCMFSA_2: 67

                  .= (s . d) by SCMFSA_3: 3

                  .= (( Exec (INS,s)) . d) by A20, A25, SCMFSA_2: 67

                  .= (( Exec (( IncAddr (INS,j)),s)) . d) by A20, COMPOS_0: 4

                  .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

                end;

              end;

            end;

              suppose

               A26: da = db;

              per cases ;

                suppose

                 A27: da = d;

                

                thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A20, COMPOS_0: 4

                .= ((( IncIC (s,k)) . da) mod (( IncIC (s,k)) . db)) by A26, A27, A20, SCMFSA_2: 67

                .= ((s . da) mod (( IncIC (s,k)) . db)) by SCMFSA_3: 3

                .= ((s . da) mod (s . db)) by SCMFSA_3: 3

                .= (( Exec (INS,s)) . d) by A20, A26, A27, SCMFSA_2: 67

                .= (( Exec (( IncAddr (INS,j)),s)) . d) by A20, COMPOS_0: 4

                .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

              end;

                suppose

                 A28: da <> d;

                

                thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A20, COMPOS_0: 4

                .= (( IncIC (s,k)) . d) by A20, A26, A28, SCMFSA_2: 67

                .= (s . d) by SCMFSA_3: 3

                .= (( Exec (INS,s)) . d) by A20, A26, A28, SCMFSA_2: 67

                .= (( Exec (( IncAddr (INS,j)),s)) . d) by A20, COMPOS_0: 4

                .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

              end;

            end;

          end;

          hence thesis by A21, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 6;

          then

          consider loc be Nat such that

           A29: INS = ( goto loc) by SCMFSA_2: 35;

          

           A30: ( IncAddr (INS,(j + k))) = ( goto (loc + (j + k))) by A29, Th1;

          reconsider jj = j as Element of NAT by ORDINAL1:def 12;

          

           A31: ( IncAddr (INS,jj)) = ( goto (loc + jj)) by A29, Th1;

           A32:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( IncIC (s,k)) . f) by A30, SCMFSA_2: 69

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A31, SCMFSA_2: 69

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( IncIC (s,k)) . d) by A30, SCMFSA_2: 69

            .= (s . d) by SCMFSA_3: 3

            .= (( Exec (( IncAddr (INS,j)),s)) . d) by A31, SCMFSA_2: 69

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

          end;

          hence thesis by A32, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 7;

          then

          consider loc be Nat, da be Int-Location such that

           A33: INS = (da =0_goto loc) by SCMFSA_2: 36;

          

           A34: ( IncAddr (INS,(j + k))) = (da =0_goto (loc + (j + k))) by A33, Th2;

          reconsider jj = j as Element of NAT by ORDINAL1:def 12;

          

           A35: ( IncAddr (INS,jj)) = (da =0_goto (loc + jj)) by A33, Th2;

           A36:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( IncIC (s,k)) . f) by A34, SCMFSA_2: 70

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A35, SCMFSA_2: 70

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( IncIC (s,k)) . d) by A34, SCMFSA_2: 70

            .= (s . d) by SCMFSA_3: 3

            .= (( Exec (( IncAddr (INS,j)),s)) . d) by A35, SCMFSA_2: 70

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

          end;

          hence thesis by A1, A36, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 8;

          then

          consider loc be Nat, da be Int-Location such that

           A37: INS = (da >0_goto loc) by SCMFSA_2: 37;

          

           A38: ( IncAddr (INS,(j + k))) = (da >0_goto (loc + (j + k))) by A37, Th3;

          reconsider jj = j as Element of NAT by ORDINAL1:def 12;

          

           A39: ( IncAddr (INS,jj)) = (da >0_goto (loc + jj)) by A37, Th3;

           A40:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( IncIC (s,k)) . f) by A38, SCMFSA_2: 71

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A39, SCMFSA_2: 71

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( IncIC (s,k)) . d) by A38, SCMFSA_2: 71

            .= (s . d) by SCMFSA_3: 3

            .= (( Exec (( IncAddr (INS,j)),s)) . d) by A39, SCMFSA_2: 71

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

          end;

          hence thesis by A40, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 9;

          then

          consider db,da be Int-Location, f be FinSeq-Location such that

           A41: INS = (da := (f,db)) by SCMFSA_2: 38;

           A42:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( Exec (INS,( IncIC (s,k)))) . f) by A41, COMPOS_0: 4

            .= (( IncIC (s,k)) . f) by A41, SCMFSA_2: 72

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (INS,s)) . f) by A41, SCMFSA_2: 72

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A41, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            per cases ;

              suppose

               A43: da = d;

              consider m be Nat such that

               A44: m = |.(s . db).| and

               A45: (( Exec (INS,s)) . da) = ((s . f) /. m) by A41, SCMFSA_2: 72;

              

               A46: ex m1 be Nat st m1 = |.(( IncIC (s,k)) . db).| & (( Exec (INS,( IncIC (s,k)))) . da) = ((( IncIC (s,k)) . f) /. m1) by A41, SCMFSA_2: 72;

              

               A47: (( IncIC (s,k)) . db) = (s . db) by SCMFSA_3: 3;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A41, COMPOS_0: 4

              .= ((s . f) /. m) by A44, A46, A43, A47, SCMFSA_3: 4

              .= (( IncIC (( Exec (INS,s)),k)) . d) by A45, A43, SCMFSA_3: 3

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by A41, COMPOS_0: 4;

            end;

              suppose

               A48: da <> d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A41, COMPOS_0: 4

              .= (( IncIC (s,k)) . d) by A41, A48, SCMFSA_2: 72

              .= (s . d) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A41, A48, SCMFSA_2: 72

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A41, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

          end;

          hence thesis by A42, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 10;

          then

          consider db,da be Int-Location, f be FinSeq-Location such that

           A49: INS = ((f,db) := da) by SCMFSA_2: 39;

           A50:

          now

            let g be FinSeq-Location;

            consider m be Nat such that

             A51: m = |.(s . db).| and

             A52: (( Exec (INS,s)) . f) = ((s . f) +* (m,(s . da))) by A49, SCMFSA_2: 73;

            

             A53: ex m1 be Nat st m1 = |.(( IncIC (s,k)) . db).| & (( Exec (INS,( IncIC (s,k)))) . f) = ((( IncIC (s,k)) . f) +* (m1,(( IncIC (s,k)) . da))) by A49, SCMFSA_2: 73;

            per cases ;

              suppose

               A54: f = g;

              

               A55: (( IncIC (s,k)) . f) = (s . f) & (( IncIC (s,k)) . db) = (s . db) by SCMFSA_3: 3, SCMFSA_3: 4;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . g) = (( Exec (INS,( IncIC (s,k)))) . g) by A49, COMPOS_0: 4

              .= ((s . f) +* (m,(s . da))) by A51, A53, A54, A55, SCMFSA_3: 3

              .= (( IncIC (( Exec (INS,s)),k)) . g) by A52, A54, SCMFSA_3: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . g) by A49, COMPOS_0: 4;

            end;

              suppose

               A56: f <> g;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . g) = (( Exec (INS,( IncIC (s,k)))) . g) by A49, COMPOS_0: 4

              .= (( IncIC (s,k)) . g) by A49, A56, SCMFSA_2: 73

              .= (s . g) by SCMFSA_3: 4

              .= (( Exec (INS,s)) . g) by A49, A56, SCMFSA_2: 73

              .= (( Exec (( IncAddr (INS,j)),s)) . g) by A49, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . g) by SCMFSA_3: 4;

            end;

          end;

          now

            let d be Int-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A49, COMPOS_0: 4

            .= (( IncIC (s,k)) . d) by A49, SCMFSA_2: 73

            .= (s . d) by SCMFSA_3: 3

            .= (( Exec (INS,s)) . d) by A49, SCMFSA_2: 73

            .= (( Exec (( IncAddr (INS,j)),s)) . d) by A49, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

          end;

          hence thesis by A50, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 11;

          then

          consider da be Int-Location, f be FinSeq-Location such that

           A57: INS = (da :=len f) by SCMFSA_2: 40;

           A58:

          now

            let f be FinSeq-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . f) = (( Exec (INS,( IncIC (s,k)))) . f) by A57, COMPOS_0: 4

            .= (( IncIC (s,k)) . f) by A57, SCMFSA_2: 74

            .= (s . f) by SCMFSA_3: 4

            .= (( Exec (INS,s)) . f) by A57, SCMFSA_2: 74

            .= (( Exec (( IncAddr (INS,j)),s)) . f) by A57, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . f) by SCMFSA_3: 4;

          end;

          now

            let d be Int-Location;

            per cases ;

              suppose

               A59: da = d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A57, COMPOS_0: 4

              .= ( len (( IncIC (s,k)) . f)) by A59, A57, SCMFSA_2: 74

              .= ( len (s . f)) by SCMFSA_3: 4

              .= (( Exec (INS,s)) . d) by A57, A59, SCMFSA_2: 74

              .= (( IncIC (( Exec (INS,s)),k)) . d) by SCMFSA_3: 3

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by A57, COMPOS_0: 4;

            end;

              suppose

               A60: da <> d;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A57, COMPOS_0: 4

              .= (( IncIC (s,k)) . d) by A57, A60, SCMFSA_2: 74

              .= (s . d) by SCMFSA_3: 3

              .= (( Exec (INS,s)) . d) by A57, A60, SCMFSA_2: 74

              .= (( Exec (( IncAddr (INS,j)),s)) . d) by A57, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

            end;

          end;

          hence thesis by A58, A1, SCMFSA_2: 104;

        end;

          suppose ( InsCode INS) = 12;

          then

          consider da be Int-Location, f be FinSeq-Location such that

           A61: INS = (f :=<0,...,0> da) by SCMFSA_2: 41;

           A62:

          now

            let g be FinSeq-Location;

            

             A63: (ex m be Nat st m = |.(s . da).| & (( Exec (INS,s)) . f) = (m |-> 0 )) & ex m be Nat st m = |.(( IncIC (s,k)) . da).| & (( Exec (INS,( IncIC (s,k)))) . f) = (m |-> 0 ) by A61, SCMFSA_2: 75;

            per cases ;

              suppose

               A64: f = g;

              

               A65: (( IncIC (s,k)) . da) = (s . da) by SCMFSA_3: 3;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . g) = (( Exec (INS,( IncIC (s,k)))) . g) by A61, COMPOS_0: 4

              .= (( IncIC (( Exec (INS,s)),k)) . g) by A63, A64, A65, SCMFSA_3: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . g) by A61, COMPOS_0: 4;

            end;

              suppose

               A66: f <> g;

              

              thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . g) = (( Exec (INS,( IncIC (s,k)))) . g) by A61, COMPOS_0: 4

              .= (( IncIC (s,k)) . g) by A61, A66, SCMFSA_2: 75

              .= (s . g) by SCMFSA_3: 4

              .= (( Exec (INS,s)) . g) by A61, A66, SCMFSA_2: 75

              .= (( Exec (( IncAddr (INS,j)),s)) . g) by A61, COMPOS_0: 4

              .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . g) by SCMFSA_3: 4;

            end;

          end;

          now

            let d be Int-Location;

            

            thus (( Exec (( IncAddr (INS,(j + k))),( IncIC (s,k)))) . d) = (( Exec (INS,( IncIC (s,k)))) . d) by A61, COMPOS_0: 4

            .= (( IncIC (s,k)) . d) by A61, SCMFSA_2: 75

            .= (s . d) by SCMFSA_3: 3

            .= (( Exec (INS,s)) . d) by A61, SCMFSA_2: 75

            .= (( Exec (( IncAddr (INS,j)),s)) . d) by A61, COMPOS_0: 4

            .= (( IncIC (( Exec (( IncAddr (INS,j)),s)),k)) . d) by SCMFSA_3: 3;

          end;

          hence thesis by A62, A1, SCMFSA_2: 104;

        end;

      end;

    end

    theorem :: SCMFSA_4:4

     not ( InsCode i) in {6, 7, 8} implies ( IncAddr (i,k)) = i

    proof

      assume not ( InsCode i) in {6, 7, 8};

      then

       A1: ( InsCode i) <> 6 & ( InsCode i) <> 7 & ( InsCode i) <> 8 by ENUMSET1:def 1;

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

      per cases by A1;

        suppose ( InsCode i) = 0 ;

        then i = ( halt SCM+FSA ) by SCMFSA_2: 95;

        hence thesis by COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 1;

        then

        consider da,db be Int-Location such that

         A2: i = (da := db) by SCMFSA_2: 30;

        thus thesis by A2, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 2;

        then

        consider da,db be Int-Location such that

         A3: i = ( AddTo (da,db)) by SCMFSA_2: 31;

        thus thesis by A3, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 3;

        then

        consider da,db be Int-Location such that

         A4: i = ( SubFrom (da,db)) by SCMFSA_2: 32;

        thus thesis by A4, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 4;

        then

        consider da,db be Int-Location such that

         A5: i = ( MultBy (da,db)) by SCMFSA_2: 33;

        thus thesis by A5, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 5;

        then

        consider da,db be Int-Location such that

         A6: i = ( Divide (da,db)) by SCMFSA_2: 34;

        thus thesis by A6, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 9;

        then

        consider db,da be Int-Location, f be FinSeq-Location such that

         A7: i = (da := (f,db)) by SCMFSA_2: 38;

        thus thesis by A7, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 10;

        then

        consider db,da be Int-Location, f be FinSeq-Location such that

         A8: i = ((f,db) := da) by SCMFSA_2: 39;

        thus thesis by A8, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 11;

        then

        consider da be Int-Location, f be FinSeq-Location such that

         A9: i = (da :=len f) by SCMFSA_2: 40;

        thus thesis by A9, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 12;

        then

        consider da be Int-Location, f be FinSeq-Location such that

         A10: i = (f :=<0,...,0> da) by SCMFSA_2: 41;

        thus thesis by A10, COMPOS_0: 4;

      end;

    end;