scmfsa10.miz



    begin

    reserve a,b,d1,d2,d3,d4 for Int-Location,

A,B for Data-Location,

f,f1,f2,f3 for FinSeq-Location,

il,i1,i2 for Nat,

L for Nat,

I for Instruction of SCM+FSA ,

s,s1,s2 for State of SCM+FSA ,

T for InsType of the InstructionsF of SCM+FSA ,

k for Nat;

    definition

      let la,lb be Int-Location, a,b be Integer;

      :: original: -->

      redefine

      func (la,lb) --> (a,b) -> PartState of SCM+FSA ;

      coherence

      proof

        

         A1: ( Values lb) = INT by SCMFSA_2: 11;

        b is Element of INT by INT_1:def 2;

        then

        reconsider b as Element of ( Values lb) by A1;

        

         A2: ( Values la) = INT by SCMFSA_2: 11;

        a is Element of INT by INT_1:def 2;

        then

        reconsider a as Element of ( Values la) by A2;

        ((la,lb) --> (a,b)) is PartState of SCM+FSA ;

        hence thesis;

      end;

    end

    theorem :: SCMFSA10:1

    

     Th1: for o be Object of SCM+FSA st o in ( Data-Locations SCM+FSA ) holds o is Int-Location or o is FinSeq-Location

    proof

      let o be Object of SCM+FSA ;

      assume o in ( Data-Locations SCM+FSA );

      then o in SCM-Data-Loc or o in SCM+FSA-Data*-Loc by SCMFSA_2: 100, XBOOLE_0:def 3;

      hence thesis by AMI_2:def 16, SCMFSA_2:def 5;

    end;

    theorem :: SCMFSA10:2

    

     Th2: (a := b) = [1, {} , <*a, b*>]

    proof

      ex A, B st a = A & b = B & (a := b) = (A := B) by SCMFSA_2:def 8;

      hence thesis;

    end;

    theorem :: SCMFSA10:3

    

     Th3: ( AddTo (a,b)) = [2, {} , <*a, b*>]

    proof

      ex A, B st a = A & b = B & ( AddTo (a,b)) = ( AddTo (A,B)) by SCMFSA_2:def 9;

      hence thesis;

    end;

    theorem :: SCMFSA10:4

    

     Th4: ( SubFrom (a,b)) = [3, {} , <*a, b*>]

    proof

      ex A, B st a = A & b = B & ( SubFrom (a,b)) = ( SubFrom (A,B)) by SCMFSA_2:def 10;

      hence thesis;

    end;

    theorem :: SCMFSA10:5

    

     Th5: ( MultBy (a,b)) = [4, {} , <*a, b*>]

    proof

      ex A, B st a = A & b = B & ( MultBy (a,b)) = ( MultBy (A,B)) by SCMFSA_2:def 11;

      hence thesis;

    end;

    theorem :: SCMFSA10:6

    

     Th6: ( Divide (a,b)) = [5, {} , <*a, b*>]

    proof

      ex A, B st a = A & b = B & ( Divide (a,b)) = ( Divide (A,B)) by SCMFSA_2:def 12;

      hence thesis;

    end;

    theorem :: SCMFSA10:7

    

     Th7: (a =0_goto il) = [7, <*il*>, <*a*>]

    proof

      ex A st A = a & (A =0_goto il) = (a =0_goto il) by SCMFSA_2:def 14;

      hence thesis;

    end;

    theorem :: SCMFSA10:8

    

     Th8: (a >0_goto il) = [8, <*il*>, <*a*>]

    proof

      ex A st A = a & (A >0_goto il) = (a >0_goto il) by SCMFSA_2:def 15;

      hence thesis;

    end;

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

b,b1,c,c1 for Element of SCM-Data-Loc ,

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

    theorem :: SCMFSA10:9

    

     Th9: ( JumpPart ( halt SCM+FSA )) = {} ;

    reserve a,b,d1,d2,d3,d4 for Int-Location,

A,B for Data-Location,

f,f1,f2,f3 for FinSeq-Location;

    theorem :: SCMFSA10:10

    

     Th10: ( JumpPart (a := b)) = {}

    proof

      

      thus ( JumpPart (a := b)) = ( [1, {} , <*a, b*>] `2_3 ) by Th2

      .= {} ;

    end;

    theorem :: SCMFSA10:11

    

     Th11: ( JumpPart ( AddTo (a,b))) = {}

    proof

      

      thus ( JumpPart ( AddTo (a,b))) = ( [2, {} , <*a, b*>] `2_3 ) by Th3

      .= {} ;

    end;

    theorem :: SCMFSA10:12

    

     Th12: ( JumpPart ( SubFrom (a,b))) = {}

    proof

      

      thus ( JumpPart ( SubFrom (a,b))) = ( [3, {} , <*a, b*>] `2_3 ) by Th4

      .= {} ;

    end;

    theorem :: SCMFSA10:13

    

     Th13: ( JumpPart ( MultBy (a,b))) = {}

    proof

      

      thus ( JumpPart ( MultBy (a,b))) = ( [4, {} , <*a, b*>] `2_3 ) by Th5

      .= {} ;

    end;

    theorem :: SCMFSA10:14

    

     Th14: ( JumpPart ( Divide (a,b))) = {}

    proof

      

      thus ( JumpPart ( Divide (a,b))) = ( [5, {} , <*a, b*>] `2_3 ) by Th6

      .= {} ;

    end;

    theorem :: SCMFSA10:15

    

     Th15: ( JumpPart (a =0_goto i1)) = <*i1*>

    proof

      

      thus ( JumpPart (a =0_goto i1)) = ( [7, <*i1*>, <*a*>] `2_3 ) by Th7

      .= <*i1*>;

    end;

    theorem :: SCMFSA10:16

    

     Th16: ( JumpPart (a >0_goto i1)) = <*i1*>

    proof

      

      thus ( JumpPart (a >0_goto i1)) = ( [8, <*i1*>, <*a*>] `2_3 ) by Th8

      .= <*i1*>;

    end;

    theorem :: SCMFSA10:17

    T = 0 implies ( JumpParts T) = { 0 }

    proof

      assume

       A1: T = 0 ;

      hereby

        let a be object;

        assume a in ( JumpParts T);

        then

        consider I such that

         A2: a = ( JumpPart I) and

         A3: ( InsCode I) = T;

        I = ( halt SCM+FSA ) by A1, A3, SCMFSA_2: 95;

        hence a in { 0 } by A2, TARSKI:def 1;

      end;

      let a be object;

      assume a in { 0 };

      then

       A4: a = 0 by TARSKI:def 1;

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

      hence thesis by A1, Th9, A4;

    end;

    theorem :: SCMFSA10:18

    T = 1 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 1;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = (a := b) by A1, A3, SCMFSA_2: 30;

        x = {} by A2, Th10, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart (a := a)) by Th10;

      ( InsCode (a := a)) = 1 by SCMFSA_2: 18;

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:19

    T = 2 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 2;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( AddTo (a,b)) by A1, A3, SCMFSA_2: 31;

        x = {} by A2, Th11, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( AddTo (a,a))) by Th11;

      ( InsCode ( AddTo (a,a))) = 2 by SCMFSA_2: 19;

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:20

    T = 3 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 3;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( SubFrom (a,b)) by A1, A3, SCMFSA_2: 32;

        x = {} by A2, Th12, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( SubFrom (a,a))) by Th12;

      ( InsCode ( SubFrom (a,a))) = 3 by SCMFSA_2: 20;

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:21

    T = 4 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 4;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( MultBy (a,b)) by A1, A3, SCMFSA_2: 33;

        x = {} by A2, Th13, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( MultBy (a,a))) by Th13;

      ( InsCode ( MultBy (a,a))) = 4 by SCMFSA_2: 21;

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:22

    T = 5 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 5;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( Divide (a,b)) by A1, A3, SCMFSA_2: 34;

        x = {} by A2, Th14, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( Divide (a,a))) by Th14;

      ( InsCode ( Divide (a,a))) = 5 by SCMFSA_2: 22;

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:23

    

     Th23: T = 6 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Nat;

      assume

       A1: T = 6;

      hereby

        let x be object;

        ( InsCode ( goto i1)) = 6;

        then

         A2: ( JumpPart ( goto i1)) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart ( goto i1))) by A2, CARD_3: 108;

        hence x in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      end;

      let x be object;

      assume

       A3: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A4: f = ( JumpPart I) and

         A5: ( InsCode I) = T;

        consider i1 such that

         A6: I = ( goto i1) by A1, A5, SCMFSA_2: 35;

        f = <*i1*> by A4, A6;

        hence thesis by A3, FINSEQ_1: 2, FINSEQ_1:def 8;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: SCMFSA10:24

    

     Th24: T = 7 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Nat, a = the Int-Location;

      assume

       A1: T = 7;

      

       A2: ( JumpPart (a =0_goto i1)) = <*i1*> by Th15;

      hereby

        let x be object;

        ( InsCode (a =0_goto i1)) = 7 by SCMFSA_2: 24;

        then

         A3: ( JumpPart (a =0_goto i1)) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart (a =0_goto i1))) by A3, CARD_3: 108;

        hence x in {1} by A2, FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      let x be object;

      assume

       A4: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A5: f = ( JumpPart I) and

         A6: ( InsCode I) = T;

        consider i1, a such that

         A7: I = (a =0_goto i1) by A1, A6, SCMFSA_2: 36;

        f = <*i1*> by A5, A7, Th15;

        hence thesis by A4, FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: SCMFSA10:25

    

     Th25: T = 8 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Nat, a = the Int-Location;

      assume

       A1: T = 8;

      

       A2: ( JumpPart (a >0_goto i1)) = <*i1*> by Th16;

      hereby

        let x be object;

        ( InsCode (a >0_goto i1)) = 8 by SCMFSA_2: 25;

        then

         A3: ( JumpPart (a >0_goto i1)) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart (a >0_goto i1))) by A3, CARD_3: 108;

        hence x in {1} by A2, FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      let x be object;

      assume

       A4: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A5: f = ( JumpPart I) and

         A6: ( InsCode I) = T;

        consider i1, a such that

         A7: I = (a >0_goto i1) by A1, A6, SCMFSA_2: 37;

        f = <*i1*> by A5, A7, Th16;

        hence thesis by A4, FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: SCMFSA10:26

    T = 9 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 9;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b, f such that

         A4: I = (b := (f,a)) by A1, A3, SCMFSA_2: 38;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location, f = the FinSeq-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart (a := (f,a)));

      ( InsCode (a := (f,a))) = 9;

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:27

    T = 10 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 10;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b, f such that

         A4: I = ((f,a) := b) by A1, A3, SCMFSA_2: 39;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location, f = the FinSeq-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ((f,a) := a));

      ( InsCode ((f,a) := a)) = 10;

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:28

    T = 11 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 11;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, f such that

         A4: I = (a :=len f) by A1, A3, SCMFSA_2: 40;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location, f = the FinSeq-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart (a :=len f));

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

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:29

    T = 12 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 12;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM+FSA such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, f such that

         A4: I = (f :=<0,...,0> a) by A1, A3, SCMFSA_2: 41;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Int-Location, f = the FinSeq-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart (f :=<0,...,0> a));

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

      hence thesis by A5, A1;

    end;

    theorem :: SCMFSA10:30

    (( product" ( JumpParts ( InsCode ( goto i1)))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode ( goto i1))))) = {1} by Th23;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode ( goto i1))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode ( goto i1)))) . 1);

        then x in ( pi (( JumpParts ( InsCode ( goto i1))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode ( goto i1))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of SCM+FSA such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode ( goto i1)) by A2;

        consider i2 such that

         A6: I = ( goto i2) by A5, SCMFSA_2: 35;

        g = <*i2*> by A4, A6;

        then x = i2 by A3, FINSEQ_1:def 8;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Nat;

      

       A7: ( <*x*> . 1) = x by FINSEQ_1:def 8;

      

       A8: ( InsCode ( goto i1)) = ( InsCode ( goto x));

      ( JumpPart ( goto x)) = <*x*>;

      then <*x*> in ( JumpParts ( InsCode ( goto i1))) by A8;

      then x in ( pi (( JumpParts ( InsCode ( goto i1))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    theorem :: SCMFSA10:31

    (( product" ( JumpParts ( InsCode (a =0_goto i1)))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode (a =0_goto i1))))) = {1} by Th24, SCMFSA_2: 24;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode (a =0_goto i1))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode (a =0_goto i1)))) . 1);

        then x in ( pi (( JumpParts ( InsCode (a =0_goto i1))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode (a =0_goto i1))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of SCM+FSA such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode (a =0_goto i1)) by A2;

        consider i2, b such that

         A6: I = (b =0_goto i2) by A5, SCMFSA_2: 24, SCMFSA_2: 36;

        g = <*i2*> qua FinSequence by A4, A6, Th15;

        then x = i2 by A3, FINSEQ_1: 40;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      

       A7: ( <*x*> . 1) = x by FINSEQ_1: 40;

      ( InsCode (a =0_goto i1)) = 7 by SCMFSA_2: 24;

      then

       A8: ( InsCode (a =0_goto i1)) = ( InsCode (a =0_goto x)) by SCMFSA_2: 24;

      ( JumpPart (a =0_goto x)) = <*x*> by Th15;

      then <*x*> in ( JumpParts ( InsCode (a =0_goto i1))) by A8;

      then x in ( pi (( JumpParts ( InsCode (a =0_goto i1))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    theorem :: SCMFSA10:32

    (( product" ( JumpParts ( InsCode (a >0_goto i1)))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode (a >0_goto i1))))) = {1} by Th25, SCMFSA_2: 25;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode (a >0_goto i1))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode (a >0_goto i1)))) . 1);

        then x in ( pi (( JumpParts ( InsCode (a >0_goto i1))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode (a >0_goto i1))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of SCM+FSA such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode (a >0_goto i1)) by A2;

        consider i2, b such that

         A6: I = (b >0_goto i2) by A5, SCMFSA_2: 25, SCMFSA_2: 37;

        g = <*i2*> by A4, A6, Th16;

        then x = i2 by A3, FINSEQ_1: 40;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      

       A7: ( <*x*> . 1) = x by FINSEQ_1: 40;

      ( InsCode (a >0_goto i1)) = 8 by SCMFSA_2: 25;

      then

       A8: ( InsCode (a >0_goto i1)) = ( InsCode (a >0_goto x)) by SCMFSA_2: 25;

      ( JumpPart (a >0_goto x)) = <*x*> by Th16;

      then <*x*> in ( JumpParts ( InsCode (a >0_goto i1))) by A8;

      then x in ( pi (( JumpParts ( InsCode (a >0_goto i1))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    

     Lm1: for i be Instruction of SCM+FSA holds (for l be Nat holds ( NIC (i,l)) = {(l + 1)}) implies ( JUMP i) is empty

    proof

      reconsider p = 0 , q = 1 as Nat;

      let i be Instruction of SCM+FSA ;

      assume

       A1: for l be Nat holds ( NIC (i,l)) = {(l + 1)};

      set X = the set of all ( NIC (i,f)) where f be Nat;

      reconsider p, q as Nat;

      assume not thesis;

      then

      consider x be object such that

       A2: x in ( meet X);

      ( NIC (i,p)) = {(p + 1)} by A1;

      then {(p + 1)} in X;

      then x in {(p + 1)} by A2, SETFAM_1:def 1;

      then

       A3: x = (p + 1) by TARSKI:def 1;

      ( NIC (i,q)) = {(q + 1)} by A1;

      then {(q + 1)} in X;

      then x in {(q + 1)} by A2, SETFAM_1:def 1;

      hence contradiction by A3, TARSKI:def 1;

    end;

    registration

      cluster ( JUMP ( halt SCM+FSA )) -> empty;

      coherence ;

    end

    registration

      let a, b;

      cluster (a := b) -> sequential;

      coherence by SCMFSA_2: 63;

      cluster ( AddTo (a,b)) -> sequential;

      coherence by SCMFSA_2: 64;

      cluster ( SubFrom (a,b)) -> sequential;

      coherence by SCMFSA_2: 65;

      cluster ( MultBy (a,b)) -> sequential;

      coherence by SCMFSA_2: 66;

      cluster ( Divide (a,b)) -> sequential;

      coherence by SCMFSA_2: 67;

    end

    registration

      let a, b;

      cluster ( JUMP (a := b)) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC ((a := b),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

      cluster ( JUMP ( AddTo (a,b))) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC (( AddTo (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

      cluster ( JUMP ( SubFrom (a,b))) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC (( SubFrom (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

      cluster ( JUMP ( MultBy (a,b))) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC (( MultBy (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

      cluster ( JUMP ( Divide (a,b))) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC (( Divide (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    theorem :: SCMFSA10:33

    

     Th33: ( NIC (( goto i1),il)) = {i1}

    proof

      now

        let x be object;

         A1:

        now

          il in NAT by ORDINAL1:def 12;

          then

          reconsider il1 = il as Element of ( Values ( IC SCM+FSA )) by MEMSTR_0:def 6;

          reconsider n = il1 as Nat;

          set I = ( goto i1);

          set t = the State of SCM+FSA , Q = the Instruction-Sequence of SCM+FSA ;

          assume

           A2: x = i1;

          reconsider u = (t +* (( IC SCM+FSA ),il1)) as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

          reconsider P = (Q +* (il,I)) as Instruction-Sequence of SCM+FSA ;

          ( IC SCM+FSA ) in ( dom t) by MEMSTR_0: 2;

          then

           A3: ( IC u) = n by FUNCT_7: 31;

          il in NAT by ORDINAL1:def 12;

          then

           A4: (P /. il) = (P . il) by PBOOLE: 143;

          il in NAT by ORDINAL1:def 12;

          then il in ( dom Q) by PARTFUN1:def 2;

          then

           A5: (P . n) = I by FUNCT_7: 31;

          then ( IC ( Following (P,u))) = i1 by A3, A4, SCMFSA_2: 69;

          hence x in { ( IC ( Exec (( goto i1),s))) where s be Element of ( product ( the_Values_of SCM+FSA )) : ( IC s) = il } by A2, A3, A5, A4;

        end;

        now

          assume x in { ( IC ( Exec (( goto i1),s))) where s be Element of ( product ( the_Values_of SCM+FSA )) : ( IC s) = il };

          then ex s be Element of ( product ( the_Values_of SCM+FSA )) st x = ( IC ( Exec (( goto i1),s))) & ( IC s) = il;

          hence x = i1 by SCMFSA_2: 69;

        end;

        hence x in {i1} iff x in { ( IC ( Exec (( goto i1),s))) where s be Element of ( product ( the_Values_of SCM+FSA )) : ( IC s) = il } by A1, TARSKI:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: SCMFSA10:34

    

     Th34: ( JUMP ( goto i1)) = {i1}

    proof

      set X = the set of all ( NIC (( goto i1),il));

      now

        let x be object;

        hereby

          set il1 = 1;

          

           A1: ( NIC (( goto i1),il1)) in X;

          assume x in ( meet X);

          then x in ( NIC (( goto i1),il1)) by A1, SETFAM_1:def 1;

          hence x in {i1} by Th33;

        end;

        assume x in {i1};

        then

         A2: x = i1 by TARSKI:def 1;

         A3:

        now

          let Y be set;

          assume Y in X;

          then

          consider il be Nat such that

           A4: Y = ( NIC (( goto i1),il));

          ( NIC (( goto i1),il)) = {i1} by Th33;

          hence i1 in Y by A4, TARSKI:def 1;

        end;

        ( NIC (( goto i1),i1)) in X;

        hence x in ( meet X) by A2, A3, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let i1;

      cluster ( JUMP ( goto i1)) -> 1 -element;

      coherence

      proof

        ( JUMP ( goto i1)) = {i1} by Th34;

        hence thesis;

      end;

    end

    theorem :: SCMFSA10:35

    

     Th35: ( NIC ((a =0_goto i1),il)) = {i1, (il + 1)}

    proof

      set t = the State of SCM+FSA , Q = the Instruction-Sequence of SCM+FSA ;

      hereby

        let x be object;

        assume x in ( NIC ((a =0_goto i1),il));

        then

        consider s be Element of ( product ( the_Values_of SCM+FSA )) such that

         A1: x = ( IC ( Exec ((a =0_goto i1),s))) and

         A2: ( IC s) = il;

        per cases ;

          suppose (s . a) = 0 ;

          then x = i1 by A1, SCMFSA_2: 70;

          hence x in {i1, (il + 1)} by TARSKI:def 2;

        end;

          suppose (s . a) <> 0 ;

          then x = (il + 1) by A1, A2, SCMFSA_2: 70;

          hence x in {i1, (il + 1)} by TARSKI:def 2;

        end;

      end;

      let x be object;

      set I = (a =0_goto i1);

      

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

      il in NAT by ORDINAL1:def 12;

      then

      reconsider il1 = il as Element of ( Values ( IC SCM+FSA )) by MEMSTR_0:def 6;

      reconsider u = (t +* (( IC SCM+FSA ),il1)) as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

      reconsider P = (Q +* (il,I)) as Instruction-Sequence of SCM+FSA ;

      reconsider n = il as Nat;

      assume

       A4: x in {i1, (il + 1)};

      per cases by A4, TARSKI:def 2;

        suppose

         A5: x = i1;

        reconsider v = (u +* (a .--> 0 )) as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

        

         A6: ( IC SCM+FSA ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM+FSA ) in ( dom (a .--> 0 )) by A3, TARSKI:def 1;

        

        then

         A8: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A6, FUNCT_7: 31;

        il in NAT by ORDINAL1:def 12;

        then

         A9: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT by ORDINAL1:def 12;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A10: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 0 ) . a) by FUNCT_4: 13

        .= 0 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = i1 by A8, A10, A9, SCMFSA_2: 70;

        hence thesis by A5, A8, A10, A9;

      end;

        suppose

         A11: x = (il + 1);

        reconsider v = (u +* (a .--> 1)) as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

        

         A12: ( IC SCM+FSA ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM+FSA ) in ( dom (a .--> 1)) by A3, TARSKI:def 1;

        

        then

         A14: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A12, FUNCT_7: 31;

        il in NAT by ORDINAL1:def 12;

        then

         A15: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT by ORDINAL1:def 12;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A16: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 1) . a) by FUNCT_4: 13

        .= 1 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = (il + 1) by A14, A16, A15, SCMFSA_2: 70;

        hence thesis by A11, A14, A16, A15;

      end;

    end;

    theorem :: SCMFSA10:36

    

     Th36: ( JUMP (a =0_goto i1)) = {i1}

    proof

      set X = the set of all ( NIC ((a =0_goto i1),il));

      now

        let x be object;

         A1:

        now

          let Y be set;

          assume Y in X;

          then

          consider il be Nat such that

           A2: Y = ( NIC ((a =0_goto i1),il));

          ( NIC ((a =0_goto i1),il)) = {i1, (il + 1)} by Th35;

          hence i1 in Y by A2, TARSKI:def 2;

        end;

        hereby

          set il1 = 1, il2 = 2;

          assume

           A3: x in ( meet X);

          

           A4: ( NIC ((a =0_goto i1),il2)) = {i1, (il2 + 1)} by Th35;

          ( NIC ((a =0_goto i1),il2)) in X;

          then x in ( NIC ((a =0_goto i1),il2)) by A3, SETFAM_1:def 1;

          then

           A5: x = i1 or x = (il2 + 1) by A4, TARSKI:def 2;

          

           A6: ( NIC ((a =0_goto i1),il1)) = {i1, (il1 + 1)} by Th35;

          ( NIC ((a =0_goto i1),il1)) in X;

          then x in ( NIC ((a =0_goto i1),il1)) by A3, SETFAM_1:def 1;

          then x = i1 or x = (il1 + 1) by A6, TARSKI:def 2;

          hence x in {i1} by A5, TARSKI:def 1;

        end;

        assume x in {i1};

        then

         A7: x = i1 by TARSKI:def 1;

        ( NIC ((a =0_goto i1),i1)) in X;

        hence x in ( meet X) by A7, A1, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let a, i1;

      cluster ( JUMP (a =0_goto i1)) -> 1 -element;

      coherence

      proof

        ( JUMP (a =0_goto i1)) = {i1} by Th36;

        hence thesis;

      end;

    end

    theorem :: SCMFSA10:37

    

     Th37: ( NIC ((a >0_goto i1),il)) = {i1, (il + 1)}

    proof

      set t = the State of SCM+FSA , Q = the Instruction-Sequence of SCM+FSA ;

      hereby

        let x be object;

        assume x in ( NIC ((a >0_goto i1),il));

        then

        consider s be Element of ( product ( the_Values_of SCM+FSA )) such that

         A1: x = ( IC ( Exec ((a >0_goto i1),s))) and

         A2: ( IC s) = il;

        per cases ;

          suppose (s . a) > 0 ;

          then x = i1 by A1, SCMFSA_2: 71;

          hence x in {i1, (il + 1)} by TARSKI:def 2;

        end;

          suppose (s . a) <= 0 ;

          then x = (il + 1) by A1, A2, SCMFSA_2: 71;

          hence x in {i1, (il + 1)} by TARSKI:def 2;

        end;

      end;

      let x be object;

      set I = (a >0_goto i1);

      

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

      il in NAT by ORDINAL1:def 12;

      then

      reconsider il1 = il as Element of ( Values ( IC SCM+FSA )) by MEMSTR_0:def 6;

      reconsider n = il as Nat;

      reconsider u = (t +* (( IC SCM+FSA ),il1)) as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

      reconsider P = (Q +* (il,I)) as Instruction-Sequence of SCM+FSA ;

      assume

       A4: x in {i1, (il + 1)};

      per cases by A4, TARSKI:def 2;

        suppose

         A5: x = i1;

        reconsider v = (u +* (a .--> 1)) as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

        

         A6: ( IC SCM+FSA ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM+FSA ) in ( dom (a .--> 1)) by A3, TARSKI:def 1;

        

        then

         A8: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A6, FUNCT_7: 31;

        il in NAT by ORDINAL1:def 12;

        then

         A9: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT by ORDINAL1:def 12;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A10: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 1) . a) by FUNCT_4: 13

        .= 1 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = i1 by A8, A10, A9, SCMFSA_2: 71;

        hence thesis by A5, A8, A10, A9;

      end;

        suppose

         A11: x = (il + 1);

        reconsider v = (u +* (a .--> 0 )) as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

        

         A12: ( IC SCM+FSA ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM+FSA ) in ( dom (a .--> 0 )) by A3, TARSKI:def 1;

        

        then

         A14: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A12, FUNCT_7: 31;

        il in NAT by ORDINAL1:def 12;

        then

         A15: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT by ORDINAL1:def 12;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A16: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 0 ) . a) by FUNCT_4: 13

        .= 0 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = (il + 1) by A14, A16, A15, SCMFSA_2: 71;

        hence thesis by A11, A14, A16, A15;

      end;

    end;

    theorem :: SCMFSA10:38

    

     Th38: ( JUMP (a >0_goto i1)) = {i1}

    proof

      set X = the set of all ( NIC ((a >0_goto i1),il));

      now

        let x be object;

         A1:

        now

          let Y be set;

          assume Y in X;

          then

          consider il be Nat such that

           A2: Y = ( NIC ((a >0_goto i1),il));

          ( NIC ((a >0_goto i1),il)) = {i1, (il + 1)} by Th37;

          hence i1 in Y by A2, TARSKI:def 2;

        end;

        hereby

          set il1 = 1, il2 = 2;

          assume

           A3: x in ( meet X);

          

           A4: ( NIC ((a >0_goto i1),il2)) = {i1, (il2 + 1)} by Th37;

          ( NIC ((a >0_goto i1),il2)) in X;

          then x in ( NIC ((a >0_goto i1),il2)) by A3, SETFAM_1:def 1;

          then

           A5: x = i1 or x = (il2 + 1) by A4, TARSKI:def 2;

          

           A6: ( NIC ((a >0_goto i1),il1)) = {i1, (il1 + 1)} by Th37;

          ( NIC ((a >0_goto i1),il1)) in X;

          then x in ( NIC ((a >0_goto i1),il1)) by A3, SETFAM_1:def 1;

          then x = i1 or x = (il1 + 1) by A6, TARSKI:def 2;

          hence x in {i1} by A5, TARSKI:def 1;

        end;

        assume x in {i1};

        then

         A7: x = i1 by TARSKI:def 1;

        ( NIC ((a >0_goto i1),i1)) in X;

        hence x in ( meet X) by A7, A1, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let a, i1;

      cluster ( JUMP (a >0_goto i1)) -> 1 -element;

      coherence

      proof

        ( JUMP (a >0_goto i1)) = {i1} by Th38;

        hence thesis;

      end;

    end

    registration

      let a, b, f;

      cluster (a := (f,b)) -> sequential;

      coherence by SCMFSA_2: 72;

    end

    registration

      let a, b, f;

      cluster ( JUMP (a := (f,b))) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC ((a := (f,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    registration

      let a, b, f;

      cluster ((f,b) := a) -> sequential;

      coherence by SCMFSA_2: 73;

    end

    registration

      let a, b, f;

      cluster ( JUMP ((f,b) := a)) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC (((f,b) := a),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    registration

      let a, f;

      cluster (a :=len f) -> sequential;

      coherence by SCMFSA_2: 74;

    end

    registration

      let a, f;

      cluster ( JUMP (a :=len f)) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC ((a :=len f),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    registration

      let a, f;

      cluster (f :=<0,...,0> a) -> sequential;

      coherence by SCMFSA_2: 75;

    end

    registration

      let a, f;

      cluster ( JUMP (f :=<0,...,0> a)) -> empty;

      coherence

      proof

        for l be Nat holds ( NIC ((f :=<0,...,0> a),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    theorem :: SCMFSA10:39

    

     Th39: ( SUCC (il, SCM+FSA )) = {il, (il + 1)}

    proof

      set X = the set of all (( NIC (I,il)) \ ( JUMP I)) where I be Element of the InstructionsF of SCM+FSA ;

      set N = {il, (il + 1)};

      now

        let x be object;

        hereby

          assume x in ( union X);

          then

          consider Y be set such that

           A1: x in Y and

           A2: Y in X by TARSKI:def 4;

          consider i be Element of the InstructionsF of SCM+FSA such that

           A3: Y = (( NIC (i,il)) \ ( JUMP i)) by A2;

          per cases by SCMFSA_2: 93;

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

            then x in ( {il} \ ( JUMP ( halt SCM+FSA ))) by A1, A3, AMISTD_1: 2;

            then x = il by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

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

            then

            consider a, b such that

             A4: i = (a := b);

            x in ( {(il + 1)} \ ( JUMP (a := b))) by A1, A3, A4, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

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

            then

            consider a, b such that

             A5: i = ( AddTo (a,b));

            x in ( {(il + 1)} \ ( JUMP ( AddTo (a,b)))) by A1, A3, A5, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

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

            then

            consider a, b such that

             A6: i = ( SubFrom (a,b));

            x in ( {(il + 1)} \ ( JUMP ( SubFrom (a,b)))) by A1, A3, A6, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

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

            then

            consider a, b such that

             A7: i = ( MultBy (a,b));

            x in ( {(il + 1)} \ ( JUMP ( MultBy (a,b)))) by A1, A3, A7, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

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

            then

            consider a, b such that

             A8: i = ( Divide (a,b));

            x in ( {(il + 1)} \ ( JUMP ( Divide (a,b)))) by A1, A3, A8, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex i1 st i = ( goto i1);

            then

            consider i1 such that

             A9: i = ( goto i1);

            x in ( {i1} \ ( JUMP i)) by A1, A3, A9, Th33;

            then x in ( {i1} \ {i1}) by A9, Th34;

            hence x in N by XBOOLE_1: 37;

          end;

            suppose ex i1, a st i = (a =0_goto i1);

            then

            consider i1, a such that

             A10: i = (a =0_goto i1);

            

             A11: ( NIC (i,il)) = {i1, (il + 1)} by A10, Th35;

            x in ( NIC (i,il)) by A1, A3, XBOOLE_0:def 5;

            then

             A12: x = i1 or x = (il + 1) by A11, TARSKI:def 2;

            x in (( NIC (i,il)) \ {i1}) by A1, A3, A10, Th36;

            then not x in {i1} by XBOOLE_0:def 5;

            hence x in N by A12, TARSKI:def 1, TARSKI:def 2;

          end;

            suppose ex i1, a st i = (a >0_goto i1);

            then

            consider i1, a such that

             A13: i = (a >0_goto i1);

            

             A14: ( NIC (i,il)) = {i1, (il + 1)} by A13, Th37;

            x in ( NIC (i,il)) by A1, A3, XBOOLE_0:def 5;

            then

             A15: x = i1 or x = (il + 1) by A14, TARSKI:def 2;

            x in (( NIC (i,il)) \ {i1}) by A1, A3, A13, Th38;

            then not x in {i1} by XBOOLE_0:def 5;

            hence x in N by A15, TARSKI:def 1, TARSKI:def 2;

          end;

            suppose ex a, b, f st i = (b := (f,a));

            then

            consider a, b, f such that

             A16: i = (b := (f,a));

            x in ( {(il + 1)} \ ( JUMP (b := (f,a)))) by A1, A3, A16, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b, f st i = ((f,a) := b);

            then

            consider a, b, f such that

             A17: i = ((f,a) := b);

            x in ( {(il + 1)} \ ( JUMP ((f,a) := b))) by A1, A3, A17, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

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

            then

            consider a, f such that

             A18: i = (a :=len f);

            x in ( {(il + 1)} \ ( JUMP (a :=len f))) by A1, A3, A18, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

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

            then

            consider a, f such that

             A19: i = (f :=<0,...,0> a);

            x in ( {(il + 1)} \ ( JUMP (f :=<0,...,0> a))) by A1, A3, A19, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

        end;

        assume

         A20: x in {il, (il + 1)};

        per cases by A20, TARSKI:def 2;

          suppose

           A21: x = il;

          set i = ( halt SCM+FSA );

          (( NIC (i,il)) \ ( JUMP i)) = {il} by AMISTD_1: 2;

          then

           A22: {il} in X;

          x in {il} by A21, TARSKI:def 1;

          hence x in ( union X) by A22, TARSKI:def 4;

        end;

          suppose

           A23: x = (il + 1);

          set a = the Int-Location;

          set i = ( AddTo (a,a));

          (( NIC (i,il)) \ ( JUMP i)) = {(il + 1)} by AMISTD_1: 12;

          then

           A24: {(il + 1)} in X;

          x in {(il + 1)} by A23, TARSKI:def 1;

          hence x in ( union X) by A24, TARSKI:def 4;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: SCMFSA10:40

    

     Th40: for k be Nat holds (k + 1) in ( SUCC (k, SCM+FSA )) & for j be Nat st j in ( SUCC (k, SCM+FSA )) holds k <= j

    proof

      let k be Nat;

      

       A1: ( SUCC (k, SCM+FSA )) = {k, (k + 1)} by Th39;

      hence (k + 1) in ( SUCC (k, SCM+FSA )) by TARSKI:def 2;

      let j be Nat;

      assume

       A2: j in ( SUCC (k, SCM+FSA ));

      per cases by A1, A2, TARSKI:def 2;

        suppose j = k;

        hence thesis;

      end;

        suppose j = (k + 1);

        hence thesis by NAT_1: 11;

      end;

    end;

    registration

      cluster SCM+FSA -> standard;

      coherence by Th40, AMISTD_1: 3;

    end

    registration

      cluster ( InsCode ( halt SCM+FSA )) -> jump-only;

      coherence

      proof

        now

          let s be State of SCM+FSA , o be Object of SCM+FSA , I be Instruction of SCM+FSA ;

          assume that

           A1: ( InsCode I) = ( InsCode ( halt SCM+FSA )) and o in ( Data-Locations SCM+FSA );

          I = ( halt SCM+FSA ) by A1, SCMFSA_2: 95;

          hence (( Exec (I,s)) . o) = (s . o) by EXTPRO_1:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      cluster ( halt SCM+FSA ) -> jump-only;

      coherence ;

    end

    registration

      let i1;

      cluster ( InsCode ( goto i1)) -> jump-only;

      coherence

      proof

        set S = SCM+FSA ;

        now

          let s be State of S, o be Object of S, I be Instruction of S;

          assume that

           A1: ( InsCode I) = ( InsCode ( goto i1)) and

           A2: o in ( Data-Locations S);

          

           A3: ex i2 st I = ( goto i2) by A1, SCMFSA_2: 35;

          per cases by A2, Th1;

            suppose o is Int-Location;

            hence (( Exec (I,s)) . o) = (s . o) by A3, SCMFSA_2: 69;

          end;

            suppose o is FinSeq-Location;

            hence (( Exec (I,s)) . o) = (s . o) by A3, SCMFSA_2: 69;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let i1;

      cluster ( goto i1) -> jump-only non sequential non ins-loc-free;

      coherence

      proof

        thus ( InsCode ( goto i1)) is jump-only;

        ( JUMP ( goto i1)) <> {} ;

        hence ( goto i1) is non sequential by AMISTD_1: 13;

        thus not ( JumpPart ( goto i1)) is empty;

      end;

    end

    registration

      let a, i1;

      cluster ( InsCode (a =0_goto i1)) -> jump-only;

      coherence

      proof

        set S = SCM+FSA ;

        now

          let s be State of S, o be Object of S, I be Instruction of S;

          assume that

           A1: ( InsCode I) = ( InsCode (a =0_goto i1)) and

           A2: o in ( Data-Locations S);

          

           A3: ex i2, b st I = (b =0_goto i2) by A1, SCMFSA_2: 24, SCMFSA_2: 36;

          per cases by A2, Th1;

            suppose o is Int-Location;

            hence (( Exec (I,s)) . o) = (s . o) by A3, SCMFSA_2: 70;

          end;

            suppose o is FinSeq-Location;

            hence (( Exec (I,s)) . o) = (s . o) by A3, SCMFSA_2: 70;

          end;

        end;

        hence thesis;

      end;

      cluster ( InsCode (a >0_goto i1)) -> jump-only;

      coherence

      proof

        set S = SCM+FSA ;

        now

          let s be State of S, o be Object of S, I be Instruction of S;

          assume that

           A4: ( InsCode I) = ( InsCode (a >0_goto i1)) and

           A5: o in ( Data-Locations S);

          

           A6: ex i2, b st I = (b >0_goto i2) by A4, SCMFSA_2: 25, SCMFSA_2: 37;

          per cases by A5, Th1;

            suppose o is Int-Location;

            hence (( Exec (I,s)) . o) = (s . o) by A6, SCMFSA_2: 71;

          end;

            suppose o is FinSeq-Location;

            hence (( Exec (I,s)) . o) = (s . o) by A6, SCMFSA_2: 71;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let a, i1;

      cluster (a =0_goto i1) -> jump-only non sequential non ins-loc-free;

      coherence

      proof

        thus ( InsCode (a =0_goto i1)) is jump-only;

        ( JUMP (a =0_goto i1)) <> {} ;

        hence (a =0_goto i1) is non sequential by AMISTD_1: 13;

        ( dom ( JumpPart (a =0_goto i1))) = ( dom <*i1*>) by Th15

        .= {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        hence not ( JumpPart (a =0_goto i1)) is empty;

      end;

      cluster (a >0_goto i1) -> jump-only non sequential non ins-loc-free;

      coherence

      proof

        thus ( InsCode (a >0_goto i1)) is jump-only;

        ( JUMP (a >0_goto i1)) <> {} ;

        hence (a >0_goto i1) is non sequential by AMISTD_1: 13;

        ( dom ( JumpPart (a >0_goto i1))) = ( dom <*i1*>) by Th16

        .= {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        hence not ( JumpPart (a >0_goto i1)) is empty;

      end;

    end

    

     Lm2: ( intloc 0 ) <> ( intloc 1) by AMI_3: 10;

    registration

      let a, b;

      cluster ( InsCode (a := b)) -> non jump-only;

      coherence

      proof

        set w = the State of SCM+FSA ;

        set t = (w +* ((( intloc 0 ),( intloc 1)) --> ( 0 ,1)));

        

         A1: ( InsCode (a := b)) = 1 by SCMFSA_2: 18

        .= ( InsCode (( intloc 0 ) := ( intloc 1))) by SCMFSA_2: 18;

        

         A2: ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) = {( intloc 0 ), ( intloc 1)} by FUNCT_4: 62;

        then

         A3: ( intloc 1) in ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) by TARSKI:def 2;

        ( intloc 0 ) in ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) by A2, TARSKI:def 2;

        

        then

         A4: (t . ( intloc 0 )) = (((( intloc 0 ),( intloc 1)) --> ( 0 ,1)) . ( intloc 0 )) by FUNCT_4: 13

        .= 0 by AMI_3: 10, FUNCT_4: 63;

        ( intloc 0 ) in Int-Locations by AMI_2:def 16;

        then

         A5: ( intloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        (( Exec ((( intloc 0 ) := ( intloc 1)),t)) . ( intloc 0 )) = (t . ( intloc 1)) by SCMFSA_2: 63

        .= (((( intloc 0 ),( intloc 1)) --> ( 0 ,1)) . ( intloc 1)) by A3, FUNCT_4: 13

        .= 1 by FUNCT_4: 63;

        hence thesis by A1, A4, A5;

      end;

      cluster ( InsCode ( AddTo (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM+FSA ;

        set t = (w +* ((( intloc 0 ),( intloc 1)) --> ( 0 ,1)));

        

         A6: ( InsCode ( AddTo (a,b))) = 2 by SCMFSA_2: 19

        .= ( InsCode ( AddTo (( intloc 0 ),( intloc 1)))) by SCMFSA_2: 19;

        

         A7: ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) = {( intloc 0 ), ( intloc 1)} by FUNCT_4: 62;

        then ( intloc 0 ) in ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) by TARSKI:def 2;

        

        then

         A8: (t . ( intloc 0 )) = (((( intloc 0 ),( intloc 1)) --> ( 0 ,1)) . ( intloc 0 )) by FUNCT_4: 13

        .= 0 by AMI_3: 10, FUNCT_4: 63;

        ( intloc 0 ) in Int-Locations by AMI_2:def 16;

        then

         A9: ( intloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

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

        

        then (t . ( intloc 1)) = (((( intloc 0 ),( intloc 1)) --> ( 0 ,1)) . ( intloc 1)) by FUNCT_4: 13

        .= 1 by FUNCT_4: 63;

        then (( Exec (( AddTo (( intloc 0 ),( intloc 1))),t)) . ( intloc 0 )) = ( 0 qua Nat + 1) by A8, SCMFSA_2: 64;

        hence thesis by A6, A8, A9;

      end;

      cluster ( InsCode ( SubFrom (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM+FSA ;

        set t = (w +* ((( intloc 0 ),( intloc 1)) --> ( 0 ,1)));

        

         A10: ( InsCode ( SubFrom (a,b))) = 3 by SCMFSA_2: 20

        .= ( InsCode ( SubFrom (( intloc 0 ),( intloc 1)))) by SCMFSA_2: 20;

        

         A11: ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) = {( intloc 0 ), ( intloc 1)} by FUNCT_4: 62;

        then ( intloc 0 ) in ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) by TARSKI:def 2;

        

        then

         A12: (t . ( intloc 0 )) = (((( intloc 0 ),( intloc 1)) --> ( 0 ,1)) . ( intloc 0 )) by FUNCT_4: 13

        .= 0 by AMI_3: 10, FUNCT_4: 63;

        ( intloc 0 ) in Int-Locations by AMI_2:def 16;

        then

         A13: ( intloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        ( intloc 1) in ( dom ((( intloc 0 ),( intloc 1)) --> ( 0 ,1))) by A11, TARSKI:def 2;

        

        then

         A14: (t . ( intloc 1)) = (((( intloc 0 ),( intloc 1)) --> ( 0 ,1)) . ( intloc 1)) by FUNCT_4: 13

        .= 1 by FUNCT_4: 63;

        (( Exec (( SubFrom (( intloc 0 ),( intloc 1))),t)) . ( intloc 0 )) = ((t . ( intloc 0 )) - (t . ( intloc 1))) by SCMFSA_2: 65

        .= ( - 1) by A12, A14;

        hence thesis by A10, A12, A13;

      end;

      cluster ( InsCode ( MultBy (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM+FSA ;

        set t = (w +* ((( intloc 0 ),( intloc 1)) --> (1, 0 )));

        

         A15: ( InsCode ( MultBy (a,b))) = 4 by SCMFSA_2: 21

        .= ( InsCode ( MultBy (( intloc 0 ),( intloc 1)))) by SCMFSA_2: 21;

        

         A16: ( dom ((( intloc 0 ),( intloc 1)) --> (1, 0 ))) = {( intloc 0 ), ( intloc 1)} by FUNCT_4: 62;

        then ( intloc 0 ) in ( dom ((( intloc 0 ),( intloc 1)) --> (1, 0 ))) by TARSKI:def 2;

        

        then

         A17: (t . ( intloc 0 )) = (((( intloc 0 ),( intloc 1)) --> (1, 0 )) . ( intloc 0 )) by FUNCT_4: 13

        .= 1 by AMI_3: 10, FUNCT_4: 63;

        ( intloc 0 ) in Int-Locations by AMI_2:def 16;

        then

         A18: ( intloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        ( intloc 1) in ( dom ((( intloc 0 ),( intloc 1)) --> (1, 0 ))) by A16, TARSKI:def 2;

        

        then

         A19: (t . ( intloc 1)) = (((( intloc 0 ),( intloc 1)) --> (1, 0 )) . ( intloc 1)) by FUNCT_4: 13

        .= 0 by FUNCT_4: 63;

        (( Exec (( MultBy (( intloc 0 ),( intloc 1))),t)) . ( intloc 0 )) = ((t . ( intloc 0 )) * (t . ( intloc 1))) by SCMFSA_2: 66

        .= 0 by A19;

        hence thesis by A15, A17, A18;

      end;

      cluster ( InsCode ( Divide (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM+FSA ;

        set t = (w +* ((( intloc 0 ),( intloc 1)) --> (7,3)));

        

         A20: ( InsCode ( Divide (a,b))) = 5 by SCMFSA_2: 22

        .= ( InsCode ( Divide (( intloc 0 ),( intloc 1)))) by SCMFSA_2: 22;

        

         A21: ( dom ((( intloc 0 ),( intloc 1)) --> (7,3))) = {( intloc 0 ), ( intloc 1)} by FUNCT_4: 62;

        then ( intloc 0 ) in ( dom ((( intloc 0 ),( intloc 1)) --> (7,3))) by TARSKI:def 2;

        

        then

         A22: (t . ( intloc 0 )) = (((( intloc 0 ),( intloc 1)) --> (7,3)) . ( intloc 0 )) by FUNCT_4: 13

        .= 7 by AMI_3: 10, FUNCT_4: 63;

        

         A23: 7 = ((2 * 3) + 1);

        ( intloc 0 ) in Int-Locations by AMI_2:def 16;

        then

         A24: ( intloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        ( intloc 1) in ( dom ((( intloc 0 ),( intloc 1)) --> (7,3))) by A21, TARSKI:def 2;

        

        then (t . ( intloc 1)) = (((( intloc 0 ),( intloc 1)) --> (7,3)) . ( intloc 1)) by FUNCT_4: 13

        .= 3 by FUNCT_4: 63;

        

        then (( Exec (( Divide (( intloc 0 ),( intloc 1))),t)) . ( intloc 0 )) = (7 div 3 qua Element of NAT ) by A22, Lm2, SCMFSA_2: 67

        .= 2 by A23, NAT_D:def 1;

        hence thesis by A20, A22, A24;

      end;

    end

    

     Lm3: ( fsloc 0 ) <> ( intloc 0 ) by SCMFSA_2: 99;

    

     Lm4: ( fsloc 0 ) <> ( intloc 1) by SCMFSA_2: 99;

    registration

      let a, b, f;

      cluster ( InsCode (b := (f,a))) -> non jump-only;

      coherence

      proof

        ( Values ( intloc 1)) = INT by SCMFSA_2: 11;

        then

        reconsider E = 1 as Element of ( Values ( intloc 1)) by INT_1:def 1;

        ( Values ( intloc 0 )) = INT by SCMFSA_2: 11;

        then

        reconsider D = 1 as Element of ( Values ( intloc 0 )) by INT_1:def 1;

        reconsider DWA = 2 as Element of INT by INT_1:def 1;

        set w = the State of SCM+FSA ;

         <*DWA*> in ( INT * ) by FINSEQ_1:def 11;

        then

        reconsider F = <*2*> as Element of ( Values ( fsloc 0 )) by SCMFSA_2: 12;

        reconsider t = (((w +* (( fsloc 0 ) .--> F)) +* (( intloc 0 ) .--> D)) +* (( intloc 1) .--> E)) as State of SCM+FSA ;

        

         A1: (t . ( intloc 0 )) = D by AMI_3: 10, BVFUNC14: 12;

        

         A2: (t . ( fsloc 0 )) = F by Lm3, Lm4, FUNCT_7: 114;

        then ( dom (t . ( fsloc 0 ))) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        then

         A3: 1 in ( dom (t . ( fsloc 0 ))) by TARSKI:def 1;

        consider k be Nat such that

         A4: k = |.(t . ( intloc 1)).| and

         A5: (( Exec ((( intloc 0 ) := (( fsloc 0 ),( intloc 1))),t)) . ( intloc 0 )) = ((t . ( fsloc 0 )) /. k) by SCMFSA_2: 72;

        ( intloc 0 ) in Int-Locations by AMI_2:def 16;

        then

         A6: ( intloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        (t . ( intloc 1)) = E by FUNCT_7: 94;

        then k = 1 by A4, ABSVALUE:def 1;

        

        then

         A7: (( Exec ((( intloc 0 ) := (( fsloc 0 ),( intloc 1))),t)) . ( intloc 0 )) = ((t . ( fsloc 0 )) . 1) by A5, A3, PARTFUN1:def 6

        .= 2 by A2, FINSEQ_1:def 8;

        ( InsCode (b := (f,a))) = 9

        .= ( InsCode (( intloc 0 ) := (( fsloc 0 ),( intloc 1))));

        hence thesis by A1, A7, A6;

      end;

      cluster ( InsCode ((f,a) := b)) -> non jump-only;

      coherence

      proof

        ( Values ( intloc 0 )) = INT by SCMFSA_2: 11;

        then

        reconsider D = 1 as Element of ( Values ( intloc 0 )) by INT_1:def 1;

        reconsider DWA = 2 as Element of INT by INT_1:def 1;

        set w = the State of SCM+FSA ;

        

         A8: ( InsCode ((f,a) := b)) = 10

        .= ( InsCode ((( fsloc 0 ),( intloc 1)) := ( intloc 0 )));

        ( Values ( intloc 1)) = INT by SCMFSA_2: 11;

        then

        reconsider E = 1 as Element of ( Values ( intloc 1)) by INT_1:def 1;

         <*DWA*> in ( INT * ) by FINSEQ_1:def 11;

        then

        reconsider F = <*2*> as Element of ( Values ( fsloc 0 )) by SCMFSA_2: 12;

        reconsider t = (((w +* (( fsloc 0 ) .--> F)) +* (( intloc 0 ) .--> D)) +* (( intloc 1) .--> E)) as State of SCM+FSA ;

        consider k be Nat such that

         A9: k = |.(t . ( intloc 1)).| and

         A10: (( Exec (((( fsloc 0 ),( intloc 1)) := ( intloc 0 )),t)) . ( fsloc 0 )) = ((t . ( fsloc 0 )) +* (k,(t . ( intloc 0 )))) by SCMFSA_2: 73;

        (t . ( intloc 1)) = E by FUNCT_7: 94;

        then

         A11: k = 1 by A9, ABSVALUE:def 1;

        ( fsloc 0 ) in FinSeq-Locations by SCMFSA_2:def 5;

        then

         A12: ( fsloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

         A13: F <> <*D*> by FINSEQ_1: 76;

        

         A14: (t . ( fsloc 0 )) = F by Lm3, Lm4, FUNCT_7: 114;

        (t . ( intloc 0 )) = D by AMI_3: 10, BVFUNC14: 12;

        then (( Exec (((( fsloc 0 ),( intloc 1)) := ( intloc 0 )),t)) . ( fsloc 0 )) = <*D*> by A14, A10, A11, FUNCT_7: 95;

        hence thesis by A8, A14, A13, A12;

      end;

    end

    registration

      let a, b, f;

      cluster (b := (f,a)) -> non jump-only;

      coherence ;

      cluster ((f,a) := b) -> non jump-only;

      coherence ;

    end

    registration

      let a, f;

      cluster ( InsCode (a :=len f)) -> non jump-only;

      coherence

      proof

        ( Values ( intloc 0 )) = INT by SCMFSA_2: 11;

        then

        reconsider D = 3 as Element of ( Values ( intloc 0 )) by INT_1:def 1;

        reconsider DWA = 2 as Element of INT by INT_1:def 1;

        set w = the State of SCM+FSA ;

        

         A1: ( InsCode (a :=len f)) = 11

        .= ( InsCode (( intloc 0 ) :=len ( fsloc 0 )));

         <*DWA*> in ( INT * ) by FINSEQ_1:def 11;

        then

        reconsider F = <*2*> as Element of ( Values ( fsloc 0 )) by SCMFSA_2: 12;

        reconsider t = ((w +* (( fsloc 0 ) .--> F)) +* (( intloc 0 ) .--> D)) as State of SCM+FSA ;

        

         A2: (t . ( fsloc 0 )) = F by BVFUNC14: 12, SCMFSA_2: 99;

        ( intloc 0 ) in Int-Locations by AMI_2:def 16;

        then

         A3: ( intloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        

         A4: (t . ( intloc 0 )) = D by FUNCT_7: 94;

        (( Exec ((( intloc 0 ) :=len ( fsloc 0 )),t)) . ( intloc 0 )) = ( len (t . ( fsloc 0 ))) by SCMFSA_2: 74

        .= 1 by A2, FINSEQ_1: 39;

        hence thesis by A1, A4, A3;

      end;

      cluster ( InsCode (f :=<0,...,0> a)) -> non jump-only;

      coherence

      proof

        ( Values ( intloc 0 )) = INT by SCMFSA_2: 11;

        then

        reconsider D = 1 as Element of ( Values ( intloc 0 )) by INT_1:def 1;

        reconsider DWA = 2 as Element of INT by INT_1:def 1;

        set w = the State of SCM+FSA ;

         <*DWA*> in ( INT * ) by FINSEQ_1:def 11;

        then

        reconsider F = <*2*> as Element of ( Values ( fsloc 0 )) by SCMFSA_2: 12;

        reconsider t = ((w +* (( fsloc 0 ) .--> F)) +* (( intloc 0 ) .--> D)) as State of SCM+FSA ;

        

         A5: (t . ( fsloc 0 )) = F by BVFUNC14: 12, SCMFSA_2: 99;

        

         A6: F <> <* 0 *> by FINSEQ_1: 76;

        consider k be Nat such that

         A7: k = |.(t . ( intloc 0 )).| and

         A8: (( Exec ((( fsloc 0 ) :=<0,...,0> ( intloc 0 )),t)) . ( fsloc 0 )) = (k |-> 0 ) by SCMFSA_2: 75;

        ( fsloc 0 ) in FinSeq-Locations by SCMFSA_2:def 5;

        then

         A9: ( fsloc 0 ) in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

        (t . ( intloc 0 )) = D by FUNCT_7: 94;

        then k = 1 by A7, ABSVALUE:def 1;

        then

         A10: (( Exec ((( fsloc 0 ) :=<0,...,0> ( intloc 0 )),t)) . ( fsloc 0 )) = <* 0 *> by A8, FINSEQ_2: 59;

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

        .= ( InsCode (( fsloc 0 ) :=<0,...,0> ( intloc 0 )));

        hence thesis by A5, A6, A10, A9;

      end;

    end

    registration

      let a, f;

      cluster (a :=len f) -> non jump-only;

      coherence ;

      cluster (f :=<0,...,0> a) -> non jump-only;

      coherence ;

    end

    registration

      cluster SCM+FSA -> with_explicit_jumps;

      coherence

      proof

        let I be Instruction of SCM+FSA ;

        thus ( JUMP I) c= ( rng ( JumpPart I))

        proof

          let f be object such that

           A1: f in ( JUMP I);

          per cases by SCMFSA_2: 93;

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

            hence thesis by A1, SCMFSA_2: 96;

          end;

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

            hence thesis by A1;

          end;

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

            hence thesis by A1;

          end;

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

            hence thesis by A1;

          end;

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

            hence thesis by A1;

          end;

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

            hence thesis by A1;

          end;

            suppose

             A2: ex i1 st I = ( goto i1);

            consider i1 such that

             A3: I = ( goto i1) by A2;

            ( rng <*i1*>) = {i1} by FINSEQ_1: 39;

            hence thesis by A1, A3, Th34;

          end;

            suppose

             A4: ex i1, a st I = (a =0_goto i1);

            consider a, i1 such that

             A5: I = (a =0_goto i1) by A4;

            

             A6: ( JumpPart (a =0_goto i1)) = <*i1*> by Th15;

            ( rng <*i1*>) = {i1} by FINSEQ_1: 39;

            hence thesis by A1, A5, A6, Th36;

          end;

            suppose

             A7: ex i1, a st I = (a >0_goto i1);

            consider a, i1 such that

             A8: I = (a >0_goto i1) by A7;

            

             A9: ( JumpPart (a >0_goto i1)) = <*i1*> by Th16;

            ( rng <*i1*>) = {i1} by FINSEQ_1: 39;

            hence thesis by A1, A8, A9, Th38;

          end;

            suppose ex a, b, f st I = (b := (f,a));

            hence thesis by A1;

          end;

            suppose ex a, b, f st I = ((f,a) := b);

            hence thesis by A1;

          end;

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

            hence thesis by A1;

          end;

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

            hence thesis by A1;

          end;

        end;

        let f be object;

        assume f in ( rng ( JumpPart I));

        then

        consider k be object such that

         A10: k in ( dom ( JumpPart I)) and

         A11: f = (( JumpPart I) . k) by FUNCT_1:def 3;

        per cases by SCMFSA_2: 93;

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

          then ( dom ( JumpPart I)) = ( dom {} );

          hence thesis by A10;

        end;

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

          then

          consider a, b such that

           A12: I = (a := b);

          k in ( dom {} ) by A10, A12, Th10;

          hence thesis;

        end;

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

          then

          consider a, b such that

           A13: I = ( AddTo (a,b));

          k in ( dom {} ) by A10, A13, Th11;

          hence thesis;

        end;

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

          then

          consider a, b such that

           A14: I = ( SubFrom (a,b));

          k in ( dom {} ) by A10, A14, Th12;

          hence thesis;

        end;

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

          then

          consider a, b such that

           A15: I = ( MultBy (a,b));

          k in ( dom {} ) by A10, A15, Th13;

          hence thesis;

        end;

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

          then

          consider a, b such that

           A16: I = ( Divide (a,b));

          k in ( dom {} ) by A10, A16, Th14;

          hence thesis;

        end;

          suppose ex i1 st I = ( goto i1);

          then

          consider i1 such that

           A17: I = ( goto i1);

          

           A18: ( JumpPart I) = <*i1*> by A17;

          then k = 1 by A10, FINSEQ_1: 90;

          then

           A19: f = i1 by A18, A11, FINSEQ_1:def 8;

          ( JUMP I) = {i1} by A17, Th34;

          hence thesis by A19, TARSKI:def 1;

        end;

          suppose ex i1, a st I = (a =0_goto i1);

          then

          consider a, i1 such that

           A20: I = (a =0_goto i1);

          

           A21: ( JumpPart I) = <*i1*> by A20, Th15;

          then k = 1 by A10, FINSEQ_1: 90;

          then

           A22: f = i1 by A21, A11, FINSEQ_1:def 8;

          ( JUMP I) = {i1} by A20, Th36;

          hence thesis by A22, TARSKI:def 1;

        end;

          suppose ex i1, a st I = (a >0_goto i1);

          then

          consider a, i1 such that

           A23: I = (a >0_goto i1);

          

           A24: ( JumpPart I) = <*i1*> by A23, Th16;

          then k = 1 by A10, FINSEQ_1: 90;

          then

           A25: f = i1 by A24, A11, FINSEQ_1:def 8;

          ( JUMP I) = {i1} by A23, Th38;

          hence thesis by A25, TARSKI:def 1;

        end;

          suppose ex a, b, f st I = (b := (f,a));

          then

          consider a, b, f such that

           A26: I = (b := (f,a));

          k in ( dom {} ) by A10, A26;

          hence thesis;

        end;

          suppose ex a, b, f st I = ((f,a) := b);

          then

          consider a, b, f such that

           A27: I = ((f,a) := b);

          k in ( dom {} ) by A10, A27;

          hence thesis;

        end;

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

          then

          consider a, f such that

           A28: I = (a :=len f);

          k in ( dom {} ) by A10, A28;

          hence thesis;

        end;

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

          then

          consider a, f such that

           A29: I = (f :=<0,...,0> a);

          k in ( dom {} ) by A10, A29;

          hence thesis;

        end;

      end;

    end

    theorem :: SCMFSA10:41

    

     Th41: ( IncAddr (( goto i1),k)) = ( goto (i1 + k))

    proof

      

       A1: ( InsCode ( IncAddr (( goto i1),k))) = ( InsCode ( goto i1)) by COMPOS_0:def 9

      .= 6

      .= ( InsCode ( goto (i1 + k)));

      

       A2: ( AddressPart ( IncAddr (( goto i1),k))) = ( AddressPart ( goto i1)) by COMPOS_0:def 9

      .= {}

      .= ( AddressPart ( goto (i1 + k)));

      

       A3: ( JumpPart ( IncAddr (( goto i1),k))) = (k + ( JumpPart ( goto i1))) by COMPOS_0:def 9;

      then

       A4: ( dom ( JumpPart ( IncAddr (( goto i1),k)))) = ( dom ( JumpPart ( goto i1))) by VALUED_1:def 2;

      

       A5: for x be object st x in ( dom ( JumpPart ( goto i1))) holds (( JumpPart ( IncAddr (( goto i1),k))) . x) = (( JumpPart ( goto (i1 + k))) . x)

      proof

        let x be object;

        assume

         A6: x in ( dom ( JumpPart ( goto i1)));

        then x in ( dom <*i1*>);

        then

         A7: x = 1 by FINSEQ_1: 90;

        set f = (( JumpPart ( goto i1)) . x);

        

         A8: (( JumpPart ( IncAddr (( goto i1),k))) . x) = (k + f) by A4, A3, A6, VALUED_1:def 2;

        f = ( <*i1*> . x)

        .= i1 by A7, FINSEQ_1:def 8;

        

        hence (( JumpPart ( IncAddr (( goto i1),k))) . x) = ( <*(i1 + k)*> . x) by A7, A8, FINSEQ_1:def 8

        .= (( JumpPart ( goto (i1 + k))) . x);

      end;

      ( dom ( JumpPart ( goto (i1 + k)))) = ( dom <*(i1 + k)*>)

      .= ( Seg 1) by FINSEQ_1:def 8

      .= ( dom <*i1*>) by FINSEQ_1:def 8

      .= ( dom ( JumpPart ( goto i1)));

      then ( JumpPart ( IncAddr (( goto i1),k))) = ( JumpPart ( goto (i1 + k))) by A4, A5, FUNCT_1: 2;

      hence thesis by A1, A2, COMPOS_0: 1;

    end;

    theorem :: SCMFSA10:42

    

     Th42: ( IncAddr ((a =0_goto i1),k)) = (a =0_goto (i1 + k))

    proof

      

       A1: ( InsCode ( IncAddr ((a =0_goto i1),k))) = ( InsCode (a =0_goto i1)) by COMPOS_0:def 9

      .= 7 by SCMFSA_2: 24

      .= ( InsCode (a =0_goto (i1 + k))) by SCMFSA_2: 24;

      

       A2: (a =0_goto i1) = [7, <*i1*>, <*a*>] by Th7;

      

       A3: (a =0_goto (i1 + k)) = [7, <*(i1 + k)*>, <*a*>] by Th7;

      

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

      .= <*a*> by A2

      .= ( AddressPart (a =0_goto (i1 + k))) by A3;

      

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

      then

       A6: ( dom ( JumpPart ( IncAddr ((a =0_goto i1),k)))) = ( dom ( JumpPart (a =0_goto i1))) by VALUED_1:def 2;

      

       A7: for x be object st x in ( dom ( JumpPart (a =0_goto i1))) holds (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = (( JumpPart (a =0_goto (i1 + k))) . x)

      proof

        let x be object;

        assume

         A8: x in ( dom ( JumpPart (a =0_goto i1)));

        then x in ( dom <*i1*>) by Th15;

        then

         A9: x = 1 by FINSEQ_1: 90;

        set f = (( JumpPart (a =0_goto i1)) . x);

        

         A10: (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = (k + f) by A6, A5, A8, VALUED_1:def 2;

        f = ( <*i1*> . x) by Th15

        .= i1 by A9, FINSEQ_1: 40;

        

        hence (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = ( <*(i1 + k)*> . x) by A9, A10, FINSEQ_1: 40

        .= (( JumpPart (a =0_goto (i1 + k))) . x) by Th15;

      end;

      ( dom ( JumpPart (a =0_goto (i1 + k)))) = ( dom <*(i1 + k)*>) by Th15

      .= ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*i1*>) by FINSEQ_1: 38

      .= ( dom ( JumpPart (a =0_goto i1))) by Th15;

      then ( JumpPart ( IncAddr ((a =0_goto i1),k))) = ( JumpPart (a =0_goto (i1 + k))) by A6, A7, FUNCT_1: 2;

      hence thesis by A1, A4, COMPOS_0: 1;

    end;

    theorem :: SCMFSA10:43

    

     Th43: ( IncAddr ((a >0_goto i1),k)) = (a >0_goto (i1 + k))

    proof

      

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

      .= 8 by SCMFSA_2: 25

      .= ( InsCode (a >0_goto (i1 + k))) by SCMFSA_2: 25;

      

       A2: (a >0_goto i1) = [8, <*i1*>, <*a*>] by Th8;

      

       A3: (a >0_goto (i1 + k)) = [8, <*(i1 + k)*>, <*a*>] by Th8;

      

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

      .= <*a*> by A2

      .= ( AddressPart (a >0_goto (i1 + k))) by A3;

      

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

      then

       A6: ( dom ( JumpPart ( IncAddr ((a >0_goto i1),k)))) = ( dom ( JumpPart (a >0_goto i1))) by VALUED_1:def 2;

      

       A7: for x be object st x in ( dom ( JumpPart (a >0_goto i1))) holds (( JumpPart ( IncAddr ((a >0_goto i1),k))) . x) = (( JumpPart (a >0_goto (i1 + k))) . x)

      proof

        let x be object;

        assume

         A8: x in ( dom ( JumpPart (a >0_goto i1)));

        then x in ( dom <*i1*>) by Th16;

        then

         A9: x = 1 by FINSEQ_1: 90;

        set f = (( JumpPart (a >0_goto i1)) . 1);

        

         A10: (( JumpPart ( IncAddr ((a >0_goto i1),k))) . 1) = (k + f) by A9, A6, A5, A8, VALUED_1:def 2;

        f = ( <*i1*> . x) by Th16, A9

        .= i1 by A9, FINSEQ_1: 40;

        

        hence (( JumpPart ( IncAddr ((a >0_goto i1),k))) . x) = ( <*(i1 + k)*> . x) by A9, A10, FINSEQ_1: 40

        .= (( JumpPart (a >0_goto (i1 + k))) . x) by Th16;

      end;

      ( dom ( JumpPart (a >0_goto (i1 + k)))) = ( dom <*(i1 + k)*>) by Th16

      .= ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*i1*>) by FINSEQ_1: 38

      .= ( dom ( JumpPart (a >0_goto i1))) by Th16;

      then ( JumpPart ( IncAddr ((a >0_goto i1),k))) = ( JumpPart (a >0_goto (i1 + k))) by A6, A7, FUNCT_1: 2;

      hence thesis by A1, A4, COMPOS_0: 1;

    end;

    registration

      cluster SCM+FSA -> IC-relocable;

      coherence

      proof

        let I be Instruction of SCM+FSA ;

        per cases by SCMFSA_2: 93;

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

          hence thesis by SCMFSA_2: 96;

        end;

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

          hence thesis;

        end;

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

          hence thesis;

        end;

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

          hence thesis;

        end;

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

          hence thesis;

        end;

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

          hence thesis;

        end;

          suppose

           A1: ex i1 st I = ( goto i1);

          let j,k be Nat, s1 be State of SCM+FSA ;

          set s2 = ( IncIC (s1,k));

          consider i1 such that

           A2: I = ( goto i1) by A1;

          

          thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec (( goto (j + i1)),s1))) + k) by A2, Th41

          .= ((j + i1) + k) by SCMFSA_2: 69

          .= ( IC ( Exec (( goto ((j + k) + i1)),s2))) by SCMFSA_2: 69

          .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A2, Th41;

        end;

          suppose ex i1, a st I = (a =0_goto i1);

          then

          consider a, i1 such that

           A3: I = (a =0_goto i1);

          let j,k be Nat, s1 be State of SCM+FSA ;

          set s2 = ( IncIC (s1,k));

          a <> ( IC SCM+FSA ) & ( dom (( IC SCM+FSA ) .--> (( IC s1) + k))) = {( IC SCM+FSA )} by SCMFSA_2: 56;

          then not a in ( dom (( IC SCM+FSA ) .--> (( IC s1) + k))) by TARSKI:def 1;

          then

           A4: (s1 . a) = (s2 . a) by FUNCT_4: 11;

          per cases ;

            suppose

             A5: (s1 . a) = 0 ;

            

            thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec ((a =0_goto (j + i1)),s1))) + k) by A3, Th42

            .= ((j + i1) + k) by A5, SCMFSA_2: 70

            .= ( IC ( Exec ((a =0_goto ((j + k) + i1)),s2))) by A4, A5, SCMFSA_2: 70

            .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A3, Th42;

          end;

            suppose

             A6: (s1 . a) <> 0 ;

            

             A7: ( IncAddr (I,j)) = (a =0_goto (i1 + j)) by A3, Th42;

            

             A8: ( IncAddr (I,(j + k))) = (a =0_goto (i1 + (j + k))) by A3, Th42;

            ( IC SCM+FSA ) in ( dom (( IC SCM+FSA ) .--> (( IC s1) + k))) by TARSKI:def 1;

            

            then

             A9: ( IC s2) = ((( IC SCM+FSA ) .--> (( IC s1) + k)) . ( IC SCM+FSA )) by FUNCT_4: 13

            .= (( IC s1) + k) by FUNCOP_1: 72;

            

            thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = ((( IC s1) + 1) + k) by A7, A6, SCMFSA_2: 70

            .= (( IC s2) + 1) by A9

            .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A8, A6, A4, SCMFSA_2: 70;

          end;

        end;

          suppose ex i1, a st I = (a >0_goto i1);

          then

          consider i1, a such that

           A10: I = (a >0_goto i1);

          let j,k be Nat, s1 be State of SCM+FSA ;

          set s2 = ( IncIC (s1,k));

          a <> ( IC SCM+FSA ) & ( dom (( IC SCM+FSA ) .--> (( IC s1) + k))) = {( IC SCM+FSA )} by SCMFSA_2: 56;

          then not a in ( dom (( IC SCM+FSA ) .--> (( IC s1) + k))) by TARSKI:def 1;

          then

           A11: (s1 . a) = (s2 . a) by FUNCT_4: 11;

          per cases ;

            suppose

             A12: (s1 . a) > 0 ;

            

            thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec ((a >0_goto (j + i1)),s1))) + k) by A10, Th43

            .= ((j + i1) + k) by A12, SCMFSA_2: 71

            .= ( IC ( Exec ((a >0_goto ((j + k) + i1)),s2))) by A11, A12, SCMFSA_2: 71

            .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A10, Th43;

          end;

            suppose

             A13: (s1 . a) <= 0 ;

            

             A14: ( IncAddr (I,j)) = (a >0_goto (i1 + j)) by A10, Th43;

            

             A15: ( IncAddr (I,(j + k))) = (a >0_goto (i1 + (j + k))) by A10, Th43;

            ( IC SCM+FSA ) in ( dom (( IC SCM+FSA ) .--> (( IC s1) + k))) by TARSKI:def 1;

            

            then

             A16: ( IC s2) = ((( IC SCM+FSA ) .--> (( IC s1) + k)) . ( IC SCM+FSA )) by FUNCT_4: 13

            .= (( IC s1) + k) by FUNCOP_1: 72;

            

            thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = ((( IC s1) + 1) + k) by A14, A13, SCMFSA_2: 71

            .= (( IC s2) + 1) by A16

            .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A15, A13, A11, SCMFSA_2: 71;

          end;

        end;

          suppose ex a, b, f st I = (b := (f,a));

          hence thesis;

        end;

          suppose ex a, b, f st I = ((f,a) := b);

          hence thesis;

        end;

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

          hence thesis;

        end;

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

          hence thesis;

        end;

      end;

    end