scmfsa_3.miz



    begin

    ::$Canceled

    reserve k for Nat,

da,db for Int-Location,

fa for FinSeq-Location;

    theorem :: SCMFSA_3:3

    for s be State of SCM+FSA , iloc be Nat, a be Int-Location holds (s . a) = ((s +* ( Start-At (iloc, SCM+FSA ))) . a)

    proof

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

      a in the carrier of SCM+FSA ;

      then a in ( dom s) by PARTFUN1:def 2;

      then

       A1: ( dom ( Start-At (iloc, SCM+FSA ))) = {( IC SCM+FSA )} & a in (( dom s) \/ ( dom ( Start-At (iloc, SCM+FSA )))) by XBOOLE_0:def 3;

      a <> ( IC SCM+FSA ) by SCMFSA_2: 56;

      then not a in {( IC SCM+FSA )} by TARSKI:def 1;

      hence thesis by A1, FUNCT_4:def 1;

    end;

    theorem :: SCMFSA_3:4

    for s be State of SCM+FSA , iloc be Nat, a be FinSeq-Location holds (s . a) = ((s +* ( Start-At (iloc, SCM+FSA ))) . a)

    proof

      let s be State of SCM+FSA , iloc be Nat, a be FinSeq-Location;

      a in the carrier of SCM+FSA ;

      then a in ( dom s) by PARTFUN1:def 2;

      then

       A1: ( dom ( Start-At (iloc, SCM+FSA ))) = {( IC SCM+FSA )} & a in (( dom s) \/ ( dom ( Start-At (iloc, SCM+FSA )))) by XBOOLE_0:def 3;

      a <> ( IC SCM+FSA ) by SCMFSA_2: 57;

      then not a in {( IC SCM+FSA )} by TARSKI:def 1;

      hence thesis by A1, FUNCT_4:def 1;

    end;

    begin

    definition

      let la be Int-Location;

      let a be Integer;

      :: original: .-->

      redefine

      func la .--> a -> FinPartState of SCM+FSA ;

      coherence

      proof

        a is Element of INT & ( Values la) = INT by INT_1:def 2, SCMFSA_2: 11;

        hence thesis;

      end;

    end

    registration

      cluster SCM+FSA -> IC-recognized;

      coherence

      proof

        for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic FinPartState of SCM+FSA st ( DataPart p) <> {} holds ( IC SCM+FSA ) in ( dom p)

        proof

          let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

          let p be q -autonomic FinPartState of SCM+FSA ;

          assume ( DataPart p) <> {} ;

          then

           A1: ( dom ( DataPart p)) <> {} ;

          assume not ( IC SCM+FSA ) in ( dom p);

          then

           A2: ( dom p) misses {( IC SCM+FSA )} by ZFMISC_1: 50;

           not p is q -autonomic

          proof

            set il = the Element of ( NAT \ ( dom q));

            set d2 = the Element of ( Int-Locations \ ( dom p));

            set d1 = the Element of ( dom ( DataPart p));

            

             A3: ( dom ( DataPart p)) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

             not NAT c= ( dom q);

            then

             A4: ( NAT \ ( dom q)) <> {} by XBOOLE_1: 37;

            then

            reconsider il as Element of NAT by XBOOLE_0:def 5;

             not Int-Locations c= ( dom p);

            then

             A5: ( Int-Locations \ ( dom p)) <> {} by XBOOLE_1: 37;

            then d2 in Int-Locations by XBOOLE_0:def 5;

            then

            reconsider d2 as Int-Location by AMI_2:def 16;

            

             A6: d1 in ( dom ( DataPart p)) by A1;

            ( DataPart p) c= p by MEMSTR_0: 12;

            then

             A7: ( dom ( DataPart p)) c= ( dom p) by RELAT_1: 11;

            ( dom ( DataPart p)) c= the carrier of SCM+FSA by RELAT_1:def 18;

            then

            reconsider d1 as Element of SCM+FSA by A6;

            per cases by A6, A3, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose d1 in Int-Locations ;

              then

              reconsider d1 as Int-Location by AMI_2:def 16;

              set p1 = (p +* ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))));

              set p2 = (p +* ((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))));

              set q1 = (q +* (il .--> (d1 := d2)));

              set q2 = (q +* (il .--> (d1 := d2)));

              consider s1 be State of SCM+FSA such that

               A8: p1 c= s1 by PBOOLE: 141;

              consider S1 be Instruction-Sequence of SCM+FSA such that

               A9: q1 c= S1 by PBOOLE: 145;

               not d2 in ( dom p) by A5, XBOOLE_0:def 5;

              then

               A10: ( dom p) misses {d2} by ZFMISC_1: 50;

              consider s2 be State of SCM+FSA such that

               A11: p2 c= s2 by PBOOLE: 141;

              consider S2 be Instruction-Sequence of SCM+FSA such that

               A12: q2 c= S2 by PBOOLE: 145;

              take P = S1, Q = S2;

              

               A14: not il in ( dom q) by A4, XBOOLE_0:def 5;

              ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 0 )) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1

              .= (( dom (d2 .--> 0 )) \/ {( IC SCM+FSA )})

              .= ( {d2} \/ {( IC SCM+FSA )});

              

              then (( dom p) /\ ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))))) = ((( dom p) /\ {d2}) \/ (( dom p) /\ {( IC SCM+FSA )})) by XBOOLE_1: 23

              .= ((( dom p) /\ {d2}) \/ {} ) by A2, XBOOLE_0:def 7

              .= {} by A10, XBOOLE_0:def 7;

              then ( dom p) misses ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) by XBOOLE_0:def 7;

              then p c= p1 by FUNCT_4: 32;

              then

               A15: p c= s1 by A8, XBOOLE_1: 1;

              ( dom q) misses ( dom (il .--> (d1 := d2))) by A14, ZFMISC_1: 50;

              then q c= q1 by FUNCT_4: 32;

              hence q c= P by A9, XBOOLE_1: 1;

              ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 1)) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1

              .= (( dom (d2 .--> 1)) \/ {( IC SCM+FSA )})

              .= ( {d2} \/ {( IC SCM+FSA )});

              

              then (( dom p) /\ ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))))) = ((( dom p) /\ {d2}) \/ (( dom p) /\ {( IC SCM+FSA )})) by XBOOLE_1: 23

              .= ((( dom p) /\ {d2}) \/ {} ) by A2, XBOOLE_0:def 7

              .= {} by A10, XBOOLE_0:def 7;

              then ( dom p) misses ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) by XBOOLE_0:def 7;

              then p c= p2 by FUNCT_4: 32;

              then

               A16: p c= s2 by A11, XBOOLE_1: 1;

              ( dom q) misses ( dom (il .--> (d1 := d2))) by A14, ZFMISC_1: 50;

              then q c= q1 by FUNCT_4: 32;

              hence q c= Q by A12, XBOOLE_1: 1;

              take s1, s2;

              thus p c= s1 by A15;

              thus p c= s2 by A16;

              take 1;

              

               A17: ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 1)) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1;

              

               A18: ( dom p) c= the carrier of SCM+FSA by RELAT_1:def 18;

              

               A19: ( dom ( Comput (S2,s2,1))) = the carrier of SCM+FSA by PARTFUN1:def 2;

              

               A20: ( dom (( Comput (S2,s2,1)) | ( dom p))) = ( dom p) by A18, A19, RELAT_1: 62;

              

               A21: ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 0 )) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1;

              

               A22: ( dom p1) = (( dom p) \/ ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))))) by FUNCT_4:def 1;

              

               A24: ( IC SCM+FSA ) in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

              then

               A25: ( IC SCM+FSA ) in ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) by A21, XBOOLE_0:def 3;

              then ( IC SCM+FSA ) in ( dom p1) by A22, XBOOLE_0:def 3;

              

              then

               A26: ( IC s1) = (p1 . ( IC SCM+FSA )) by A8, GRFUNC_1: 2

              .= (((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))) . ( IC SCM+FSA )) by A25, FUNCT_4: 13

              .= (( Start-At (il, SCM+FSA )) . ( IC SCM+FSA )) by A24, FUNCT_4: 13

              .= il by FUNCOP_1: 72;

              d2 <> ( IC SCM+FSA ) by SCMFSA_2: 56;

              then

               A27: not d2 in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

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

              then

               A28: d2 in ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) by A21, XBOOLE_0:def 3;

              then d2 in ( dom p1) by A22, XBOOLE_0:def 3;

              

              then

               A29: (s1 . d2) = (p1 . d2) by A8, GRFUNC_1: 2

              .= (((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))) . d2) by A28, FUNCT_4: 13

              .= ((d2 .--> 0 ) . d2) by A27, FUNCT_4: 11

              .= 0 by FUNCOP_1: 72;

              

               A30: il in ( dom (il .--> (d1 := d2))) by TARSKI:def 1;

              ( dom q1) = (( dom q) \/ ( dom (il .--> (d1 := d2)))) by FUNCT_4:def 1;

              then il in ( dom q1) by A30, XBOOLE_0:def 3;

              

              then

               A31: (S1 . il) = (q1 . il) by A9, GRFUNC_1: 2

              .= ((il .--> (d1 := d2)) . il) by A30, FUNCT_4: 13

              .= (d1 := d2) by FUNCOP_1: 72;

              

               A32: ( dom p) c= the carrier of SCM+FSA by RELAT_1:def 18;

              

               A33: ( dom ( Comput (S1,s1,1))) = the carrier of SCM+FSA by PARTFUN1:def 2;

              

               A34: ( dom (( Comput (S1,s1,1)) | ( dom p))) = ( dom p) by A32, A33, RELAT_1: 62;

              

               A35: ( dom p2) = (( dom p) \/ ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))))) by FUNCT_4:def 1;

              

               A36: ( dom q2) = (( dom q) \/ ( dom (il .--> (d1 := d2)))) by FUNCT_4:def 1;

              

               A38: ( IC SCM+FSA ) in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

              then

               A39: ( IC SCM+FSA ) in ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) by A17, XBOOLE_0:def 3;

              then ( IC SCM+FSA ) in ( dom p2) by A35, XBOOLE_0:def 3;

              

              then

               A40: ( IC s2) = (p2 . ( IC SCM+FSA )) by A11, GRFUNC_1: 2

              .= (((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))) . ( IC SCM+FSA )) by A39, FUNCT_4: 13

              .= (( Start-At (il, SCM+FSA )) . ( IC SCM+FSA )) by A38, FUNCT_4: 13

              .= il by FUNCOP_1: 72;

              d2 <> ( IC SCM+FSA ) by SCMFSA_2: 56;

              then

               A41: not d2 in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

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

              then

               A42: d2 in ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) by A17, XBOOLE_0:def 3;

              then d2 in ( dom p2) by A35, XBOOLE_0:def 3;

              

              then

               A43: (s2 . d2) = (p2 . d2) by A11, GRFUNC_1: 2

              .= (((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))) . d2) by A42, FUNCT_4: 13

              .= ((d2 .--> 1) . d2) by A41, FUNCT_4: 11

              .= 1 by FUNCOP_1: 72;

              

               A44: il in ( dom (il .--> (d1 := d2))) by TARSKI:def 1;

              il in ( dom q2) by A36, A44, XBOOLE_0:def 3;

              

              then

               A45: (S2 . il) = (q2 . il) by A12, GRFUNC_1: 2

              .= ((il .--> (d1 := d2)) . il) by A44, FUNCT_4: 13

              .= (d1 := d2) by FUNCOP_1: 72;

              

               A46: (S2 /. ( IC s2)) = (S2 . ( IC s2)) by PBOOLE: 143;

              

               A47: (( Comput (S2,s2,( 0 + 1))) . d1) = (( Following (S2,( Comput (S2,s2, 0 )))) . d1) by EXTPRO_1: 3

              .= (( Following (S2,s2)) . d1)

              .= 1 by A40, A45, A43, A46, SCMFSA_2: 63;

              

               A48: (S1 /. ( IC s1)) = (S1 . ( IC s1)) by PBOOLE: 143;

              (( Comput (S1,s1,( 0 + 1))) . d1) = (( Following (S1,( Comput (S1,s1, 0 )))) . d1) by EXTPRO_1: 3

              .= (( Following (S1,s1)) . d1)

              .= 0 by A26, A31, A29, A48, SCMFSA_2: 63;

              then ((( Comput (S1,s1,1)) | ( dom p)) . d1) = 0 by A7, A34, A6, FUNCT_1: 47;

              hence (( Comput (P,s1,1)) | ( dom p)) <> (( Comput (Q,s2,1)) | ( dom p)) by A47, A6, A7, A20, FUNCT_1: 47;

            end;

              suppose d1 in FinSeq-Locations ;

              then

              reconsider d1 as FinSeq-Location by SCMFSA_2:def 5;

              set p1 = (p +* ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))));

              set p2 = (p +* ((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))));

              set q1 = (q +* (il .--> (d1 :=<0,...,0> d2)));

              set q2 = (q +* (il .--> (d1 :=<0,...,0> d2)));

              consider s1 be State of SCM+FSA such that

               A49: p1 c= s1 by PBOOLE: 141;

              consider S1 be Instruction-Sequence of SCM+FSA such that

               A50: q1 c= S1 by PBOOLE: 145;

              

               A51: ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 0 )) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1;

              consider k such that

               A52: k = |.(s1 . d2).| and

               A53: (( Exec ((d1 :=<0,...,0> d2),s1)) . d1) = (k |-> 0 ) by SCMFSA_2: 75;

              

               A54: ( dom p1) = (( dom p) \/ ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))))) by FUNCT_4:def 1;

              

               A55: ( dom q1) = (( dom q) \/ ( dom (il .--> (d1 :=<0,...,0> d2)))) by FUNCT_4:def 1;

              

               A57: ( IC SCM+FSA ) in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

              then

               A58: ( IC SCM+FSA ) in ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) by A51, XBOOLE_0:def 3;

              then ( IC SCM+FSA ) in ( dom p1) by A54, XBOOLE_0:def 3;

              

              then

               A59: ( IC s1) = (p1 . ( IC SCM+FSA )) by A49, GRFUNC_1: 2

              .= (((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))) . ( IC SCM+FSA )) by A58, FUNCT_4: 13

              .= (( Start-At (il, SCM+FSA )) . ( IC SCM+FSA )) by A57, FUNCT_4: 13

              .= il by FUNCOP_1: 72;

              consider s2 be State of SCM+FSA such that

               A60: p2 c= s2 by PBOOLE: 141;

              consider S2 be Instruction-Sequence of SCM+FSA such that

               A61: q2 c= S2 by PBOOLE: 145;

              d2 <> ( IC SCM+FSA ) by SCMFSA_2: 56;

              then

               A62: not d2 in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

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

              then

               A63: d2 in ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) by A51, XBOOLE_0:def 3;

              then d2 in ( dom p1) by A54, XBOOLE_0:def 3;

              

              then (s1 . d2) = (p1 . d2) by A49, GRFUNC_1: 2

              .= (((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))) . d2) by A63, FUNCT_4: 13

              .= ((d2 .--> 0 ) . d2) by A62, FUNCT_4: 11

              .= 0 by FUNCOP_1: 72;

              

              then

               A64: (k |-> 0 ) = ( 0 |-> 0 ) by A52, ABSVALUE: 2

              .= {} by FINSEQ_2: 58;

               not d2 in ( dom p) by A5, XBOOLE_0:def 5;

              then

               A65: ( dom p) misses {d2} by ZFMISC_1: 50;

              

               A67: il in ( dom (il .--> (d1 :=<0,...,0> d2))) by ZFMISC_1: 31;

              then il in ( dom q1) by A55, XBOOLE_0:def 3;

              

              then

               A68: (S1 . il) = (q1 . il) by A50, GRFUNC_1: 2

              .= ((il .--> (d1 :=<0,...,0> d2)) . il) by A67, FUNCT_4: 13

              .= (d1 :=<0,...,0> d2) by FUNCOP_1: 72;

              

               A69: ( dom p) c= the carrier of SCM+FSA by RELAT_1:def 18;

              

               A70: ( dom ( Comput (S1,s1,1))) = the carrier of SCM+FSA by PARTFUN1:def 2;

              

               A71: ( dom (( Comput (S1,s1,1)) | ( dom p))) = ( dom p) by A69, A70, RELAT_1: 62;

              consider k such that

               A72: k = |.(s2 . d2).| and

               A73: (( Exec ((d1 :=<0,...,0> d2),s2)) . d1) = (k |-> 0 ) by SCMFSA_2: 75;

              

               A74: ( dom p2) = (( dom p) \/ ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))))) by FUNCT_4:def 1;

              take P = S1, Q = S2;

              

               A76: not il in ( dom q) by A4, XBOOLE_0:def 5;

              

               A77: ( dom q2) = (( dom q) \/ ( dom (il .--> (d1 :=<0,...,0> d2)))) by FUNCT_4:def 1;

              ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 0 )) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1

              .= (( dom (d2 .--> 0 )) \/ {( IC SCM+FSA )})

              .= ( {d2} \/ {( IC SCM+FSA )});

              

              then (( dom p) /\ ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA ))))) = ((( dom p) /\ {d2}) \/ (( dom p) /\ {( IC SCM+FSA )})) by XBOOLE_1: 23

              .= ((( dom p) /\ {d2}) \/ {} ) by A2, XBOOLE_0:def 7

              .= {} by A65, XBOOLE_0:def 7;

              then ( dom p) misses ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM+FSA )))) by XBOOLE_0:def 7;

              then p c= p1 by FUNCT_4: 32;

              then

               A78: p c= s1 by A49, XBOOLE_1: 1;

              ( dom q) misses ( dom (il .--> (d1 :=<0,...,0> d2))) by A76, ZFMISC_1: 50;

              then q c= q1 by FUNCT_4: 32;

              hence q c= P by A50, XBOOLE_1: 1;

              ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 1)) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1

              .= (( dom (d2 .--> 1)) \/ {( IC SCM+FSA )})

              .= ( {d2} \/ {( IC SCM+FSA )});

              

              then (( dom p) /\ ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))))) = ((( dom p) /\ {d2}) \/ (( dom p) /\ {( IC SCM+FSA )})) by XBOOLE_1: 23

              .= ((( dom p) /\ {d2}) \/ {} ) by A2, XBOOLE_0:def 7

              .= {} by A65, XBOOLE_0:def 7;

              then ( dom p) misses ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) by XBOOLE_0:def 7;

              then p c= p2 by FUNCT_4: 32;

              then

               A79: p c= s2 by A60, XBOOLE_1: 1;

              ( dom q) misses ( dom (il .--> (d1 :=<0,...,0> d2))) by A76, ZFMISC_1: 50;

              then q c= q2 by FUNCT_4: 32;

              hence q c= Q by A61, XBOOLE_1: 1;

              take s1, s2;

              thus p c= s1 by A78;

              thus p c= s2 by A79;

              take 1;

              

               A80: ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) = (( dom (d2 .--> 1)) \/ ( dom ( Start-At (il, SCM+FSA )))) by FUNCT_4:def 1;

              

               A82: ( IC SCM+FSA ) in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

              then

               A83: ( IC SCM+FSA ) in ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) by A80, XBOOLE_0:def 3;

              then ( IC SCM+FSA ) in ( dom p2) by A74, XBOOLE_0:def 3;

              

              then

               A84: ( IC s2) = (p2 . ( IC SCM+FSA )) by A60, GRFUNC_1: 2

              .= (((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))) . ( IC SCM+FSA )) by A83, FUNCT_4: 13

              .= (( Start-At (il, SCM+FSA )) . ( IC SCM+FSA )) by A82, FUNCT_4: 13

              .= il by FUNCOP_1: 72;

              d2 <> ( IC SCM+FSA ) by SCMFSA_2: 56;

              then

               A85: not d2 in ( dom ( Start-At (il, SCM+FSA ))) by TARSKI:def 1;

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

              then

               A86: d2 in ( dom ((d2 .--> 1) +* ( Start-At (il, SCM+FSA )))) by A80, XBOOLE_0:def 3;

              then d2 in ( dom p2) by A74, XBOOLE_0:def 3;

              

              then (s2 . d2) = (p2 . d2) by A60, GRFUNC_1: 2

              .= (((d2 .--> 1) +* ( Start-At (il, SCM+FSA ))) . d2) by A86, FUNCT_4: 13

              .= ((d2 .--> 1) . d2) by A85, FUNCT_4: 11

              .= 1 by FUNCOP_1: 72;

              

              then

               A87: (k |-> 0 ) = (1 |-> 0 ) by A72, ABSVALUE:def 1

              .= <* 0 *> by FINSEQ_2: 59;

              

               A88: il in ( dom (il .--> (d1 :=<0,...,0> d2))) by TARSKI:def 1;

              then il in ( dom q2) by A77, XBOOLE_0:def 3;

              

              then

               A89: (S2 . il) = (q2 . il) by A61, GRFUNC_1: 2

              .= ((il .--> (d1 :=<0,...,0> d2)) . il) by A88, FUNCT_4: 13

              .= (d1 :=<0,...,0> d2) by FUNCOP_1: 72;

              

               A90: (( Comput (S2,s2,( 0 + 1))) . d1) = (( Following (S2,( Comput (S2,s2, 0 )))) . d1) by EXTPRO_1: 3

              .= (( Following (S2,s2)) . d1)

              .= <* 0 *> by A84, A89, A73, A87, PBOOLE: 143;

              

               A91: ( dom p) c= the carrier of SCM+FSA by RELAT_1:def 18;

              

               A92: ( dom ( Comput (S2,s2,1))) = the carrier of SCM+FSA by PARTFUN1:def 2;

              

               A93: ( dom (( Comput (S2,s2,1)) | ( dom p))) = ( dom p) by A91, A92, RELAT_1: 62;

              (( Comput (S1,s1,( 0 + 1))) . d1) = (( Following (S1,( Comput (S1,s1, 0 )))) . d1) by EXTPRO_1: 3

              .= (( Following (S1,s1)) . d1)

              .= {} by A59, A68, A53, A64, PBOOLE: 143;

              then ((( Comput (S1,s1,1)) | ( dom p)) . d1) = {} by A6, A7, A71, FUNCT_1: 47;

              hence (( Comput (P,s1,1)) | ( dom p)) <> (( Comput (Q,s2,1)) | ( dom p)) by A90, A6, A7, A93, FUNCT_1: 47;

            end;

          end;

          hence contradiction;

        end;

        hence thesis by AMISTD_5: 3;

      end;

    end

    registration

      cluster SCM+FSA -> CurIns-recognized;

      coherence

      proof

        let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

        let p be q -autonomic non empty FinPartState of SCM+FSA , s be State of SCM+FSA such that

         A1: p c= s;

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

         A2: q c= P;

        let i be Nat;

        set Csi = ( Comput (P,s,i));

        set loc = ( IC Csi);

        set loc1 = (loc + 1);

        assume

         A3: not ( IC ( Comput (P,s,i))) in ( dom q);

        set I = (( intloc 0 ) := ( intloc 0 ));

        set q1 = (q +* (loc .--> I));

        set q2 = (q +* (loc .--> ( halt SCM+FSA )));

        reconsider P1 = (P +* (loc .--> I)) as Instruction-Sequence of SCM+FSA ;

        reconsider P2 = (P +* (loc .--> ( halt SCM+FSA ))) as Instruction-Sequence of SCM+FSA ;

        

         A5: loc in ( dom (loc .--> ( halt SCM+FSA ))) by TARSKI:def 1;

        

         A7: loc in ( dom (loc .--> I)) by TARSKI:def 1;

        

         A8: ( dom q) misses ( dom (loc .--> ( halt SCM+FSA ))) by A3, ZFMISC_1: 50;

        

         A9: ( dom q) misses ( dom (loc .--> I)) by A3, ZFMISC_1: 50;

        

         A10: q1 c= P1 by A2, FUNCT_4: 123;

        

         A11: q2 c= P2 by A2, FUNCT_4: 123;

        set Cs2i = ( Comput (P2,s,i)), Cs1i = ( Comput (P1,s,i));

         not p is q -autonomic

        proof

          ((loc .--> ( halt SCM+FSA )) . loc) = ( halt SCM+FSA ) by FUNCOP_1: 72;

          then

           A12: (P2 . loc) = ( halt SCM+FSA ) by A5, FUNCT_4: 13;

          

           A13: ((loc .--> I) . loc) = I by FUNCOP_1: 72;

          take P1, P2;

          q c= q1 by A9, FUNCT_4: 32;

          hence

           A14: q c= P1 by A10, XBOOLE_1: 1;

          q c= q2 by A8, FUNCT_4: 32;

          hence

           A15: q c= P2 by A11, XBOOLE_1: 1;

          take s, s;

          thus p c= s by A1;

          

           A16: (Cs1i | ( dom p)) = (Csi | ( dom p)) by A14, A2, A1, EXTPRO_1:def 10;

          thus p c= s by A1;

          

           A17: (Cs1i | ( dom p)) = (Cs2i | ( dom p)) by A14, A15, A1, EXTPRO_1:def 10;

          take k = (i + 1);

          set Cs1k = ( Comput (P1,s,k));

          

           A18: ( IC SCM+FSA ) in ( dom p) by AMISTD_5: 6;

          ( IC Csi) = ( IC (Csi | ( dom p))) by A18, FUNCT_1: 49;

          then ( IC Cs1i) = loc by A16, A18, FUNCT_1: 49;

          

          then

           A19: ( CurInstr (P1,Cs1i)) = (P1 . loc) by PBOOLE: 143

          .= I by A13, A7, FUNCT_4: 13;

          

           A20: Cs1k = ( Following (P1,Cs1i)) by EXTPRO_1: 3

          .= ( Exec (I,Cs1i)) by A19;

          

           A21: ( IC ( Exec (I,Cs1i))) = (( IC Cs1i) + 1) by SCMFSA_2: 63;

          

           A22: ( IC SCM+FSA ) in ( dom p) by AMISTD_5: 6;

          

           A23: ( IC Csi) = ( IC (Csi | ( dom p))) by A22, FUNCT_1: 49;

          

          then

           A24: ( IC Cs1k) = (loc + 1) by A20, A21, A16, A22, FUNCT_1: 49

          .= loc1;

          set Cs2k = ( Comput (P2,s,k));

          

           A25: Cs2k = ( Following (P2,Cs2i)) by EXTPRO_1: 3

          .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

          

           A26: (P2 /. ( IC Cs2i)) = (P2 . ( IC Cs2i)) by PBOOLE: 143;

          ( IC Cs2i) = loc by A16, A23, A17, A22, FUNCT_1: 49;

          then

           A27: ( IC Cs2k) = loc by A25, A12, A26, EXTPRO_1:def 3;

          ( IC (Cs1k | ( dom p))) = ( IC Cs1k) & ( IC (Cs2k | ( dom p))) = ( IC Cs2k) by A22, FUNCT_1: 49;

          hence thesis by A24, A27;

        end;

        hence contradiction;

      end;

    end

    theorem :: SCMFSA_3:5

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = (da := db) & da in ( dom p) holds (( Comput (P1,s1,i)) . db) = (( Comput (P2,s2,i)) . db)

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      

       A4: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      assume that

       A5: I = (da := db) and

       A6: da in ( dom p) & (( Comput (P1,s1,i)) . db) <> (( Comput (P2,s2,i)) . db);

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A7: (Cs1i1 . da) = (Cs1i . db) by A5, SCMFSA_2: 63;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then (Cs2i1 . da) = (Cs2i . db) by A3, A5, SCMFSA_2: 63;

      hence contradiction by A4, A6, A7, A2, A1, EXTPRO_1:def 10;

    end;

    theorem :: SCMFSA_3:6

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( AddTo (da,db)) & da in ( dom p) holds ((( Comput (P1,s1,i)) . da) + (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) + (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      

       A4: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      assume that

       A5: I = ( AddTo (da,db)) and

       A6: da in ( dom p) & ((( Comput (P1,s1,i)) . da) + (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) + (( Comput (P2,s2,i)) . db));

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A7: (Cs1i1 . da) = ((Cs1i . da) + (Cs1i . db)) by A5, SCMFSA_2: 64;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then (Cs2i1 . da) = ((Cs2i . da) + (Cs2i . db)) by A3, A5, SCMFSA_2: 64;

      hence contradiction by A1, A4, A6, A7, A2, EXTPRO_1:def 10;

    end;

    theorem :: SCMFSA_3:7

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( SubFrom (da,db)) & da in ( dom p) holds ((( Comput (P1,s1,i)) . da) - (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) - (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      

       A4: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      assume that

       A5: I = ( SubFrom (da,db)) and

       A6: da in ( dom p) & ((( Comput (P1,s1,i)) . da) - (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) - (( Comput (P2,s2,i)) . db));

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A7: (Cs1i1 . da) = ((Cs1i . da) - (Cs1i . db)) by A5, SCMFSA_2: 65;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then (Cs2i1 . da) = ((Cs2i . da) - (Cs2i . db)) by A3, A5, SCMFSA_2: 65;

      hence contradiction by A1, A4, A6, A7, A2, EXTPRO_1:def 10;

    end;

    theorem :: SCMFSA_3:8

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( MultBy (da,db)) & da in ( dom p) holds ((( Comput (P1,s1,i)) . da) * (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) * (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      

       A4: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      assume that

       A5: I = ( MultBy (da,db)) and

       A6: da in ( dom p) & ((( Comput (P1,s1,i)) . da) * (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) * (( Comput (P2,s2,i)) . db));

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A7: (Cs1i1 . da) = ((Cs1i . da) * (Cs1i . db)) by A5, SCMFSA_2: 66;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then (Cs2i1 . da) = ((Cs2i . da) * (Cs2i . db)) by A3, A5, SCMFSA_2: 66;

      hence contradiction by A1, A4, A6, A7, A2, EXTPRO_1:def 10;

    end;

    theorem :: SCMFSA_3:9

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( Divide (da,db)) & da in ( dom p) & da <> db holds ((( Comput (P1,s1,i)) . da) div (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) div (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      

       A4: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      assume that

       A5: I = ( Divide (da,db)) and

       A6: da in ( dom p) and

       A7: da <> db and

       A8: ((( Comput (P1,s1,i)) . da) div (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) div (( Comput (P2,s2,i)) . db));

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A9: (Cs1i1 . da) = ((Cs1i . da) div (Cs1i . db)) by A5, A7, SCMFSA_2: 67;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then (Cs2i1 . da) = ((Cs2i . da) div (Cs2i . db)) by A3, A5, A7, SCMFSA_2: 67;

      hence contradiction by A1, A4, A8, A9, A2, A6, EXTPRO_1:def 10;

    end;

    theorem :: SCMFSA_3:10

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( Divide (da,db)) & db in ( dom p) holds ((( Comput (P1,s1,i)) . da) mod (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) mod (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A4: I = ( Divide (da,db)) and

       A5: db in ( dom p) and

       A6: ((( Comput (P1,s1,i)) . da) mod (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) mod (( Comput (P2,s2,i)) . db));

      

       A7: ((Cs1i1 | ( dom p)) . db) = (Cs1i1 . db) & ((Cs2i1 | ( dom p)) . db) = (Cs2i1 . db) by A5, FUNCT_1: 49;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A8: (Cs1i1 . db) = ((Cs1i . da) mod (Cs1i . db)) by A4, SCMFSA_2: 67;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then (Cs2i1 . db) = ((Cs2i . da) mod (Cs2i . db)) by A3, A4, SCMFSA_2: 67;

      hence contradiction by A1, A6, A7, A8, A2, EXTPRO_1:def 10;

    end;

    theorem :: SCMFSA_3:11

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da be Int-Location, loc be Nat st ( CurInstr (P1,( Comput (P1,s1,i)))) = (da =0_goto loc) & loc <> (( IC ( Comput (P1,s1,i))) + 1) holds ((( Comput (P1,s1,i)) . da) = 0 iff (( Comput (P2,s2,i)) . da) = 0 )

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da be Int-Location, loc be Nat;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A4: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      ( IC SCM+FSA ) in ( dom p) by AMISTD_5: 6;

      then

       A5: ((Cs1i1 | ( dom p)) . ( IC SCM+FSA )) = (Cs1i1 . ( IC SCM+FSA )) & ((Cs2i1 | ( dom p)) . ( IC SCM+FSA )) = (Cs2i1 . ( IC SCM+FSA )) by FUNCT_1: 49;

      assume that

       A6: I = (da =0_goto loc) and

       A7: loc <> (( IC ( Comput (P1,s1,i))) + 1);

      

       A8: I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

       A9:

      now

        assume (( Comput (P2,s2,i)) . da) = 0 & (( Comput (P1,s1,i)) . da) <> 0 ;

        then (Cs2i1 . ( IC SCM+FSA )) = loc & (Cs1i1 . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A8, A3, A4, A6, SCMFSA_2: 70;

        hence contradiction by A1, A5, A7, A2, EXTPRO_1:def 10;

      end;

      

       A10: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, EXTPRO_1:def 10;

      now

        assume (( Comput (P1,s1,i)) . da) = 0 & (( Comput (P2,s2,i)) . da) <> 0 ;

        then (Cs1i1 . ( IC SCM+FSA )) = loc & (Cs2i1 . ( IC SCM+FSA )) = (( IC Cs2i) + 1) by A8, A3, A4, A6, SCMFSA_2: 70;

        hence contradiction by A1, A5, A10, A7, A2, AMISTD_5: 7;

      end;

      hence thesis by A9;

    end;

    theorem :: SCMFSA_3:12

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da be Int-Location, loc be Nat st ( CurInstr (P1,( Comput (P1,s1,i)))) = (da >0_goto loc) & loc <> (( IC ( Comput (P1,s1,i))) + 1) holds (( Comput (P1,s1,i)) . da) > 0 iff (( Comput (P2,s2,i)) . da) > 0

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da be Int-Location, loc be Nat;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, EXTPRO_1:def 10;

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      ( IC SCM+FSA ) in ( dom p) by AMISTD_5: 6;

      then

       A5: ((Cs1i1 | ( dom p)) . ( IC SCM+FSA )) = (Cs1i1 . ( IC SCM+FSA )) & ((Cs2i1 | ( dom p)) . ( IC SCM+FSA )) = (Cs2i1 . ( IC SCM+FSA )) by FUNCT_1: 49;

      

       A6: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A7: I = (da >0_goto loc) and

       A8: loc <> (( IC ( Comput (P1,s1,i))) + 1);

      

       A9: I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

       A10:

      now

        assume that

         A11: (( Comput (P2,s2,i)) . da) > 0 and

         A12: (( Comput (P1,s1,i)) . da) <= 0 ;

        (Cs2i1 . ( IC SCM+FSA )) = loc by A9, A6, A7, A11, SCMFSA_2: 71;

        hence contradiction by A4, A5, A3, A7, A8, A12, SCMFSA_2: 71;

      end;

      

       A13: ( IC Cs1i) = ( IC Cs2i) by A1, A2, AMISTD_5: 7;

      now

        assume that

         A14: (( Comput (P1,s1,i)) . da) > 0 and

         A15: (( Comput (P2,s2,i)) . da) <= 0 ;

        (Cs1i1 . ( IC SCM+FSA )) = loc by A4, A7, A14, SCMFSA_2: 71;

        hence contradiction by A13, A9, A6, A5, A3, A7, A8, A15, SCMFSA_2: 71;

      end;

      hence thesis by A10;

    end;

    theorem :: SCMFSA_3:13

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location, f be FinSeq-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = (da := (f,db)) & da in ( dom p) holds for k1,k2 be Element of NAT st k1 = |.(( Comput (P1,s1,i)) . db).| & k2 = |.(( Comput (P2,s2,i)) . db).| holds ((( Comput (P1,s1,i)) . f) /. k1) = ((( Comput (P2,s2,i)) . f) /. k2)

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location, f be FinSeq-Location;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, EXTPRO_1:def 10;

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      

       A6: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A7: I = (da := (f,db)) and

       A8: da in ( dom p);

      

       A9: (ex k1 be Nat st k1 = |.(Cs1i . db).| & (( Exec (I,Cs1i)) . da) = ((Cs1i . f) /. k1)) & ex k2 be Nat st k2 = |.(Cs2i . db).| & (( Exec (I,Cs2i)) . da) = ((Cs2i . f) /. k2) by A7, SCMFSA_2: 72;

      let i1,i2 be Element of NAT ;

      assume i1 = |.(( Comput (P1,s1,i)) . db).| & i2 = |.(( Comput (P2,s2,i)) . db).| & ((( Comput (P1,s1,i)) . f) /. i1) <> ((( Comput (P2,s2,i)) . f) /. i2);

      hence contradiction by A1, A4, A6, A5, A3, A9, A8, A2, AMISTD_5: 7;

    end;

    theorem :: SCMFSA_3:14

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da,db be Int-Location, f be FinSeq-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = ((f,db) := da) & f in ( dom p) holds for k1,k2 be Nat st k1 = |.(( Comput (P1,s1,i)) . db).| & k2 = |.(( Comput (P2,s2,i)) . db).| holds ((( Comput (P1,s1,i)) . f) +* (k1,(( Comput (P1,s1,i)) . da))) = ((( Comput (P2,s2,i)) . f) +* (k2,(( Comput (P2,s2,i)) . da)))

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Int-Location, f be FinSeq-Location;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, EXTPRO_1:def 10;

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: f in ( dom p) implies ((Cs1i1 | ( dom p)) . f) = (Cs1i1 . f) & ((Cs2i1 | ( dom p)) . f) = (Cs2i1 . f) by FUNCT_1: 49;

      

       A6: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A7: I = ((f,db) := da) and

       A8: f in ( dom p);

      

       A9: (ex k1 be Nat st k1 = |.(Cs1i . db).| & (( Exec (I,Cs1i)) . f) = ((Cs1i . f) +* (k1,(Cs1i . da)))) & ex k2 be Nat st k2 = |.(Cs2i . db).| & (( Exec (I,Cs2i)) . f) = ((Cs2i . f) +* (k2,(Cs2i . da))) by A7, SCMFSA_2: 73;

      let i1,i2 be Nat;

      assume i1 = |.(Cs1i . db).| & i2 = |.(Cs2i . db).| & ((Cs1i . f) +* (i1,(Cs1i . da))) <> ((Cs2i . f) +* (i2,(Cs2i . da)));

      hence contradiction by A1, A4, A6, A5, A3, A9, A8, A2, AMISTD_5: 7;

    end;

    theorem :: SCMFSA_3:15

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da be Int-Location, f be FinSeq-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = (da :=len f) & da in ( dom p) holds ( len (( Comput (P1,s1,i)) . f)) = ( len (( Comput (P2,s2,i)) . f))

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da be Int-Location, f be FinSeq-Location;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, EXTPRO_1:def 10;

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      

       A6: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A7: I = (da :=len f) and

       A8: da in ( dom p) & ( len (( Comput (P1,s1,i)) . f)) <> ( len (( Comput (P2,s2,i)) . f));

      (( Exec (I,Cs1i)) . da) = ( len (Cs1i . f)) & (( Exec (I,Cs2i)) . da) = ( len (Cs2i . f)) by A7, SCMFSA_2: 74;

      hence contradiction by A1, A4, A6, A5, A3, A8, A2, AMISTD_5: 7;

    end;

    theorem :: SCMFSA_3:16

    for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds for i be Nat, da be Int-Location, f be FinSeq-Location st ( CurInstr (P1,( Comput (P1,s1,i)))) = (f :=<0,...,0> da) & f in ( dom p) holds for k1,k2 be Nat st k1 = |.(( Comput (P1,s1,i)) . da).| & k2 = |.(( Comput (P2,s2,i)) . da).| holds (k1 |-> 0 ) = (k2 |-> 0 )

    proof

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da be Int-Location, f be FinSeq-Location;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, EXTPRO_1:def 10;

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: f in ( dom p) implies ((Cs1i1 | ( dom p)) . f) = (Cs1i1 . f) & ((Cs2i1 | ( dom p)) . f) = (Cs2i1 . f) by FUNCT_1: 49;

      

       A6: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A7: I = (f :=<0,...,0> da) and

       A8: f in ( dom p);

      

       A9: (ex k1 be Nat st k1 = |.(Cs1i . da).| & (( Exec (I,Cs1i)) . f) = (k1 |-> 0 )) & ex k2 be Nat st k2 = |.(Cs2i . da).| & (( Exec (I,Cs2i)) . f) = (k2 |-> 0 ) by A7, SCMFSA_2: 75;

      let i1,i2 be Nat;

      assume i1 = |.(Cs1i . da).| & i2 = |.(Cs2i . da).| & (i1 |-> 0 ) <> (i2 |-> 0 );

      hence contradiction by A1, A4, A6, A5, A3, A9, A8, A2, AMISTD_5: 7;

    end;