compos_1.miz



    begin

    reserve x,A for set,

i,j,k,m,n,l,l1,l2 for Nat;

    reserve D for non empty set,

z for Nat;

    definition

      struct COM-Struct (# the InstructionsF -> Instructions #)

       attr strict strict;

    end

    definition

      ::$Canceled

      :: COMPOS_1:def8

      func Trivial-COM -> strict COM-Struct means

      : Def1: the InstructionsF of it = { [ 0 , {} , {} ]};

      existence

      proof

        take S = COM-Struct (# { [ 0 , {} , {} ]} #);

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let S be COM-Struct;

      mode Instruction of S is Element of the InstructionsF of S;

    end

    definition

      ::$Canceled

      let S be COM-Struct;

      :: COMPOS_1:def10

      func halt S -> Instruction of S equals ( halt the InstructionsF of S);

      coherence ;

    end

    definition

      let S be COM-Struct;

      let I be the InstructionsF of S -valued Function;

      :: COMPOS_1:def11

      attr I is halt-free means

      : Def3: not ( halt S) in ( rng I);

    end

    begin

    reserve S for COM-Struct;

    reserve ins for Element of the InstructionsF of S;

    definition

      let S be COM-Struct;

      mode Instruction-Sequence of S is the InstructionsF of S -valued ManySortedSet of NAT ;

    end

    definition

      let S be COM-Struct;

      let P be Instruction-Sequence of S, k be Nat;

      :: original: .

      redefine

      func P . k -> Instruction of S ;

      coherence

      proof

        

         A1: k in NAT by ORDINAL1:def 12;

        ( dom P) = NAT by PARTFUN1:def 2;

        then

         A2: (P . k) in ( rng P) by A1, FUNCT_1: 3;

        ( rng P) c= the InstructionsF of S by RELAT_1:def 19;

        hence (P . k) is Instruction of S by A2;

      end;

    end

    begin

    definition

      let S be COM-Struct;

      let p be NAT -definedthe InstructionsF of S -valued Function, l be set;

      :: COMPOS_1:def12

      pred p halts_at l means l in ( dom p) & (p . l) = ( halt S);

    end

    definition

      let S be COM-Struct;

      let s be Instruction-Sequence of S, l be Nat;

      :: original: halts_at

      redefine

      :: COMPOS_1:def13

      pred s halts_at l means (s . l) = ( halt S);

      compatibility

      proof

        thus s halts_at l implies (s . l) = ( halt S);

        assume

         A1: (s . l) = ( halt S);

        l in NAT by ORDINAL1:def 12;

        hence l in ( dom s) by PARTFUN1:def 2;

        thus (s . l) = ( halt S) by A1;

      end;

    end

    begin

    notation

      let S be COM-Struct;

      let i be Instruction of S;

      synonym Load i for <%i%>;

    end

    registration

      let S;

      cluster initial1 -element NAT -definedthe InstructionsF of S -valued for Function;

      existence

      proof

        set p = <% the Instruction of S%>;

        take p;

        thus thesis;

      end;

    end

    definition

      let S be COM-Struct;

      mode preProgram of S is finite NAT -definedthe InstructionsF of S -valued Function;

    end

    definition

      let S be COM-Struct, F be non empty preProgram of S;

      :: COMPOS_1:def14

      attr F is halt-ending means

      : Def6: (F . ( LastLoc F)) = ( halt S);

      :: COMPOS_1:def15

      attr F is unique-halt means

      : Def7: for f be Nat st (F . f) = ( halt S) & f in ( dom F) holds f = ( LastLoc F);

    end

    registration

      let S be COM-Struct;

      cluster halt-ending -> non halt-free for non empty preProgram of S;

      coherence

      proof

        let I be non empty preProgram of S;

        assume I is halt-ending;

        then

         A1: (I . ( LastLoc I)) = ( halt S);

        ( LastLoc I) in ( dom I) by VALUED_1: 30;

        hence ( halt S) in ( rng I) by A1, FUNCT_1: 3;

      end;

    end

    registration

      let S be COM-Struct;

      cluster trivial initial non empty for preProgram of S;

      existence

      proof

        reconsider F = <%( halt S)%> as initial non empty preProgram of S;

        take F;

        thus thesis;

      end;

    end

    definition

      let S be COM-Struct;

      mode Program of S is initial non empty preProgram of S;

    end

    ::$Canceled

    theorem :: COMPOS_1:2

    for ins be Element of the InstructionsF of Trivial-COM holds ( InsCode ins) = 0

    proof

      let ins be Element of the InstructionsF of Trivial-COM ;

      the InstructionsF of Trivial-COM = { [ 0 , {} , {} ]} by Def1;

      then ins = [ 0 , {} , {} ] by TARSKI:def 1;

      hence thesis;

    end;

    begin

    definition

      let S be COM-Struct;

      :: COMPOS_1:def16

      func Stop S -> preProgram of S equals ( Load ( halt S));

      coherence ;

    end

    registration

      let S be COM-Struct;

      cluster ( Stop S) -> initial non empty NAT -definedthe InstructionsF of S -valued trivial;

      coherence ;

    end

    

     Lm2: for S be COM-Struct holds (( card ( Stop S)) -' 1) = 0

    proof

      let S be COM-Struct;

      

      thus (( card ( Stop S)) -' 1) = (( card ( Stop S)) - 1) by PRE_CIRC: 20

      .= (1 - 1) by AFINSQ_1: 34

      .= 0 ;

    end;

    

     Lm3: for S be COM-Struct holds ( LastLoc ( Stop S)) = 0

    proof

      let S be COM-Struct;

      (( card ( Stop S)) -' 1) = 0 by Lm2;

      hence thesis by AFINSQ_1: 70;

    end;

    registration

      let S be COM-Struct;

      cluster ( Stop S) -> halt-ending unique-halt;

      coherence

      proof

        

        thus (( Stop S) . ( LastLoc ( Stop S))) = (( 0 .--> ( halt S)) . 0 ) by Lm3

        .= ( halt S) by FUNCOP_1: 72;

        let l be Nat such that (( Stop S) . l) = ( halt S);

        assume l in ( dom ( Stop S));

        then l in { 0 };

        then l = 0 by TARSKI:def 1;

        hence thesis by Lm3;

      end;

    end

    registration

      let S;

      cluster halt-ending unique-halt trivial for Program of S;

      existence

      proof

        take F = ( Stop S);

        thus thesis;

      end;

    end

    definition

      let S;

      mode MacroInstruction of S is halt-ending unique-halt Program of S;

    end

    registration

      let S be COM-Struct;

      cluster initial non empty for preProgram of S;

      existence

      proof

        take ( Stop S);

        thus thesis;

      end;

    end

    theorem :: COMPOS_1:3

    

     Th2: 0 in ( dom ( Stop S)) by TARSKI:def 1;

    theorem :: COMPOS_1:4

    ( card ( Stop S)) = 1 by AFINSQ_1: 34;

    reserve k,m for Nat,

x,x1,x2,x3,y,y1,y2,y3,X,Y,Z for set;

    

     Lm4: ( - 1) < k;

    

     Lm5: for a,b,c be Element of NAT st 1 <= a & 2 <= b holds k < (a - 1) or a <= k & k <= ((a + b) - 3) or k = ((a + b) - 2) or ((a + b) - 2) < k or k = (a - 1)

    proof

      let a,b,c be Element of NAT such that

       A1: 1 <= a and

       A2: 2 <= b and

       A3: (a - 1) <= k and

       A4: a > k or k > ((a + b) - 3) and

       A5: k <> ((a + b) - 2) and

       A6: k <= ((a + b) - 2);

      

       A7: (a - 1) is Element of NAT by A1, INT_1: 5;

      now

        per cases by A4;

          case k < a;

          then k < ((a - 1) + 1);

          hence k <= (a - 1) by A7, NAT_1: 13;

        end;

          case

           A8: ((a + b) - 3) < k;

          (1 + 2) <= (a + b) by A1, A2, XREAL_1: 7;

          then

           A9: ((a + b) - 3) is Element of NAT by INT_1: 5;

          k < (((a + b) - 3) + 1) by A5, A6, XXREAL_0: 1;

          hence k <= (a - 1) by A8, A9, NAT_1: 13;

        end;

      end;

      hence thesis by A3, XXREAL_0: 1;

    end;

    begin

    theorem :: COMPOS_1:5

    

     Th4: for I be Instruction of Trivial-COM holds ( JumpPart I) = 0

    proof

      let I be Instruction of Trivial-COM ;

      the InstructionsF of Trivial-COM = { [ 0 , 0 , 0 ]} by Def1;

      then I = [ 0 , 0 , 0 ] by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: COMPOS_1:6

    for T be InsType of the InstructionsF of Trivial-COM holds ( JumpParts T) = { 0 }

    proof

      let T be InsType of the InstructionsF of Trivial-COM ;

      set A = { ( JumpPart I) where I be Instruction of Trivial-COM : ( InsCode I) = T };

       { 0 } = A

      proof

        hereby

          let a be object;

          assume a in { 0 };

          then

           A1: a = 0 by TARSKI:def 1;

          the InstructionsF of Trivial-COM = { [ 0 , 0 , 0 ]} by Def1;

          then

           A2: ( InsCodes the InstructionsF of Trivial-COM ) = { 0 } by MCART_1: 92;

          

           A3: T = 0 by A2, TARSKI:def 1;

           [ 0 , 0 , 0 ] = ( halt Trivial-COM );

          then

          reconsider I = [ 0 , 0 , 0 ] as Instruction of Trivial-COM ;

          

           A4: ( JumpPart I) = 0 ;

          ( InsCode I) = 0 ;

          hence a in A by A1, A3, A4;

        end;

        let a be object;

        assume a in A;

        then ex I be Instruction of Trivial-COM st a = ( JumpPart I) & ( InsCode I) = T;

        then a = 0 by Th4;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    registration

      let S be COM-Struct;

      cluster trivial -> unique-halt for non empty preProgram of S;

      coherence

      proof

        let F be non empty non empty preProgram of S;

        assume

         A1: F is trivial;

        let f be Nat such that (F . f) = ( halt S) and

         A2: f in ( dom F);

        consider x be object such that

         A3: F = {x} by A1, ZFMISC_1: 131;

        x in F by A3, TARSKI:def 1;

        then

        consider a,b be object such that

         A4: [a, b] = x by RELAT_1:def 1;

        

         A5: ( LastLoc F) in ( dom F) by VALUED_1: 30;

        

         A6: ( dom F) = {a} by A3, A4, RELAT_1: 9;

        

        hence f = a by A2, TARSKI:def 1

        .= ( LastLoc F) by A5, A6, TARSKI:def 1;

      end;

    end

    ::$Canceled

    theorem :: COMPOS_1:8

    

     Th6: for F be MacroInstruction of S st ( card F) = 1 holds F = ( Stop S)

    proof

      let F be MacroInstruction of S;

      assume

       A1: ( card F) = 1;

      then

      consider x be object such that

       A2: F = {x} by CARD_2: 42;

      x in F by A2, TARSKI:def 1;

      then

      consider a,b be object such that

       A3: [a, b] = x by RELAT_1:def 1;

      

       A4: ( dom F) = {a} by A2, A3, RELAT_1: 9;

      

       A5: 0 in ( dom F) by AFINSQ_1: 65;

      then

       A6: a = 0 by A4;

      (( card F) -' 1) = (( card F) - 1) by PRE_CIRC: 20

      .= 0 by A1;

      then ( LastLoc F) = 0 by AFINSQ_1: 70;

      then (F . 0 ) = ( halt S) by Def6;

      then ( halt S) in ( rng F) by A5, FUNCT_1:def 3;

      then ( halt S) in {b} by A2, A3, RELAT_1: 9;

      

      then F = { [ 0 , ( halt S)]} by A2, A3, A6, TARSKI:def 1

      .= ( 0 .--> ( halt S)) by FUNCT_4: 82;

      hence thesis;

    end;

    theorem :: COMPOS_1:9

    for S be COM-Struct holds ( LastLoc ( Stop S)) = 0 by Lm3;

    begin

    definition

      ::$Canceled

      let S be COM-Struct, p be preProgram of S, k be Nat;

      

       A1: ( dom p) c= NAT by RELAT_1:def 18;

      :: COMPOS_1:def21

      func IncAddr (p,k) -> NAT -definedthe InstructionsF of S -valued finite Function means

      : Def9: ( dom it ) = ( dom p) & for m be Nat st m in ( dom p) holds (it . m) = ( IncAddr ((p /. m),k));

      existence

      proof

        defpred P[ object, object] means ex m be Element of NAT st $1 = m & $2 = ( IncAddr ((p /. m),k));

        

         A2: for e be object st e in ( dom p) holds ex u be object st P[e, u]

        proof

          let e be object;

          assume e in ( dom p);

          then

          reconsider l = e as Element of NAT by A1;

          consider m be Nat such that

           A3: l = m;

          take ( IncAddr ((p /. m),k));

          thus thesis by A3;

        end;

        consider f be Function such that

         A4: ( dom f) = ( dom p) and

         A5: for e be object st e in ( dom p) holds P[e, (f . e)] from CLASSES1:sch 1( A2);

        

         A6: ( rng f) c= the InstructionsF of S

        proof

          let e be object;

          assume e in ( rng f);

          then

          consider u be object such that

           A7: u in ( dom f) and

           A8: e = (f . u) by FUNCT_1:def 3;

           P[u, (f . u)] by A7, A5, A4;

          hence e in the InstructionsF of S by A8;

        end;

        reconsider f as NAT -definedthe InstructionsF of S -valued finite Function by A1, A4, A6, FINSET_1: 10, RELAT_1:def 18, RELAT_1:def 19;

        take f;

        thus ( dom f) = ( dom p) by A4;

        let m be Nat;

        assume m in ( dom p);

        then ex j be Element of NAT st m = j & (f . m) = ( IncAddr ((p /. j),k)) by A5;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be NAT -definedthe InstructionsF of S -valued finite Function such that

         A9: ( dom IT1) = ( dom p) and

         A10: for m be Nat st m in ( dom p) holds (IT1 . m) = ( IncAddr ((p /. m),k)) and

         A11: ( dom IT2) = ( dom p) and

         A12: for m be Nat st m in ( dom p) holds (IT2 . m) = ( IncAddr ((p /. m),k));

        for x be object st x in ( dom p) holds (IT1 . x) = (IT2 . x)

        proof

          let x be object;

          assume

           A13: x in ( dom p);

          then

          reconsider l = x as Element of NAT by A1;

          consider m be Nat such that

           A14: l = m;

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

          

          thus (IT1 . x) = ( IncAddr ((p /. m),k)) by A10, A13, A14

          .= (IT2 . x) by A12, A13, A14;

        end;

        hence thesis by A9, A11, FUNCT_1: 2;

      end;

    end

    registration

      let S be COM-Struct, F be preProgram of S, k be Nat;

      cluster ( IncAddr (F,k)) -> NAT -definedthe InstructionsF of S -valued;

      coherence ;

    end

    registration

      let S be COM-Struct, F be empty preProgram of S, k be Nat;

      cluster ( IncAddr (F,k)) -> empty;

      coherence

      proof

        assume not thesis;

        then

        reconsider f = ( IncAddr (F,k)) as non empty Function;

        

         A1: ( dom f) <> {} ;

        ( dom ( IncAddr (F,k))) = ( dom F) by Def9;

        hence thesis by A1;

      end;

    end

    registration

      let S be COM-Struct, F be non empty preProgram of S, k be Nat;

      cluster ( IncAddr (F,k)) -> non empty;

      coherence

      proof

        ( dom ( IncAddr (F,k))) = ( dom F) by Def9;

        hence thesis;

      end;

    end

    registration

      let S be COM-Struct, F be initial preProgram of S, k be Nat;

      cluster ( IncAddr (F,k)) -> initial;

      coherence

      proof

        ( dom ( IncAddr (F,k))) = ( dom F) by Def9;

        hence thesis by AFINSQ_1: 67;

      end;

    end

    ::$Canceled

    registration

      let S be COM-Struct, F be preProgram of S;

      reduce ( IncAddr (F, 0 )) to F;

      reducibility

      proof

        for m be Nat st m in ( dom F) holds (F . m) = ( IncAddr ((F /. m), 0 ))

        proof

          let m be Nat;

          assume m in ( dom F);

          then (F /. m) = (F . m) by PARTFUN1:def 6;

          hence thesis by COMPOS_0: 3;

        end;

        hence thesis by Def9;

      end;

    end

    ::$Canceled

    theorem :: COMPOS_1:17

    

     Th8: for S be COM-Struct, F be preProgram of S holds ( IncAddr (( IncAddr (F,k)),m)) = ( IncAddr (F,(k + m)))

    proof

      let S be COM-Struct, F be preProgram of S;

      

       A1: ( dom ( IncAddr (( IncAddr (F,k)),m))) = ( dom ( IncAddr (F,k))) by Def9

      .= ( dom F) by Def9;

      

       A2: ( dom ( IncAddr (F,(k + m)))) = ( dom F) by Def9;

      for x be object st x in ( dom F) holds (( IncAddr (( IncAddr (F,k)),m)) . x) = (( IncAddr (F,(k + m))) . x)

      proof

        let x be object such that

         A3: x in ( dom F);

        reconsider x as Element of NAT by A3, ORDINAL1:def 12;

        

         A4: x in ( dom ( IncAddr (F,k))) by A3, Def9;

        

         A5: ( IncAddr ((F /. x),k)) = (( IncAddr (F,k)) . x) by A3, Def9

        .= (( IncAddr (F,k)) /. x) by A4, PARTFUN1:def 6;

        (( IncAddr (( IncAddr (F,k)),m)) . x) = ( IncAddr ((( IncAddr (F,k)) /. x),m)) by A4, Def9

        .= ( IncAddr ((F /. x),(k + m))) by A5, COMPOS_0: 7

        .= (( IncAddr (F,(k + m))) . x) by A3, Def9;

        hence thesis;

      end;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    definition

      let S be COM-Struct, p be preProgram of S, k be Nat;

      :: COMPOS_1:def22

      func Reloc (p,k) -> finite NAT -definedthe InstructionsF of S -valued Function equals ( Shift (( IncAddr (p,k)),k));

      coherence ;

    end

    theorem :: COMPOS_1:18

    

     Th9: for S be COM-Struct, F be Program of S, G be non empty preProgram of S holds ( dom ( CutLastLoc F)) misses ( dom ( Reloc (G,(( card F) -' 1))))

    proof

      let S be COM-Struct, F be Program of S, G be non empty preProgram of S;

      set k = (( card F) -' 1);

      assume not thesis;

      then

      consider il be object such that

       A1: il in (( dom ( CutLastLoc F)) /\ ( dom ( Reloc (G,k)))) by XBOOLE_0: 4;

      

       A2: il in ( dom ( CutLastLoc F)) by A1, XBOOLE_0:def 4;

      

       A3: il in ( dom ( Reloc (G,k))) by A1, XBOOLE_0:def 4;

      ( dom ( Reloc (G,k))) = { (m + k) where m be Nat : m in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

      then

      consider m be Nat such that

       A4: il = (m + k) and m in ( dom ( IncAddr (G,k))) by A3;

      reconsider f = ( CutLastLoc F) as non empty NAT -defined finite Function by A1;

      (m + k) <= ( LastLoc f) by A2, A4, VALUED_1: 32;

      then

       A5: (m + k) <= (( card f) -' 1) by AFINSQ_1: 70;

      

       A6: ( card f) = (( card F) - 1) by VALUED_1: 38

      .= (( card F) -' 1) by PRE_CIRC: 20;

      per cases ;

        suppose (k - 1) >= 0 ;

        then (m + k) <= (k - 1) by A5, A6, XREAL_0:def 2;

        then ((m + k) - k) <= ((k - 1) - k) by XREAL_1: 9;

        hence thesis by Lm4;

      end;

        suppose (k - 1) < 0 ;

        then (m + k) = 0 or (m + k) < 0 by A5, A6, XREAL_0:def 2;

        hence thesis by A6;

      end;

    end;

    theorem :: COMPOS_1:19

    

     Th10: for F be unique-halt Program of S, I be Nat st I in ( dom ( CutLastLoc F)) holds (( CutLastLoc F) . I) <> ( halt S)

    proof

      let F be unique-halt Program of S, I be Nat such that

       A1: I in ( dom ( CutLastLoc F)) and

       A2: (( CutLastLoc F) . I) = ( halt S);

      

       A3: ( dom ( CutLastLoc F)) c= ( dom F) by GRFUNC_1: 2;

      (F . I) = ( halt S) by A1, A2, GRFUNC_1: 2;

      then

       A4: I = ( LastLoc F) by A1, A3, Def7;

      ( dom ( CutLastLoc F)) = (( dom F) \ {( LastLoc F)}) by VALUED_1: 36;

      then not I in {( LastLoc F)} by A1, XBOOLE_0:def 5;

      hence thesis by A4, TARSKI:def 1;

    end;

    definition

      let S be COM-Struct;

      let F,G be non empty preProgram of S;

      :: COMPOS_1:def23

      func F ';' G -> preProgram of S equals (( CutLastLoc F) +* ( Reloc (G,(( card F) -' 1))));

      coherence ;

    end

    registration

      let S be COM-Struct, F,G be non empty preProgram of S;

      cluster (F ';' G) -> non emptythe InstructionsF of S -valued NAT -defined;

      coherence ;

    end

    theorem :: COMPOS_1:20

    

     Th11: for S be COM-Struct, F be Program of S, G be non empty preProgram of S holds ( card (F ';' G)) = ((( card F) + ( card G)) - 1) & ( card (F ';' G)) = ((( card F) + ( card G)) -' 1)

    proof

      let S be COM-Struct, F be Program of S, G be non empty preProgram of S;

      set k = (( card F) -' 1);

      (( dom ( IncAddr (G,k))),( dom ( Reloc (G,k)))) are_equipotent by VALUED_1: 27;

      then

       A1: (( IncAddr (G,k)),( Reloc (G,k))) are_equipotent by PRE_CIRC: 21;

      ( dom ( CutLastLoc F)) misses ( dom ( Reloc (G,k))) by Th9;

      

      hence ( card (F ';' G)) = (( card ( CutLastLoc F)) + ( card ( Reloc (G,k)))) by PRE_CIRC: 22

      .= (( card ( CutLastLoc F)) + ( card ( IncAddr (G,k)))) by A1, CARD_1: 5

      .= (( card ( CutLastLoc F)) + ( card ( dom ( IncAddr (G,k))))) by CARD_1: 62

      .= (( card ( CutLastLoc F)) + ( card ( dom G))) by Def9

      .= (( card ( CutLastLoc F)) + ( card G)) by CARD_1: 62

      .= ((( card F) - 1) + ( card G)) by VALUED_1: 38

      .= ((( card F) + ( card G)) - 1);

      hence thesis by XREAL_0:def 2;

    end;

    registration

      let S be COM-Struct;

      let F,G be Program of S;

      cluster (F ';' G) -> initial;

      coherence

      proof

        set P = (F ';' G);

        let f,n be Nat such that

         A1: n in ( dom P) and

         A2: f < n;

        set k = (( card F) -' 1);

        

         A3: ( dom P) = (( dom ( CutLastLoc F)) \/ ( dom ( Reloc (G,k)))) by FUNCT_4:def 1;

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

          suppose n in ( dom ( CutLastLoc F));

          then f in ( dom ( CutLastLoc F)) by A2, AFINSQ_1:def 12;

          hence thesis by A3, XBOOLE_0:def 3;

        end;

          suppose n in ( dom ( Reloc (G,k)));

          then n in { (w + k) where w be Nat : w in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

          then

          consider m be Nat such that

           A4: n = (m + k) and

           A5: m in ( dom ( IncAddr (G,k)));

          

           A6: m in ( dom G) by A5, Def9;

          now

            per cases ;

              case

               A7: f < k;

              then f < (( card F) - 1) by PRE_CIRC: 20;

              then (1 + f) < (1 + (( card F) - 1)) by XREAL_1: 6;

              then

               A8: (1 + f) in ( dom F) by AFINSQ_1: 66;

              f < (1 + f) by NAT_1: 19;

              then

               A9: f in ( dom F) by A8, AFINSQ_1:def 12;

              f <> ( LastLoc F) by A7, AFINSQ_1: 70;

              then not f in {( LastLoc F)} by TARSKI:def 1;

              then f in (( dom F) \ {( LastLoc F)}) by A9, XBOOLE_0:def 5;

              hence f in ( dom ( CutLastLoc F)) by VALUED_1: 36;

            end;

              case f >= k;

              then

              consider l1 be Nat such that

               A10: f = (k + l1) by NAT_1: 10;

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

              

               A11: ( dom ( Reloc (G,k))) = { (w + k) where w be Nat : w in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

              l1 < m or l1 = m by A10, A4, A2, XREAL_1: 6;

              then l1 in ( dom G) by A6, AFINSQ_1:def 12;

              then l1 in ( dom ( IncAddr (G,k))) by Def9;

              hence f in ( dom ( Reloc (G,k))) by A11, A10;

            end;

          end;

          hence thesis by A3, XBOOLE_0:def 3;

        end;

      end;

    end

    theorem :: COMPOS_1:21

    for S be COM-Struct, F,G be Program of S holds ( dom F) c= ( dom (F ';' G))

    proof

      let S be COM-Struct, F,G be Program of S;

      set P = (F ';' G);

      

       A1: ( dom P) = (( dom ( CutLastLoc F)) \/ ( dom ( Reloc (G,(( card F) -' 1))))) by FUNCT_4:def 1;

      

       A2: ( dom F) = (( dom ( CutLastLoc F)) \/ {( LastLoc F)}) by VALUED_1: 37;

      let x be object;

      assume

       A3: x in ( dom F);

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

        suppose x in ( dom ( CutLastLoc F));

        hence thesis by A1, XBOOLE_0:def 3;

      end;

        suppose

         A4: x in {( LastLoc F)};

        then

         A5: x = ( LastLoc F) by TARSKI:def 1;

        reconsider f = x as Element of NAT by A4;

        

         A6: f = (( card F) -' 1) by A5, AFINSQ_1: 70

        .= ((( card F) - 1) + 0 qua Nat) by PRE_CIRC: 20;

        ( card P) = ((( card F) + ( card G)) - 1) by Th11

        .= ((( card F) - 1) + ( card G));

        then f < ( card P) by A6, XREAL_1: 6;

        hence thesis by AFINSQ_1: 66;

      end;

    end;

    registration

      let S be COM-Struct, F,G be Program of S;

      cluster (F ';' G) -> initial non empty;

      coherence ;

    end

    theorem :: COMPOS_1:22

    

     Th13: for S be COM-Struct, F,G be Program of S holds ( CutLastLoc F) c= ( CutLastLoc (F ';' G))

    proof

      let S be COM-Struct, F,G be Program of S;

      set k = (( card F) -' 1);

      set P = (F ';' G);

      

       A1: ( dom P) = (( dom ( CutLastLoc F)) \/ ( dom ( Reloc (G,k)))) by FUNCT_4:def 1;

      

       A2: ( dom ( CutLastLoc F)) = { m where m be Element of NAT : m < ( card ( CutLastLoc F)) } by AFINSQ_1: 68;

      

       A3: ( card ( CutLastLoc P)) = (( card P) - 1) by VALUED_1: 38

      .= (((( card F) + ( card G)) - 1) - 1) by Th11

      .= ((( card F) - 1) + (( card G) - 1));

      

       A4: for m be Element of NAT st m < ( card ( CutLastLoc F)) holds m < ( card ( CutLastLoc P))

      proof

        let m be Element of NAT such that

         A5: m < ( card ( CutLastLoc F));

        

         A6: ( card ( CutLastLoc F)) = (( card F) - 1) by VALUED_1: 38;

        1 <= ( card G) by NAT_1: 14;

        then (1 - 1) <= (( card G) - 1) by XREAL_1: 9;

        then ((( card F) - 1) + 0 qua Nat) <= ((( card F) - 1) + (( card G) - 1)) by XREAL_1: 6;

        hence thesis by A3, A5, A6, XXREAL_0: 2;

      end;

      

       A7: ( dom ( CutLastLoc F)) c= ( dom ( CutLastLoc P))

      proof

        let x be object;

        assume x in ( dom ( CutLastLoc F));

        then

        consider m be Element of NAT such that

         A8: x = m and

         A9: m < ( card ( CutLastLoc F)) by A2;

        m < ( card ( CutLastLoc P)) by A4, A9;

        hence thesis by A8, AFINSQ_1: 66;

      end;

      for x be object st x in ( dom ( CutLastLoc F)) holds (( CutLastLoc F) . x) = (( CutLastLoc P) . x)

      proof

        let x be object;

        assume

         A10: x in ( dom ( CutLastLoc F));

        then

        consider m be Element of NAT such that

         A11: x = m and

         A12: m < ( card ( CutLastLoc F)) by A2;

        

         A13: ( dom ( Reloc (G,k))) = { (w + k) where w be Nat : w in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

         A14:

        now

          assume x in ( dom ( Reloc (G,k)));

          then

          consider w be Nat such that

           A15: x = (w + k) and w in ( dom ( IncAddr (G,k))) by A13;

          m < (( card F) - 1) by A12, VALUED_1: 38;

          then m < k by PRE_CIRC: 20;

          hence contradiction by A11, A15, NAT_1: 11;

        end;

        

         A16: x in ( dom P) by A1, A10, XBOOLE_0:def 3;

        now

          assume x = ( LastLoc P);

          

          then

           A17: m = (( card P) -' 1) by A11, AFINSQ_1: 70

          .= (( card P) - 1) by PRE_CIRC: 20;

          ( card ( CutLastLoc P)) = (( card P) - 1) by VALUED_1: 38;

          hence contradiction by A4, A12, A17;

        end;

        then not x in {( LastLoc P)} by TARSKI:def 1;

        then not x in ( dom (( LastLoc P) .--> (P . ( LastLoc P))));

        then x in (( dom P) \ ( dom (( LastLoc P) .--> (P . ( LastLoc P))))) by A16, XBOOLE_0:def 5;

        

        hence (( CutLastLoc P) . x) = ((( CutLastLoc F) +* ( Reloc (G,k))) . x) by GRFUNC_1: 32

        .= (( CutLastLoc F) . x) by A14, FUNCT_4: 11;

      end;

      hence thesis by A7, GRFUNC_1: 2;

    end;

    theorem :: COMPOS_1:23

    

     Th14: for S be COM-Struct, F,G be Program of S holds ((F ';' G) . ( LastLoc F)) = (( IncAddr (G,(( card F) -' 1))) . 0 )

    proof

      let S be COM-Struct, F,G be Program of S;

      set k = (( card F) -' 1);

      

       A1: ( LastLoc F) = ( 0 qua Nat + k) by AFINSQ_1: 70;

      

       A2: 0 in ( dom ( IncAddr (G,k))) by AFINSQ_1: 65;

      ( dom ( Reloc (G,k))) = { (m + k) where m be Nat : m in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

      then ( LastLoc F) in ( dom ( Reloc (G,k))) by A1, A2;

      

      hence ((F ';' G) . ( LastLoc F)) = (( Reloc (G,k)) . ( LastLoc F)) by FUNCT_4: 13

      .= (( IncAddr (G,k)) . 0 ) by A1, A2, VALUED_1:def 12;

    end;

    

     Lm6: for S be COM-Struct, F,G be Program of S, f be Nat st f < (( card F) - 1) holds (F . f) = ((F ';' G) . f)

    proof

      let S be COM-Struct, F,G be Program of S, f be Nat;

      set k = (( card F) -' 1), P = (F ';' G);

      assume f < (( card F) - 1);

      then f < ( card ( CutLastLoc F)) by VALUED_1: 38;

      then

       A1: f in ( dom ( CutLastLoc F)) by AFINSQ_1: 66;

      ( dom ( CutLastLoc F)) misses ( dom ( Reloc (G,k))) by Th9;

      then (( dom ( CutLastLoc F)) /\ ( dom ( Reloc (G,k)))) = {} ;

      then not f in ( dom ( Reloc (G,k))) by A1, XBOOLE_0:def 4;

      

      hence (P . f) = (( CutLastLoc F) . f) by FUNCT_4: 11

      .= (F . f) by A1, GRFUNC_1: 2;

    end;

    theorem :: COMPOS_1:24

    for S be COM-Struct, F,G be Program of S, f be Nat st f < (( card F) - 1) holds (( IncAddr (F,(( card F) -' 1))) . f) = (( IncAddr ((F ';' G),(( card F) -' 1))) . f)

    proof

      let S be COM-Struct, F,G be Program of S, f be Nat;

      set k = (( card F) -' 1), P = (F ';' G);

      assume

       A1: f < (( card F) - 1);

      then f < ( card ( CutLastLoc F)) by VALUED_1: 38;

      then

       A2: f in ( dom ( CutLastLoc F)) by AFINSQ_1: 66;

      

       A3: ( dom ( CutLastLoc F)) c= ( dom F) by GRFUNC_1: 2;

      ( CutLastLoc F) c= ( CutLastLoc P) by Th13;

      then ( CutLastLoc F) c= P by XBOOLE_1: 1;

      then

       A4: ( dom ( CutLastLoc F)) c= ( dom P) by GRFUNC_1: 2;

      

       A5: (F . f) = (F /. f) by A2, A3, PARTFUN1:def 6;

      

       A6: (P . f) = (F . f) by Lm6, A1;

      

      thus (( IncAddr (F,k)) . f) = ( IncAddr ((F /. f),k)) by A2, A3, Def9

      .= ( IncAddr ((P /. f),k)) by A2, A4, A5, A6, PARTFUN1:def 6

      .= (( IncAddr (P,k)) . f) by A2, A4, Def9;

    end;

    registration

      let S be COM-Struct;

      let F be Program of S;

      let G be halt-ending Program of S;

      cluster (F ';' G) -> halt-ending;

      coherence

      proof

        set P = (F ';' G), k = (( card F) -' 1);

        

         A1: ( dom ( Reloc (G,k))) = { (m + k) where m be Nat : m in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

        

         A2: (( card G) -' 1) = ( LastLoc G) by AFINSQ_1: 70;

        then

         A3: (( card G) -' 1) in ( dom G) by VALUED_1: 30;

        then

         A4: (( card G) -' 1) in ( dom ( IncAddr (G,k))) by Def9;

        then

         A5: (k + (( card G) -' 1)) in ( dom ( Reloc (G,k))) by A1;

        

         A6: (G /. (( card G) -' 1)) = (G . (( card G) -' 1)) by A2, PARTFUN1:def 6, VALUED_1: 30

        .= ( halt S) by A2, Def6;

        

         A7: (( card G) - 1) >= 0 by NAT_1: 14, XREAL_1: 48;

        then (k + (( card G) - 1)) >= (k + 0 qua Nat) by XREAL_1: 6;

        

        then

         A8: ((k + ( card G)) -' 1) = ((k + ( card G)) - 1) by XREAL_0:def 2

        .= (k + (( card G) - 1))

        .= (k + (( card G) -' 1)) by A7, XREAL_0:def 2;

        

        thus (P . ( LastLoc P)) = (P . (( card P) -' 1)) by AFINSQ_1: 70

        .= (P . (((( card F) + ( card G)) -' 1) -' 1)) by Th11

        .= (P . ((k + ( card G)) -' 1)) by NAT_1: 14, NAT_D: 38

        .= (( Reloc (G,k)) . (k + (( card G) -' 1))) by A5, A8, FUNCT_4: 13

        .= (( IncAddr (G,k)) . (( card G) -' 1)) by A4, VALUED_1:def 12

        .= ( IncAddr ((G /. (( card G) -' 1)),k)) by A3, Def9

        .= ( halt S) by A6, COMPOS_0: 4;

      end;

    end

    registration

      let S be COM-Struct;

      let F be MacroInstruction of S;

      let G be unique-halt Program of S;

      cluster (F ';' G) -> unique-halt;

      coherence

      proof

        set P = (F ';' G), k = (( card F) -' 1);

        

         A1: ( dom P) = (( dom ( CutLastLoc F)) \/ ( dom ( Reloc (G,k)))) by FUNCT_4:def 1;

        

         A2: ( dom ( Reloc (G,k))) = { (m + k) where m be Nat : m in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

        

         A3: (( card G) - 1) >= 0 by NAT_1: 14, XREAL_1: 48;

        then (k + (( card G) - 1)) >= (k + 0 qua Nat) by XREAL_1: 6;

        

        then

         A4: ((k + ( card G)) -' 1) = ((k + ( card G)) - 1) by XREAL_0:def 2

        .= (k + (( card G) - 1))

        .= (k + (( card G) -' 1)) by A3, XREAL_0:def 2;

        let f be Nat such that

         A5: (P . f) = ( halt S) and

         A6: f in ( dom P);

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

          suppose

           A7: f in ( dom ( CutLastLoc F));

          then

           A8: (( CutLastLoc F) . f) <> ( halt S) by Th10;

          ( dom ( CutLastLoc F)) misses ( dom ( Reloc (G,k))) by Th9;

          then ( CutLastLoc F) c= P by FUNCT_4: 32;

          hence thesis by A5, A7, A8, GRFUNC_1: 2;

        end;

          suppose

           A9: f in ( dom ( Reloc (G,k)));

          then

          consider m be Nat such that

           A10: f = (m + k) and

           A11: m in ( dom ( IncAddr (G,k))) by A2;

          

           A12: m in ( dom G) by A11, Def9;

          then

           A13: (G /. m) = (G . m) by PARTFUN1:def 6;

          ( IncAddr ((G /. m),k)) = (( IncAddr (G,k)) . m) by A12, Def9

          .= (( Reloc (G,k)) . (m + k)) by A11, VALUED_1:def 12

          .= ( halt S) by A5, A9, A10, FUNCT_4: 13;

          then (G . m) = ( halt S) by A13, COMPOS_0: 12;

          

          then m = ( LastLoc G) by A12, Def7

          .= (( card G) -' 1) by AFINSQ_1: 70;

          

          then (m + k) = (((( card F) + ( card G)) -' 1) -' 1) by A4, NAT_1: 14, NAT_D: 38

          .= (( card P) -' 1) by Th11;

          hence thesis by A10, AFINSQ_1: 70;

        end;

      end;

    end

    definition

      let S be COM-Struct;

      let F,G be MacroInstruction of S;

      :: original: ';'

      redefine

      func F ';' G -> MacroInstruction of S ;

      coherence ;

    end

    registration

      let S be COM-Struct, k;

      reduce ( IncAddr (( Stop S),k)) to ( Stop S);

      reducibility

      proof

        

         A1: ( dom ( IncAddr (( Stop S),k))) = ( dom ( Stop S)) by Def9

        .= { 0 };

        

         A2: ( dom ( Stop S)) = { 0 };

        for x be object st x in { 0 } holds (( IncAddr (( Stop S),k)) . x) = (( Stop S) . x)

        proof

          let x be object;

          assume

           A3: x in { 0 };

          then

           A4: x = 0 by TARSKI:def 1;

          

          then

           A5: (( Stop S) /. 0 ) = (( Stop S) . 0 ) by A2, A3, PARTFUN1:def 6

          .= ( halt S);

          

          thus (( IncAddr (( Stop S),k)) . x) = ( IncAddr ((( Stop S) /. 0 ),k)) by A2, A3, A4, Def9

          .= ( halt S) by A5, COMPOS_0: 4

          .= (( Stop S) . x) by A4;

        end;

        hence thesis by A1, A2, FUNCT_1: 2;

      end;

    end

    ::$Canceled

    theorem :: COMPOS_1:26

    

     Th16: for k be Nat holds for S be COM-Struct holds ( Shift (( Stop S),k)) = (k .--> ( halt S))

    proof

      let k be Nat;

      let S be COM-Struct;

      

       A1: ( dom ( Shift (( Stop S),k))) = { (m + k) where m be Nat : m in ( dom ( Stop S)) } by VALUED_1:def 12;

      

       A2: 0 in ( dom ( Stop S)) by TARSKI:def 1;

      

       A3: ( dom ( Shift (( Stop S),k))) = {k}

      proof

        hereby

          let x be object;

          assume x in ( dom ( Shift (( Stop S),k)));

          then

          consider m be Nat such that

           A4: x = (m + k) and

           A5: m in ( dom ( Stop S)) by A1;

          m in { 0 } by A5;

          then m = 0 by TARSKI:def 1;

          hence x in {k} by A4, TARSKI:def 1;

        end;

        let x be object;

        assume x in {k};

        then x = ( 0 qua Nat + k) by TARSKI:def 1;

        hence thesis by A1, A2;

      end;

      

       A6: ( dom (k .--> ( halt S))) = {k};

      for x be object st x in {k} holds (( Shift (( Stop S),k)) . x) = ((k .--> ( halt S)) . x)

      proof

        let x be object;

        assume x in {k};

        then

         A7: x = ( 0 qua Nat + k) by TARSKI:def 1;

         0 in ( dom ( Stop S)) by TARSKI:def 1;

        

        hence (( Shift (( Stop S),k)) . x) = (( Stop S) . 0 ) by A7, VALUED_1:def 12

        .= ( halt S)

        .= ((k .--> ( halt S)) . x) by A7, FUNCOP_1: 72;

      end;

      hence thesis by A3, A6, FUNCT_1: 2;

    end;

    registration

      let S be COM-Struct, F be MacroInstruction of S;

      reduce (F ';' ( Stop S)) to F;

      reducibility

      proof

        set k = (( card F) -' 1);

        

         A1: ( dom F) = (( dom ( CutLastLoc F)) \/ {( LastLoc F)}) by VALUED_1: 37;

        ( dom ( Shift (( Stop S),k))) = ( dom (k .--> ( halt S))) by Th16

        .= {k}

        .= {( LastLoc F)} by AFINSQ_1: 70;

        then

         A2: ( dom (F ';' ( Stop S))) = ( dom F) by A1, FUNCT_4:def 1;

        for x be object st x in ( dom F) holds ((F ';' ( Stop S)) . x) = (F . x)

        proof

          let x be object such that

           A3: x in ( dom F);

          ( dom ( CutLastLoc F)) misses ( dom ( Reloc (( Stop S),k))) by Th9;

          then

           A4: {} = (( dom ( CutLastLoc F)) /\ ( dom ( Reloc (( Stop S),k))));

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

            suppose

             A5: x in ( dom ( CutLastLoc F));

            then not x in ( dom ( Reloc (( Stop S),k))) by A4, XBOOLE_0:def 4;

            

            hence ((F ';' ( Stop S)) . x) = (( CutLastLoc F) . x) by FUNCT_4: 11

            .= (F . x) by A5, GRFUNC_1: 2;

          end;

            suppose x in {( LastLoc F)};

            then

             A6: x = ( LastLoc F) by TARSKI:def 1;

            then

             A7: x = k by AFINSQ_1: 70;

            

             A8: 0 in ( dom ( Stop S)) by TARSKI:def 1;

            ( dom ( Shift (( Stop S),k))) = { (m + k) where m be Nat : m in ( dom ( Stop S)) } by VALUED_1:def 12;

            then ( 0 qua Nat + k) in ( dom ( Shift (( Stop S),k))) by A8;

            

            hence ((F ';' ( Stop S)) . x) = (( Shift (( Stop S),( 0 qua Nat + k))) . x) by A7, FUNCT_4: 13

            .= (( Stop S) . 0 ) by A7, A8, VALUED_1:def 12

            .= ( halt S)

            .= (F . x) by A6, Def6;

          end;

        end;

        hence thesis by A2, FUNCT_1: 2;

      end;

    end

    theorem :: COMPOS_1:27

    for S be COM-Struct, F be MacroInstruction of S holds (F ';' ( Stop S)) = F;

    registration

      let S be COM-Struct, F be MacroInstruction of S;

      reduce (( Stop S) ';' F) to F;

      reducibility

      proof

        (( card ( Stop S)) -' 1) = 0 by Lm2;

        

        hence (( Stop S) ';' F) = ( {} +* ( Reloc (F, 0 )))

        .= ( Reloc (F, 0 ))

        .= F;

      end;

    end

    theorem :: COMPOS_1:28

    for S be COM-Struct, F be MacroInstruction of S holds (( Stop S) ';' F) = F;

    theorem :: COMPOS_1:29

    for S be COM-Struct, F,G,H be MacroInstruction of S holds ((F ';' G) ';' H) = (F ';' (G ';' H))

    proof

      let S be COM-Struct, F,G,H be MacroInstruction of S;

      per cases ;

        suppose

         A1: F = ( Stop S);

        

        hence ((F ';' G) ';' H) = ((( Stop S) ';' G) ';' H)

        .= (F ';' (G ';' H)) by A1;

      end;

        suppose

         A2: G = ( Stop S);

        

        hence ((F ';' G) ';' H) = ((F ';' ( Stop S)) ';' H)

        .= (F ';' (G ';' H)) by A2;

      end;

        suppose that

         A3: F <> ( Stop S) and

         A4: G <> ( Stop S);

        set X = { k where k be Element of NAT : k < ((((( card F) + ( card G)) + ( card H)) - 1) - 1) };

        

         A5: ( card ((F ';' G) ';' H)) = ((( card (F ';' G)) + ( card H)) - 1) by Th11

        .= ((((( card F) + ( card G)) - 1) + ( card H)) - 1) by Th11

        .= ((((( card F) + ( card G)) + ( card H)) - 1) - 1);

        

         A6: ( card (F ';' (G ';' H))) = ((( card F) + ( card (G ';' H))) - 1) by Th11

        .= ((( card F) + ((( card G) + ( card H)) - 1)) - 1) by Th11

        .= ((((( card F) + ( card G)) + ( card H)) - 1) - 1);

        

         A7: ( dom ((F ';' G) ';' H)) = X by A5, AFINSQ_1: 68;

        

         A8: ( dom (F ';' (G ';' H))) = X by A6, AFINSQ_1: 68;

        for x be object st x in X holds (((F ';' G) ';' H) . x) = ((F ';' (G ';' H)) . x)

        proof

          let x be object;

          assume x in X;

          then

          consider k be Element of NAT such that

           A9: x = k and

           A10: k < ((((( card F) + ( card G)) + ( card H)) - 1) - 1);

          

           A11: ( dom ( Reloc ((G ';' H),(( card F) -' 1)))) = { (m + (( card F) -' 1)) where m be Nat : m in ( dom ( IncAddr ((G ';' H),(( card F) -' 1)))) } by VALUED_1:def 12;

          

           A12: ( dom ( Reloc (H,(( card (F ';' G)) -' 1)))) = { (m + (( card (F ';' G)) -' 1)) where m be Nat : m in ( dom ( IncAddr (H,(( card (F ';' G)) -' 1)))) } by VALUED_1:def 12;

          

           A13: ( dom ( Reloc (H,(( card G) -' 1)))) = { (m + (( card G) -' 1)) where m be Nat : m in ( dom ( IncAddr (H,(( card G) -' 1)))) } by VALUED_1:def 12;

          

           A14: (( card (F ';' G)) -' 1) = (( card (F ';' G)) - 1) by PRE_CIRC: 20

          .= (((( card F) + ( card G)) - 1) - 1) by Th11;

          then (( card (F ';' G)) -' 1) = ((( card F) - 1) + (( card G) - 1));

          

          then

           A15: (( card (F ';' G)) -' 1) = ((( card G) -' 1) + (( card F) - 1)) by PRE_CIRC: 20

          .= ((( card G) -' 1) + (( card F) -' 1)) by PRE_CIRC: 20;

          

           A16: ( dom ( Reloc (G,(( card F) -' 1)))) = { (m + (( card F) -' 1)) where m be Nat : m in ( dom ( IncAddr (G,(( card F) -' 1)))) } by VALUED_1:def 12;

          

           A17: (( card F) -' 1) = (( card F) - 1) by PRE_CIRC: 20;

          

           A18: (( card G) -' 1) = (( card G) - 1) by PRE_CIRC: 20;

          

           A19: for W be MacroInstruction of S st W <> ( Stop S) holds 2 <= ( card W)

          proof

            let W be MacroInstruction of S;

            assume

             A20: W <> ( Stop S);

            assume 2 > ( card W);

            then (1 + 1) > ( card W);

            then ( card W) <= 1 by NAT_1: 13;

            hence contradiction by A20, Th6, NAT_1: 25;

          end;

          then 2 <= ( card F) by A3;

          then

           A21: 1 <= ( card F) by XXREAL_0: 2;

          

           A22: 2 <= ( card G) by A4, A19;

          per cases by A21, A22, Lm5;

            suppose

             A23: k < (( card F) - 1);

            

             A24: ( CutLastLoc F) c= ( CutLastLoc (F ';' G)) by Th13;

             A25:

            now

              assume x in ( dom ( Reloc ((G ';' H),(( card F) -' 1))));

              then

              consider m be Nat such that

               A26: x = (m + (( card F) -' 1)) and m in ( dom ( IncAddr ((G ';' H),(( card F) -' 1)))) by A11;

              k = (m + (( card F) - 1)) by A9, A26, PRE_CIRC: 20;

              then (m + (( card F) - 1)) < (( card F) -' 1) by A23, PRE_CIRC: 20;

              then (m + (( card F) -' 1)) < (( card F) -' 1) by PRE_CIRC: 20;

              hence contradiction by NAT_1: 11;

            end;

             A27:

            now

              assume x in ( dom ( Reloc (H,(( card (F ';' G)) -' 1))));

              then

              consider m be Nat such that

               A28: x = (m + (( card (F ';' G)) -' 1)) and m in ( dom ( IncAddr (H,(( card (F ';' G)) -' 1)))) by A12;

              ((m + (( card G) -' 1)) + (( card F) -' 1)) < (( card F) -' 1) by A23, A9, A15, A28, PRE_CIRC: 20;

              hence contradiction by NAT_1: 11;

            end;

            k < ( card ( CutLastLoc F)) by A23, VALUED_1: 38;

            then

             A29: x in ( dom ( CutLastLoc F)) by A9, AFINSQ_1: 66;

            

            thus (((F ';' G) ';' H) . x) = (( CutLastLoc (F ';' G)) . x) by A27, FUNCT_4: 11

            .= (( CutLastLoc F) . x) by A24, A29, GRFUNC_1: 2

            .= ((F ';' (G ';' H)) . x) by A25, FUNCT_4: 11;

          end;

            suppose

             A30: k = (( card F) - 1);

             A31:

            now

              assume x in ( dom ( Reloc (H,(( card (F ';' G)) -' 1))));

              then

              consider m be Nat such that

               A32: x = (m + (( card (F ';' G)) -' 1)) and m in ( dom ( IncAddr (H,(( card (F ';' G)) -' 1)))) by A12;

              ((m + (( card G) -' 1)) + (( card F) -' 1)) = (( card F) -' 1) by A30, A15, A32, A9, PRE_CIRC: 20;

              then (( card G) -' 1) = 0 ;

              then (( card G) - 1) = 0 by PRE_CIRC: 20;

              hence contradiction by A4, Th6;

            end;

            

             A33: 0 in ( dom ( IncAddr ((G ';' H),(( card F) -' 1)))) by AFINSQ_1: 65;

            

             A34: 0 in ( dom ( IncAddr (G,(( card F) -' 1)))) by AFINSQ_1: 65;

            

             A35: 0 in ( dom G) by AFINSQ_1: 65;

            

             A36: 0 in ( dom (G ';' H)) by AFINSQ_1: 65;

            k = ( 0 qua Nat + (( card F) -' 1)) by A30, PRE_CIRC: 20;

            then

             A37: x in ( dom ( Reloc ((G ';' H),(( card F) -' 1)))) by A9, A11, A33;

            

             A38: k = (( card F) -' 1) by A30, PRE_CIRC: 20;

            

             A39: x = ( 0 qua Nat + k) by A9;

             0 in ( dom ( IncAddr (G,(( card F) -' 1)))) by AFINSQ_1: 65;

            then

             A40: x in ( dom ( Reloc (G,(( card F) -' 1)))) by A16, A38, A39;

            then x in (( dom ( CutLastLoc F)) \/ ( dom ( Reloc (G,(( card F) -' 1))))) by XBOOLE_0:def 3;

            then

             A41: x in ( dom (F ';' G)) by FUNCT_4:def 1;

            now

              

               A42: ( dom (( LastLoc (F ';' G)) .--> ((F ';' G) . ( LastLoc (F ';' G))))) = {( LastLoc (F ';' G))}

              .= {(( card (F ';' G)) -' 1)} by AFINSQ_1: 70;

              assume x in ( dom (( LastLoc (F ';' G)) .--> ((F ';' G) . ( LastLoc (F ';' G)))));

              then x = (( card (F ';' G)) -' 1) by A42, TARSKI:def 1;

              then (( card G) - 1) = 0 by A38, A9, A15, PRE_CIRC: 20;

              hence contradiction by A4, Th6;

            end;

            then

             A43: x in (( dom (F ';' G)) \ ( dom (( LastLoc (F ';' G)) .--> ((F ';' G) . ( LastLoc (F ';' G)))))) by A41, XBOOLE_0:def 5;

            1 <= ( card G) by NAT_1: 14;

            then ( card G) > 1 by A4, Th6, XXREAL_0: 1;

            then

             A44: (( card G) - 1) > (1 - 1) by XREAL_1: 9;

            then (( card G) -' 1) > (1 - 1) by PRE_CIRC: 20;

            then

             A45: not 0 in ( dom ( Reloc (H,(( card G) -' 1)))) by VALUED_1: 29;

            ( card ( CutLastLoc G)) <> {} by A44, VALUED_1: 38;

            then

             A46: 0 in ( dom ( CutLastLoc G)) by AFINSQ_1: 65, CARD_1: 27;

            

             A47: (G /. 0 ) = (G . 0 ) by A35, PARTFUN1:def 6

            .= (( CutLastLoc G) . 0 ) by A46, GRFUNC_1: 2

            .= ((G ';' H) . 0 ) by A45, FUNCT_4: 11

            .= ((G ';' H) /. 0 ) by A36, PARTFUN1:def 6;

            

            thus (((F ';' G) ';' H) . x) = (((F ';' G) \ (( LastLoc (F ';' G)) .--> ((F ';' G) . ( LastLoc (F ';' G))))) . x) by A31, FUNCT_4: 11

            .= ((( CutLastLoc F) +* ( Reloc (G,(( card F) -' 1)))) . x) by A43, GRFUNC_1: 32

            .= (( Reloc (G,(( card F) -' 1))) . x) by A40, FUNCT_4: 13

            .= (( IncAddr (G,(( card F) -' 1))) . 0 ) by A34, A38, A39, VALUED_1:def 12

            .= ( IncAddr (((G ';' H) /. 0 ),(( card F) -' 1))) by A35, A47, Def9

            .= (( IncAddr ((G ';' H),(( card F) -' 1))) . 0 ) by A36, Def9

            .= (( Reloc ((G ';' H),(( card F) -' 1))) . x) by A33, A38, A39, VALUED_1:def 12

            .= ((F ';' (G ';' H)) . x) by A37, FUNCT_4: 13;

          end;

            suppose that

             A48: ( card F) <= k and

             A49: k <= ((( card F) + ( card G)) - 3);

             A50:

            now

              assume x in ( dom ( Reloc (H,(( card (F ';' G)) -' 1))));

              then

              consider m be Nat such that

               A51: x = (m + (( card (F ';' G)) -' 1)) and m in ( dom ( IncAddr (H,(( card (F ';' G)) -' 1)))) by A12;

              (m + ((( card G) -' 1) + (( card F) -' 1))) <= (( - 1) + ((( card G) -' 1) + (( card F) -' 1))) by A9, A15, A17, A18, A49, A51;

              hence contradiction by XREAL_1: 6;

            end;

            (( card F) -' 1) <= ( card F) by NAT_D: 35;

            then

             A52: x = ((k -' (( card F) -' 1)) + (( card F) -' 1)) by A9, A48, XREAL_1: 235, XXREAL_0: 2;

            

             A53: (( card F) - ( card F)) <= (k - ( card F)) by A48, XREAL_1: 9;

            (( card F) - 1) < (( card F) - 0 ) by XREAL_1: 15;

            then (k - (( card F) - 1)) >= 0 by A53, XREAL_1: 15;

            then

             A54: (k - (( card F) -' 1)) >= 0 by PRE_CIRC: 20;

            

             A55: ((( card F) + ( card G)) - 3) < (((( card F) + ( card G)) - 3) + 1) by XREAL_1: 29;

            then

             A56: k < ((( card G) - 1) + (( card F) - 1)) by A49, XXREAL_0: 2;

            ((k - (( card F) - 1)) + (( card F) - 1)) < ((( card G) - 1) + (( card F) - 1)) by A49, A55, XXREAL_0: 2;

            then (k - (( card F) - 1)) < (( card G) - 1) by XREAL_1: 7;

            then (k - (( card F) -' 1)) < (( card G) - 1) by PRE_CIRC: 20;

            then (k -' (( card F) -' 1)) < (( card G) - 1) by A54, XREAL_0:def 2;

            then (k -' (( card F) -' 1)) < ( card ( CutLastLoc G)) by VALUED_1: 38;

            then

             A57: (k -' (( card F) -' 1)) in ( dom ( CutLastLoc G)) by AFINSQ_1: 66;

            then (k -' (( card F) -' 1)) in (( dom ( CutLastLoc G)) \/ ( dom ( Reloc (H,(( card G) -' 1))))) by XBOOLE_0:def 3;

            then

             A58: (k -' (( card F) -' 1)) in ( dom (G ';' H)) by FUNCT_4:def 1;

            then

             A59: (k -' (( card F) -' 1)) in ( dom ( IncAddr ((G ';' H),(( card F) -' 1)))) by Def9;

            then

             A60: x in ( dom ( Reloc ((G ';' H),(( card F) -' 1)))) by A11, A52;

            ((( card G) + ( card F)) - 2) < ((( card F) + ( card G)) - 1) by XREAL_1: 15;

            then k < ((( card F) + ( card G)) - 1) by A56, XXREAL_0: 2;

            then k < ( card (F ';' G)) by Th11;

            then

             A61: x in ( dom (F ';' G)) by A9, AFINSQ_1: 66;

            now

              assume x in ( dom (( LastLoc (F ';' G)) .--> ((F ';' G) . ( LastLoc (F ';' G)))));

              then x in {( LastLoc (F ';' G))};

              

              then x = ( LastLoc (F ';' G)) by TARSKI:def 1

              .= (( card (F ';' G)) -' 1) by AFINSQ_1: 70;

              then k = ((( card G) - 1) + (( card F) - 1)) by A9, A15, A18, PRE_CIRC: 20;

              hence contradiction by A49, A55;

            end;

            then

             A62: x in (( dom (F ';' G)) \ ( dom (( LastLoc (F ';' G)) .--> ((F ';' G) . ( LastLoc (F ';' G)))))) by A61, XBOOLE_0:def 5;

            

             A63: ( dom ( CutLastLoc G)) c= ( dom G) by GRFUNC_1: 2;

            then (k -' (( card F) -' 1)) in ( dom G) by A57;

            then

             A64: (k -' (( card F) -' 1)) in ( dom ( IncAddr (G,(( card F) -' 1)))) by Def9;

            then

             A65: x in ( dom ( Reloc (G,(( card F) -' 1)))) by A16, A52;

             A66:

            now

              assume (k -' (( card F) -' 1)) in ( dom ( Reloc (H,(( card G) -' 1))));

              then

              consider m be Nat such that

               A67: (k -' (( card F) -' 1)) = (m + (( card G) -' 1)) and m in ( dom ( IncAddr (H,(( card G) -' 1)))) by A13;

              

               A68: m = ((k -' (( card F) -' 1)) - (( card G) -' 1)) by A67

              .= ((k - (( card F) -' 1)) - (( card G) -' 1)) by A54, XREAL_0:def 2

              .= ((k - (( card F) - 1)) - (( card G) -' 1)) by PRE_CIRC: 20

              .= ((k - (( card F) - 1)) - (( card G) - 1)) by PRE_CIRC: 20

              .= (k - ((( card F) + ( card G)) - 2));

              (k - ((( card F) + ( card G)) - 2)) <= (((( card F) + ( card G)) - 3) - ((( card F) + ( card G)) - 2)) by A49, XREAL_1: 9;

              hence contradiction by A68, Lm4;

            end;

            

             A69: ((G ';' H) /. (k -' (( card F) -' 1))) = ((( CutLastLoc G) +* ( Reloc (H,(( card G) -' 1)))) . (k -' (( card F) -' 1))) by A58, PARTFUN1:def 6

            .= (( CutLastLoc G) . (k -' (( card F) -' 1))) by A66, FUNCT_4: 11

            .= (G . (k -' (( card F) -' 1))) by A57, GRFUNC_1: 2;

            

            thus (((F ';' G) ';' H) . x) = (((F ';' G) \ (( LastLoc (F ';' G)) .--> ((F ';' G) . ( LastLoc (F ';' G))))) . x) by A50, FUNCT_4: 11

            .= ((( CutLastLoc F) +* ( Reloc (G,(( card F) -' 1)))) . x) by A62, GRFUNC_1: 32

            .= (( Reloc (G,(( card F) -' 1))) . x) by A65, FUNCT_4: 13

            .= (( IncAddr (G,(( card F) -' 1))) . (k -' (( card F) -' 1))) by A52, A64, VALUED_1:def 12

            .= ( IncAddr ((G /. (k -' (( card F) -' 1))),(( card F) -' 1))) by A57, A63, Def9

            .= ( IncAddr (((G ';' H) /. (k -' (( card F) -' 1))),(( card F) -' 1))) by A57, A63, A69, PARTFUN1:def 6

            .= (( IncAddr ((G ';' H),(( card F) -' 1))) . (k -' (( card F) -' 1))) by A58, Def9

            .= (( Reloc ((G ';' H),(( card F) -' 1))) . x) by A52, A59, VALUED_1:def 12

            .= ((F ';' (G ';' H)) . x) by A60, FUNCT_4: 13;

          end;

            suppose

             A70: k = ((( card F) + ( card G)) - 2);

            then

             A71: x = ((k -' (( card (F ';' G)) -' 1)) + (( card (F ';' G)) -' 1)) by A9, A14, XREAL_1: 235;

            (k - (( card (F ';' G)) -' 1)) = 0 by A14, A70;

            then

             A72: (k -' (( card (F ';' G)) -' 1)) = 0 by XREAL_0:def 2;

            then

             A73: (k -' (( card (F ';' G)) -' 1)) in ( dom ( IncAddr (H,(( card (F ';' G)) -' 1)))) by AFINSQ_1: 65;

            then

             A74: x in ( dom ( Reloc (H,(( card (F ';' G)) -' 1)))) by A12, A71;

            

             A75: x = ((( card G) -' 1) + (( card F) -' 1)) by A9, A17, A18, A70;

            ((( card G) - 1) + 0 qua Nat) < ((( card G) - 1) + ( card H)) by XREAL_1: 6;

            then (( card G) -' 1) < ((( card G) + ( card H)) - 1) by PRE_CIRC: 20;

            then (( card G) -' 1) < ( card (G ';' H)) by Th11;

            then

             A76: (( card G) -' 1) in ( dom (G ';' H)) by AFINSQ_1: 66;

            then

             A77: (( card G) -' 1) in ( dom ( IncAddr ((G ';' H),(( card F) -' 1)))) by Def9;

            then

             A78: x in ( dom ( Reloc ((G ';' H),(( card F) -' 1)))) by A11, A75;

            

             A79: 0 in ( dom H) by AFINSQ_1: 65;

            

             A80: ((G ';' H) /. (( card G) -' 1)) = ((G ';' H) . (( card G) -' 1)) by A76, PARTFUN1:def 6;

            

             A81: 0 in ( dom ( IncAddr (H,(( card G) -' 1)))) by AFINSQ_1: 65;

            

            then

             A82: (( IncAddr (H,(( card G) -' 1))) /. 0 ) = (( IncAddr (H,(( card G) -' 1))) . 0 ) by PARTFUN1:def 6

            .= ( IncAddr ((H /. 0 ),(( card G) -' 1))) by A79, Def9;

            ((G ';' H) /. (( card G) -' 1)) = ((G ';' H) . ( LastLoc G)) by A80, AFINSQ_1: 70

            .= (( IncAddr (H,(( card G) -' 1))) . 0 ) by Th14

            .= (( IncAddr (H,(( card G) -' 1))) /. 0 ) by A81, PARTFUN1:def 6;

            then

             A83: ( IncAddr (((G ';' H) /. (( card G) -' 1)),(( card F) -' 1))) = ( IncAddr ((H /. 0 ),(( card (F ';' G)) -' 1))) by A15, A82, COMPOS_0: 7;

            

            thus (((F ';' G) ';' H) . x) = (( Reloc (H,(( card (F ';' G)) -' 1))) . x) by A74, FUNCT_4: 13

            .= (( IncAddr (H,(( card (F ';' G)) -' 1))) . (k -' (( card (F ';' G)) -' 1))) by A71, A73, VALUED_1:def 12

            .= ( IncAddr ((H /. 0 ),(( card (F ';' G)) -' 1))) by A72, A79, Def9

            .= (( IncAddr ((G ';' H),(( card F) -' 1))) . (( card G) -' 1)) by A76, A83, Def9

            .= (( Reloc ((G ';' H),(( card F) -' 1))) . x) by A75, A77, VALUED_1:def 12

            .= ((F ';' (G ';' H)) . x) by A78, FUNCT_4: 13;

          end;

            suppose

             A84: ((( card F) + ( card G)) - 2) < k;

            then

             A85: x = ((k -' (( card (F ';' G)) -' 1)) + (( card (F ';' G)) -' 1)) by A9, A14, XREAL_1: 235;

            (k + 0 qua Nat) < (((( card F) + ( card G)) - (1 + 1)) + ( card H)) by A10;

            then (k - ((( card F) + ( card G)) - (1 + 1))) < (( card H) - 0 ) by XREAL_1: 21;

            then (k -' (( card (F ';' G)) -' 1)) < ( card H) by A14, XREAL_0:def 2;

            then

             A86: (k -' (( card (F ';' G)) -' 1)) in ( dom H) by AFINSQ_1: 66;

            then

             A87: (k -' (( card (F ';' G)) -' 1)) in ( dom ( IncAddr (H,(( card (F ';' G)) -' 1)))) by Def9;

            then

             A88: x in ( dom ( Reloc (H,(( card (F ';' G)) -' 1)))) by A12, A85;

            

             A89: (( card F) -' 1) <= ((( card G) -' 1) + (( card F) -' 1)) by NAT_1: 11;

            then

             A90: k >= (( card F) -' 1) by A14, A15, A84, XXREAL_0: 2;

            

             A91: x = ((k -' (( card F) -' 1)) + (( card F) -' 1)) by A9, A14, A15, A84, A89, XREAL_1: 235, XXREAL_0: 2;

            

             A92: (k - (( card F) -' 1)) >= 0 by A90, XREAL_1: 48;

            

             A93: (k - (( card F) -' 1)) < (((((( card F) + ( card G)) + ( card H)) - 1) - 1) - (( card F) -' 1)) by A10, XREAL_1: 9;

            then

             A94: (k -' (( card F) -' 1)) < ((((( card F) + ( card G)) + ( card H)) - ( card F)) - 1) by A17, A92, XREAL_0:def 2;

            (k -' (( card F) -' 1)) < ((((( card F) - ( card F)) + ( card G)) + ( card H)) - 1) by A17, A92, A93, XREAL_0:def 2;

            then (k -' (( card F) -' 1)) < ( card (G ';' H)) by Th11;

            then

             A95: (k -' (( card F) -' 1)) in ( dom (G ';' H)) by AFINSQ_1: 66;

            then (k -' (( card F) -' 1)) in ( dom ( IncAddr ((G ';' H),(( card F) -' 1)))) by Def9;

            then

             A96: x in ( dom ( Reloc ((G ';' H),(( card F) -' 1)))) by A11, A91;

            

             A97: (k -' (( card F) -' 1)) in ( dom ( IncAddr ((G ';' H),(( card F) -' 1)))) by A95, Def9;

            

             A98: (k - (( card F) -' 1)) >= ((( card (F ';' G)) -' 1) - (( card F) -' 1)) by A14, A84, XREAL_1: 9;

            then

             A99: (k -' (( card F) -' 1)) >= (((( card F) -' 1) + (( card G) -' 1)) - (( card F) -' 1)) by A14, A15, A84, A89, XREAL_1: 233, XXREAL_0: 2;

            

             A100: (k -' (( card F) -' 1)) >= (( card G) -' 1) by A14, A15, A84, A89, A98, XREAL_1: 233, XXREAL_0: 2;

            

             A101: (k -' (( card F) -' 1)) = (((k -' (( card F) -' 1)) -' (( card G) -' 1)) + (( card G) -' 1)) by A99, XREAL_1: 235;

            ((k -' (( card F) -' 1)) - (( card G) -' 1)) < (((( card G) + ( card H)) - 1) - (( card G) - 1)) by A18, A94, XREAL_1: 9;

            then ((k -' (( card F) -' 1)) -' (( card G) -' 1)) < ((( card H) + (( card G) - 1)) - (( card G) - 1)) by A100, XREAL_1: 233;

            then ((k -' (( card F) -' 1)) -' (( card G) -' 1)) in ( dom H) by AFINSQ_1: 66;

            then

             A102: ((k -' (( card F) -' 1)) -' (( card G) -' 1)) in ( dom ( IncAddr (H,(( card G) -' 1)))) by Def9;

            then

             A103: (k -' (( card F) -' 1)) in ( dom ( Reloc (H,(( card G) -' 1)))) by A13, A101;

            

             A104: ((k -' (( card F) -' 1)) -' (( card G) -' 1)) = ((k -' (( card F) -' 1)) - (( card G) -' 1)) by A99, XREAL_1: 233

            .= ((k - (( card F) -' 1)) - (( card G) -' 1)) by A14, A15, A84, A89, XREAL_1: 233, XXREAL_0: 2

            .= (k - ((( card F) -' 1) + (( card G) -' 1)))

            .= (k -' (( card (F ';' G)) -' 1)) by A14, A15, A84, XREAL_1: 233;

            

             A105: ((G ';' H) /. (k -' (( card F) -' 1))) = ((( CutLastLoc G) +* ( Reloc (H,(( card G) -' 1)))) . (k -' (( card F) -' 1))) by A95, PARTFUN1:def 6

            .= (( Reloc (H,(( card G) -' 1))) . (k -' (( card F) -' 1))) by A103, FUNCT_4: 13

            .= (( IncAddr (H,(( card G) -' 1))) . (k -' (( card (F ';' G)) -' 1))) by A101, A102, A104, VALUED_1:def 12

            .= ( IncAddr ((H /. (k -' (( card (F ';' G)) -' 1))),(( card G) -' 1))) by A86, Def9;

            

            thus (((F ';' G) ';' H) . x) = (( Reloc (H,(( card (F ';' G)) -' 1))) . x) by A88, FUNCT_4: 13

            .= (( IncAddr (H,(( card (F ';' G)) -' 1))) . (k -' (( card (F ';' G)) -' 1))) by A85, A87, VALUED_1:def 12

            .= ( IncAddr ((H /. (k -' (( card (F ';' G)) -' 1))),(( card (F ';' G)) -' 1))) by A86, Def9

            .= ( IncAddr (((G ';' H) /. (k -' (( card F) -' 1))),(( card F) -' 1))) by A15, A105, COMPOS_0: 7

            .= (( IncAddr ((G ';' H),(( card F) -' 1))) . (k -' (( card F) -' 1))) by A95, Def9

            .= (( Reloc ((G ';' H),(( card F) -' 1))) . x) by A91, A97, VALUED_1:def 12

            .= ((F ';' (G ';' H)) . x) by A96, FUNCT_4: 13;

          end;

        end;

        hence thesis by A7, A8, FUNCT_1: 2;

      end;

    end;

    ::$Canceled

    begin

    reserve i,j,k for Nat,

n for Nat,

l,il for Nat;

    theorem :: COMPOS_1:32

    

     Th20: for k be Nat holds for p be finite NAT -definedthe InstructionsF of S -valued Function holds ( dom ( Reloc (p,k))) = ( dom ( Shift (p,k)))

    proof

      let k be Nat;

      let p be finite NAT -definedthe InstructionsF of S -valued Function;

      

       A1: ( dom ( IncAddr (p,k))) = ( dom p) by Def9;

      

      thus ( dom ( Reloc (p,k))) = { (m + k) where m be Nat : m in ( dom p) } by A1, VALUED_1:def 12

      .= ( dom ( Shift (p,k))) by VALUED_1:def 12;

    end;

    theorem :: COMPOS_1:33

    

     Th21: for k be Nat holds for p be finite NAT -definedthe InstructionsF of S -valued Function holds ( dom ( Reloc (p,k))) = { (j + k) where j be Nat : j in ( dom p) }

    proof

      let k be Nat;

      let p be finite NAT -definedthe InstructionsF of S -valued Function;

      

      thus ( dom ( Reloc (p,k))) = ( dom ( Shift (p,k))) by Th20

      .= { (j + k) where j be Nat : j in ( dom p) } by VALUED_1:def 12;

    end;

    theorem :: COMPOS_1:34

    

     Th22: for i,j be Nat holds for p be NAT -definedthe InstructionsF of S -valued finite Function holds ( Shift (( IncAddr (p,i)),j)) = ( IncAddr (( Shift (p,j)),i))

    proof

      let i,j be Nat;

      let p be NAT -definedthe InstructionsF of S -valued finite Function;

      set f = ( Shift (( IncAddr (p,i)),j));

      set g = ( IncAddr (( Shift (p,j)),i));

      ( dom ( IncAddr (p,i))) = ( dom p) by Def9;

      

      then ( dom ( Shift (p,j))) = { (m + j) where m be Nat : m in ( dom ( IncAddr (p,i))) } by VALUED_1:def 12

      .= ( dom f) by VALUED_1:def 12;

      then

       A1: ( dom f) = ( dom g) by Def9;

      now

        let x be object;

        

         A2: ( dom f) c= NAT by RELAT_1:def 18;

        assume

         A3: x in ( dom f);

        then

        reconsider x9 = x as Element of NAT by A2;

        reconsider xx = x9 as Element of NAT ;

        x in { (m + j) where m be Nat : m in ( dom ( IncAddr (p,i))) } by A3, VALUED_1:def 12;

        then

        consider m be Nat such that

         A4: x = (m + j) and

         A5: m in ( dom ( IncAddr (p,i)));

        

         A6: m in ( dom p) by A5, Def9;

        ( dom ( Shift (p,j))) = { (mm + j) where mm be Nat : mm in ( dom p) } by VALUED_1:def 12;

        then

         A7: x9 in ( dom ( Shift (p,j))) by A4, A6;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        

         A8: (p /. mm) = (p . m) by A6, PARTFUN1:def 6

        .= (( Shift (p,j)) . (m + j)) by A6, VALUED_1:def 12

        .= (( Shift (p,j)) /. xx) by A4, A7, PARTFUN1:def 6;

        

        thus (f . x) = (( IncAddr (p,i)) . m) by A5, A4, VALUED_1:def 12

        .= ( IncAddr ((( Shift (p,j)) /. xx),i)) by A6, A8, Def9

        .= (g . x) by A7, Def9;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: COMPOS_1:35

    for g be NAT -definedthe InstructionsF of S -valued finite Function holds for k be Nat holds for I be Instruction of S holds il in ( dom g) & I = (g . il) implies ( IncAddr (I,k)) = (( Reloc (g,k)) . (il + k))

    proof

      let g be NAT -definedthe InstructionsF of S -valued finite Function;

      let k be Nat;

      let I be Instruction of S;

      assume that

       A1: il in ( dom g) and

       A2: I = (g . il);

      reconsider ii = il as Element of NAT by ORDINAL1:def 12;

      

       A3: il in ( dom ( IncAddr (g,k))) by A1, Def9;

      

      thus (( Reloc (g,k)) . (il + k)) = (( IncAddr (g,k)) . ii) by A3, VALUED_1:def 12

      .= ( IncAddr ((g /. ii),k)) by A1, Def9

      .= ( IncAddr (I,k)) by A1, A2, PARTFUN1:def 6;

    end;

    reserve i,j,k for Instruction of S,

I,J,K for Program of S;

    definition

      let S be COM-Struct;

      let i be Instruction of S;

      :: original: Load

      redefine

      func Load i -> preProgram of S ;

      coherence ;

    end

    reserve k1,k2 for Integer;

    reserve l,l1,loc for Nat;

    definition

      let S be COM-Struct;

      let I be initial preProgram of S;

      :: COMPOS_1:def24

      func stop I -> preProgram of S equals (I ^ ( Stop S));

      coherence ;

    end

    registration

      let S be COM-Struct;

      let I be initial preProgram of S;

      cluster ( stop I) -> initial non empty;

      correctness ;

    end

    reserve i1,i2 for Instruction of S;

    theorem :: COMPOS_1:36

     0 in ( dom ( stop I)) by AFINSQ_1: 66;

    begin

    reserve i,j,k for Instruction of S,

I,J,K for Program of S;

    definition

      let S be COM-Struct;

      let i be Instruction of S;

      :: COMPOS_1:def25

      func Macro i -> preProgram of S equals ( stop ( Load i));

      coherence ;

    end

    registration

      let S;

      let i;

      cluster ( Macro i) -> initial non empty;

      coherence ;

    end

    begin

    reserve m for Nat;

    registration

      let S be COM-Struct;

      cluster ( Stop S) -> halt-ending;

      coherence ;

    end

    registration

      let S be COM-Struct;

      cluster non halt-free for Program of S;

      existence

      proof

        take ( Stop S);

        thus thesis;

      end;

    end

    registration

      let S be COM-Struct;

      let p be NAT -definedthe InstructionsF of S -valued Function, q be non halt-free NAT -definedthe InstructionsF of S -valued Function;

      cluster (p +* q) -> non halt-free;

      coherence

      proof

        

         A1: ( halt S) in ( rng q) by Def3;

        ( rng q) c= ( rng (p +* q)) by FUNCT_4: 18;

        hence ( halt S) in ( rng (p +* q)) by A1;

      end;

    end

    registration

      let S be COM-Struct;

      let p be finite non halt-free NAT -definedthe InstructionsF of S -valued Function, k be Nat;

      cluster ( Reloc (p,k)) -> non halt-free;

      coherence

      proof

        

         A1: ( dom p) c= NAT by RELAT_1:def 18;

        ( halt S) in ( rng p) by Def3;

        then

        consider x be object such that

         A2: x in ( dom p) and

         A3: (p . x) = ( halt S) by FUNCT_1:def 3;

        

         A4: x in ( dom ( IncAddr (p,k))) by A2, Def9;

        

         A5: ( dom ( IncAddr (p,k))) c= NAT by RELAT_1:def 18;

        reconsider m = x as Element of NAT by A1, A2;

        (( IncAddr (p,k)) . m) = ( IncAddr ((p /. m),k)) by A2, Def9

        .= ( IncAddr (( halt S),k)) by A3, A2, PARTFUN1:def 6

        .= ( halt S) by COMPOS_0: 4;

        then ( halt S) in ( rng ( IncAddr (p,k))) by A4, FUNCT_1: 3;

        hence ( halt S) in ( rng ( Reloc (p,k))) by A5, VALUED_1: 26;

      end;

    end

    registration

      let S be COM-Struct;

      cluster non halt-free non empty for Program of S;

      existence

      proof

        take ( Stop S);

        thus thesis;

      end;

    end

    ::$Canceled

    theorem :: COMPOS_1:41

    

     Th25: for S be COM-Struct holds for p,q be finite NAT -definedthe InstructionsF of S -valued Function holds ( IncAddr ((p +* q),n)) = (( IncAddr (p,n)) +* ( IncAddr (q,n)))

    proof

      let S be COM-Struct;

      let p,q be finite NAT -definedthe InstructionsF of S -valued Function;

      

       A1: ( dom ( IncAddr (q,n))) = ( dom q) by Def9;

       A2:

      now

        let m be Nat such that

         A3: m in ( dom (p +* q));

        per cases ;

          suppose

           A4: m in ( dom q);

          

           A5: ((p +* q) /. m) = ((p +* q) . m) by A3, PARTFUN1:def 6

          .= (q . m) by A4, FUNCT_4: 13

          .= (q /. m) by A4, PARTFUN1:def 6;

          

          thus ((( IncAddr (p,n)) +* ( IncAddr (q,n))) . m) = (( IncAddr (q,n)) . m) by A1, A4, FUNCT_4: 13

          .= ( IncAddr (((p +* q) /. m),n)) by A4, A5, Def9;

        end;

          suppose

           A6: not m in ( dom q);

          m in (( dom p) \/ ( dom q)) by A3, FUNCT_4:def 1;

          then

           A7: m in ( dom p) by A6, XBOOLE_0:def 3;

          

           A8: ((p +* q) /. m) = ((p +* q) . m) by A3, PARTFUN1:def 6

          .= (p . m) by A6, FUNCT_4: 11

          .= (p /. m) by A7, PARTFUN1:def 6;

          

          thus ((( IncAddr (p,n)) +* ( IncAddr (q,n))) . m) = (( IncAddr (p,n)) . m) by A1, A6, FUNCT_4: 11

          .= ( IncAddr (((p +* q) /. m),n)) by A7, A8, Def9;

        end;

      end;

      ( dom ( IncAddr (p,n))) = ( dom p) by Def9;

      

      then ( dom (( IncAddr (p,n)) +* ( IncAddr (q,n)))) = (( dom p) \/ ( dom q)) by A1, FUNCT_4:def 1

      .= ( dom (p +* q)) by FUNCT_4:def 1;

      hence ( IncAddr ((p +* q),n)) = (( IncAddr (p,n)) +* ( IncAddr (q,n))) by A2, Def9;

    end;

    theorem :: COMPOS_1:42

    for S be COM-Struct holds for p,q be finite NAT -definedthe InstructionsF of S -valued Function, k be Nat holds ( Reloc ((p +* q),k)) = (( Reloc (p,k)) +* ( Reloc (q,k)))

    proof

      let S be COM-Struct;

      let p,q be finite NAT -definedthe InstructionsF of S -valued Function, k be Nat;

      

       A1: ( Reloc ((p +* q),k)) = ( IncAddr (( Shift ((p +* q),k)),k)) by Th22;

      

       A2: ( Reloc (p,k)) = ( IncAddr (( Shift (p,k)),k)) by Th22;

      

       A3: ( Reloc (q,k)) = ( IncAddr (( Shift (q,k)),k)) by Th22;

      

      thus ( Reloc ((p +* q),k)) = ( IncAddr ((( Shift (p,k)) +* ( Shift (q,k))),k)) by A1, VALUED_1: 23

      .= (( Reloc (p,k)) +* ( Reloc (q,k))) by A2, A3, Th25;

    end;

    theorem :: COMPOS_1:43

    for S be COM-Struct holds for p be finite NAT -definedthe InstructionsF of S -valued Function, m,n be Nat holds ( Reloc (( Reloc (p,m)),n)) = ( Reloc (p,(m + n)))

    proof

      let S be COM-Struct;

      let p be finite NAT -definedthe InstructionsF of S -valued Function, m,n be Nat;

      

      thus ( Reloc (( Reloc (p,m)),n)) = ( Shift (( Shift (( IncAddr (( IncAddr (p,m)),n)),m)),n)) by Th22

      .= ( Shift (( Shift (( IncAddr (p,(m + n))),m)),n)) by Th8

      .= ( Reloc (p,(m + n))) by VALUED_1: 21;

    end;

    theorem :: COMPOS_1:44

    for S be COM-Struct holds for P,Q be NAT -definedthe InstructionsF of S -valued finite Function, k be Nat st P c= Q holds ( Reloc (P,k)) c= ( Reloc (Q,k))

    proof

      let S be COM-Struct;

      let P,Q be NAT -definedthe InstructionsF of S -valued finite Function;

      let k be Nat;

      set rP = ( Reloc (P,k));

      set rQ = ( Reloc (Q,k));

      

       A1: ( dom ( Reloc (P,k))) = { (m + k) where m be Nat : m in ( dom P) } by Th21;

      

       A2: ( dom ( Shift (P,k))) = { (m + k) where m be Nat : m in ( dom P) } by VALUED_1:def 12;

      

       A3: ( dom ( Shift (Q,k))) = { (m + k) where m be Nat : m in ( dom Q) } by VALUED_1:def 12;

      

       A4: rQ = ( IncAddr (( Shift (Q,k)),k)) by Th22;

      assume

       A5: P c= Q;

      then

       A6: ( Shift (P,k)) c= ( Shift (Q,k)) by VALUED_1: 20;

      

       A7: ( dom P) c= ( dom Q) by A5, GRFUNC_1: 2;

       A8:

      now

        let x be object;

        assume x in ( dom ( Reloc (P,k)));

        then

        consider m1 be Nat such that

         A9: x = (m1 + k) and

         A10: m1 in ( dom P) by A1;

        

         A11: (m1 + k) in ( dom ( Shift (Q,k))) by A7, A3, A10;

        

         A12: (m1 + k) in ( dom ( Shift (P,k))) by A2, A10;

        

        then

         A13: (( Shift (P,k)) /. (m1 + k)) = (( Shift (P,k)) . (m1 + k)) by PARTFUN1:def 6

        .= (( Shift (Q,k)) . (m1 + k)) by A6, A12, GRFUNC_1: 2

        .= (( Shift (Q,k)) /. (m1 + k)) by A11, PARTFUN1:def 6;

        

        thus (rP . x) = (( IncAddr (( Shift (P,k)),k)) . x) by Th22

        .= ( IncAddr ((( Shift (Q,k)) /. (m1 + k)),k)) by A12, A13, A9, Def9

        .= (rQ . x) by A9, A11, A4, Def9;

      end;

      

       A14: ( dom ( Shift (P,k))) c= ( dom ( Shift (Q,k))) by A6, GRFUNC_1: 2;

      now

        let x be object;

        assume x in ( dom rP);

        then x in ( dom ( Shift (P,k))) by Th20;

        then x in ( dom ( Shift (Q,k))) by A14;

        hence x in ( dom rQ) by Th20;

      end;

      then ( dom rP) c= ( dom rQ);

      hence thesis by A8, GRFUNC_1: 2;

    end;

    registration

      let S be COM-Struct;

      let P be preProgram of S;

      reduce ( Reloc (P, 0 )) to P;

      reducibility ;

    end

    theorem :: COMPOS_1:45

    for S be COM-Struct holds for P be preProgram of S holds ( Reloc (P, 0 )) = P;

    theorem :: COMPOS_1:46

    for S be COM-Struct holds for k be Nat holds for P be preProgram of S holds il in ( dom P) iff (il + k) in ( dom ( Reloc (P,k)))

    proof

      let S be COM-Struct;

      let k be Nat;

      let P be preProgram of S;

      

       A1: ( dom ( Reloc (P,k))) = { (j + k) where j be Nat : j in ( dom P) } by Th21;

      reconsider il1 = il as Element of NAT by ORDINAL1:def 12;

      il1 in ( dom P) implies (il1 + k) in ( dom ( Reloc (P,k))) by A1;

      hence il in ( dom P) implies (il + k) in ( dom ( Reloc (P,k)));

      assume (il + k) in ( dom ( Reloc (P,k)));

      then ex j be Nat st (il + k) = (j + k) & j in ( dom P) by A1;

      hence thesis;

    end;

    theorem :: COMPOS_1:47

    for S be COM-Struct holds for i be Instruction of S holds for f be Function of the InstructionsF of S, the InstructionsF of S st f = (( id the InstructionsF of S) +* (( halt S) .--> i)) holds for s be finite NAT -definedthe InstructionsF of S -valued Function holds ( IncAddr ((f * s),n)) = ((( id the InstructionsF of S) +* (( halt S) .--> ( IncAddr (i,n)))) * ( IncAddr (s,n)))

    proof

      let S be COM-Struct;

      let i be Instruction of S;

      let f be Function of the InstructionsF of S, the InstructionsF of S such that

       A1: f = (( id the InstructionsF of S) +* (( halt S) .--> i));

      let s be finite NAT -definedthe InstructionsF of S -valued Function;

      ( rng (( halt S) .--> ( IncAddr (i,n)))) = {( IncAddr (i,n))} by FUNCOP_1: 8;

      then

       A2: ( rng (( id the InstructionsF of S) +* (( halt S) .--> ( IncAddr (i,n))))) c= (( rng ( id the InstructionsF of S)) \/ {( IncAddr (i,n))}) by FUNCT_4: 17;

      

       A3: (( rng ( id the InstructionsF of S)) \/ {( IncAddr (i,n))}) = the InstructionsF of S by ZFMISC_1: 40;

      

       A4: ( dom (( halt S) .--> ( IncAddr (i,n)))) = {( halt S)};

      

      then ( dom (( id the InstructionsF of S) +* (( halt S) .--> ( IncAddr (i,n))))) = (( dom ( id the InstructionsF of S)) \/ {( halt S)}) by FUNCT_4:def 1

      .= the InstructionsF of S by ZFMISC_1: 40;

      then

      reconsider g = (( id the InstructionsF of S) +* (( halt S) .--> ( IncAddr (i,n)))) as Function of the InstructionsF of S, the InstructionsF of S by A2, A3, RELSET_1: 4;

      

       A5: ( dom ( IncAddr (s,n))) = ( dom s) by Def9

      .= ( dom (f * s)) by FUNCT_2: 123;

      

       A6: ( dom (( halt S) .--> i)) = {( halt S)};

       A7:

      now

        let m be Nat;

        assume

         A8: m in ( dom (f * s));

        then

         A9: m in ( dom s) by FUNCT_2: 123;

        per cases ;

          suppose

           A10: (s . m) = ( halt S);

          reconsider mm = m as Element of NAT by ORDINAL1:def 12;

          

           A11: (( IncAddr (s,n)) . m) = ( IncAddr ((s /. mm),n)) by A9, Def9

          .= ( IncAddr (( halt S),n)) by A9, A10, PARTFUN1:def 6

          .= ( halt S) by COMPOS_0: 4;

          

           A12: ( halt S) in {( halt S)} by TARSKI:def 1;

          

           A13: ((f * s) /. m) = ((f * s) . m) by A8, PARTFUN1:def 6

          .= (f . ( halt S)) by A9, A10, FUNCT_1: 13

          .= ((( halt S) .--> i) . ( halt S)) by A1, A6, A12, FUNCT_4: 13

          .= i by FUNCOP_1: 72;

          

          thus ((g * ( IncAddr (s,n))) . m) = (g . (( IncAddr (s,n)) . m)) by A5, A8, FUNCT_1: 13

          .= ((( halt S) .--> ( IncAddr (i,n))) . (( IncAddr (s,n)) . m)) by A4, A11, A12, FUNCT_4: 13

          .= ( IncAddr (((f * s) /. m),n)) by A11, A13, FUNCOP_1: 72;

        end;

          suppose

           A14: (s . m) <> ( halt S);

          

           A15: (s /. m) = (s . m) by A9, PARTFUN1:def 6;

          

           A16: not ( IncAddr ((s /. m),n)) = ( halt S) by A14, A15, COMPOS_0: 12;

          

           A17: not (s /. m) in {( halt S)} by A14, A15, TARSKI:def 1;

          

           A18: not ( IncAddr ((s /. m),n)) in {( halt S)} by A16, TARSKI:def 1;

          

           A19: ((f * s) /. m) = ((f * s) . m) by A8, PARTFUN1:def 6

          .= (f . (s . m)) by A9, FUNCT_1: 13

          .= (( id the InstructionsF of S) . (s /. m)) by A1, A6, A15, A17, FUNCT_4: 11

          .= (s /. m);

          

          thus ((g * ( IncAddr (s,n))) . m) = (g . (( IncAddr (s,n)) . m)) by A5, A8, FUNCT_1: 13

          .= (g . ( IncAddr ((s /. m),n))) by A9, Def9

          .= (( id the InstructionsF of S) . ( IncAddr ((s /. m),n))) by A4, A18, FUNCT_4: 11

          .= ( IncAddr (((f * s) /. m),n)) by A19;

        end;

      end;

      ( dom (g * ( IncAddr (s,n)))) = ( dom ( IncAddr (s,n))) by FUNCT_2: 123;

      hence thesis by A5, A7, Def9;

    end;

    reserve I,J for Program of S;

    theorem :: COMPOS_1:48

    ( dom I) misses ( dom ( Reloc (J,( card I))))

    proof

      assume

       A1: ( dom I) meets ( dom ( Reloc (J,( card I))));

      ( dom ( Reloc (J,( card I)))) = ( dom ( Shift (J,( card I)))) by Th20

      .= { (l + ( card I)) where l be Nat : l in ( dom J) } by VALUED_1:def 12;

      then

      consider x be object such that

       A2: x in ( dom I) and

       A3: x in { (l + ( card I)) where l be Nat : l in ( dom J) } by A1, XBOOLE_0: 3;

      consider l be Nat such that

       A4: x = (l + ( card I)) and l in ( dom J) by A3;

      (l + ( card I)) < ( card I) by A2, A4, AFINSQ_1: 66;

      hence contradiction by NAT_1: 11;

    end;

    theorem :: COMPOS_1:49

    for I be preProgram of S holds ( card ( Reloc (I,m))) = ( card I)

    proof

      let I be preProgram of S;

      deffunc U( Nat) = $1;

      set B = { l where l be Element of NAT : U(l) in ( dom I) };

      

       A1: for x be set st x in ( dom I) holds ex d be Element of NAT st x = U(d)

      proof

        let x be set;

        assume

         A2: x in ( dom I);

        ( dom I) c= NAT by RELAT_1:def 18;

        then

        reconsider l = x as Element of NAT by A2;

        reconsider d = l as Element of NAT ;

        l = U(d);

        hence thesis;

      end;

      

       A3: for d1,d2 be Element of NAT st U(d1) = U(d2) holds d1 = d2;

      

       A4: (( dom I),B) are_equipotent from FUNCT_7:sch 3( A1, A3);

      defpred Z[ Nat] means $1 in ( dom I);

      deffunc V( Nat) = ($1 + m);

      defpred X[ Nat] means U($1) in ( dom I);

      set D = { l where l be Element of NAT : X[l] };

      set C = { V(l) where l be Element of NAT : l in B };

      defpred X[ set] means not contradiction;

      D is Subset of NAT from DOMAIN_1:sch 7;

      then

       A5: B c= NAT ;

      

       A6: for d1,d2 be Element of NAT st V(d1) = V(d2) holds d1 = d2;

      

       A7: (B,C) are_equipotent from FUNCT_7:sch 4( A5, A6);

      set C = { V(l) where l be Element of NAT : l in { n where n be Element of NAT : Z[n] } & X[l] }, A = { V(l) where l be Element of NAT : Z[l] & X[l] };

      

       A8: C = { (l + m) where l be Element of NAT : l in B }

      proof

        thus C c= { (l + m) where l be Element of NAT : l in B }

        proof

          let e be object;

          assume e in C;

          then ex l be Element of NAT st e = V(l) & l in B;

          hence thesis;

        end;

        let e be object;

        assume e in { (l + m) where l be Element of NAT : l in B };

        then ex l be Element of NAT st e = (l + m) & l in B;

        hence thesis;

      end;

      A = { (l + m) where l be Nat : l in ( dom I) }

      proof

        thus A c= { (l + m) where l be Nat : l in ( dom I) }

        proof

          let e be object;

          assume e in A;

          then ex l be Element of NAT st e = V(l) & l in ( dom I);

          hence thesis;

        end;

        let e be object;

        assume e in { (l + m) where l be Nat : l in ( dom I) };

        then

        consider l be Nat such that

         A9: e = (l + m) & l in ( dom I);

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

        l in ( dom I) by A9;

        hence thesis by A9;

      end;

      then

       A10: ( dom ( Shift (I,m))) = A by VALUED_1:def 12;

      C = A from FRAENKEL:sch 14;

      then

       A11: (( dom ( Shift (I,m))),( dom I)) are_equipotent by A4, A7, A8, A10, WELLORD2: 15;

      

      thus ( card ( Reloc (I,m))) = ( card ( dom ( Reloc (I,m)))) by CARD_1: 62

      .= ( card ( dom ( Shift (I,m)))) by Th20

      .= ( card ( dom I)) by A11, CARD_1: 5

      .= ( card I) by CARD_1: 62;

    end;

    reserve i for Instruction of S,

I for Program of S;

    theorem :: COMPOS_1:50

    x in ( dom ( Load i)) iff x = 0 by TARSKI:def 1;

    reserve loc for Nat;

    theorem :: COMPOS_1:51

    loc in ( dom ( stop I)) & (( stop I) . loc) <> ( halt S) implies loc in ( dom I)

    proof

      assume that

       A1: loc in ( dom ( stop I)) and

       A2: (( stop I) . loc) <> ( halt S);

      set SS = ( Stop S), S2 = ( Shift (SS,( card I)));

      

       A3: ( stop I) = (I +* S2) by AFINSQ_1: 77;

      assume not loc in ( dom I);

      then loc in ( dom S2) by A1, A3, FUNCT_4: 12;

      then loc in { (l1 + ( card I)) where l1 be Nat : l1 in ( dom SS) } by VALUED_1:def 12;

      then

      consider l1 be Nat such that

       A4: loc = (l1 + ( card I)) and

       A5: l1 in ( dom SS);

      

       A6: 0 in ( dom ( Stop S)) by Th2;

      

       A7: (( Stop S) . 0 ) = ( halt S);

      l1 = 0 by A5, TARSKI:def 1;

      hence contradiction by A2, A4, A7, A6, AFINSQ_1:def 3;

    end;

    theorem :: COMPOS_1:52

    ( dom ( Load i)) = { 0 } & (( Load i) . 0 ) = i;

    theorem :: COMPOS_1:53

    

     Th37: 0 in ( dom ( Load i)) by TARSKI:def 1;

    theorem :: COMPOS_1:54

    

     Th38: ( card ( Load i)) = 1

    proof

      

      thus ( card ( Load i)) = ( card ( dom ( Load i)))

      .= 1 by CARD_1: 30;

    end;

    theorem :: COMPOS_1:55

    

     Th39: ( card ( stop I)) = (( card I) + 1)

    proof

      

      thus ( card ( stop I)) = (( card I) + ( card ( Stop S))) by AFINSQ_1: 17

      .= (( card I) + 1) by AFINSQ_1: 34;

    end;

    theorem :: COMPOS_1:56

    

     Th40: ( card ( Macro i)) = 2

    proof

      

      thus ( card ( Macro i)) = (( card ( Load i)) + ( card ( Stop S))) by AFINSQ_1: 17

      .= (( card ( Load i)) + 1) by AFINSQ_1: 34

      .= (1 + 1) by Th38

      .= 2;

    end;

    theorem :: COMPOS_1:57

    

     Th41: 0 in ( dom ( Macro i)) & 1 in ( dom ( Macro i))

    proof

      ( card ( Macro i)) = 2 by Th40;

      hence thesis by AFINSQ_1: 66;

    end;

    theorem :: COMPOS_1:58

    

     Th42: (( Macro i) . 0 ) = i

    proof

      set I = ( Load i);

       0 in ( dom I) by Th37;

      

      hence (( Macro i) . 0 ) = (I . 0 ) by AFINSQ_1:def 3

      .= i;

    end;

    theorem :: COMPOS_1:59

    

     Th43: (( Macro i) . 1) = ( halt S)

    proof

      

       A1: 0 in ( dom ( Stop S)) by Th2;

      

       A2: (( Stop S) . 0 ) = ( halt S);

      1 = ( 0 qua Nat + ( card ( Load i))) by Th38;

      hence thesis by A2, A1, AFINSQ_1:def 3;

    end;

    theorem :: COMPOS_1:60

    

     Th44: x in ( dom ( Macro i)) iff x = 0 or x = 1

    proof

      set si = ( Macro i), A = NAT ;

      

       A1: ( card si) = 2 by Th40;

      hereby

        assume

         A2: x in ( dom si);

        reconsider l = x as Element of NAT by A2;

        reconsider n = l as Element of NAT ;

        n < (1 + 1) by A1, A2, AFINSQ_1: 66;

        then n <= 1 by NAT_1: 13;

        hence x = 0 or x = 1 by NAT_1: 25;

      end;

      thus thesis by A1, AFINSQ_1: 66;

    end;

    theorem :: COMPOS_1:61

    

     Th45: ( dom ( Macro i)) = { 0 , 1}

    proof

      for x be object holds x in ( dom ( Macro i)) iff x = 0 or x = 1 by Th44;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: COMPOS_1:62

    loc in ( dom I) implies loc in ( dom ( stop I))

    proof

      ( dom I) c= ( dom (I ^ ( Stop S))) by AFINSQ_1: 21;

      hence thesis;

    end;

    theorem :: COMPOS_1:63

    for I be initial preProgram of S st loc in ( dom I) holds (( stop I) . loc) = (I . loc) by AFINSQ_1:def 3;

    theorem :: COMPOS_1:64

    

     Th48: ( card I) in ( dom ( stop I)) & (( stop I) . ( card I)) = ( halt S)

    proof

      

       A1: (( Stop S) . 0 ) = ( halt S);

      

       A2: 0 in ( dom ( Stop S)) by Th2;

      set pI = ( stop I);

      ( card pI) = (( card I) + 1) by Th39;

      then ( card I) < ( card pI) by XREAL_1: 29;

      hence ( card I) in ( dom pI) by AFINSQ_1: 66;

      (pI . ( 0 qua Nat + ( card I))) = ( halt S) by A1, A2, AFINSQ_1:def 3;

      hence thesis;

    end;

    theorem :: COMPOS_1:65

    

     Th49: loc in ( dom I) implies (( Shift (( stop I),n)) . (loc + n)) = (( Shift (I,n)) . (loc + n))

    proof

      

       A1: ( dom I) c= ( dom ( stop I)) by AFINSQ_1: 21;

      reconsider l = loc as Element of NAT by ORDINAL1:def 12;

      assume

       A2: loc in ( dom I);

      

      hence (( Shift (I,n)) . (loc + n)) = (I . l) by VALUED_1:def 12

      .= (( stop I) . l) by A2, AFINSQ_1:def 3

      .= (( Shift (( stop I),n)) . (loc + n)) by A2, A1, VALUED_1:def 12;

    end;

    theorem :: COMPOS_1:66

    (( Shift (( stop I),n)) . n) = (( Shift (I,n)) . n)

    proof

      

       A1: 0 in ( dom I) by AFINSQ_1: 66;

      

      thus (( Shift (( stop I),n)) . n) = (( Shift (I,n)) . ( 0 qua Nat + n)) by A1, Th49

      .= (( Shift (I,n)) . n);

    end;

    registration

      let S be COM-Struct;

      cluster empty for preProgram of S;

      existence

      proof

        reconsider p = ( <%> the InstructionsF of S) as preProgram of S;

        take p;

        thus thesis;

      end;

    end

    registration

      let S be COM-Struct;

      cluster empty -> halt-free for preProgram of S;

      coherence ;

    end

    definition

      ::$Canceled

      let S be COM-Struct;

      let IT be NAT -definedthe InstructionsF of S -valued Function;

      :: original: halt-free

      redefine

      :: COMPOS_1:def27

      attr IT is halt-free means

      : Def14: for x be Nat st x in ( dom IT) holds (IT . x) <> ( halt S);

      compatibility

      proof

        thus IT is halt-free implies for x be Nat st x in ( dom IT) holds (IT . x) <> ( halt S) by FUNCT_1: 3;

        assume

         A1: for x be Nat st x in ( dom IT) holds (IT . x) <> ( halt S);

        assume ( halt S) in ( rng IT);

        then

        consider x be object such that

         A2: x in ( dom IT) and

         A3: ( halt S) = (IT . x) by FUNCT_1:def 3;

        thus contradiction by A2, A3, A1;

      end;

    end

    registration

      let S be COM-Struct;

      cluster halt-free -> unique-halt for non empty preProgram of S;

      coherence ;

    end

    theorem :: COMPOS_1:67

    ( rng ( Macro i)) = {i, ( halt S)}

    proof

      

      thus ( rng ( Macro i)) = (( rng ( Load i)) \/ ( rng ( Stop S))) by AFINSQ_1: 26

      .= ( {i} \/ ( rng ( Stop S))) by AFINSQ_1: 33

      .= ( {i} \/ {( halt S)}) by AFINSQ_1: 33

      .= {i, ( halt S)} by ENUMSET1: 1;

    end;

    registration

      let S;

      let p be initial preProgram of S;

      reduce ( CutLastLoc ( stop p)) to p;

      reducibility by AFINSQ_2: 83;

    end

    theorem :: COMPOS_1:68

    for p be initial preProgram of S holds ( CutLastLoc ( stop p)) = p;

    registration

      let S be COM-Struct;

      let p be halt-free initial preProgram of S;

      cluster ( stop p) -> unique-halt;

      coherence

      proof

        let k be Nat such that

         A1: (( stop p) . k) = ( halt S) and

         A2: k in ( dom ( stop p));

        

         A3: ( dom ( stop p)) = (( dom ( CutLastLoc ( stop p))) \/ {( LastLoc ( stop p))}) by VALUED_1: 37;

        now

          assume k in ( dom ( CutLastLoc ( stop p)));

          then

           A4: k in ( dom p);

          then (p . k) = ( halt S) by A1, AFINSQ_1:def 3;

          hence contradiction by Def14, A4;

        end;

        then k in {( LastLoc ( stop p))} by A2, A3, XBOOLE_0:def 3;

        hence k = ( LastLoc ( stop p)) by TARSKI:def 1;

      end;

    end

    registration

      let S;

      let I be Program of S, J be non halt-free Program of S;

      cluster (I ';' J) -> non halt-free;

      coherence ;

    end

    theorem :: COMPOS_1:69

    for I be Program of S holds ( CutLastLoc ( stop I)) = I;

    theorem :: COMPOS_1:70

    ( InsCode ( halt S)) = 0 ;

    theorem :: COMPOS_1:71

    

     Th55: for S be COM-Struct, I be initial preProgram of S holds (( card ( stop I)) -' 1) = ( card I)

    proof

      let S be COM-Struct, I be initial preProgram of S;

      

      thus (( card ( stop I)) -' 1) = (( card ( stop I)) - 1) by PRE_CIRC: 20

      .= ((( card I) + ( card ( Stop S))) - 1) by AFINSQ_1: 17

      .= ((( card I) + 1) - 1) by AFINSQ_1: 34

      .= ( card I);

    end;

    theorem :: COMPOS_1:72

    for S be COM-Struct, I be initial preProgram of S holds ( card ( stop I)) = (( card I) + 1)

    proof

      let S be COM-Struct, I be initial preProgram of S;

      

      thus ( card ( stop I)) = (( card I) + ( card ( Stop S))) by AFINSQ_1: 17

      .= (( card I) + 1) by AFINSQ_1: 34;

    end;

    theorem :: COMPOS_1:73

    

     Th57: ( LastLoc ( stop I)) = ( card I)

    proof

      

      thus ( LastLoc ( stop I)) = (( card ( stop I)) -' 1) by AFINSQ_1: 70

      .= ( card I) by Th55;

    end;

    registration

      let S, I;

      cluster ( stop I) -> halt-ending;

      coherence

      proof

        

        thus (( stop I) . ( LastLoc ( stop I))) = (( stop I) . ( card I)) by Th57

        .= ( halt S) by Th48;

      end;

    end

    theorem :: COMPOS_1:74

    ( Macro ( IncAddr (i,n))) = ( IncAddr (( Macro i),n))

    proof

      

       A1: ( dom ( Macro ( IncAddr (i,n)))) = { 0 , 1} by Th45

      .= ( dom ( Macro i)) by Th45;

      for m be Nat st m in ( dom ( Macro i)) holds (( Macro ( IncAddr (i,n))) . m) = ( IncAddr ((( Macro i) /. m),n))

      proof

        let m be Nat;

        assume m in ( dom ( Macro i));

        per cases by Th44;

          suppose

           A2: m = 0 ;

          then m in ( dom ( Macro i)) by Th41;

          

          then

           A3: (( Macro i) /. m) = (( Macro i) . m) by PARTFUN1:def 6

          .= i by A2, Th42;

          

          thus (( Macro ( IncAddr (i,n))) . m) = ( IncAddr (i,n)) by A2, Th42

          .= ( IncAddr ((( Macro i) /. m),n)) by A3;

        end;

          suppose

           A4: m = 1;

          then m in ( dom ( Macro i)) by Th41;

          

          then

           A5: (( Macro i) /. m) = (( Macro i) . m) by PARTFUN1:def 6

          .= ( halt S) by A4, Th43;

          

          thus (( Macro ( IncAddr (i,n))) . m) = ( halt S) by Th43, A4

          .= ( IncAddr (( halt S),n)) by COMPOS_0: 4

          .= ( IncAddr ((( Macro i) /. m),n)) by A5;

        end;

      end;

      hence thesis by A1, Def9;

    end;

    theorem :: COMPOS_1:75

    (I ';' J) = (( CutLastLoc I) ^ ( IncAddr (J,(( card I) -' 1))))

    proof

      ( card ( CutLastLoc I)) = (( card I) -' 1) by VALUED_1: 65;

      hence (I ';' J) = (( CutLastLoc I) ^ ( IncAddr (J,(( card I) -' 1)))) by AFINSQ_1: 77;

    end;

    theorem :: COMPOS_1:76

    ( IncAddr (( Macro i),n)) = (( IncAddr (( Load i),n)) ^ ( Stop S))

    proof

      

       A1: ( dom ( Macro i)) = { 0 , 1} by Th45;

      

       A2: ( dom (( IncAddr (( Load i),n)) ^ ( Stop S))) = ( len (( IncAddr (( Load i),n)) ^ ( Stop S)))

      .= (( len ( IncAddr (( Load i),n))) + 1) by AFINSQ_1: 75

      .= (( len ( Load i)) + 1) by Def9

      .= (1 + 1) by AFINSQ_1: 34

      .= { 0 , 1} by CARD_1: 50

      .= ( dom ( Macro i)) by Th45;

      for m be Nat st m in ( dom ( Macro i)) holds ((( IncAddr (( Load i),n)) ^ ( Stop S)) . m) = ( IncAddr ((( Macro i) /. m),n))

      proof

        let m be Nat;

        assume m in ( dom ( Macro i));

        per cases by A1, TARSKI:def 2;

          suppose

           A3: m = 0 ;

          

           A4: 0 in ( dom ( Load i)) by AFINSQ_1: 65;

          then

           A5: (( Load i) /. m) = (( Load i) . m) by A3, PARTFUN1:def 6;

          ( dom ( Load i)) c= ( dom (( Load i) ^ ( Stop S))) by AFINSQ_1: 21;

          then m in ( dom (( Load i) ^ ( Stop S))) by A4, A3;

          then

           A6: ((( Load i) ^ ( Stop S)) . m) = ((( Load i) ^ ( Stop S)) /. m) by PARTFUN1:def 6;

          m in ( dom ( IncAddr (( Load i),n))) by Def9, A4, A3;

          

          hence ((( IncAddr (( Load i),n)) ^ ( Stop S)) . m) = (( IncAddr (( Load i),n)) . m) by AFINSQ_1:def 3

          .= ( IncAddr ((( Load i) /. m),n)) by A4, Def9, A3

          .= ( IncAddr ((( stop ( Load i)) /. m),n)) by A6, A4, AFINSQ_1:def 3, A5, A3

          .= ( IncAddr ((( Macro i) /. m),n));

        end;

          suppose

           A7: m = 1;

          

           A8: ( len ( Load i)) = 1 by AFINSQ_1: 34;

          then

           A9: ( len ( IncAddr (( Load i),n))) = 1 by Def9;

          

           A10: 0 in ( dom ( Stop S)) by AFINSQ_1: 65;

          ( len (( Load i) ^ ( Stop S))) = (( len ( Load i)) + ( len ( Stop S))) by AFINSQ_1:def 3

          .= (( len ( Load i)) + 1) by AFINSQ_1: 34

          .= (1 + 1) by AFINSQ_1: 34

          .= { 0 , 1} by CARD_1: 50;

          then 1 in ( dom (( Load i) ^ ( Stop S))) by TARSKI:def 2;

          then

           A11: ((( Load i) ^ ( Stop S)) /. m) = ((( Load i) ^ ( Stop S)) . (1 + 0 )) by PARTFUN1:def 6, A7;

          

           A12: (( Stop S) /. 0 ) = (( Stop S) . 0 ) by A10, PARTFUN1:def 6;

          

          thus ((( IncAddr (( Load i),n)) ^ ( Stop S)) . m) = ((( IncAddr (( Load i),n)) ^ ( Stop S)) . (1 + 0 )) by A7

          .= (( IncAddr (( Stop S),n)) . 0 ) by AFINSQ_1:def 3, A9, A10

          .= ( IncAddr ((( Stop S) /. 0 ),n)) by A10, Def9

          .= ( IncAddr ((( stop ( Load i)) /. m),n)) by A11, A12, AFINSQ_1:def 3, A8, A10

          .= ( IncAddr ((( Macro i) /. m),n));

        end;

      end;

      hence thesis by A2, Def9;

    end;

    theorem :: COMPOS_1:77

    for S be COM-Struct, F,G be Program of S, n be Nat st n < ( LastLoc F) holds (F . n) = ((F ';' G) . n)

    proof

      let S be COM-Struct, F,G be Program of S, f be Nat;

      assume f < ( LastLoc F);

      then f < (( card F) - 1) by AFINSQ_1: 91;

      hence thesis by Lm6;

    end;