compos_2.miz



    begin

    registration

      cluster with_non_trivial_Instructions for COM-Struct;

      existence

      proof

        take C = COM-Struct (# the non trivial Instructions #);

        thus the InstructionsF of C is non trivial;

      end;

    end

    reserve S for with_non_trivial_Instructions COM-Struct;

    registration

      let S;

      cluster No-StopCode for Instruction of S;

      existence

      proof

        the InstructionsF of S is non trivial by AMISTD_4:def 1;

        then

        consider x,y be object such that

         A1: x in the InstructionsF of S & y in the InstructionsF of S and

         A2: x <> y by ZFMISC_1:def 10;

        x <> ( halt S) or y <> ( halt S) by A2;

        then

        consider i be Instruction of S such that

         A3: i <> ( halt S) by A1;

        take i;

        thus i is No-StopCode by A3, COMPOS_0:def 12;

      end;

    end

    registration

      let S;

      let i be No-StopCode Instruction of S;

      cluster ( Macro i) -> halt-ending unique-halt;

      coherence

      proof

        

         A1: ( LastLoc ( Macro i)) = (( card ( Macro i)) -' 1) by AFINSQ_1: 70

        .= (2 -' 1) by COMPOS_1: 56

        .= (2 - 1) by XREAL_1: 233

        .= 1;

        hence (( Macro i) . ( LastLoc ( Macro i))) = ( halt S) by COMPOS_1: 59;

        thus ( Macro i) is unique-halt

        proof

          let f be Nat such that

           A2: (( Macro i) . f) = ( halt S);

          assume

           A3: f in ( dom ( Macro i));

          now

            assume f = 0 ;

            then (( Macro i) . f) = i by COMPOS_1: 58;

            hence contradiction by A2, COMPOS_0:def 12;

          end;

          hence f = ( LastLoc ( Macro i)) by A3, A1, COMPOS_1: 60;

        end;

      end;

    end

    definition

      let S;

      let i be No-StopCode Instruction of S, J be MacroInstruction of S;

      :: COMPOS_2:def1

      func i ';' J -> MacroInstruction of S equals (( Macro i) ';' J);

      correctness ;

    end

    definition

      let S;

      let I be MacroInstruction of S, j be No-StopCode Instruction of S;

      :: COMPOS_2:def2

      func I ';' j -> MacroInstruction of S equals (I ';' ( Macro j));

      correctness ;

    end

    definition

      let S;

      let i,j be No-StopCode Instruction of S;

      :: COMPOS_2:def3

      func i ';' j -> MacroInstruction of S equals (( Macro i) ';' ( Macro j));

      correctness ;

    end

    reserve i,j,k for No-StopCode Instruction of S,

I,J,K for MacroInstruction of S;

    theorem :: COMPOS_2:1

    ((I ';' J) ';' k) = (I ';' (J ';' k)) by COMPOS_1: 29;

    theorem :: COMPOS_2:2

    ((I ';' j) ';' K) = (I ';' (j ';' K)) by COMPOS_1: 29;

    theorem :: COMPOS_2:3

    ((I ';' j) ';' k) = (I ';' (j ';' k)) by COMPOS_1: 29;

    theorem :: COMPOS_2:4

    ((i ';' J) ';' K) = (i ';' (J ';' K)) by COMPOS_1: 29;

    theorem :: COMPOS_2:5

    ((i ';' J) ';' k) = (i ';' (J ';' k)) by COMPOS_1: 29;

    theorem :: COMPOS_2:6

    ((i ';' j) ';' K) = (i ';' (j ';' K)) by COMPOS_1: 29;

    theorem :: COMPOS_2:7

    ((i ';' j) ';' k) = (i ';' (j ';' k)) by COMPOS_1: 29;

    theorem :: COMPOS_2:8

    (i ';' j) = (( Macro i) ';' j);

    theorem :: COMPOS_2:9

    (i ';' j) = (i ';' ( Macro j));

    theorem :: COMPOS_2:10

    ( card (i ';' J)) = (( card J) + 1)

    proof

      

      thus ( card (i ';' J)) = ((( card ( Macro i)) + ( card J)) - 1) by COMPOS_1: 20

      .= ((2 + ( card J)) - 1) by COMPOS_1: 56

      .= (( card J) + 1);

    end;

    theorem :: COMPOS_2:11

    

     Th11: ( card (I ';' j)) = (( card I) + 1)

    proof

      

      thus ( card (I ';' j)) = ((( card I) + ( card ( Macro j))) - 1) by COMPOS_1: 20

      .= ((2 + ( card I)) - 1) by COMPOS_1: 56

      .= (( card I) + 1);

    end;

    theorem :: COMPOS_2:12

    

     Th12: ( card (i ';' j)) = 3

    proof

      

      thus ( card (i ';' j)) = ((( card ( Macro i)) + ( card ( Macro j))) - 1) by COMPOS_1: 20

      .= ((2 + ( card ( Macro i))) - 1) by COMPOS_1: 56

      .= ((2 + 2) - 1) by COMPOS_1: 56

      .= 3;

    end;

    theorem :: COMPOS_2:13

    

     Th13: ( card ((i ';' j) ';' k)) = 4

    proof

      

      thus ( card ((i ';' j) ';' k)) = (( card (i ';' j)) + 1) by Th11

      .= (3 + 1) by Th12

      .= 4;

    end;

    reserve i1,i2,i3,i4,i5,i6 for No-StopCode Instruction of S;

    theorem :: COMPOS_2:14

    

     Th14: ( card (((i1 ';' i2) ';' i3) ';' i4)) = 5

    proof

      

      thus ( card (((i1 ';' i2) ';' i3) ';' i4)) = (( card ((i1 ';' i2) ';' i3)) + 1) by Th11

      .= (4 + 1) by Th13

      .= 5;

    end;

    theorem :: COMPOS_2:15

    

     Th15: ( card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 6

    proof

      

      thus ( card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = (( card (((i1 ';' i2) ';' i3) ';' i4)) + 1) by Th11

      .= (5 + 1) by Th14

      .= 6;

    end;

    theorem :: COMPOS_2:16

    

     Th16: ( card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6)) = 7

    proof

      

      thus ( card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6)) = (( card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) + 1) by Th11

      .= (6 + 1) by Th15

      .= 7;

    end;

    reserve I,J for non empty NAT -defined finite Function;

    definition

      let I;

      let J be set;

      :: COMPOS_2:def4

      pred I <= J means ( CutLastLoc I) c= J;

    end

    definition

      let I, J;

      :: original: <=

      redefine

      pred I <= J;

      reflexivity ;

    end

    theorem :: COMPOS_2:17

    

     Th17: for F be non empty NAT -defined finite Function holds not ( LastLoc F) in ( dom ( CutLastLoc F))

    proof

      let F be non empty NAT -defined finite Function;

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

      then (F | {( LastLoc F)}) = (( LastLoc F) .--> (F . ( LastLoc F))) by FUNCT_7: 6;

      then

       A1: ( dom ( CutLastLoc F)) = (( dom F) \ {( LastLoc F)}) by RELAT_1: 177;

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

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    registration

      let S;

      let I be unique-halt non empty preProgram of S;

      cluster ( CutLastLoc I) -> halt-free;

      coherence

      proof

        now

          assume ( halt S) in ( rng ( CutLastLoc I));

          then

          consider x be object such that

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

           A2: (( CutLastLoc I) . x) = ( halt S) by FUNCT_1:def 3;

          ( dom ( CutLastLoc I)) c= ( dom I) by RELAT_1: 11;

          then

           A3: x in ( dom I) by A1;

          

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

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

          then x = ( LastLoc I) by A3, A4, COMPOS_1:def 15;

          hence contradiction by A1, Th17;

        end;

        hence ( CutLastLoc I) is halt-free;

      end;

    end

    

     Lm1: for f,g be Function st f c= g holds for x,y be set st not x in ( rng f) holds f c= (g \ (y .--> x))

    proof

      let f,g be Function such that

       A1: f c= g;

      let x,y be set;

      assume not x in ( rng f);

      then

       A2: not [y, x] in f by XTUPLE_0:def 13;

      (y .--> x) = { [y, x]} by ZFMISC_1: 29;

      hence f c= (g \ (y .--> x)) by A2, A1, ZFMISC_1: 34;

    end;

    theorem :: COMPOS_2:18

    

     Th18: for I be unique-halt Program of S, J be halt-ending Program of S st ( CutLastLoc I) c= J holds ( CutLastLoc I) c= ( CutLastLoc J)

    proof

      let I be unique-halt Program of S, J be halt-ending Program of S such that

       A1: ( CutLastLoc I) c= J;

      

       A2: not ( halt S) in ( rng ( CutLastLoc I)) by COMPOS_1:def 11;

      (J . ( LastLoc J)) = ( halt S) by COMPOS_1:def 14;

      hence ( CutLastLoc I) c= ( CutLastLoc J) by A2, A1, Lm1;

    end;

    reserve I,J for MacroInstruction of S;

    theorem :: COMPOS_2:19

    for K be set st I <= J & J <= K holds I <= K

    proof

      let K be set such that

       A1: ( CutLastLoc I) c= J and

       A2: ( CutLastLoc J) c= K;

      ( CutLastLoc I) c= ( CutLastLoc J) by A1, Th18;

      hence ( CutLastLoc I) c= K by A2;

    end;

    theorem :: COMPOS_2:20

    

     Th20: for I be halt-ending Program of S holds I = (( CutLastLoc I) +* (( LastLoc I) .--> ( halt S)))

    proof

      let I be halt-ending Program of S;

      

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

      

       A2: {( LastLoc I)} misses ( dom ( CutLastLoc I)) by Th17, ZFMISC_1: 50;

      

       A3: ( dom (( LastLoc I) .--> (I . ( LastLoc I)))) = {( LastLoc I)};

      I = (( CutLastLoc I) \/ (( LastLoc I) .--> (I . ( LastLoc I)))) by A1, FUNCOP_1: 84, XBOOLE_1: 45

      .= (( CutLastLoc I) +* (( LastLoc I) .--> (I . ( LastLoc I)))) by A3, A2, FUNCT_4: 31;

      hence thesis by COMPOS_1:def 14;

    end;

    theorem :: COMPOS_2:21

    

     Th21: for I be halt-ending Program of S holds ( CutLastLoc I) = ( CutLastLoc J) implies I = J

    proof

      let I be halt-ending Program of S such that

       A1: ( CutLastLoc I) = ( CutLastLoc J);

      (( card I) - 1) = ( card ( CutLastLoc J)) by A1, VALUED_1: 38

      .= (( card J) - 1) by VALUED_1: 38;

      

      then ( LastLoc I) = (( card J) -' 1) by AFINSQ_1: 70

      .= ( LastLoc J) by AFINSQ_1: 70;

      

      hence I = (( CutLastLoc I) +* (( LastLoc J) .--> ( halt S))) by Th20

      .= J by A1, Th20;

    end;

    theorem :: COMPOS_2:22

    I <= J & J <= I implies I = J

    proof

      assume ( CutLastLoc I) c= J;

      then

       A1: ( CutLastLoc I) c= ( CutLastLoc J) by Th18;

      assume ( CutLastLoc J) c= I;

      then ( CutLastLoc J) c= ( CutLastLoc I) by Th18;

      then ( CutLastLoc I) = ( CutLastLoc J) by A1, XBOOLE_0:def 10;

      hence I = J by Th21;

    end;

    theorem :: COMPOS_2:23

    

     Th23: I <= (I ';' J)

    proof

      ( dom ( CutLastLoc I)) misses ( dom ( Reloc (J,(( card I) -' 1)))) by COMPOS_1: 18;

      hence ( CutLastLoc I) c= (I ';' J) by FUNCT_4: 32;

    end;

    theorem :: COMPOS_2:24

    for X be set st I c= X holds I <= X

    proof

      let X be set such that

       A1: I c= X;

      thus ( CutLastLoc I) c= X by A1;

    end;

    theorem :: COMPOS_2:25

    I <= J implies for X be set st J c= X holds I <= X

    proof

      assume

       A1: ( CutLastLoc I) c= J;

      let X be set;

      assume J c= X;

      hence ( CutLastLoc I) c= X by A1;

    end;

    theorem :: COMPOS_2:26

    

     Th26: for k be Nat holds k < ( LastLoc I) iff k in ( dom ( CutLastLoc I))

    proof

      let k be Nat;

      ( card I) > 0 ;

      then

       A1: ( card I) >= ( 0 + 1) by NAT_1: 13;

      ( card ( CutLastLoc I)) = (( card I) - 1) by VALUED_1: 38

      .= (( card I) -' 1) by A1, XREAL_1: 233

      .= ( LastLoc I) by AFINSQ_1: 70;

      hence thesis by AFINSQ_1: 86;

    end;

    theorem :: COMPOS_2:27

    

     Th27: for k be Nat st k < ( LastLoc I) holds (( CutLastLoc I) . k) = (I . k)

    proof

      let k be Nat;

      assume k < ( LastLoc I);

      then

       A1: k in ( dom ( CutLastLoc I)) by Th26;

      thus thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: COMPOS_2:28

    

     Th28: for k be Nat st k < ( LastLoc I) & I <= J holds (I . k) = (J . k)

    proof

      let k be Nat such that

       A1: k < ( LastLoc I);

      assume

       A2: ( CutLastLoc I) c= J;

      

       A3: k in ( dom ( CutLastLoc I)) by A1, Th26;

      

      thus (I . k) = (( CutLastLoc I) . k) by A1, Th27

      .= (J . k) by A2, A3, GRFUNC_1: 2;

    end;

    ::$Canceled

    theorem :: COMPOS_2:30

    

     Th29: ( LastLoc ( Macro i)) = 1

    proof

      

      thus ( LastLoc ( Macro i)) = (( card ( Macro i)) - 1) by AFINSQ_1: 91

      .= (2 - 1) by COMPOS_1: 56

      .= 1;

    end;

    theorem :: COMPOS_2:31

    

     Th30: ( LastLoc (i ';' j)) = 2

    proof

      

      thus ( LastLoc (i ';' j)) = (( card (i ';' j)) - 1) by AFINSQ_1: 91

      .= (3 - 1) by Th12

      .= 2;

    end;

    theorem :: COMPOS_2:32

    

     Th31: ( LastLoc ((i ';' j) ';' k)) = 3

    proof

      

      thus ( LastLoc ((i ';' j) ';' k)) = (( card ((i ';' j) ';' k)) - 1) by AFINSQ_1: 91

      .= (4 - 1) by Th13

      .= 3;

    end;

    theorem :: COMPOS_2:33

    

     Th32: ( LastLoc (((i1 ';' i2) ';' i3) ';' i4)) = 4

    proof

      

      thus ( LastLoc (((i1 ';' i2) ';' i3) ';' i4)) = (( card (((i1 ';' i2) ';' i3) ';' i4)) - 1) by AFINSQ_1: 91

      .= (5 - 1) by Th14

      .= 4;

    end;

    theorem :: COMPOS_2:34

    

     Th33: ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 5

    proof

      

      thus ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = (( card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) - 1) by AFINSQ_1: 91

      .= (6 - 1) by Th15

      .= 5;

    end;

    theorem :: COMPOS_2:35

    

     Th34: ( LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6)) = 6

    proof

      

      thus ( LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6)) = (( card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6)) - 1) by AFINSQ_1: 91

      .= (7 - 1) by Th16

      .= 6;

    end;

    theorem :: COMPOS_2:36

    

     Th35: ((i ';' J) . 0 ) = i

    proof

      ( LastLoc ( Macro i)) = 1 by Th29;

      

      hence ((i ';' J) . 0 ) = (( Macro i) . 0 ) by Th23, Th28

      .= i by COMPOS_1: 58;

    end;

    theorem :: COMPOS_2:37

    

     Th36: (((i ';' j) ';' K) . 0 ) = i

    proof

      ( LastLoc (i ';' j)) = 2 by Th30;

      

      hence (((i ';' j) ';' K) . 0 ) = ((i ';' j) . 0 ) by Th23, Th28

      .= ((i ';' ( Macro j)) . 0 )

      .= i by Th35;

    end;

    theorem :: COMPOS_2:38

    

     Th37: ((((i ';' j) ';' k) ';' K) . 0 ) = i

    proof

      ( LastLoc ((i ';' j) ';' k)) = 3 by Th31;

      

      hence ((((i ';' j) ';' k) ';' K) . 0 ) = (((i ';' j) ';' k) . 0 ) by Th23, Th28

      .= (((i ';' j) ';' ( Macro k)) . 0 )

      .= i by Th36;

    end;

    theorem :: COMPOS_2:39

    

     Th38: (((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 ) = i1

    proof

      ( LastLoc (((i1 ';' i2) ';' i3) ';' i4)) = 4 by Th32;

      

      hence (((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 ) = ((((i1 ';' i2) ';' i3) ';' i4) . 0 ) by Th23, Th28

      .= ((((i1 ';' i2) ';' i3) ';' ( Macro i4)) . 0 )

      .= i1 by Th37;

    end;

    theorem :: COMPOS_2:40

    

     Th39: ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' K) . 0 ) = i1

    proof

      ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 5 by Th33;

      

      hence ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' K) . 0 ) = (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 0 ) by Th23, Th28

      .= (((((i1 ';' i2) ';' i3) ';' i4) ';' ( Macro i5)) . 0 )

      .= i1 by Th38;

    end;

    theorem :: COMPOS_2:41

    (((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) ';' K) . 0 ) = i1

    proof

      ( LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6)) = 6 by Th34;

      

      hence (((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) ';' K) . 0 ) = ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 0 ) by Th23, Th28

      .= ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' ( Macro i6)) . 0 )

      .= i1 by Th39;

    end;

    theorem :: COMPOS_2:42

    for k be Nat st k < ( LastLoc I) holds ((I ';' J) . k) = (I . k)

    proof

      let k be Nat;

      assume k < ( LastLoc I);

      then

       A1: k in ( dom ( CutLastLoc I)) by Th26;

      ( dom ( CutLastLoc I)) misses ( dom ( Reloc (J,(( card I) -' 1)))) by COMPOS_1: 18;

      then not k in ( dom ( Reloc (J,(( card I) -' 1)))) by A1, XBOOLE_0: 3;

      

      hence ((I ';' J) . k) = (( CutLastLoc I) . k) by FUNCT_4: 11

      .= (I . k) by A1, GRFUNC_1: 2;

    end;

    theorem :: COMPOS_2:43

    ( LastLoc (I ';' J)) = (( LastLoc I) + ( LastLoc J))

    proof

      

      thus ( LastLoc (I ';' J)) = (( card (I ';' J)) - 1) by AFINSQ_1: 91

      .= (((( card I) + ( card J)) - 1) - 1) by COMPOS_1: 20

      .= ((( card I) - 1) + (( card J) - 1))

      .= (( LastLoc I) + (( card J) - 1)) by AFINSQ_1: 91

      .= (( LastLoc I) + ( LastLoc J)) by AFINSQ_1: 91;

    end;

    theorem :: COMPOS_2:44

    

     Th43: for j be Nat st j <= ( LastLoc J) holds ((I ';' J) . (( LastLoc I) + j)) = ( IncAddr ((J /. j),( LastLoc I)))

    proof

      let j be Nat such that

       A1: j <= ( LastLoc J);

      set k = (( LastLoc I) + j);

      

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

      

       A3: j <= (( card J) - 1) by A1, AFINSQ_1: 91;

      (( card J) - 1) < ( card J) by XREAL_1: 44;

      then j < ( card J) by A3, XXREAL_0: 2;

      then

       A4: j in ( dom J) by AFINSQ_1: 86;

      then

       A5: j in ( dom ( IncAddr (J,( LastLoc I)))) by COMPOS_1:def 21;

      

       A6: (( LastLoc I) + j) in ( dom ( Reloc (J,( LastLoc I)))) by A4, COMPOS_1: 46;

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

      ((I ';' J) . (( LastLoc I) + j)) = (( Reloc (J,( LastLoc I))) . (( LastLoc I) + j)) by A6, A2, FUNCT_4: 13

      .= (( IncAddr (J,( LastLoc I))) . j) by A5, VALUED_1:def 12

      .= ( IncAddr ((J /. j),( LastLoc I))) by A4, COMPOS_1:def 21;

      hence thesis;

    end;

    theorem :: COMPOS_2:45

    

     Th44: ((i ';' j) . 1) = ( IncAddr (j,1))

    proof

       0 in ( dom ( Macro j)) by COMPOS_1: 57;

      

      then

       A1: (( Macro j) /. 0 ) = (( Macro j) . 0 ) by PARTFUN1:def 6

      .= j by COMPOS_1: 58;

      

       A2: ( LastLoc ( Macro j)) = 1 by Th29;

      

      thus ((i ';' j) . 1) = ((i ';' ( Macro j)) . (( LastLoc ( Macro i)) + 0 )) by Th29

      .= ( IncAddr ((( Macro j) /. 0 ),( LastLoc ( Macro i)))) by A2, Th43

      .= ( IncAddr (j,1)) by A1, Th29;

    end;

    theorem :: COMPOS_2:46

    

     Th45: (((i ';' j) ';' k) . 1) = ( IncAddr (j,1))

    proof

      ( LastLoc (i ';' j)) = 2 by Th30;

      

      hence (((i ';' j) ';' k) . 1) = ((i ';' j) . 1) by Th23, Th28

      .= ( IncAddr (j,1)) by Th44;

    end;

    theorem :: COMPOS_2:47

    

     Th46: ((((i1 ';' i2) ';' i3) ';' i4) . 1) = ( IncAddr (i2,1))

    proof

      ( LastLoc ((i1 ';' i2) ';' i3)) = 3 by Th31;

      

      hence ((((i1 ';' i2) ';' i3) ';' i4) . 1) = (((i1 ';' i2) ';' i3) . 1) by Th23, Th28

      .= ( IncAddr (i2,1)) by Th45;

    end;

    theorem :: COMPOS_2:48

    

     Th47: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1) = ( IncAddr (i2,1))

    proof

      ( LastLoc (((i1 ';' i2) ';' i3) ';' i4)) = 4 by Th32;

      

      hence (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1) = ((((i1 ';' i2) ';' i3) ';' i4) . 1) by Th23, Th28

      .= ( IncAddr (i2,1)) by Th46;

    end;

    theorem :: COMPOS_2:49

    ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 1) = ( IncAddr (i2,1))

    proof

      ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 5 by Th33;

      

      hence ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 1) = (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1) by Th23, Th28

      .= ( IncAddr (i2,1)) by Th47;

    end;

    theorem :: COMPOS_2:50

    

     Th49: ((I ';' j) . ( LastLoc I)) = ( IncAddr (j,( LastLoc I)))

    proof

      

       A1: 0 <= ( LastLoc ( Macro j));

       0 in ( dom ( Macro j)) by COMPOS_1: 57;

      

      then

       A2: (( Macro j) /. 0 ) = (( Macro j) . 0 ) by PARTFUN1:def 6

      .= j by COMPOS_1: 58;

      

      thus ((I ';' j) . ( LastLoc I)) = ((I ';' ( Macro j)) . (( LastLoc I) + 0 ))

      .= ( IncAddr ((( Macro j) /. 0 ),( LastLoc I))) by A1, Th43

      .= ( IncAddr (j,( LastLoc I))) by A2;

    end;

    theorem :: COMPOS_2:51

    

     Th50: (((i1 ';' i2) ';' i3) . 2) = ( IncAddr (i3,2))

    proof

      ( LastLoc (i1 ';' i2)) = 2 by Th30;

      hence thesis by Th49;

    end;

    theorem :: COMPOS_2:52

    

     Th51: ((((i1 ';' i2) ';' i3) ';' i4) . 2) = ( IncAddr (i3,2))

    proof

      ( LastLoc ((i1 ';' i2) ';' i3)) = 3 by Th31;

      

      hence ((((i1 ';' i2) ';' i3) ';' i4) . 2) = (((i1 ';' i2) ';' i3) . 2) by Th23, Th28

      .= ( IncAddr (i3,2)) by Th50;

    end;

    theorem :: COMPOS_2:53

    

     Th52: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2) = ( IncAddr (i3,2))

    proof

      ( LastLoc (((i1 ';' i2) ';' i3) ';' i4)) = 4 by Th32;

      

      hence (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2) = ((((i1 ';' i2) ';' i3) ';' i4) . 2) by Th23, Th28

      .= ( IncAddr (i3,2)) by Th51;

    end;

    theorem :: COMPOS_2:54

    ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 2) = ( IncAddr (i3,2))

    proof

      ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 5 by Th33;

      

      hence ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 2) = (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2) by Th23, Th28

      .= ( IncAddr (i3,2)) by Th52;

    end;

    theorem :: COMPOS_2:55

    

     Th54: ((((i1 ';' i2) ';' i3) ';' i4) . 3) = ( IncAddr (i4,3))

    proof

      ( LastLoc ((i1 ';' i2) ';' i3)) = 3 by Th31;

      hence thesis by Th49;

    end;

    theorem :: COMPOS_2:56

    

     Th55: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3) = ( IncAddr (i4,3))

    proof

      

       A1: ( LastLoc (((i1 ';' i2) ';' i3) ';' i4)) = 4 by Th32;

      

      thus (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3) = ((((i1 ';' i2) ';' i3) ';' i4) . 3) by Th23, A1, Th28

      .= ( IncAddr (i4,3)) by Th54;

    end;

    theorem :: COMPOS_2:57

    ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 3) = ( IncAddr (i4,3))

    proof

      

       A1: ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 5 by Th33;

      

      thus ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 3) = (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3) by Th23, A1, Th28

      .= ( IncAddr (i4,3)) by Th55;

    end;

    theorem :: COMPOS_2:58

    

     Th57: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4) = ( IncAddr (i5,4))

    proof

      ( LastLoc (((i1 ';' i2) ';' i3) ';' i4)) = 4 by Th32;

      hence thesis by Th49;

    end;

    theorem :: COMPOS_2:59

    ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 4) = ( IncAddr (i5,4))

    proof

      

       A1: ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 5 by Th33;

      

      thus ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 4) = (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4) by Th23, A1, Th28

      .= ( IncAddr (i5,4)) by Th57;

    end;

    theorem :: COMPOS_2:60

    ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5) = ( IncAddr (i6,5))

    proof

      ( LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) = 5 by Th33;

      hence thesis by Th49;

    end;

    definition

      let S;

      let I be preProgram of S;

      :: COMPOS_2:def5

      attr I is closed means

      : Def5: for i be Instruction of S st i in ( rng I) holds ( rng ( JumpPart i)) c= ( dom I);

    end

    registration

      let S;

      cluster ( Stop S) -> closed;

      coherence

      proof

        let i be Instruction of S;

        assume

         A1: i in ( rng ( Stop S));

        ( rng ( Stop S)) = {( halt S)} by AFINSQ_1: 33;

        then i = ( halt S) by A1, TARSKI:def 1;

        then ( rng ( JumpPart i)) = {} ;

        hence ( rng ( JumpPart i)) c= ( dom ( Stop S));

      end;

    end

    registration

      let S;

      cluster closed for MacroInstruction of S;

      existence

      proof

        take ( Stop S);

        thus thesis;

      end;

    end

    theorem :: COMPOS_2:61

    for i be No-StopCode Instruction of S st i is ins-loc-free holds ( Macro i) is closed

    proof

      let i be No-StopCode Instruction of S such that

       A1: i is ins-loc-free;

      let i1 be Instruction of S;

      assume i1 in ( rng ( Macro i));

      then i1 in {i, ( halt S)} by COMPOS_1: 67;

      then i1 = i or i1 = ( halt S) by TARSKI:def 2;

      then ( rng ( JumpPart i1)) = {} by A1;

      hence ( rng ( JumpPart i1)) c= ( dom ( Macro i));

    end;

    registration

      let S;

      let I be closed MacroInstruction of S, k be Nat;

      cluster ( Reloc (I,k)) -> closed;

      coherence

      proof

        let i be Instruction of S;

        assume i in ( rng ( Reloc (I,k)));

        then

        consider n be object such that

         A1: n in ( dom ( Reloc (I,k))) and

         A2: (( Reloc (I,k)) . n) = i by FUNCT_1:def 3;

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

        then

        reconsider n as Nat by A1;

        

         A3: ( dom ( Reloc (I,k))) = ( dom ( Shift (I,k))) by COMPOS_1: 32;

        then

        consider j be Nat such that

         A4: j in ( dom I) and

         A5: n = (j + k) by A1, VALUED_1: 39;

        (I . j) = (I /. j) by A4, PARTFUN1:def 6;

        then

        reconsider i1 = (I . j) as Instruction of S;

        

         A6: ( IncAddr (i1,k)) = i by A2, A4, A5, COMPOS_1: 35;

        let x be object;

        assume

         A7: x in ( rng ( JumpPart i));

        then

        consider y be object such that

         A8: y in ( dom ( JumpPart i)) and

         A9: (( JumpPart i) . y) = x by FUNCT_1:def 3;

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

        then

        reconsider y as Nat by A8;

        

         A10: ( JumpPart i) = (( JumpPart i1) + k) by A6, COMPOS_0:def 9;

        then

         A11: ( dom ( JumpPart i)) = ( dom ( JumpPart i1)) by VALUED_1:def 2;

        ( rng ( JumpPart i)) c= NAT by RELAT_1:def 19;

        then

        reconsider m = x as Nat by A7;

        reconsider n = (( JumpPart i1) . y) as Nat;

        

         A12: m = (n + k) by A9, A10, A8, VALUED_1:def 2;

        

         A13: n in ( rng ( JumpPart i1)) by A8, A11, FUNCT_1: 3;

        i1 in ( rng I) by A4, FUNCT_1: 3;

        then ( rng ( JumpPart i1)) c= ( dom I) by Def5;

        hence x in ( dom ( Reloc (I,k))) by A3, A12, A13, VALUED_1: 24;

      end;

    end

    registration

      let S;

      let I,J be closed MacroInstruction of S;

      cluster (I ';' J) -> closed;

      coherence

      proof

        let i be Instruction of S such that

         A1: i in ( rng (I ';' J));

        ( rng (I ';' J)) c= (( rng ( CutLastLoc I)) \/ ( rng ( Reloc (J,(( card I) -' 1))))) by FUNCT_4: 17;

        per cases by A1, XBOOLE_0:def 3;

          suppose

           A2: i in ( rng ( CutLastLoc I));

          ( rng ( CutLastLoc I)) c= ( rng I) by RELAT_1: 11;

          then

           A3: ( rng ( JumpPart i)) c= ( dom I) by A2, Def5;

          ( dom I) c= ( dom (I ';' J)) by COMPOS_1: 21;

          hence ( rng ( JumpPart i)) c= ( dom (I ';' J)) by A3;

        end;

          suppose i in ( rng ( Reloc (J,(( card I) -' 1))));

          then

           A4: ( rng ( JumpPart i)) c= ( dom ( Reloc (J,(( card I) -' 1)))) by Def5;

          ( dom ( Reloc (J,(( card I) -' 1)))) c= ( dom (I ';' J)) by FUNCT_4: 10;

          hence ( rng ( JumpPart i)) c= ( dom (I ';' J)) by A4;

        end;

      end;

    end

    registration

      let S;

      cluster halt-free for Program of S;

      existence

      proof

        set i = the No-StopCode Instruction of S;

        take ( Load i);

        

         A1: ( rng ( Load i)) = {i} by AFINSQ_1: 33;

        now

          assume ( halt S) in ( rng ( Load i));

          then ( halt S) = i by A1, TARSKI:def 1;

          hence contradiction by COMPOS_0:def 12;

        end;

        hence ( Load i) is halt-free;

      end;

    end

    registration

      let S;

      let I,J be halt-free Program of S;

      cluster (I ^ J) -> halt-free;

      coherence

      proof

        set P = (I ^ J);

        

         A1: not ( halt S) in ( rng I) by COMPOS_1:def 11;

        

         A2: not ( halt S) in ( rng J) by COMPOS_1:def 11;

        ( rng P) = (( rng I) \/ ( rng J)) by AFINSQ_1: 26;

        then not ( halt S) in ( rng P) by A1, A2, XBOOLE_0:def 3;

        hence P is halt-free;

      end;

    end

    registration

      let S;

      let i be No-StopCode Instruction of S;

      cluster ( Load i) -> halt-free;

      coherence

      proof

        

         A1: ( rng ( Load i)) = {i} by AFINSQ_1: 33;

        now

          assume ( halt S) in ( rng ( Load i));

          then ( halt S) = i by A1, TARSKI:def 1;

          hence contradiction by COMPOS_0:def 12;

        end;

        hence ( Load i) is halt-free;

      end;

    end