scmfsa_2.miz



    begin

    reserve J,J1,K for Element of ( Segm 13),

b,b1,b2,c,c1,c2 for Element of SCM+FSA-Data-Loc ,

f,f1,f2 for Element of SCM+FSA-Data*-Loc ;

    definition

      :: SCMFSA_2:def1

      func SCM+FSA -> strict AMI-Struct over ( Segm 3) equals AMI-Struct (# SCM+FSA-Memory , ( In ( NAT , SCM+FSA-Memory )), SCM+FSA-Instr , SCM+FSA-OK , SCM*-VAL , SCM+FSA-Exec #);

      coherence ;

    end

    registration

      cluster SCM+FSA -> non empty with_non-empty_values;

      coherence ;

    end

    registration

      cluster SCM+FSA -> with_non_trivial_Instructions;

      coherence

      proof

        

         A1: [ 0 , {} , {} ] in SCM+FSA-Instr by SCMFSA_I: 3;

         [6, <* 0 *>, {} ] in SCM-Instr by SCM_INST: 2;

        then

         A2: [6, <* 0 *>, {} ] in SCM+FSA-Instr by SCMFSA_I: 1;

         [ 0 , {} , {} ] <> [6, <* 0 *>, {} ] by XTUPLE_0: 3;

        hence the InstructionsF of SCM+FSA is non trivial by A1, A2, ZFMISC_1:def 10;

      end;

    end

    theorem :: SCMFSA_2:1

    

     Th1: ( IC SCM+FSA ) = NAT by SCMFSA_1: 5, SUBSET_1:def 8;

    begin

    reserve k for Nat,

J,K,L for Element of ( Segm 13),

O,P,R for Element of ( Segm 9);

    notation

      synonym Int-Locations for SCM+FSA-Data-Loc ;

    end

    definition

      :: original: Int-Locations

      redefine

      func Int-Locations -> Subset of SCM+FSA ;

      coherence

      proof

         Int-Locations = SCM+FSA-Data-Loc ;

        hence thesis;

      end;

      ::$Canceled

      :: SCMFSA_2:def3

      func FinSeq-Locations -> Subset of SCM+FSA equals SCM+FSA-Data*-Loc ;

      coherence ;

    end

    registration

      cluster Int-like for Object of SCM+FSA ;

      existence

      proof

        reconsider x = the Element of SCM+FSA-Data-Loc as Object of SCM+FSA ;

        take x;

        thus thesis;

      end;

    end

    definition

      mode Int-Location is Int-like Object of SCM+FSA ;

      ::$Canceled

      :: SCMFSA_2:def5

      mode FinSeq-Location -> Object of SCM+FSA means

      : Def3: it in SCM+FSA-Data*-Loc ;

      existence

      proof

        set x = the Element of SCM+FSA-Data*-Loc ;

        reconsider x as Object of SCM+FSA ;

        take x;

        thus thesis;

      end;

    end

    reserve da for Int-Location,

fa for FinSeq-Location,

x,y for set;

    ::$Canceled

    definition

      let k be Nat;

      :: SCMFSA_2:def6

      func intloc k -> Int-Location equals ( dl. k);

      coherence

      proof

        

         A1: Int-Locations = SCM+FSA-Data-Loc ;

        ( dl. k) in SCM-Data-Loc by AMI_2:def 16;

        hence thesis by A1;

      end;

      :: SCMFSA_2:def7

      func fsloc k -> FinSeq-Location equals ( - (k + 1));

      coherence

      proof

        ( - (k + 1)) < ( - 0 ) by XREAL_1: 24;

        then ( - (k + 1)) in INT & not ( - (k + 1)) in NAT by INT_1:def 1;

        then ( - (k + 1)) in SCM+FSA-Data*-Loc by XBOOLE_0:def 5;

        hence thesis by Def3;

      end;

    end

    theorem :: SCMFSA_2:7

    for k1,k2 be Nat st k1 <> k2 holds ( fsloc k1) <> ( fsloc k2);

    theorem :: SCMFSA_2:8

    for dl be Int-Location holds ex i be Nat st dl = ( intloc i)

    proof

      let dl be Int-Location;

      dl in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider D = dl as Data-Location;

      consider i be Nat such that

       A1: D = ( dl. i) by AMI_5: 1;

      take i;

      thus thesis by A1;

    end;

    theorem :: SCMFSA_2:9

    

     Th4: for fl be FinSeq-Location holds ex i be Nat st fl = ( fsloc i)

    proof

      let fl be FinSeq-Location;

      

       A1: fl in SCM+FSA-Data*-Loc by Def3;

      then

      consider k be Nat such that

       A2: fl = k or fl = ( - k) by INT_1:def 1;

      k <> 0 by A1, A2, XBOOLE_0:def 5;

      then

      consider i be Nat such that

       A3: k = (i + 1) by NAT_1: 6;

      reconsider i as Nat;

      take i;

      thus thesis by A1, A2, A3, XBOOLE_0:def 5;

    end;

    registration

      cluster FinSeq-Locations -> infinite;

      coherence

      proof

        deffunc U( Nat) = ( fsloc $1);

        consider f be sequence of the carrier of SCM+FSA such that

         A1: for k be Element of NAT holds (f . k) = U(k) from FUNCT_2:sch 4;

        ( NAT , FinSeq-Locations ) are_equipotent

        proof

          take f;

          thus f is one-to-one

          proof

            let x1,x2 be object such that

             A2: x1 in ( dom f) & x2 in ( dom f) and

             A3: (f . x1) = (f . x2);

            reconsider k1 = x1, k2 = x2 as Element of NAT by A2;

            ( fsloc k1) = (f . k1) by A1

            .= ( fsloc k2) by A1, A3;

            hence thesis;

          end;

          thus ( dom f) = NAT by FUNCT_2:def 1;

          thus ( rng f) c= FinSeq-Locations

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

             A4: x in ( dom f) and

             A5: y = (f . x) by FUNCT_1:def 3;

            reconsider x as Element of NAT by A4;

            y = ( fsloc x) by A1, A5;

            hence thesis by Def3;

          end;

          thus FinSeq-Locations c= ( rng f)

          proof

            let y be object;

            assume y in FinSeq-Locations ;

            then y is FinSeq-Location by Def3;

            then

            consider i be Nat such that

             A6: y = ( fsloc i) by Th4;

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

            i in NAT ;

            then

             A7: i in ( dom f) by FUNCT_2:def 1;

            y = (f . i) by A1, A6;

            hence thesis by A7, FUNCT_1:def 3;

          end;

        end;

        hence thesis by CARD_1: 38;

      end;

    end

    theorem :: SCMFSA_2:10

    

     Th5: for I be Int-Location holds I is Data-Location

    proof

      let I be Int-Location;

      I in SCM-Data-Loc by AMI_2:def 16;

      hence thesis;

    end;

    theorem :: SCMFSA_2:11

    

     Th6: for l be Int-Location holds ( Values l) = INT

    proof

      let l be Int-Location;

      l in SCM-Data-Loc by AMI_2:def 16;

      hence thesis by SCMFSA_1: 10;

    end;

    theorem :: SCMFSA_2:12

    

     Th7: for l be FinSeq-Location holds ( Values l) = ( INT * )

    proof

      let l be FinSeq-Location;

      l in SCM+FSA-Data*-Loc by Def3;

      hence thesis by SCMFSA_1: 11;

    end;

    reserve la,lb for Nat,

La for Nat,

i for Instruction of SCM+FSA ,

I for Instruction of SCM ,

l for Nat,

LA,LB for Nat,

dA,dB,dC,dD for Element of SCM+FSA-Data-Loc ,

DA,DB,DC for Element of SCM-Data-Loc ,

fA,fB,fC for Element of SCM+FSA-Data*-Loc ,

f,g for FinSeq-Location,

A,B for Data-Location,

a,b,c,db for Int-Location;

    begin

    ::$Canceled

    theorem :: SCMFSA_2:15

    

     Th8: for I be Instruction of SCM+FSA st ( InsCode I) <= 8 holds I is Instruction of SCM

    proof

      let I be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode I) <= 8;

      now

        assume I in { [K, {} , <*dC, fB*>] : K in {11, 12} };

        then

        consider K, dC, fB such that

         A2: I = [K, {} , <*dC, fB*>] and

         A3: K in {11, 12};

        

         A4: (I `1_3 ) = K by A2;

        K = 12 or K = 11 by A3, TARSKI:def 2;

        hence contradiction by A1, A4;

      end;

      then

       A5: I in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) by XBOOLE_0:def 3;

      now

        assume I in { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} };

        then

        consider L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc such that

         A6: I = [L, {} , <*dB, fA, dA*>] and

         A7: L in {9, 10};

        

         A8: (I `1_3 ) = L by A6;

        L = 9 or L = 10 by A7, TARSKI:def 2;

        hence contradiction by A1, A8;

      end;

      hence thesis by A5, XBOOLE_0:def 3;

    end;

    theorem :: SCMFSA_2:16

    

     Th9: for I be Instruction of SCM+FSA holds ( InsCode I) <= 12

    proof

      let I be Instruction of SCM+FSA ;

      

       A1: I in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) or I in { [K, {} , <*dC, fB*>] : K in {11, 12} } by XBOOLE_0:def 3;

      per cases by A1, XBOOLE_0:def 3;

        suppose I in SCM-Instr ;

        then

        reconsider i = I as Instruction of SCM ;

        ( InsCode i) <= 8 by AMI_5: 5;

        hence thesis by XXREAL_0: 2;

      end;

        suppose I in { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} };

        then

        consider L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc such that

         A2: I = [L, {} , <*dB, fA, dA*>] and

         A3: L in {9, 10};

        

         A4: (I `1_3 ) = L by A2;

        L = 9 or L = 10 by A3, TARSKI:def 2;

        hence thesis by A4;

      end;

        suppose I in { [K, {} , <*dC, fB*>] : K in {11, 12} };

        then

        consider K, dC, fB such that

         A5: I = [K, {} , <*dC, fB*>] and

         A6: K in {11, 12};

        

         A7: (I `1_3 ) = K by A5;

        K = 11 or K = 12 by A6, TARSKI:def 2;

        hence thesis by A7;

      end;

    end;

    theorem :: SCMFSA_2:17

    

     Th10: for I be Instruction of SCM holds I is Instruction of SCM+FSA

    proof

      let I be Instruction of SCM ;

      I in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    definition

      let a, b;

      :: SCMFSA_2:def8

      func a := b -> Instruction of SCM+FSA means

      : Def6: ex A, B st a = A & b = B & it = (A := B);

      existence

      proof

        reconsider A = a, B = b as Data-Location by Th5;

        reconsider i = (A := B) as Instruction of SCM+FSA by Th10;

        take i, A, B;

        thus thesis;

      end;

      correctness ;

      :: SCMFSA_2:def9

      func AddTo (a,b) -> Instruction of SCM+FSA means

      : Def7: ex A, B st a = A & b = B & it = ( AddTo (A,B));

      existence

      proof

        reconsider A = a, B = b as Data-Location by Th5;

        reconsider i = ( AddTo (A,B)) as Instruction of SCM+FSA by Th10;

        take i, A, B;

        thus thesis;

      end;

      correctness ;

      :: SCMFSA_2:def10

      func SubFrom (a,b) -> Instruction of SCM+FSA means

      : Def8: ex A, B st a = A & b = B & it = ( SubFrom (A,B));

      existence

      proof

        reconsider A = a, B = b as Data-Location by Th5;

        reconsider i = ( SubFrom (A,B)) as Instruction of SCM+FSA by Th10;

        take i, A, B;

        thus thesis;

      end;

      correctness ;

      :: SCMFSA_2:def11

      func MultBy (a,b) -> Instruction of SCM+FSA means

      : Def9: ex A, B st a = A & b = B & it = ( MultBy (A,B));

      existence

      proof

        reconsider A = a, B = b as Data-Location by Th5;

        reconsider i = ( MultBy (A,B)) as Instruction of SCM+FSA by Th10;

        take i, A, B;

        thus thesis;

      end;

      correctness ;

      :: SCMFSA_2:def12

      func Divide (a,b) -> Instruction of SCM+FSA means

      : Def10: ex A, B st a = A & b = B & it = ( Divide (A,B));

      existence

      proof

        reconsider A = a, B = b as Data-Location by Th5;

        reconsider i = ( Divide (A,B)) as Instruction of SCM+FSA by Th10;

        take i, A, B;

        thus thesis;

      end;

      correctness ;

    end

    definition

      let la be Nat;

      :: SCMFSA_2:def13

      func goto la -> Instruction of SCM+FSA equals ( SCM-goto la);

      coherence by Th10;

      let a;

      :: SCMFSA_2:def14

      func a =0_goto la -> Instruction of SCM+FSA means

      : Def12: ex A st a = A & it = (A =0_goto la);

      existence

      proof

        reconsider A = a as Data-Location by Th5;

        reconsider i = (A =0_goto la) as Instruction of SCM+FSA by Th10;

        take i, A;

        thus thesis;

      end;

      correctness ;

      :: SCMFSA_2:def15

      func a >0_goto la -> Instruction of SCM+FSA means

      : Def13: ex A st a = A & it = (A >0_goto la);

      existence

      proof

        reconsider A = a as Data-Location by Th5;

        reconsider i = (A >0_goto la) as Instruction of SCM+FSA by Th10;

        take i, A;

        thus thesis;

      end;

      correctness ;

    end

    definition

      let c,i be Int-Location;

      let a be FinSeq-Location;

      :: SCMFSA_2:def16

      func c := (a,i) -> Instruction of SCM+FSA equals [9, {} , <*c, a, i*>];

      coherence

      proof

        reconsider A = a as Element of SCM+FSA-Data*-Loc by Def3;

        reconsider C = c, I = i as Element of SCM-Data-Loc by AMI_2:def 16;

        9 in {9, 10} by TARSKI:def 2;

        then [9, {} , <*C, A, I*>] in SCM+FSA-Instr by SCMFSA_I: 4;

        hence thesis;

      end;

      :: SCMFSA_2:def17

      func (a,i) := c -> Instruction of SCM+FSA equals [10, {} , <*c, a, i*>];

      coherence

      proof

        reconsider A = a as Element of SCM+FSA-Data*-Loc by Def3;

        reconsider C = c, I = i as Element of SCM-Data-Loc by AMI_2:def 16;

        10 in {9, 10} by TARSKI:def 2;

        then [10, {} , <*C, A, I*>] in SCM+FSA-Instr by SCMFSA_I: 4;

        hence thesis;

      end;

    end

    definition

      let i be Int-Location;

      let a be FinSeq-Location;

      :: SCMFSA_2:def18

      func i :=len a -> Instruction of SCM+FSA equals [11, {} , <*i, a*>];

      coherence

      proof

        reconsider A = a as Element of SCM+FSA-Data*-Loc by Def3;

        reconsider I = i as Element of SCM-Data-Loc by AMI_2:def 16;

        11 in {11, 12} by TARSKI:def 2;

        then [11, {} , <*I, A*>] in SCM+FSA-Instr by SCMFSA_I: 5;

        hence thesis;

      end;

      :: SCMFSA_2:def19

      func a :=<0,...,0> i -> Instruction of SCM+FSA equals [12, {} , <*i, a*>];

      coherence

      proof

        reconsider A = a as Element of SCM+FSA-Data*-Loc by Def3;

        reconsider I = i as Element of SCM-Data-Loc by AMI_2:def 16;

        12 in {11, 12} by TARSKI:def 2;

        then [12, {} , <*I, A*>] in SCM+FSA-Instr by SCMFSA_I: 5;

        hence thesis;

      end;

    end

    theorem :: SCMFSA_2:18

    ( InsCode (a := b)) = 1

    proof

      ex A, B st a = A & b = B & (a := b) = (A := B) by Def6;

      hence thesis;

    end;

    theorem :: SCMFSA_2:19

    ( InsCode ( AddTo (a,b))) = 2

    proof

      ex A, B st a = A & b = B & ( AddTo (a,b)) = ( AddTo (A,B)) by Def7;

      hence thesis;

    end;

    theorem :: SCMFSA_2:20

    ( InsCode ( SubFrom (a,b))) = 3

    proof

      ex A, B st a = A & b = B & ( SubFrom (a,b)) = ( SubFrom (A,B)) by Def8;

      hence thesis;

    end;

    theorem :: SCMFSA_2:21

    ( InsCode ( MultBy (a,b))) = 4

    proof

      ex A, B st a = A & b = B & ( MultBy (a,b)) = ( MultBy (A,B)) by Def9;

      hence thesis;

    end;

    theorem :: SCMFSA_2:22

    ( InsCode ( Divide (a,b))) = 5

    proof

      ex A, B st a = A & b = B & ( Divide (a,b)) = ( Divide (A,B)) by Def10;

      hence thesis;

    end;

    theorem :: SCMFSA_2:23

    ( InsCode ( goto lb)) = 6;

    theorem :: SCMFSA_2:24

    ( InsCode (a =0_goto lb)) = 7

    proof

      ex A st a = A & (a =0_goto lb) = (A =0_goto lb) by Def12;

      hence thesis;

    end;

    theorem :: SCMFSA_2:25

    ( InsCode (a >0_goto lb)) = 8

    proof

      ex A st a = A & (a >0_goto lb) = (A >0_goto lb) by Def13;

      hence thesis;

    end;

    theorem :: SCMFSA_2:26

    ( InsCode (c := (fa,a))) = 9;

    theorem :: SCMFSA_2:27

    ( InsCode ((fa,a) := c)) = 10;

    theorem :: SCMFSA_2:28

    ( InsCode (a :=len fa)) = 11;

    theorem :: SCMFSA_2:29

    ( InsCode (fa :=<0,...,0> a)) = 12;

    theorem :: SCMFSA_2:30

    

     Th23: for ins be Instruction of SCM+FSA st ( InsCode ins) = 1 holds ex da, db st ins = (da := db)

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 1;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider A, B such that

       A2: I = (A := B) by A1, AMI_5: 8;

      

       A3: Int-Locations = SCM+FSA-Data-Loc ;

      A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider da = A, db = B as Int-Location by A3;

      take da, db;

      thus thesis by A2, Def6;

    end;

    theorem :: SCMFSA_2:31

    

     Th24: for ins be Instruction of SCM+FSA st ( InsCode ins) = 2 holds ex da, db st ins = ( AddTo (da,db))

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 2;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider A, B such that

       A2: I = ( AddTo (A,B)) by A1, AMI_5: 9;

      

       A3: Int-Locations = SCM+FSA-Data-Loc ;

      A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider da = A, db = B as Int-Location by A3;

      take da, db;

      thus thesis by A2, Def7;

    end;

    theorem :: SCMFSA_2:32

    

     Th25: for ins be Instruction of SCM+FSA st ( InsCode ins) = 3 holds ex da, db st ins = ( SubFrom (da,db))

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 3;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider A, B such that

       A2: I = ( SubFrom (A,B)) by A1, AMI_5: 10;

      

       A3: Int-Locations = SCM+FSA-Data-Loc ;

      A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider da = A, db = B as Int-Location by A3;

      take da, db;

      thus thesis by A2, Def8;

    end;

    theorem :: SCMFSA_2:33

    

     Th26: for ins be Instruction of SCM+FSA st ( InsCode ins) = 4 holds ex da, db st ins = ( MultBy (da,db))

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 4;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider A, B such that

       A2: I = ( MultBy (A,B)) by A1, AMI_5: 11;

      

       A3: Int-Locations = SCM+FSA-Data-Loc ;

      A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider da = A, db = B as Int-Location by A3;

      take da, db;

      thus thesis by A2, Def9;

    end;

    theorem :: SCMFSA_2:34

    

     Th27: for ins be Instruction of SCM+FSA st ( InsCode ins) = 5 holds ex da, db st ins = ( Divide (da,db))

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 5;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider A, B such that

       A2: I = ( Divide (A,B)) by A1, AMI_5: 12;

      

       A3: Int-Locations = SCM+FSA-Data-Loc ;

      A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider da = A, db = B as Int-Location by A3;

      take da, db;

      thus thesis by A2, Def10;

    end;

    theorem :: SCMFSA_2:35

    

     Th28: for ins be Instruction of SCM+FSA st ( InsCode ins) = 6 holds ex lb st ins = ( goto lb)

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 6;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider La be Nat such that

       A2: I = ( SCM-goto La) by A1, AMI_5: 13;

      take La;

      thus thesis by A2;

    end;

    theorem :: SCMFSA_2:36

    

     Th29: for ins be Instruction of SCM+FSA st ( InsCode ins) = 7 holds ex lb, da st ins = (da =0_goto lb)

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 7;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider La be Nat, A such that

       A2: I = (A =0_goto La) by A1, AMI_5: 14;

      

       A3: Int-Locations = SCM+FSA-Data-Loc ;

      A in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider da = A as Int-Location by A3;

      take La, da;

      thus thesis by A2, Def12;

    end;

    theorem :: SCMFSA_2:37

    

     Th30: for ins be Instruction of SCM+FSA st ( InsCode ins) = 8 holds ex lb, da st ins = (da >0_goto lb)

    proof

      let ins be Instruction of SCM+FSA ;

      assume

       A1: ( InsCode ins) = 8;

      then

      reconsider I = ins as Instruction of SCM by Th8;

      consider La be Nat, A such that

       A2: I = (A >0_goto La) by A1, AMI_5: 15;

      

       A3: Int-Locations = SCM+FSA-Data-Loc ;

      A in SCM-Data-Loc by AMI_2:def 16;

      then

      reconsider da = A as Int-Location by A3;

      take La, da;

      thus thesis by A2, Def13;

    end;

    theorem :: SCMFSA_2:38

    

     Th31: for ins be Instruction of SCM+FSA st ( InsCode ins) = 9 holds ex a, b, fa st ins = (b := (fa,a))

    proof

      let ins be Instruction of SCM+FSA such that

       A1: ( InsCode ins) = 9;

       A2:

      now

        assume ins in { [K, {} , <*dC, fB*>] : K in {11, 12} };

        then

        consider K, dC, fB such that

         A3: ins = [K, {} , <*dC, fB*>] and

         A4: K in {11, 12};

        K = 11 or K = 12 by A4, TARSKI:def 2;

        hence contradiction by A1, A3;

      end;

      ins in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) or ins in { [K, {} , <*dC, fB*>] : K in {11, 12} } by XBOOLE_0:def 3;

      then ins in SCM-Instr or ins in { [L, {} , <*dB, fA, dA*>] : L in {9, 10} } by A2, XBOOLE_0:def 3;

      then

      consider L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc such that

       A5: ins = [L, {} , <*dB, fA, dA*>] and L in {9, 10} by A1, AMI_5: 5;

      reconsider f = fA as FinSeq-Location by Def3;

      reconsider c = dB, b = dA as Int-Location by AMI_2:def 16;

      take b, c, f;

      thus thesis by A1, A5;

    end;

    theorem :: SCMFSA_2:39

    

     Th32: for ins be Instruction of SCM+FSA st ( InsCode ins) = 10 holds ex a, b, fa st ins = ((fa,a) := b)

    proof

      let ins be Instruction of SCM+FSA such that

       A1: ( InsCode ins) = 10;

       A2:

      now

        assume ins in { [K, {} , <*dC, fB*>] : K in {11, 12} };

        then

        consider K, dC, fB such that

         A3: ins = [K, {} , <*dC, fB*>] and

         A4: K in {11, 12};

        K = 11 or K = 12 by A4, TARSKI:def 2;

        hence contradiction by A1, A3;

      end;

      ins in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) or ins in { [K, {} , <*dC, fB*>] : K in {11, 12} } by XBOOLE_0:def 3;

      then ins in SCM-Instr or ins in { [L, {} , <*dB, fA, dA*>] : L in {9, 10} } by A2, XBOOLE_0:def 3;

      then

      consider L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc such that

       A5: ins = [L, {} , <*dB, fA, dA*>] and L in {9, 10} by A1, AMI_5: 5;

      reconsider f = fA as FinSeq-Location by Def3;

      reconsider c = dB, b = dA as Int-Location by AMI_2:def 16;

      take b, c, f;

      thus thesis by A1, A5;

    end;

    theorem :: SCMFSA_2:40

    

     Th33: for ins be Instruction of SCM+FSA st ( InsCode ins) = 11 holds ex a, fa st ins = (a :=len fa)

    proof

      let ins be Instruction of SCM+FSA such that

       A1: ( InsCode ins) = 11;

       A2:

      now

        assume ins in { [L, {} , <*dB, fA, dA*>] : L in {9, 10} };

        then

        consider K be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc such that

         A3: ins = [K, {} , <*dB, fA, dA*>] and

         A4: K in {9, 10};

        (ins `1_3 ) = K by A3;

        hence contradiction by A1, A4, TARSKI:def 2;

      end;

      

       A5: ins in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) or ins in { [K, {} , <*dC, fB*>] : K in {11, 12} } by XBOOLE_0:def 3;

       not ins in SCM-Instr by A1, AMI_5: 5;

      then

      consider K, dB, fA such that

       A6: ins = [K, {} , <*dB, fA*>] and K in {11, 12} by A5, A2, XBOOLE_0:def 3;

      reconsider f = fA as FinSeq-Location by Def3;

      reconsider c = dB as Int-Location by AMI_2:def 16;

      take c, f;

      thus thesis by A1, A6;

    end;

    theorem :: SCMFSA_2:41

    

     Th34: for ins be Instruction of SCM+FSA st ( InsCode ins) = 12 holds ex a, fa st ins = (fa :=<0,...,0> a)

    proof

      let ins be Instruction of SCM+FSA such that

       A1: ( InsCode ins) = 12;

       A2:

      now

        assume ins in { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} };

        then

        consider K be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc such that

         A3: ins = [K, {} , <*dB, fA, dA*>] and

         A4: K in {9, 10};

        (ins `1_3 ) = K by A3;

        hence contradiction by A1, A4, TARSKI:def 2;

      end;

      

       A5: ins in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) or ins in { [K, {} , <*dC, fB*>] : K in {11, 12} } by XBOOLE_0:def 3;

       not ins in SCM-Instr by A1, AMI_5: 5;

      then

      consider K, dB, fA such that

       A6: ins = [K, {} , <*dB, fA*>] and K in {11, 12} by A5, A2, XBOOLE_0:def 3;

      reconsider f = fA as FinSeq-Location by Def3;

      reconsider c = dB as Int-Location by AMI_2:def 16;

      take c, f;

      thus thesis by A1, A6;

    end;

    begin

    reserve S for State of SCM ,

s,s1 for State of SCM+FSA ;

    theorem :: SCMFSA_2:42

    for s be State of SCM+FSA , d be Int-Location holds d in ( dom s)

    proof

      let s be State of SCM+FSA , d be Int-Location;

      ( dom s) = the carrier of SCM+FSA by PARTFUN1:def 2;

      hence thesis;

    end;

    theorem :: SCMFSA_2:43

    f in ( dom s)

    proof

      ( dom s) = SCM+FSA-Memory by PARTFUN1:def 2;

      hence thesis;

    end;

    theorem :: SCMFSA_2:44

    

     Th37: not f in ( dom S)

    proof

      f in SCM+FSA-Data*-Loc by Def3;

      hence thesis by SCMFSA_1: 30, XBOOLE_0: 3;

    end;

    theorem :: SCMFSA_2:45

    

     Th38: for s be State of SCM+FSA holds Int-Locations c= ( dom s)

    proof

      let s be State of SCM+FSA ;

      ( dom s) = the carrier of SCM+FSA by PARTFUN1:def 2;

      hence thesis;

    end;

    theorem :: SCMFSA_2:46

    

     Th39: for s be State of SCM+FSA holds FinSeq-Locations c= ( dom s)

    proof

      let s be State of SCM+FSA ;

      ( dom s) = the carrier of SCM+FSA by PARTFUN1:def 2;

      hence thesis;

    end;

    theorem :: SCMFSA_2:47

    for s be State of SCM+FSA holds ( dom (s | Int-Locations )) = Int-Locations

    proof

      let s be State of SCM+FSA ;

       Int-Locations c= ( dom s) by Th38;

      hence thesis by RELAT_1: 62;

    end;

    theorem :: SCMFSA_2:48

    for s be State of SCM+FSA holds ( dom (s | FinSeq-Locations )) = FinSeq-Locations

    proof

      let s be State of SCM+FSA ;

       FinSeq-Locations c= ( dom s) by Th39;

      hence thesis by RELAT_1: 62;

    end;

    theorem :: SCMFSA_2:49

    

     Th42: for s be State of SCM+FSA , i be Instruction of SCM holds (s | SCM-Memory ) is State of SCM

    proof

      let s be State of SCM+FSA , i be Instruction of SCM ;

      reconsider s as SCM+FSA-State by CARD_3: 107;

      (s | SCM-Memory ) is SCM-State by SCMFSA_1: 17;

      then (s | SCM-Memory ) is State of SCM by AMI_3: 29;

      hence thesis;

    end;

    theorem :: SCMFSA_2:50

    for s be State of SCM+FSA , s9 be State of SCM holds (s +* s9) is State of SCM+FSA

    proof

      let s be State of SCM+FSA , s9 be State of SCM ;

      reconsider s as SCM+FSA-State by CARD_3: 107;

      reconsider s9 as SCM-State by CARD_3: 107;

      (s +* s9) is SCM+FSA-State by SCMFSA_1: 18;

      then (s +* s9) is State of SCM+FSA ;

      hence thesis;

    end;

    theorem :: SCMFSA_2:51

    

     Th44: for i be Instruction of SCM , ii be Instruction of SCM+FSA , s be State of SCM , ss be State of SCM+FSA st i = ii & s = (ss | SCM-Memory ) holds ( Exec (ii,ss)) = (ss +* ( Exec (i,s)))

    proof

      let i be Instruction of SCM , ii be Instruction of SCM+FSA , s be State of SCM , ss be State of SCM+FSA such that

       A1: i = ii and

       A2: s = (ss | SCM-Memory );

      reconsider SS = ss as SCM+FSA-State by CARD_3: 107;

      reconsider II = ii as Element of SCM+FSA-Instr ;

      ( InsCode II) <= 8 by A1, AMI_5: 5;

      then

      consider I be Element of SCM-Instr , S be SCM-State such that

       A3: I = II & S = (SS | SCM-Memory ) and

       A4: ( SCM+FSA-Exec-Res (II,SS)) = (SS +* ( SCM-Exec-Res (I,S))) by SCMFSA_1:def 16;

      ( Exec (i,s)) = ( SCM-Exec-Res (I,S)) by A1, A2, A3, AMI_2:def 15;

      hence thesis by A4, SCMFSA_1:def 17;

    end;

    registration

      let s be State of SCM+FSA , d be Int-Location;

      cluster (s . d) -> integer;

      coherence

      proof

        reconsider D = d as Element of SCM-Data-Loc by AMI_2:def 16;

        reconsider S = s as SCM+FSA-State by CARD_3: 107;

        (S . D) = (s . d);

        hence thesis;

      end;

    end

    definition

      let s be State of SCM+FSA , d be FinSeq-Location;

      :: original: .

      redefine

      func s . d -> FinSequence of INT ;

      coherence

      proof

        reconsider D = d as Element of SCM+FSA-Data*-Loc by Def3;

        reconsider S = s as SCM+FSA-State by CARD_3: 107;

        (S . D) = (s . d);

        hence thesis;

      end;

    end

    theorem :: SCMFSA_2:52

    

     Th45: S = (s | SCM-Memory ) implies s = (s +* S) by FUNCT_4: 75;

    theorem :: SCMFSA_2:53

    

     Th46: s1 = (s +* S) implies (s1 . ( IC SCM+FSA )) = (S . ( IC SCM ))

    proof

      

       A1: ( dom S) = SCM-Memory by PARTFUN1:def 2;

      assume s1 = (s +* S);

      hence (s1 . ( IC SCM+FSA )) = (S . ( IC SCM )) by A1, Th1, AMI_3: 1, FUNCT_4: 13;

    end;

    theorem :: SCMFSA_2:54

    

     Th47: s1 = (s +* S) & A = a implies (S . A) = (s1 . a)

    proof

      assume that

       A1: s1 = (s +* S) and

       A2: A = a;

      ( dom S) = SCM-Memory by PARTFUN1:def 2;

      hence (s1 . a) = (S . A) by A1, A2, FUNCT_4: 13;

    end;

    theorem :: SCMFSA_2:55

    

     Th48: S = (s | SCM-Memory ) & A = a implies (S . A) = (s . a)

    proof

      assume S = (s | SCM-Memory );

      then s = (s +* S) by Th45;

      hence thesis by Th47;

    end;

    registration

      cluster SCM+FSA -> IC-Ins-separated;

      coherence by SCMFSA_1: 5, SCMFSA_1: 9, SUBSET_1:def 8;

    end

    theorem :: SCMFSA_2:56

    

     Th49: for dl be Int-Location holds dl <> ( IC SCM+FSA ) by AMI_2:def 16, Th1, FINSET_1: 15;

    theorem :: SCMFSA_2:57

    

     Th50: for dl be FinSeq-Location holds dl <> ( IC SCM+FSA )

    proof

      let dl be FinSeq-Location;

      now

        assume NAT in ( INT \ NAT );

        then

         A1: NAT in ( NAT \/ [: { 0 }, NAT :]) by NUMBERS:def 4, XBOOLE_0:def 5;

        per cases by A1, XBOOLE_0:def 3;

          suppose NAT in NAT ;

          hence contradiction;

        end;

          suppose NAT in [: { 0 }, NAT :];

          hence contradiction by FINSET_1: 15;

        end;

      end;

      hence thesis by Def3, Th1;

    end;

    theorem :: SCMFSA_2:58

    for il be Int-Location, dl be FinSeq-Location holds il <> dl

    proof

      let il be Int-Location, dl be FinSeq-Location;

      ( Values dl) = ( INT * ) by Th7;

      hence thesis by Th6, FUNCT_7: 16;

    end;

    theorem :: SCMFSA_2:59

    for il be Nat, dl be Int-Location holds il <> dl

    proof

      let il be Nat, dl be Int-Location;

      dl in [: {1}, NAT :] by AMI_2:def 16;

      then ex x,y be object st x in {1} & y in NAT & dl = [x, y] by ZFMISC_1: 84;

      hence il <> dl;

    end;

    theorem :: SCMFSA_2:60

    for il be Nat, dl be FinSeq-Location holds il <> dl

    proof

      let il be Nat, dl be FinSeq-Location;

      

       A1: dl in ( INT \ NAT ) by Def3;

      

       A2: il in NAT by ORDINAL1:def 12;

       NAT misses ( INT \ NAT ) by XBOOLE_1: 79;

      hence thesis by A1, A2, XBOOLE_0: 3;

    end;

    theorem :: SCMFSA_2:61

    for s1,s2 be State of SCM+FSA st ( IC s1) = ( IC s2) & (for a be Int-Location holds (s1 . a) = (s2 . a)) & (for f be FinSeq-Location holds (s1 . f) = (s2 . f)) holds s1 = s2

    proof

      let s1,s2 be State of SCM+FSA such that

       A1: ( IC s1) = ( IC s2) and

       A2: for a be Int-Location holds (s1 . a) = (s2 . a) and

       A3: for f be FinSeq-Location holds (s1 . f) = (s2 . f);

      s1 in ( product ( SCM*-VAL * SCM+FSA-OK )) by CARD_3: 107;

      then

      consider g1 be Function such that

       A4: s1 = g1 and

       A5: ( dom g1) = ( dom ( SCM*-VAL * SCM+FSA-OK )) and for x be object st x in ( dom ( SCM*-VAL * SCM+FSA-OK )) holds (g1 . x) in (( SCM*-VAL * SCM+FSA-OK ) . x) by CARD_3:def 5;

      s2 in ( product ( SCM*-VAL * SCM+FSA-OK )) by CARD_3: 107;

      then

      consider g2 be Function such that

       A6: s2 = g2 and

       A7: ( dom g2) = ( dom ( SCM*-VAL * SCM+FSA-OK )) and for x be object st x in ( dom ( SCM*-VAL * SCM+FSA-OK )) holds (g2 . x) in (( SCM*-VAL * SCM+FSA-OK ) . x) by CARD_3:def 5;

       A8:

      now

        let x be object;

        assume x in SCM+FSA-Memory ;

        then x in (( {( IC SCM+FSA )} \/ SCM-Data-Loc ) \/ SCM+FSA-Data*-Loc ) by Th1;

        then

         A9: x in ( {( IC SCM+FSA )} \/ SCM-Data-Loc ) or x in SCM+FSA-Data*-Loc by XBOOLE_0:def 3;

        

         A10: Int-Locations = SCM+FSA-Data-Loc ;

        per cases by A9, XBOOLE_0:def 3;

          suppose x in {( IC SCM+FSA )};

          then x = ( IC SCM+FSA ) by TARSKI:def 1;

          hence (g1 . x) = (g2 . x) by A1, A4, A6;

        end;

          suppose x in SCM-Data-Loc ;

          then x is Int-Location by A10, AMI_2:def 16;

          hence (g1 . x) = (g2 . x) by A2, A4, A6;

        end;

          suppose x in SCM+FSA-Data*-Loc ;

          then x is FinSeq-Location by Def3;

          hence (g1 . x) = (g2 . x) by A3, A4, A6;

        end;

      end;

      thus thesis by A4, A5, A6, A7, A8;

    end;

    theorem :: SCMFSA_2:62

    

     Th55: S = (s | SCM-Memory ) implies ( IC s) = ( IC S)

    proof

      assume S = (s | SCM-Memory );

      then s = (s +* S) by Th45;

      hence thesis by Th46;

    end;

    begin

    theorem :: SCMFSA_2:63

    

     Th56: (( Exec ((a := b),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (( Exec ((a := b),s)) . a) = (s . b) & (for c st c <> a holds (( Exec ((a := b),s)) . c) = (s . c)) & for f holds (( Exec ((a := b),s)) . f) = (s . f)

    proof

      consider A, B such that

       A1: a = A and

       A2: b = B and

       A3: (a := b) = (A := B) by Def6;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A4: ( Exec ((a := b),s)) = (s +* ( Exec ((A := B),S))) by A3, Th44;

      

      hence (( Exec ((a := b),s)) . ( IC SCM+FSA )) = (( Exec ((A := B),S)) . ( IC SCM )) by Th46

      .= (( IC S) + 1) by AMI_3: 2

      .= (( IC s) + 1) by Th55;

      

      thus (( Exec ((a := b),s)) . a) = (( Exec ((A := B),S)) . A) by A1, A4, Th47

      .= (S . B) by AMI_3: 2

      .= (s . b) by A2, Th48;

      hereby

        let c such that

         A5: c <> a;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec ((a := b),s)) . c) = (( Exec ((A := B),S)) . C) by A4, Th47

        .= (S . C) by A1, A5, AMI_3: 2

        .= (s . c) by Th48;

      end;

      let f;

      

       A6: not f in ( dom ( Exec ((A := B),S))) by Th37;

      thus (( Exec ((a := b),s)) . f) = (s . f) by A4, A6, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:64

    

     Th57: (( Exec (( AddTo (a,b)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (( Exec (( AddTo (a,b)),s)) . a) = ((s . a) + (s . b)) & (for c st c <> a holds (( Exec (( AddTo (a,b)),s)) . c) = (s . c)) & for f holds (( Exec (( AddTo (a,b)),s)) . f) = (s . f)

    proof

      consider A, B such that

       A1: a = A and

       A2: b = B and

       A3: ( AddTo (a,b)) = ( AddTo (A,B)) by Def7;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A4: ( Exec (( AddTo (a,b)),s)) = (s +* ( Exec (( AddTo (A,B)),S))) by A3, Th44;

      

      hence (( Exec (( AddTo (a,b)),s)) . ( IC SCM+FSA )) = (( Exec (( AddTo (A,B)),S)) . ( IC SCM )) by Th46

      .= (( IC S) + 1) by AMI_3: 3

      .= (( IC s) + 1) by Th55;

      

      thus (( Exec (( AddTo (a,b)),s)) . a) = (( Exec (( AddTo (A,B)),S)) . A) by A1, A4, Th47

      .= ((S . A) + (S . B)) by AMI_3: 3

      .= ((S . A) + (s . b)) by A2, Th48

      .= ((s . a) + (s . b)) by A1, Th48;

      hereby

        let c such that

         A5: c <> a;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec (( AddTo (a,b)),s)) . c) = (( Exec (( AddTo (A,B)),S)) . C) by A4, Th47

        .= (S . C) by A1, A5, AMI_3: 3

        .= (s . c) by Th48;

      end;

      let f;

      

       A6: not f in ( dom ( Exec (( AddTo (A,B)),S))) by Th37;

      thus (( Exec (( AddTo (a,b)),s)) . f) = (s . f) by A4, A6, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:65

    

     Th58: (( Exec (( SubFrom (a,b)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (( Exec (( SubFrom (a,b)),s)) . a) = ((s . a) - (s . b)) & (for c st c <> a holds (( Exec (( SubFrom (a,b)),s)) . c) = (s . c)) & for f holds (( Exec (( SubFrom (a,b)),s)) . f) = (s . f)

    proof

      consider A, B such that

       A1: a = A and

       A2: b = B and

       A3: ( SubFrom (a,b)) = ( SubFrom (A,B)) by Def8;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A4: ( Exec (( SubFrom (a,b)),s)) = (s +* ( Exec (( SubFrom (A,B)),S))) by A3, Th44;

      

      hence (( Exec (( SubFrom (a,b)),s)) . ( IC SCM+FSA )) = (( Exec (( SubFrom (A,B)),S)) . ( IC SCM )) by Th46

      .= (( IC S) + 1) by AMI_3: 4

      .= (( IC s) + 1) by Th55;

      

      thus (( Exec (( SubFrom (a,b)),s)) . a) = (( Exec (( SubFrom (A,B)),S)) . A) by A1, A4, Th47

      .= ((S . A) - (S . B)) by AMI_3: 4

      .= ((S . A) - (s . b)) by A2, Th48

      .= ((s . a) - (s . b)) by A1, Th48;

      hereby

        let c such that

         A5: c <> a;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec (( SubFrom (a,b)),s)) . c) = (( Exec (( SubFrom (A,B)),S)) . C) by A4, Th47

        .= (S . C) by A1, A5, AMI_3: 4

        .= (s . c) by Th48;

      end;

      let f;

      

       A6: not f in ( dom ( Exec (( SubFrom (A,B)),S))) by Th37;

      thus (( Exec (( SubFrom (a,b)),s)) . f) = (s . f) by A4, A6, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:66

    

     Th59: (( Exec (( MultBy (a,b)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (( Exec (( MultBy (a,b)),s)) . a) = ((s . a) * (s . b)) & (for c st c <> a holds (( Exec (( MultBy (a,b)),s)) . c) = (s . c)) & for f holds (( Exec (( MultBy (a,b)),s)) . f) = (s . f)

    proof

      consider A, B such that

       A1: a = A and

       A2: b = B and

       A3: ( MultBy (a,b)) = ( MultBy (A,B)) by Def9;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A4: ( Exec (( MultBy (a,b)),s)) = (s +* ( Exec (( MultBy (A,B)),S))) by A3, Th44;

      

      hence (( Exec (( MultBy (a,b)),s)) . ( IC SCM+FSA )) = (( Exec (( MultBy (A,B)),S)) . ( IC SCM )) by Th46

      .= (( IC S) + 1) by AMI_3: 5

      .= (( IC s) + 1) by Th55;

      

      thus (( Exec (( MultBy (a,b)),s)) . a) = (( Exec (( MultBy (A,B)),S)) . A) by A1, A4, Th47

      .= ((S . A) * (S . B)) by AMI_3: 5

      .= ((S . A) * (s . b)) by A2, Th48

      .= ((s . a) * (s . b)) by A1, Th48;

      hereby

        let c such that

         A5: c <> a;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec (( MultBy (a,b)),s)) . c) = (( Exec (( MultBy (A,B)),S)) . C) by A4, Th47

        .= (S . C) by A1, A5, AMI_3: 5

        .= (s . c) by Th48;

      end;

      let f;

      

       A6: not f in ( dom ( Exec (( MultBy (A,B)),S))) by Th37;

      thus (( Exec (( MultBy (a,b)),s)) . f) = (s . f) by A4, A6, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:67

    

     Th60: (( Exec (( Divide (a,b)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (a <> b implies (( Exec (( Divide (a,b)),s)) . a) = ((s . a) div (s . b))) & (( Exec (( Divide (a,b)),s)) . b) = ((s . a) mod (s . b)) & (for c st c <> a & c <> b holds (( Exec (( Divide (a,b)),s)) . c) = (s . c)) & for f holds (( Exec (( Divide (a,b)),s)) . f) = (s . f)

    proof

      consider A, B such that

       A1: a = A and

       A2: b = B and

       A3: ( Divide (a,b)) = ( Divide (A,B)) by Def10;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A4: ( Exec (( Divide (a,b)),s)) = (s +* ( Exec (( Divide (A,B)),S))) by A3, Th44;

      

      hence (( Exec (( Divide (a,b)),s)) . ( IC SCM+FSA )) = (( Exec (( Divide (A,B)),S)) . ( IC SCM )) by Th46

      .= (( IC S) + 1) by AMI_3: 6

      .= (( IC s) + 1) by Th55;

      hereby

        assume

         A5: a <> b;

        

        thus (( Exec (( Divide (a,b)),s)) . a) = (( Exec (( Divide (A,B)),S)) . A) by A1, A4, Th47

        .= ((S . A) div (S . B)) by A1, A2, A5, AMI_3: 6

        .= ((S . A) div (s . b)) by A2, Th48

        .= ((s . a) div (s . b)) by A1, Th48;

      end;

      

      thus (( Exec (( Divide (a,b)),s)) . b) = (( Exec (( Divide (A,B)),S)) . B) by A2, A4, Th47

      .= ((S . A) mod (S . B)) by AMI_3: 6

      .= ((S . A) mod (s . b)) by A2, Th48

      .= ((s . a) mod (s . b)) by A1, Th48;

      hereby

        let c such that

         A6: c <> a & c <> b;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec (( Divide (a,b)),s)) . c) = (( Exec (( Divide (A,B)),S)) . C) by A4, Th47

        .= (S . C) by A1, A2, A6, AMI_3: 6

        .= (s . c) by Th48;

      end;

      let f;

      

       A7: not f in ( dom ( Exec (( Divide (A,B)),S))) by Th37;

      thus (( Exec (( Divide (a,b)),s)) . f) = (s . f) by A4, A7, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:68

    (( Exec (( Divide (a,a)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (( Exec (( Divide (a,a)),s)) . a) = ((s . a) mod (s . a)) & (for c st c <> a holds (( Exec (( Divide (a,a)),s)) . c) = (s . c)) & for f holds (( Exec (( Divide (a,a)),s)) . f) = (s . f)

    proof

      consider A, B such that

       A1: a = A and

       A2: a = B & ( Divide (a,a)) = ( Divide (A,B)) by Def10;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A3: ( Exec (( Divide (a,a)),s)) = (s +* ( Exec (( Divide (A,A)),S))) by A1, A2, Th44;

      

      hence (( Exec (( Divide (a,a)),s)) . ( IC SCM+FSA )) = (( Exec (( Divide (A,A)),S)) . ( IC SCM )) by Th46

      .= (( IC S) + 1) by AMI_3: 6

      .= (( IC s) + 1) by Th55;

      

      thus (( Exec (( Divide (a,a)),s)) . a) = (( Exec (( Divide (A,A)),S)) . A) by A1, A3, Th47

      .= ((S . A) mod (S . A)) by AMI_3: 6

      .= ((S . A) mod (s . a)) by A1, Th48

      .= ((s . a) mod (s . a)) by A1, Th48;

      hereby

        let c such that

         A4: c <> a;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec (( Divide (a,a)),s)) . c) = (( Exec (( Divide (A,A)),S)) . C) by A3, Th47

        .= (S . C) by A1, A4, AMI_3: 6

        .= (s . c) by Th48;

      end;

      let f;

      

       A5: not f in ( dom ( Exec (( Divide (A,A)),S))) by Th37;

      thus (( Exec (( Divide (a,a)),s)) . f) = (s . f) by A3, A5, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:69

    

     Th62: (( Exec (( goto l),s)) . ( IC SCM+FSA )) = l & (for c holds (( Exec (( goto l),s)) . c) = (s . c)) & for f holds (( Exec (( goto l),s)) . f) = (s . f)

    proof

      consider La such that

       A1: l = La and

       A2: ( goto l) = ( SCM-goto La);

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A3: ( Exec (( goto l),s)) = (s +* ( Exec (( SCM-goto La),S))) by A2, Th44;

      

      hence (( Exec (( goto l),s)) . ( IC SCM+FSA )) = (( Exec (( SCM-goto La),S)) . ( IC SCM )) by Th46

      .= l by A1, AMI_3: 7;

      hereby

        let c;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec (( goto l),s)) . c) = (( Exec (( SCM-goto La),S)) . C) by A3, Th47

        .= (S . C) by AMI_3: 7

        .= (s . c) by Th48;

      end;

      let f;

      

       A4: not f in ( dom ( Exec (( SCM-goto La),S))) by Th37;

      thus (( Exec (( goto l),s)) . f) = (s . f) by A3, A4, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:70

    

     Th63: ((s . a) = 0 implies (( Exec ((a =0_goto l),s)) . ( IC SCM+FSA )) = l) & ((s . a) <> 0 implies (( Exec ((a =0_goto l),s)) . ( IC SCM+FSA )) = (( IC s) + 1)) & (for c holds (( Exec ((a =0_goto l),s)) . c) = (s . c)) & for f holds (( Exec ((a =0_goto l),s)) . f) = (s . f)

    proof

      consider A such that

       A1: a = A and

       A2: (a =0_goto l) = (A =0_goto l) by Def12;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A3: ( Exec ((a =0_goto l),s)) = (s +* ( Exec ((A =0_goto l),S))) by A2, Th44;

      hereby

        assume (s . a) = 0 ;

        then

         A4: (S . A) = 0 by A1, Th48;

        

        thus (( Exec ((a =0_goto l),s)) . ( IC SCM+FSA )) = (( Exec ((A =0_goto l),S)) . ( IC SCM )) by A3, Th46

        .= l by A4, AMI_3: 8;

      end;

      hereby

        assume (s . a) <> 0 ;

        then

         A5: (S . A) <> 0 by A1, Th48;

        

        thus (( Exec ((a =0_goto l),s)) . ( IC SCM+FSA )) = (( Exec ((A =0_goto l),S)) . ( IC SCM )) by A3, Th46

        .= (( IC S) + 1) by A5, AMI_3: 8

        .= (( IC s) + 1) by Th55;

      end;

      hereby

        let c;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec ((a =0_goto l),s)) . c) = (( Exec ((A =0_goto l),S)) . C) by A3, Th47

        .= (S . C) by AMI_3: 8

        .= (s . c) by Th48;

      end;

      let f;

      

       A6: not f in ( dom ( Exec ((A =0_goto l),S))) by Th37;

      thus (( Exec ((a =0_goto l),s)) . f) = (s . f) by A3, A6, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:71

    

     Th64: ((s . a) > 0 implies (( Exec ((a >0_goto l),s)) . ( IC SCM+FSA )) = l) & ((s . a) <= 0 implies (( Exec ((a >0_goto l),s)) . ( IC SCM+FSA )) = (( IC s) + 1)) & (for c holds (( Exec ((a >0_goto l),s)) . c) = (s . c)) & for f holds (( Exec ((a >0_goto l),s)) . f) = (s . f)

    proof

      consider A such that

       A1: a = A and

       A2: (a >0_goto l) = (A >0_goto l) by Def13;

      reconsider S = (s | SCM-Memory ) as State of SCM by Th42;

      

       A3: ( Exec ((a >0_goto l),s)) = (s +* ( Exec ((A >0_goto l),S))) by A2, Th44;

      hereby

        assume (s . a) > 0 ;

        then

         A4: (S . A) > 0 by A1, Th48;

        

        thus (( Exec ((a >0_goto l),s)) . ( IC SCM+FSA )) = (( Exec ((A >0_goto l),S)) . ( IC SCM )) by A3, Th46

        .= l by A4, AMI_3: 9;

      end;

      hereby

        assume (s . a) <= 0 ;

        then

         A5: (S . A) <= 0 by A1, Th48;

        

        thus (( Exec ((a >0_goto l),s)) . ( IC SCM+FSA )) = (( Exec ((A >0_goto l),S)) . ( IC SCM )) by A3, Th46

        .= (( IC S) + 1) by A5, AMI_3: 9

        .= (( IC s) + 1) by Th55;

      end;

      hereby

        let c;

        reconsider C = c as Data-Location by Th5;

        

        thus (( Exec ((a >0_goto l),s)) . c) = (( Exec ((A >0_goto l),S)) . C) by A3, Th47

        .= (S . C) by AMI_3: 9

        .= (s . c) by Th48;

      end;

      let f;

      

       A6: not f in ( dom ( Exec ((A >0_goto l),S))) by Th37;

      thus (( Exec ((a >0_goto l),s)) . f) = (s . f) by A3, A6, FUNCT_4: 11;

    end;

    theorem :: SCMFSA_2:72

    

     Th65: (( Exec ((c := (g,a)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (ex k st k = |.(s . a).| & (( Exec ((c := (g,a)),s)) . c) = ((s . g) /. k)) & (for b st b <> c holds (( Exec ((c := (g,a)),s)) . b) = (s . b)) & for f holds (( Exec ((c := (g,a)),s)) . f) = (s . f)

    proof

      reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;

      reconsider mk = a, ml = c as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = (c := (g,a)) as Element of SCM+FSA-Instr ;

      reconsider S = s as SCM+FSA-State by CARD_3: 107;

      reconsider J = 9 as Element of ( Segm 13) by NAT_1: 44;

      ( InsCode I) = 9;

      then

      consider i be Integer, k be Nat such that

       A1: k = |.(S . (I int_addr2 )).| and

       A2: i = ((S . (I coll_addr1 )) /. k) and

       A3: ( SCM+FSA-Exec-Res (I,S)) = ( SCM+FSA-Chg (( SCM+FSA-Chg (S,(I int_addr1 ),i)),(( IC S) + 1))) by SCMFSA_1:def 16;

      set S1 = ( SCM+FSA-Chg (S,(I int_addr1 ),i));

      

       A4: ( Exec ((c := (g,a)),s)) = ( SCM+FSA-Chg (S1,(( IC S) + 1))) by A3, SCMFSA_1:def 17;

      hence (( Exec ((c := (g,a)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th1, SCMFSA_1: 19;

      

       A5: I = [J, {} , <*ml, p, mk*>] & (I `3_3 ) = <*ml, p, mk*>;

      then

       A6: (I int_addr1 ) = ml by SCMFSA_I:def 3;

      

       A7: (I coll_addr1 ) = p by A5, SCMFSA_I:def 5;

      hereby

        reconsider k as Nat;

        take k;

        thus k = |.(s . a).| by A5, A1, SCMFSA_I:def 4;

        

        thus (( Exec ((c := (g,a)),s)) . c) = (S1 . ml) by A4, SCMFSA_1: 20

        .= ((s . g) /. k) by A2, A6, A7, SCMFSA_1: 24;

      end;

      hereby

        let b;

        reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;

        assume

         A8: b <> c;

        

        thus (( Exec ((c := (g,a)),s)) . b) = (S1 . mn) by A4, SCMFSA_1: 20

        .= (s . b) by A6, A8, SCMFSA_1: 25;

      end;

      let f;

      reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;

      

      thus (( Exec ((c := (g,a)),s)) . f) = (S1 . q) by A4, SCMFSA_1: 21

      .= (s . f) by SCMFSA_1: 26;

    end;

    theorem :: SCMFSA_2:73

    

     Th66: (( Exec (((g,a) := c),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (ex k st k = |.(s . a).| & (( Exec (((g,a) := c),s)) . g) = ((s . g) +* (k,(s . c)))) & (for b holds (( Exec (((g,a) := c),s)) . b) = (s . b)) & for f st f <> g holds (( Exec (((g,a) := c),s)) . f) = (s . f)

    proof

      reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;

      reconsider mk = a, ml = c as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = ((g,a) := c) as Element of SCM+FSA-Instr ;

      reconsider S = s as SCM+FSA-State by CARD_3: 107;

      reconsider J = 10 as Element of ( Segm 13) by NAT_1: 44;

      ( InsCode I) = 10;

      then

      consider F be FinSequence of INT , k be Nat such that

       A1: k = |.(S . (I int_addr2 )).| and

       A2: F = ((S . (I coll_addr1 )) +* (k,(S . (I int_addr1 )))) and

       A3: ( SCM+FSA-Exec-Res (I,S)) = ( SCM+FSA-Chg (( SCM+FSA-Chg (S,(I coll_addr1 ),F)),(( IC S) + 1))) by SCMFSA_1:def 16;

      set S1 = ( SCM+FSA-Chg (S,(I coll_addr1 ),F));

      

       A4: ( Exec (((g,a) := c),s)) = ( SCM+FSA-Chg (S1,(( IC S) + 1))) by A3, SCMFSA_1:def 17;

      hence (( Exec (((g,a) := c),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th1, SCMFSA_1: 19;

      

       A5: I = [J, {} , <*ml, p, mk*>] & (I `3_3 ) = <*ml, p, mk*>;

      then

       A6: (I coll_addr1 ) = p by SCMFSA_I:def 5;

      

       A7: (I int_addr1 ) = ml by A5, SCMFSA_I:def 3;

      hereby

        reconsider k as Nat;

        take k;

        thus k = |.(s . a).| by A5, A1, SCMFSA_I:def 4;

        

        thus (( Exec (((g,a) := c),s)) . g) = (S1 . p) by A4, SCMFSA_1: 21

        .= ((s . g) +* (k,(s . c))) by A2, A7, A6, SCMFSA_1: 27;

      end;

      hereby

        let b;

        reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;

        

        thus (( Exec (((g,a) := c),s)) . b) = (S1 . mn) by A4, SCMFSA_1: 20

        .= (s . b) by SCMFSA_1: 29;

      end;

      let f such that

       A8: f <> g;

      reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;

      

      thus (( Exec (((g,a) := c),s)) . f) = (S1 . q) by A4, SCMFSA_1: 21

      .= (s . f) by A6, A8, SCMFSA_1: 28;

    end;

    theorem :: SCMFSA_2:74

    

     Th67: (( Exec ((c :=len g),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (( Exec ((c :=len g),s)) . c) = ( len (s . g)) & (for b st b <> c holds (( Exec ((c :=len g),s)) . b) = (s . b)) & for f holds (( Exec ((c :=len g),s)) . f) = (s . f)

    proof

      reconsider S = s as SCM+FSA-State by CARD_3: 107;

      reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;

      reconsider I = (c :=len g) as Element of SCM+FSA-Instr ;

      set S1 = ( SCM+FSA-Chg (S,(I int_addr3 ),( len (S . (I coll_addr2 )))));

      reconsider J = 11 as Element of ( Segm 13) by NAT_1: 44;

      reconsider ml = c as Element of SCM-Data-Loc by AMI_2:def 16;

      

       A1: ( InsCode I) = 11;

      

       A2: ( Exec ((c :=len g),s)) = ( SCM+FSA-Exec-Res (I,S)) by SCMFSA_1:def 17

      .= ( SCM+FSA-Chg (S1,(( IC S) + 1))) by A1, SCMFSA_1:def 16;

      hence (( Exec ((c :=len g),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th1, SCMFSA_1: 19;

      

       A3: I = [J, {} , <*ml, p*>] & (I `3_3 ) = <*ml, p*>;

      then

       A4: (I int_addr3 ) = ml by SCMFSA_I:def 7;

      

       A5: (I coll_addr2 ) = p by A3, SCMFSA_I:def 8;

      

      thus (( Exec ((c :=len g),s)) . c) = (S1 . ml) by A2, SCMFSA_1: 20

      .= ( len (s . g)) by A4, A5, SCMFSA_1: 24;

      hereby

        let b;

        reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;

        assume

         A6: b <> c;

        

        thus (( Exec ((c :=len g),s)) . b) = (S1 . mn) by A2, SCMFSA_1: 20

        .= (s . b) by A4, A6, SCMFSA_1: 25;

      end;

      let f;

      reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;

      

      thus (( Exec ((c :=len g),s)) . f) = (S1 . q) by A2, SCMFSA_1: 21

      .= (s . f) by SCMFSA_1: 26;

    end;

    theorem :: SCMFSA_2:75

    

     Th68: (( Exec ((g :=<0,...,0> c),s)) . ( IC SCM+FSA )) = (( IC s) + 1) & (ex k st k = |.(s . c).| & (( Exec ((g :=<0,...,0> c),s)) . g) = (k |-> 0 )) & (for b holds (( Exec ((g :=<0,...,0> c),s)) . b) = (s . b)) & for f st f <> g holds (( Exec ((g :=<0,...,0> c),s)) . f) = (s . f)

    proof

      reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;

      reconsider ml = c as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = (g :=<0,...,0> c) as Element of SCM+FSA-Instr ;

      reconsider S = s as SCM+FSA-State by CARD_3: 107;

      reconsider J = 12 as Element of ( Segm 13) by NAT_1: 44;

      ( InsCode I) = 12;

      then

      consider F be FinSequence of INT , k be Nat such that

       A1: k = |.(S . (I int_addr3 )).| and

       A2: F = (k |-> 0 ) and

       A3: ( SCM+FSA-Exec-Res (I,S)) = ( SCM+FSA-Chg (( SCM+FSA-Chg (S,(I coll_addr2 ),F)),(( IC S) + 1))) by SCMFSA_1:def 16;

      set S1 = ( SCM+FSA-Chg (S,(I coll_addr2 ),F));

      

       A4: ( Exec ((g :=<0,...,0> c),s)) = ( SCM+FSA-Chg (S1,(( IC S) + 1))) by A3, SCMFSA_1:def 17;

      hence (( Exec ((g :=<0,...,0> c),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th1, SCMFSA_1: 19;

      

       A5: I = [J, {} , <*ml, p*>] & (I `3_3 ) = <*ml, p*>;

      then

       A6: (I coll_addr2 ) = p by SCMFSA_I:def 8;

      hereby

        reconsider k as Nat;

        take k;

        thus k = |.(s . c).| by A5, A1, SCMFSA_I:def 7;

        

        thus (( Exec ((g :=<0,...,0> c),s)) . g) = (S1 . p) by A4, SCMFSA_1: 21

        .= (k |-> 0 ) by A2, A6, SCMFSA_1: 27;

      end;

      hereby

        let b;

        reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;

        

        thus (( Exec ((g :=<0,...,0> c),s)) . b) = (S1 . mn) by A4, SCMFSA_1: 20

        .= (s . b) by SCMFSA_1: 29;

      end;

      let f such that

       A7: f <> g;

      reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;

      

      thus (( Exec ((g :=<0,...,0> c),s)) . f) = (S1 . q) by A4, SCMFSA_1: 21

      .= (s . f) by A6, A7, SCMFSA_1: 28;

    end;

    begin

    theorem :: SCMFSA_2:76

    for S be SCM+FSA-State st S = s holds ( IC s) = ( IC S) by SCMFSA_1: 5, SUBSET_1:def 8;

    theorem :: SCMFSA_2:77

    

     Th70: for i be Instruction of SCM , I be Instruction of SCM+FSA st i = I & i is halting holds I is halting

    proof

      let i be Instruction of SCM , I be Instruction of SCM+FSA such that

       A1: i = I;

      assume

       A2: i is halting;

      let S be State of SCM+FSA ;

      reconsider s = (S | SCM-Memory ) as State of SCM by Th42;

      

      thus ( Exec (I,S)) = (S +* ( Exec (i,s))) by A1, Th44

      .= (S +* s) by A2

      .= S by Th45;

    end;

    theorem :: SCMFSA_2:78

    

     Th71: for I be Instruction of SCM+FSA st ex s st (( Exec (I,s)) . ( IC SCM+FSA )) = (( IC s) + 1) holds I is non halting

    proof

      let I be Instruction of SCM+FSA ;

      given s such that

       A1: (( Exec (I,s)) . ( IC SCM+FSA )) = (( IC s) + 1);

      reconsider T = s as SCM+FSA-State by CARD_3: 107;

      ( IC T) = (T . NAT );

      then

      reconsider w = (T . NAT ) as Nat;

      assume I is halting;

      then

       A2: (( Exec (I,s)) . ( IC SCM+FSA )) = (T . NAT ) by Th1;

      (( Exec (I,s)) . ( IC SCM+FSA )) = (w + 1) by A1, SCMFSA_1: 5, SUBSET_1:def 8;

      hence contradiction by A2;

    end;

    registration

      let a, b;

      set s = the State of SCM+FSA ;

      cluster (a := b) -> non halting;

      coherence

      proof

        ( IC ( Exec ((a := b),s))) = (( IC s) + 1) by Th56;

        hence thesis by Th71;

      end;

      cluster ( AddTo (a,b)) -> non halting;

      coherence

      proof

        ( IC ( Exec (( AddTo (a,b)),s))) = (( IC s) + 1) by Th57;

        hence thesis by Th71;

      end;

      cluster ( SubFrom (a,b)) -> non halting;

      coherence

      proof

        ( IC ( Exec (( SubFrom (a,b)),s))) = (( IC s) + 1) by Th58;

        hence thesis by Th71;

      end;

      cluster ( MultBy (a,b)) -> non halting;

      coherence

      proof

        ( IC ( Exec (( MultBy (a,b)),s))) = (( IC s) + 1) by Th59;

        hence thesis by Th71;

      end;

      cluster ( Divide (a,b)) -> non halting;

      coherence

      proof

        ( IC ( Exec (( Divide (a,b)),s))) = (( IC s) + 1) by Th60;

        hence thesis by Th71;

      end;

    end

    theorem :: SCMFSA_2:79

    (a := b) is non halting;

    theorem :: SCMFSA_2:80

    ( AddTo (a,b)) is non halting;

    theorem :: SCMFSA_2:81

    ( SubFrom (a,b)) is non halting;

    theorem :: SCMFSA_2:82

    ( MultBy (a,b)) is non halting;

    theorem :: SCMFSA_2:83

    ( Divide (a,b)) is non halting;

    registration

      let la;

      cluster ( goto la) -> non halting;

      coherence

      proof

        set f = ( the_Values_of SCM+FSA );

        set s = the SCM+FSA-State;

        assume

         A1: ( goto la) is halting;

        reconsider a3 = la as Nat;

        set t = (s +* ( NAT .--> (a3 + 1)));

         NAT in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

        

        then

         A2: (t . NAT ) = (( NAT .--> (a3 + 1)) . NAT ) by FUNCT_4: 13

        .= (a3 + 1) by FUNCOP_1: 72;

        

         A3: for x be object st x in ( dom f) holds (t . x) in (f . x)

        proof

          let x be object such that

           A4: x in ( dom f);

          per cases ;

            suppose x = NAT ;

            hence thesis by A2, SCMFSA_1: 9;

          end;

            suppose x <> NAT ;

            then not x in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

            then (t . x) = (s . x) by FUNCT_4: 11;

            hence thesis by A4, CARD_3: 9;

          end;

        end;

        

         A5: { NAT } c= SCM+FSA-Memory by SCMFSA_1: 5, ZFMISC_1: 31;

        

         A6: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (a3 + 1)))) by FUNCT_4:def 1

        .= ( SCM+FSA-Memory \/ ( dom ( NAT .--> (a3 + 1)))) by SCMFSA_1: 33

        .= ( SCM+FSA-Memory \/ { NAT })

        .= SCM+FSA-Memory by A5, XBOOLE_1: 12;

        ( dom f) = SCM+FSA-Memory by SCMFSA_1: 32;

        then

        reconsider t as State of SCM+FSA by A6, A3, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

        reconsider w = t as SCM+FSA-State by CARD_3: 107;

         NAT in ( dom ( NAT .--> la)) by TARSKI:def 1;

        

        then

         A7: ((w +* ( NAT .--> la)) . NAT ) = (( NAT .--> la) . NAT ) by FUNCT_4: 13

        .= la by FUNCOP_1: 72;

        ((w +* ( NAT .--> la)) . NAT ) = (( SCM+FSA-Chg (w,a3)) . NAT )

        .= a3 by SCMFSA_1: 19

        .= (( Exec (( goto la),t)) . NAT ) by Th1, Th62

        .= (t . NAT ) by A1;

        hence contradiction by A2, A7;

      end;

    end

    theorem :: SCMFSA_2:84

    ( goto la) is non halting;

    registration

      let a, la;

      set f = ( the_Values_of SCM+FSA );

      set s = the SCM+FSA-State;

      cluster (a =0_goto la) -> non halting;

      coherence

      proof

        reconsider a3 = la as Nat;

        set t = (s +* ( NAT .--> (a3 + 1)));

        

         A1: { NAT } c= SCM+FSA-Memory by SCMFSA_1: 5, ZFMISC_1: 31;

        

         A2: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (a3 + 1)))) by FUNCT_4:def 1

        .= ( SCM+FSA-Memory \/ ( dom ( NAT .--> (a3 + 1)))) by SCMFSA_1: 33

        .= ( SCM+FSA-Memory \/ { NAT })

        .= SCM+FSA-Memory by A1, XBOOLE_1: 12;

        assume

         A3: (a =0_goto la) is halting;

         NAT in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

        

        then

         A4: (t . NAT ) = (( NAT .--> (a3 + 1)) . NAT ) by FUNCT_4: 13

        .= (a3 + 1) by FUNCOP_1: 72;

        

         A5: for x be object st x in ( dom f) holds (t . x) in (f . x)

        proof

          let x be object such that

           A6: x in ( dom f);

          per cases ;

            suppose x = NAT ;

            hence thesis by A4, SCMFSA_1: 9;

          end;

            suppose x <> NAT ;

            then not x in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

            then (t . x) = (s . x) by FUNCT_4: 11;

            hence thesis by A6, CARD_3: 9;

          end;

        end;

        ( dom f) = SCM+FSA-Memory by SCMFSA_1: 32;

        then

        reconsider t as State of SCM+FSA by A2, A5, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

        reconsider w = t as SCM+FSA-State by CARD_3: 107;

         NAT in ( dom ( NAT .--> la)) by TARSKI:def 1;

        

        then

         A7: ((w +* ( NAT .--> la)) . NAT ) = (( NAT .--> la) . NAT ) by FUNCT_4: 13

        .= la by FUNCOP_1: 72;

        per cases ;

          suppose

           A8: (t . a) <> 0 ;

          ( IC w) = (w . NAT );

          then

          reconsider e = (w . NAT ) as Nat;

          ( IC t) = ( IC w) by SCMFSA_1: 5, SUBSET_1:def 8;

          then

           A9: (( Exec ((a =0_goto la),t)) . ( IC SCM+FSA )) = (e + 1) by A8, Th63;

          (( Exec ((a =0_goto la),t)) . ( IC SCM+FSA )) = (w . NAT ) by A3, Th1;

          hence contradiction by A9;

        end;

          suppose

           A10: (t . a) = 0 ;

          ((w +* ( NAT .--> la)) . NAT ) = (( SCM+FSA-Chg (w,a3)) . NAT )

          .= a3 by SCMFSA_1: 19

          .= (( Exec ((a =0_goto la),t)) . NAT ) by A10, Th1, Th63

          .= (t . NAT ) by A3;

          hence contradiction by A4, A7;

        end;

      end;

      cluster (a >0_goto la) -> non halting;

      coherence

      proof

        reconsider a3 = la as Nat;

        set t = (s +* ( NAT .--> (a3 + 1)));

        

         A11: { NAT } c= SCM+FSA-Memory by SCMFSA_1: 5, ZFMISC_1: 31;

        

         A12: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (a3 + 1)))) by FUNCT_4:def 1

        .= ( SCM+FSA-Memory \/ ( dom ( NAT .--> (a3 + 1)))) by SCMFSA_1: 33

        .= ( SCM+FSA-Memory \/ { NAT })

        .= SCM+FSA-Memory by A11, XBOOLE_1: 12;

        assume

         A13: (a >0_goto la) is halting;

         NAT in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

        

        then

         A14: (t . NAT ) = (( NAT .--> (a3 + 1)) . NAT ) by FUNCT_4: 13

        .= (a3 + 1) by FUNCOP_1: 72;

        

         A15: for x be object st x in ( dom f) holds (t . x) in (f . x)

        proof

          let x be object such that

           A16: x in ( dom f);

          per cases ;

            suppose x = NAT ;

            hence thesis by A14, SCMFSA_1: 9;

          end;

            suppose x <> NAT ;

            then not x in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

            then (t . x) = (s . x) by FUNCT_4: 11;

            hence thesis by A16, CARD_3: 9;

          end;

        end;

        ( dom f) = SCM+FSA-Memory by SCMFSA_1: 32;

        then

        reconsider t as State of SCM+FSA by A12, A15, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

        reconsider w = t as SCM+FSA-State by CARD_3: 107;

         NAT in ( dom ( NAT .--> la)) by TARSKI:def 1;

        

        then

         A17: ((w +* ( NAT .--> la)) . NAT ) = (( NAT .--> la) . NAT ) by FUNCT_4: 13

        .= la by FUNCOP_1: 72;

        per cases ;

          suppose

           A18: (t . a) <= 0 ;

          ( IC w) = (w . NAT );

          then

          reconsider e = (w . NAT ) as Nat;

          ( IC t) = ( IC w) by SCMFSA_1: 5, SUBSET_1:def 8;

          then

           A19: (( Exec ((a >0_goto la),t)) . ( IC SCM+FSA )) = (e + 1) by A18, Th64;

          (( Exec ((a >0_goto la),t)) . ( IC SCM+FSA )) = (w . NAT ) by A13, Th1;

          hence contradiction by A19;

        end;

          suppose

           A20: (t . a) > 0 ;

          ((w +* ( NAT .--> la)) . NAT ) = (( SCM+FSA-Chg (w,a3)) . NAT )

          .= a3 by SCMFSA_1: 19

          .= (( Exec ((a >0_goto la),t)) . NAT ) by A20, Th1, Th64

          .= (t . NAT ) by A13;

          hence contradiction by A14, A17;

        end;

      end;

    end

    theorem :: SCMFSA_2:85

    (a =0_goto la) is non halting;

    theorem :: SCMFSA_2:86

    (a >0_goto la) is non halting;

    registration

      let c, f, a;

      set s = the State of SCM+FSA ;

      cluster (c := (f,a)) -> non halting;

      coherence

      proof

        (( Exec ((c := (f,a)),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th65;

        hence thesis by Th71;

      end;

      cluster ((f,a) := c) -> non halting;

      coherence

      proof

        (( Exec (((f,a) := c),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th66;

        hence thesis by Th71;

      end;

    end

    theorem :: SCMFSA_2:87

    (c := (f,a)) is non halting;

    theorem :: SCMFSA_2:88

    ((f,a) := c) is non halting;

    registration

      let c, f;

      set s = the State of SCM+FSA ;

      cluster (c :=len f) -> non halting;

      coherence

      proof

        (( Exec ((c :=len f),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th67;

        hence thesis by Th71;

      end;

      cluster (f :=<0,...,0> c) -> non halting;

      coherence

      proof

        (( Exec ((f :=<0,...,0> c),s)) . ( IC SCM+FSA )) = (( IC s) + 1) by Th68;

        hence thesis by Th71;

      end;

    end

    theorem :: SCMFSA_2:89

    (c :=len f) is non halting;

    theorem :: SCMFSA_2:90

    (f :=<0,...,0> c) is non halting;

    theorem :: SCMFSA_2:91

    for I be Instruction of SCM+FSA st I = [ 0 , {} , {} ] holds I is halting by Th70, AMI_3: 26;

    theorem :: SCMFSA_2:92

    

     Th85: for I be Instruction of SCM+FSA st ( InsCode I) = 0 holds I = [ 0 , {} , {} ]

    proof

      let I be Instruction of SCM+FSA such that

       A1: ( InsCode I) = 0 ;

       A2:

      now

        assume I in { [R, {} , <*DA, DC*>] : R in {1, 2, 3, 4, 5} };

        then ex R, DA, DC st I = [R, {} , <*DA, DC*>] & R in {1, 2, 3, 4, 5};

        hence contradiction by A1;

      end;

       A3:

      now

        assume I in { [O, <*LA*>, {} ] : O = 6 };

        then ex O, LA st I = [O, <*LA*>, {} ] & O = 6;

        hence contradiction by A1;

      end;

       A4:

      now

        assume I in { [P, <*LB*>, <*DB*>] : P in {7, 8} };

        then ex P, LB, DB st I = [P, <*LB*>, <*DB*>] & P in {7, 8};

        hence contradiction by A1;

      end;

       A5:

      now

        assume I in { [K, {} , <*dC, fB*>] : K in {11, 12} };

        then ex K, dC, fB st I = [K, {} , <*dC, fB*>] & K in {11, 12};

        hence contradiction by A1;

      end;

      

       A6: I in ( SCM-Instr \/ { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} }) by A5, XBOOLE_0:def 3;

      now

        assume I in { [L, {} , <*dB, fA, dA*>] where L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc : L in {9, 10} };

        then ex L be Element of ( Segm 13), dA,dB be Element of SCM+FSA-Data-Loc , fA be Element of SCM+FSA-Data*-Loc st I = [L, {} , <*dB, fA, dA*>] & L in {9, 10};

        hence contradiction by A1;

      end;

      then I in SCM-Instr by A6, XBOOLE_0:def 3;

      then I in (( { [ SCM-Halt , {} , {} ]} \/ { [O, <*LA*>, {} ] : O = 6 }) \/ { [P, <*LB*>, <*DB*>] : P in {7, 8} }) by A2, XBOOLE_0:def 3;

      then I in ( { [ SCM-Halt , {} , {} ]} \/ { [O, <*LA*>, {} ] : O = 6 }) by A4, XBOOLE_0:def 3;

      then I in { [ SCM-Halt , {} , {} ]} by A3, XBOOLE_0:def 3;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: SCMFSA_2:93

    

     Th86: for I be set holds I is Instruction of SCM+FSA iff I = [ 0 , {} , {} ] or (ex a, b st I = (a := b)) or (ex a, b st I = ( AddTo (a,b))) or (ex a, b st I = ( SubFrom (a,b))) or (ex a, b st I = ( MultBy (a,b))) or (ex a, b st I = ( Divide (a,b))) or (ex la st I = ( goto la)) or (ex lb, da st I = (da =0_goto lb)) or (ex lb, da st I = (da >0_goto lb)) or (ex b, a, fa st I = (a := (fa,b))) or (ex a, b, fa st I = ((fa,a) := b)) or (ex a, f st I = (a :=len f)) or ex a, f st I = (f :=<0,...,0> a)

    proof

      let I be set;

      thus I is Instruction of SCM+FSA implies I = [ 0 , {} , {} ] or (ex a, b st I = (a := b)) or (ex a, b st I = ( AddTo (a,b))) or (ex a, b st I = ( SubFrom (a,b))) or (ex a, b st I = ( MultBy (a,b))) or (ex a, b st I = ( Divide (a,b))) or (ex la st I = ( goto la)) or (ex lb, da st I = (da =0_goto lb)) or (ex lb, da st I = (da >0_goto lb)) or (ex b, a, fa st I = (a := (fa,b))) or (ex a, b, fa st I = ((fa,a) := b)) or (ex a, f st I = (a :=len f)) or ex a, f st I = (f :=<0,...,0> a)

      proof

        assume I is Instruction of SCM+FSA ;

        then

        reconsider J = I as Instruction of SCM+FSA ;

        set n = ( InsCode J);

        n = 0 or ... or n = 12 by Th9;

        hence thesis by Th23, Th24, Th25, Th26, Th27, Th28, Th29, Th30, Th31, Th32, Th33, Th34, Th85;

      end;

      thus thesis by SCMFSA_I: 3;

    end;

    

     Lm1: for W be Instruction of SCM+FSA st W is halting holds W = [ 0 , {} , {} ]

    proof

      set I = [ 0 , {} , {} ];

      let W be Instruction of SCM+FSA such that

       A1: W is halting;

      assume

       A2: I <> W;

      per cases by Th86;

        suppose W = [ 0 , {} , {} ];

        hence thesis by A2;

      end;

        suppose ex a, b st W = (a := b);

        hence thesis by A1;

      end;

        suppose ex a, b st W = ( AddTo (a,b));

        hence thesis by A1;

      end;

        suppose ex a, b st W = ( SubFrom (a,b));

        hence thesis by A1;

      end;

        suppose ex a, b st W = ( MultBy (a,b));

        hence thesis by A1;

      end;

        suppose ex a, b st W = ( Divide (a,b));

        hence thesis by A1;

      end;

        suppose ex la st W = ( goto la);

        hence thesis by A1;

      end;

        suppose ex lb, da st W = (da =0_goto lb);

        hence thesis by A1;

      end;

        suppose ex lb, da st W = (da >0_goto lb);

        hence thesis by A1;

      end;

        suppose ex b, a, fa st W = (a := (fa,b));

        hence thesis by A1;

      end;

        suppose ex a, b, fa st W = ((fa,a) := b);

        hence thesis by A1;

      end;

        suppose ex a, f st W = (a :=len f);

        hence thesis by A1;

      end;

        suppose ex a, f st W = (f :=<0,...,0> a);

        hence thesis by A1;

      end;

    end;

    registration

      cluster SCM+FSA -> halting;

      coherence by Th70, AMI_3: 26;

    end

    theorem :: SCMFSA_2:94

    

     Th87: for I be Instruction of SCM+FSA st I is halting holds I = ( halt SCM+FSA ) by Lm1;

    theorem :: SCMFSA_2:95

    for I be Instruction of SCM+FSA st ( InsCode I) = 0 holds I = ( halt SCM+FSA ) by Th85;

    theorem :: SCMFSA_2:96

    

     Th89: ( halt SCM ) = ( halt SCM+FSA );

    ::$Canceled

    theorem :: SCMFSA_2:98

    for i be Instruction of SCM , I be Instruction of SCM+FSA st i = I & i is non halting holds I is non halting by Th87, Th89;

    theorem :: SCMFSA_2:99

    for i,j be Nat holds ( fsloc i) <> ( intloc j)

    proof

      let i,j be Nat;

      ( fsloc i) in FinSeq-Locations by Def3;

      hence thesis by SCMFSA_1: 30, XBOOLE_0: 3;

    end;

    theorem :: SCMFSA_2:100

    

     Th92: ( Data-Locations SCM+FSA ) = ( Int-Locations \/ FinSeq-Locations )

    proof

      now

        assume NAT in FinSeq-Locations ;

        then

         A1: NAT in (( NAT \/ [: { 0 }, NAT :]) \ { [ 0 , 0 ]}) by NUMBERS:def 4;

         not NAT in NAT ;

        then NAT in [: { 0 }, NAT :] by A1, XBOOLE_0:def 3;

        then ex x,y be object st NAT = [x, y] by RELAT_1:def 1;

        hence contradiction;

      end;

      then FinSeq-Locations misses { NAT } by ZFMISC_1: 50;

      then

       A2: ( FinSeq-Locations \ { NAT }) = FinSeq-Locations by XBOOLE_1: 83;

       SCM-Data-Loc misses { NAT } by AMI_2: 20, ZFMISC_1: 50;

      then

       A3: SCM-Data-Loc misses { NAT };

      

       A4: ( SCM-Memory \ { NAT }) = ( SCM-Data-Loc \ { NAT }) by XBOOLE_1: 40

      .= Int-Locations by A3, XBOOLE_1: 83;

      

      thus ( Data-Locations SCM+FSA ) = (( SCM-Memory \/ FinSeq-Locations ) \ { NAT }) by SCMFSA_1: 5, SUBSET_1:def 8

      .= ( Int-Locations \/ FinSeq-Locations ) by A2, A4, XBOOLE_1: 42;

    end;

    theorem :: SCMFSA_2:101

    for i,j be Nat st i <> j holds ( intloc i) <> ( intloc j) by AMI_3: 10;

    reserve n for Nat,

I for Program of SCM+FSA ;

    theorem :: SCMFSA_2:102

     not a in ( dom ( Start-At (l, SCM+FSA )))

    proof

      assume a in ( dom ( Start-At (l, SCM+FSA )));

      then a = ( IC SCM+FSA ) by TARSKI:def 1;

      hence contradiction by Th49;

    end;

    theorem :: SCMFSA_2:103

     not f in ( dom ( Start-At (l, SCM+FSA )))

    proof

      assume f in ( dom ( Start-At (l, SCM+FSA )));

      then f = ( IC SCM+FSA ) by TARSKI:def 1;

      hence contradiction by Th50;

    end;

    theorem :: SCMFSA_2:104

    for s1,s2 be State of SCM+FSA st ( IC s1) = ( IC s2) & (for a be Int-Location holds (s1 . a) = (s2 . a)) & (for f be FinSeq-Location holds (s1 . f) = (s2 . f)) holds s1 = s2

    proof

      let s1,s2 be State of SCM+FSA such that

       A1: ( IC s1) = ( IC s2);

      ( IC SCM+FSA ) in ( dom s1) & ( IC SCM+FSA ) in ( dom s2) by MEMSTR_0: 2;

      then

       A2: s1 = (( DataPart s1) +* ( Start-At (( IC s1), SCM+FSA ))) & s2 = (( DataPart s2) +* ( Start-At (( IC s2), SCM+FSA ))) by MEMSTR_0: 26;

      assume that

       A3: for a be Int-Location holds (s1 . a) = (s2 . a) and

       A4: for f be FinSeq-Location holds (s1 . f) = (s2 . f);

      ( DataPart s1) = ( DataPart s2)

      proof

        

         A5: ( dom ( DataPart s1)) = ( Data-Locations SCM+FSA ) by MEMSTR_0: 9;

        hence ( dom ( DataPart s1)) = ( dom ( DataPart s2)) by MEMSTR_0: 9;

        let x be object;

        assume

         A6: x in ( dom ( DataPart s1));

        then

         A7: x in ( Int-Locations \/ FinSeq-Locations ) by A5, Th92;

        per cases by A7, XBOOLE_0:def 3;

          suppose x in Int-Locations ;

          then

           A8: x is Int-Location by AMI_2:def 16;

          

          thus (( DataPart s1) . x) = (s1 . x) by A6, A5, FUNCT_1: 49

          .= (s2 . x) by A8, A3

          .= (( DataPart s2) . x) by A6, A5, FUNCT_1: 49;

        end;

          suppose x in FinSeq-Locations ;

          then

           A9: x is FinSeq-Location by Def3;

          

          thus (( DataPart s1) . x) = (s1 . x) by A6, A5, FUNCT_1: 49

          .= (s2 . x) by A9, A4

          .= (( DataPart s2) . x) by A6, A5, FUNCT_1: 49;

        end;

      end;

      hence thesis by A1, A2;

    end;

    registration

      let f be FinSeq-Location, w be FinSequence of INT ;

      cluster (f .--> w) -> data-only;

      coherence by Th50, ZFMISC_1: 11;

    end

    registration

      let x be Int-Location, i be Integer;

      cluster (x .--> i) -> data-only;

      coherence by Th49, ZFMISC_1: 11;

    end

    registration

      let a, b;

      cluster (a := b) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let a, b;

      cluster ( AddTo (a,b)) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let a, b;

      cluster ( SubFrom (a,b)) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let a, b;

      cluster ( MultBy (a,b)) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let a, b;

      cluster ( Divide (a,b)) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let lb;

      cluster ( goto lb) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let lb, a;

      cluster (a =0_goto lb) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let lb, a;

      cluster (a >0_goto lb) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let fa, a, c;

      cluster (c := (fa,a)) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let fa, a, c;

      cluster ((fa,a) := c) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let fa, a;

      cluster (a :=len fa) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end

    registration

      let fa, a;

      cluster (fa :=<0,...,0> a) -> No-StopCode;

      coherence

      proof

        ( InsCode ( halt SCM+FSA )) = 0 ;

        hence thesis;

      end;

    end