sfmastr3.miz



    begin

    reserve s for State of SCM+FSA ,

a,c for read-write Int-Location,

aa,bb,cc,dd,x for Int-Location,

f for FinSeq-Location,

I,J for MacroInstruction of SCM+FSA ,

Ig for good MacroInstruction of SCM+FSA ,

i,k for Nat,

p for Instruction-Sequence of SCM+FSA ;

    ::$Canceled

    theorem :: SFMASTR3:2

    

     Th1: (s . ( intloc 0 )) = 1 implies ( DataPart ( IExec (( Stop SCM+FSA ),p,s))) = ( DataPart s)

    proof

      assume

       A1: (s . ( intloc 0 )) = 1;

      

      thus ( DataPart ( IExec (( Stop SCM+FSA ),p,s))) = ( DataPart ( Initialized s)) by SCMFSA8C: 14

      .= ( DataPart s) by A1, SCMFSA_M: 19;

    end;

    theorem :: SFMASTR3:3

    

     Th2: not ( Stop SCM+FSA ) refers aa

    proof

      

       A1: ( rng ( Stop SCM+FSA )) = {( halt SCM+FSA )} by AFINSQ_1: 33;

      let i be Instruction of SCM+FSA ;

      assume i in ( rng ( Stop SCM+FSA ));

      then i = ( halt SCM+FSA ) by A1, TARSKI:def 1;

      hence thesis;

    end;

    theorem :: SFMASTR3:4

    

     Th3: aa <> bb implies not (cc := bb) refers aa

    proof

      assume

       A1: aa <> bb;

      now

        let e be Int-Location;

        let l be Nat;

        let f be FinSeq-Location;

        thus (e := aa) <> (cc := bb) by A1, SF_MASTR: 1;

        

         A2: ( InsCode (cc := bb)) = 1 by SCMFSA_2: 18;

        hence ( AddTo (e,aa)) <> (cc := bb) by SCMFSA_2: 19;

        thus ( SubFrom (e,aa)) <> (cc := bb) by A2, SCMFSA_2: 20;

        thus ( MultBy (e,aa)) <> (cc := bb) by A2, SCMFSA_2: 21;

        thus ( Divide (aa,e)) <> (cc := bb) & ( Divide (e,aa)) <> (cc := bb) by A2, SCMFSA_2: 22;

        thus (aa =0_goto l) <> (cc := bb);

        thus (aa >0_goto l) <> (cc := bb);

        thus (e := (f,aa)) <> (cc := bb) by A2, SCMFSA_2: 26;

        thus ((f,e) := aa) <> (cc := bb) & ((f,aa) := e) <> (cc := bb) by A2, SCMFSA_2: 27;

        thus (f :=<0,...,0> aa) <> (cc := bb) by A2, SCMFSA_2: 29;

      end;

      hence thesis;

    end;

    theorem :: SFMASTR3:5

    

     Th4: (( Exec ((a := (f,bb)),s)) . a) = ((s . f) /. |.(s . bb).|)

    proof

      ex k be Nat st k = |.(s . bb).| & (( Exec ((a := (f,bb)),s)) . a) = ((s . f) /. k) by SCMFSA_2: 72;

      hence thesis;

    end;

    theorem :: SFMASTR3:6

    

     Th5: (( Exec (((f,aa) := bb),s)) . f) = ((s . f) +* ( |.(s . aa).|,(s . bb)))

    proof

      ex k be Nat st k = |.(s . aa).| & (( Exec (((f,aa) := bb),s)) . f) = ((s . f) +* (k,(s . bb))) by SCMFSA_2: 73;

      hence thesis;

    end;

    registration

      let a be read-write Int-Location, b be Int-Location, I,J be good MacroInstruction of SCM+FSA ;

      cluster ( if>0 (a,b,I,J)) -> good;

      coherence

      proof

        ( if>0 (a,b,I,J)) = (( SubFrom (a,b)) ";" ( if>0 (a,I,J))) by SCMFSA8B:def 5;

        hence thesis;

      end;

    end

    theorem :: SFMASTR3:7

    

     Th6: for I,J be MacroInstruction of SCM+FSA holds ( UsedILoc ( if>0 (aa,bb,I,J))) = (( {aa, bb} \/ ( UsedILoc I)) \/ ( UsedILoc J))

    proof

      let I,J be MacroInstruction of SCM+FSA ;

      set a = aa;

      

      thus ( UsedILoc ( if>0 (a,bb,I,J))) = ( UsedILoc (( SubFrom (a,bb)) ";" ( if>0 (a,I,J)))) by SCMFSA8B:def 5

      .= (( UsedIntLoc ( SubFrom (a,bb))) \/ ( UsedILoc ( if>0 (a,I,J)))) by SF_MASTR: 29

      .= ( {a, bb} \/ ( UsedILoc ( if>0 (a,I,J)))) by SF_MASTR: 14

      .= ( {a, bb} \/ (( {a} \/ ( UsedILoc I)) \/ ( UsedILoc J))) by SCMFSA9A: 9

      .= ( {a, bb} \/ ( {a} \/ (( UsedILoc I) \/ ( UsedILoc J)))) by XBOOLE_1: 4

      .= (( {a, bb} \/ {a}) \/ (( UsedILoc I) \/ ( UsedILoc J))) by XBOOLE_1: 4

      .= ( {a, bb} \/ (( UsedILoc I) \/ ( UsedILoc J))) by ZFMISC_1: 9

      .= (( {a, bb} \/ ( UsedILoc I)) \/ ( UsedILoc J)) by XBOOLE_1: 4;

    end;

    ::$Canceled

    theorem :: SFMASTR3:9

    

     Th7: for I,J be really-closed MacroInstruction of SCM+FSA holds cc <> aa & not I destroys cc & not J destroys cc implies not ( if>0 (aa,bb,I,J)) destroys cc

    proof

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      assume that

       A1: cc <> aa and

       A2: not I destroys cc & not J destroys cc;

      ( if>0 (aa,bb,I,J)) = (( SubFrom (aa,bb)) ";" ( if>0 (aa,I,J))) & not ( if>0 (aa,I,J)) destroys cc by A2, SCMFSA8B:def 5, SCMFSA8C: 88;

      hence thesis by A1, SCMFSA7B: 8, SCMFSA8C: 53;

    end;

    begin

    definition

      let p;

      let a,b,c be Int-Location, I be MacroInstruction of SCM+FSA , s be State of SCM+FSA ;

      :: SFMASTR3:def1

      func StepForUp (a,b,c,I,p,s) -> sequence of ( product ( the_Values_of SCM+FSA )) equals ( StepWhile>0 ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),( intloc 0 )))),p,((s +* ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),(((s . c) - (s . b)) + 1))) +* (a,(s . b)))));

      coherence ;

    end

    theorem :: SFMASTR3:10

    

     Th8: (s . ( intloc 0 )) = 1 implies ((( StepForUp (a,bb,cc,I,p,s)) . 0 ) . ( intloc 0 )) = 1

    proof

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set S = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      

       A1: (S . ( intloc 0 )) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . ( intloc 0 )) by FUNCT_7: 32

      .= (s . ( intloc 0 )) by FUNCT_7: 32;

      assume (s . ( intloc 0 )) = 1;

      hence thesis by A1, SCMFSA_9:def 5;

    end;

    theorem :: SFMASTR3:11

    

     Th9: ((( StepForUp (a,bb,cc,I,p,s)) . 0 ) . a) = (s . bb)

    proof

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set S = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      (( StepWhile>0 (aux,((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 )))),p,S)) . 0 ) = S & a in ( dom (s +* (aux,(((s . cc) - (s . bb)) + 1)))) by SCMFSA_2: 42, SCMFSA_9:def 5;

      hence thesis by FUNCT_7: 31;

    end;

    theorem :: SFMASTR3:12

    

     Th10: a <> bb implies ((( StepForUp (a,bb,cc,I,p,s)) . 0 ) . bb) = (s . bb)

    proof

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set S = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      bb in {a, bb, cc} by ENUMSET1:def 1;

      then bb in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A1: bb <> aux by SCMFSA_M: 25;

      assume a <> bb;

      

      then (S . bb) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . bb) by FUNCT_7: 32

      .= (s . bb) by A1, FUNCT_7: 32;

      hence thesis by SCMFSA_9:def 5;

    end;

    theorem :: SFMASTR3:13

    

     Th11: a <> cc implies ((( StepForUp (a,bb,cc,I,p,s)) . 0 ) . cc) = (s . cc)

    proof

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set S = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      cc in {a, bb, cc} by ENUMSET1:def 1;

      then cc in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A1: cc <> aux by SCMFSA_M: 25;

      assume a <> cc;

      

      then (S . cc) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . cc) by FUNCT_7: 32

      .= (s . cc) by A1, FUNCT_7: 32;

      hence thesis by SCMFSA_9:def 5;

    end;

    theorem :: SFMASTR3:14

    

     Th12: a <> dd & dd in ( UsedILoc I) implies ((( StepForUp (a,bb,cc,I,p,s)) . 0 ) . dd) = (s . dd)

    proof

      assume that

       A1: a <> dd and

       A2: dd in ( UsedILoc I);

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      dd in ( {a, bb, cc} \/ ( UsedILoc I)) by A2, XBOOLE_0:def 3;

      then

       A3: dd <> aux by SCMFSA_M: 25;

      set S = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      (S . dd) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . dd) by A1, FUNCT_7: 32

      .= (s . dd) by A3, FUNCT_7: 32;

      hence thesis by SCMFSA_9:def 5;

    end;

    theorem :: SFMASTR3:15

    

     Th13: ((( StepForUp (a,bb,cc,I,p,s)) . 0 ) . f) = (s . f)

    proof

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set S = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      (S . f) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . f) by FUNCT_7: 32, SCMFSA_2: 58

      .= (s . f) by FUNCT_7: 32, SCMFSA_2: 58;

      hence thesis by SCMFSA_9:def 5;

    end;

    theorem :: SFMASTR3:16

    

     Th14: (s . ( intloc 0 )) = 1 implies for aux be read-write Int-Location st aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))) holds ( DataPart ( IExec (((((aux := cc) ";" ( SubFrom (aux,bb))) ";" ( AddTo (aux,( intloc 0 )))) ";" (a := bb)),p,s))) = ( DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))

    proof

      assume

       A1: (s . ( intloc 0 )) = 1;

      cc = ( intloc 0 ) or cc is read-write by SCMFSA_M:def 2;

      then

       A2: (( Initialized s) . cc) = (s . cc) by A1, SCMFSA_M: 9, SCMFSA_M: 37;

      set i3 = (a := bb);

      let aux be read-write Int-Location such that

       A3: aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      bb in {a, bb, cc} by ENUMSET1:def 1;

      then bb in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A4: bb <> aux by A3, SCMFSA_M: 25;

      set s2 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      

       A5: aux in ( dom s) by SCMFSA_2: 42;

      a in {a, bb, cc} by ENUMSET1:def 1;

      then a in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A6: a <> aux by A3, SCMFSA_M: 25;

      

      then

       A7: (s2 . aux) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . aux) by FUNCT_7: 32

      .= (((s . cc) - (s . bb)) + 1) by A5, FUNCT_7: 31;

      set i2 = ( AddTo (aux,( intloc 0 )));

      set i1 = ( SubFrom (aux,bb));

      set i0 = (aux := cc);

      set s1 = ( IExec ((((i0 ";" i1) ";" i2) ";" i3),p,s));

      

       A8: (( IExec ((i0 ";" i1),p,s)) . ( intloc 0 )) = (( Exec (i1,( Exec (i0,( Initialized s))))) . ( intloc 0 )) by SCMFSA6C: 8

      .= (( Exec (i0,( Initialized s))) . ( intloc 0 )) by SCMFSA_2: 65

      .= (( Initialized s) . ( intloc 0 )) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      

       A9: a in ( dom (s +* (aux,(((s . cc) - (s . bb)) + 1)))) by SCMFSA_2: 42;

      bb = ( intloc 0 ) or bb is read-write by SCMFSA_M:def 2;

      then

       A10: (( Initialized s) . bb) = (s . bb) by A1, SCMFSA_M: 9, SCMFSA_M: 37;

      

       A11: (s1 . a) = (( Exec (i3,( IExec (((i0 ";" i1) ";" i2),p,s)))) . a) by SCMFSA6C: 6

      .= (( IExec (((i0 ";" i1) ";" i2),p,s)) . bb) by SCMFSA_2: 63

      .= (( Exec (i2,( IExec ((i0 ";" i1),p,s)))) . bb) by SCMFSA6C: 6

      .= (( IExec ((i0 ";" i1),p,s)) . bb) by A4, SCMFSA_2: 64

      .= (( Exec (i1,( Exec (i0,( Initialized s))))) . bb) by SCMFSA6C: 8

      .= (( Exec (i0,( Initialized s))) . bb) by A4, SCMFSA_2: 65

      .= (s . bb) by A4, A10, SCMFSA_2: 63;

      

       A12: (s1 . aux) = (( Exec (i3,( IExec (((i0 ";" i1) ";" i2),p,s)))) . aux) by SCMFSA6C: 6

      .= (( IExec (((i0 ";" i1) ";" i2),p,s)) . aux) by A6, SCMFSA_2: 63

      .= (( Exec (i2,( IExec ((i0 ";" i1),p,s)))) . aux) by SCMFSA6C: 6

      .= ((( IExec ((i0 ";" i1),p,s)) . aux) + 1) by A8, SCMFSA_2: 64

      .= ((( Exec (i1,( Exec (i0,( Initialized s))))) . aux) + 1) by SCMFSA6C: 8

      .= (((( Exec (i0,( Initialized s))) . aux) - (( Exec (i0,( Initialized s))) . bb)) + 1) by SCMFSA_2: 65

      .= (((( Initialized s) . cc) - (( Exec (i0,( Initialized s))) . bb)) + 1) by SCMFSA_2: 63

      .= (((s . cc) - (s . bb)) + 1) by A4, A2, A10, SCMFSA_2: 63;

      now

        hereby

          let x be Int-Location;

          per cases ;

            suppose x = a;

            hence (s1 . x) = (s2 . x) by A11, A9, FUNCT_7: 31;

          end;

            suppose x = aux;

            hence (s1 . x) = (s2 . x) by A12, A7;

          end;

            suppose

             A13: x <> aux & x <> a;

            

            then

             A14: (s2 . x) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . x) by FUNCT_7: 32

            .= (s . x) by A13, FUNCT_7: 32;

            

             A15: x = ( intloc 0 ) or x is read-write by SCMFSA_M:def 2;

            (s1 . x) = (( Exec (i3,( IExec (((i0 ";" i1) ";" i2),p,s)))) . x) by SCMFSA6C: 6

            .= (( IExec (((i0 ";" i1) ";" i2),p,s)) . x) by A13, SCMFSA_2: 63

            .= (( Exec (i2,( IExec ((i0 ";" i1),p,s)))) . x) by SCMFSA6C: 6

            .= (( IExec ((i0 ";" i1),p,s)) . x) by A13, SCMFSA_2: 64

            .= (( Exec (i1,( Exec (i0,( Initialized s))))) . x) by SCMFSA6C: 8

            .= (( Exec (i0,( Initialized s))) . x) by A13, SCMFSA_2: 65

            .= (( Initialized s) . x) by A13, SCMFSA_2: 63

            .= (s . x) by A1, A15, SCMFSA_M: 9, SCMFSA_M: 37;

            hence (s1 . x) = (s2 . x) by A14;

          end;

        end;

        let x be FinSeq-Location;

        

        thus (s1 . x) = (( Exec (i3,( IExec (((i0 ";" i1) ";" i2),p,s)))) . x) by SCMFSA6C: 7

        .= (( IExec (((i0 ";" i1) ";" i2),p,s)) . x) by SCMFSA_2: 63

        .= (( Exec (i2,( IExec ((i0 ";" i1),p,s)))) . x) by SCMFSA6C: 7

        .= (( IExec ((i0 ";" i1),p,s)) . x) by SCMFSA_2: 64

        .= (( Exec (i1,( Exec (i0,( Initialized s))))) . x) by SCMFSA6C: 9

        .= (( Exec (i0,( Initialized s))) . x) by SCMFSA_2: 65

        .= (( Initialized s) . x) by SCMFSA_2: 63

        .= (s . x) by SCMFSA_M: 37

        .= ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . x) by FUNCT_7: 32, SCMFSA_2: 58

        .= (s2 . x) by FUNCT_7: 32, SCMFSA_2: 58;

      end;

      hence thesis by SCMFSA_M: 2;

    end;

    definition

      let p;

      let a,b,c be Int-Location, I be MacroInstruction of SCM+FSA , s be State of SCM+FSA ;

      :: SFMASTR3:def2

      pred ProperForUpBody a,b,c,I,s,p means for i be Nat st i < (((s . c) - (s . b)) + 1) holds I is_halting_on ((( StepForUp (a,b,c,I,p,s)) . i),(p +* ( while>0 ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),( intloc 0 ))))))));

    end

    theorem :: SFMASTR3:17

    

     Th15: for I be parahalting MacroInstruction of SCM+FSA holds ProperForUpBody (aa,bb,cc,I,s,p) by SCMFSA7B: 19;

    theorem :: SFMASTR3:18

    

     Th16: for Ig be good really-closed MacroInstruction of SCM+FSA holds ((( StepForUp (a,bb,cc,Ig,p,s)) . k) . ( intloc 0 )) = 1 & Ig is_halting_on ((( StepForUp (a,bb,cc,Ig,p,s)) . k),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc Ig))),((Ig ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc Ig))),( intloc 0 )))))))) implies ((( StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . ( intloc 0 )) = 1

    proof

      let Ig be good really-closed MacroInstruction of SCM+FSA ;

      set I = Ig;

      assume that

       A1: ((( StepForUp (a,bb,cc,I,p,s)) . k) . ( intloc 0 )) = 1 and

       A2: I is_halting_on ((( StepForUp (a,bb,cc,I,p,s)) . k),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 ))))))));

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set SW2 = ( StepWhile>0 (aux,IB,p,((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))));

      

       A3: IB = (I ";" (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 ))))) by SCMFSA6A: 28;

      per cases ;

        suppose ((SW2 . k) . aux) <= 0 ;

        then ( DataPart (SW2 . (k + 1))) = ( DataPart (SW2 . k)) by SCMFSA9A: 31;

        hence thesis by A1, SCMFSA_M: 2;

      end;

        suppose

         A4: ((SW2 . k) . aux) > 0 ;

        

         A5: I is_halting_on (( Initialized (SW2 . k)),(p +* ( while>0 (aux,IB)))) by A1, A2, SCMFSA8B: 42;

        (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 )))) is_halting_on (( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))),(p +* ( while>0 (aux,IB)))) by SCMFSA7B: 19;

        then

         A6: ( DataPart (SW2 . (k + 1))) = ( DataPart ( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k)))) by A1, A3, A4, A5, SCMFSA9A: 32, SFMASTR1: 3;

        (( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k))) . ( intloc 0 )) = (( IExec ((( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 )))),(p +* ( while>0 (aux,IB))),( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))))) . ( intloc 0 )) by A3, A5, SFMASTR1: 7

        .= (( Exec (( SubFrom (aux,( intloc 0 ))),( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))))) . ( intloc 0 )) by SCMFSA6C: 8

        .= (( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))) . ( intloc 0 )) by SCMFSA_2: 65

        .= (( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))) . ( intloc 0 )) by SCMFSA_2: 64

        .= 1 by SCMFSA_M: 9;

        hence thesis by A6, SCMFSA_M: 2;

      end;

    end;

    theorem :: SFMASTR3:19

    

     Th17: for Ig be good really-closed MacroInstruction of SCM+FSA holds (s . ( intloc 0 )) = 1 & ProperForUpBody (a,bb,cc,Ig,s,p) implies for k st k <= (((s . cc) - (s . bb)) + 1) holds ((( StepForUp (a,bb,cc,Ig,p,s)) . k) . ( intloc 0 )) = 1 & ( not Ig destroys a implies ((( StepForUp (a,bb,cc,Ig,p,s)) . k) . a) = (k + (s . bb)) & ((( StepForUp (a,bb,cc,Ig,p,s)) . k) . a) <= ((s . cc) + 1)) & (((( StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc Ig)))) + k) = (((s . cc) - (s . bb)) + 1)

    proof

      let Ig be good really-closed MacroInstruction of SCM+FSA ;

      set I = Ig;

      assume that

       A1: (s . ( intloc 0 )) = 1 and

       A2: ProperForUpBody (a,bb,cc,I,s,p);

      set scb1 = (((s . cc) - (s . bb)) + 1);

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set SF = ( StepForUp (a,bb,cc,I,p,s));

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set s2 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))), p2 = p;

      set SW2 = ( StepWhile>0 (aux,IB,p2,s2));

      

       A3: IB = (I ";" (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 ))))) by SCMFSA6A: 28;

      defpred P[ Nat] means $1 <= scb1 implies ((SF . $1) . ( intloc 0 )) = 1 & ( not I destroys a implies ((SF . $1) . a) = ($1 + (s . bb)) & ((SF . $1) . a) <= ((s . cc) + 1)) & (((SF . $1) . aux) + $1) = scb1;

      a in {a, bb, cc} by ENUMSET1:def 1;

      then a in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A4: aux <> a by SCMFSA_M: 25;

      

       A5: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A6: P[k];

        thus P[(k + 1)]

        proof

          

           A7: not aux in ( UsedILoc I)

          proof

            assume not thesis;

            then aux in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

            hence contradiction by SCMFSA_M: 25;

          end;

          set k1 = (k + 1);

          assume

           A8: (k + 1) <= scb1;

          

           A9: k < (k + 1) by XREAL_1: 29;

          then

           A10: ((SW2 . k) . aux) > 0 by A6, A8, XREAL_1: 8, XXREAL_0: 2;

          

           A11: k < scb1 by A8, A9, XXREAL_0: 2;

          

           A12: I is_halting_on ((SF . k),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 )))))))) by A2, A11;

          then

           A13: I is_halting_on (( Initialized (SW2 . k)),(p +* ( while>0 (aux,IB)))) by A6, A8, A9, SCMFSA8B: 42, XXREAL_0: 2;

          thus ((SF . k1) . ( intloc 0 )) = 1 by A6, A8, A9, A12, Th16, XXREAL_0: 2;

          (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 )))) is_halting_on (( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))),(p +* ( while>0 (aux,IB)))) by SCMFSA7B: 19;

          then IB is_halting_on (( Initialized (SW2 . k)),(p +* ( while>0 (aux,IB)))) by A3, A13, SFMASTR1: 3;

          then

           A14: ( DataPart (SW2 . (k + 1))) = ( DataPart ( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k)))) by A6, A8, A9, A10, SCMFSA9A: 32, XXREAL_0: 2;

          hereby

            assume

             A15: not I destroys a;

            

             A16: (( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k))) . a) = (( IExec ((( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 )))),(p +* ( while>0 (aux,IB))),( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))))) . a) by A3, A13, SFMASTR1: 7

            .= (( Exec (( SubFrom (aux,( intloc 0 ))),( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))))) . a) by SCMFSA6C: 8

            .= (( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))) . a) by A4, SCMFSA_2: 65

            .= ((( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))) . a) + (( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))) . ( intloc 0 ))) by SCMFSA_2: 64

            .= ((( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))) . a) + 1) by SCMFSA_M: 9

            .= ((( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))) . a) + 1) by SCMFSA_M: 37

            .= ((( Initialized (SW2 . k)) . a) + 1) by A13, A15, SCMFSA8C: 95

            .= (((SW2 . k) . a) + 1) by SCMFSA_M: 37;

            hence ((SF . k1) . a) = (k1 + (s . bb)) by A6, A8, A9, A14, A15, SCMFSA_M: 2, XXREAL_0: 2;

            (k1 + (s . bb)) <= ((((s . cc) + 1) - (s . bb)) + (s . bb)) by A8, XREAL_1: 6;

            hence ((SF . k1) . a) <= ((s . cc) + 1) by A6, A8, A9, A14, A15, A16, SCMFSA_M: 2, XXREAL_0: 2;

          end;

          (( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k))) . aux) = (( IExec ((( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 )))),(p +* ( while>0 (aux,IB))),( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))))) . aux) by A3, A13, SFMASTR1: 7

          .= (( Exec (( SubFrom (aux,( intloc 0 ))),( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))))) . aux) by SCMFSA6C: 8

          .= ((( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))) . aux) - (( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))) . ( intloc 0 ))) by SCMFSA_2: 65

          .= ((( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))) . aux) - (( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))) . ( intloc 0 ))) by SCMFSA_2: 64

          .= ((( Exec (( AddTo (a,( intloc 0 ))),( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))))) . aux) - 1) by SCMFSA_M: 9

          .= ((( Initialized ( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k)))) . aux) - 1) by A4, SCMFSA_2: 64

          .= ((( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))) . aux) - 1) by SCMFSA_M: 37

          .= ((( Initialized (SW2 . k)) . aux) - 1) by A13, A7, SCMFSA8C: 95, SFMASTR1: 1

          .= (((SW2 . k) . aux) - 1) by SCMFSA_M: 37;

          

          hence (((SF . k1) . aux) + k1) = ((((SW2 . k) . aux) - 1) + k1) by A14, SCMFSA_M: 2

          .= scb1 by A6, A8, A9, XXREAL_0: 2;

        end;

      end;

      

       A17: a in ( dom (s +* (aux,(((s . cc) - (s . bb)) + 1)))) by SCMFSA_2: 42;

      

       A18: aux in ( dom s) by SCMFSA_2: 42;

      

       A19: P[ 0 ]

      proof

        assume

         A20: 0 <= scb1;

        

         A21: (SW2 . 0 ) = s2 by SCMFSA_9:def 5;

        

        hence ((SF . 0 ) . ( intloc 0 )) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . ( intloc 0 )) by FUNCT_7: 32

        .= 1 by A1, FUNCT_7: 32;

        hereby

          assume not I destroys a;

          thus ((SF . 0 ) . a) = ( 0 + (s . bb)) by A17, A21, FUNCT_7: 31;

          ( 0 + (s . bb)) <= ((((s . cc) + 1) - (s . bb)) + (s . bb)) by A20, XREAL_1: 6;

          hence ((SF . 0 ) . a) <= ((s . cc) + 1) by A17, A21, FUNCT_7: 31;

        end;

        

        thus (((SF . 0 ) . aux) + 0 ) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . aux) by A4, A21, FUNCT_7: 32

        .= scb1 by A18, FUNCT_7: 31;

      end;

      thus for k holds P[k] from NAT_1:sch 2( A19, A5);

    end;

    theorem :: SFMASTR3:20

    

     Th18: for Ig be good really-closed MacroInstruction of SCM+FSA holds (s . ( intloc 0 )) = 1 & ProperForUpBody (a,bb,cc,Ig,s,p) implies for k holds ((( StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc Ig)))) > 0 iff k < (((s . cc) - (s . bb)) + 1)

    proof

      let Ig be good really-closed MacroInstruction of SCM+FSA ;

      set I = Ig;

      set SF = ( StepForUp (a,bb,cc,I,p,s));

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set s2 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))), p2 = p;

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set SW2 = ( StepWhile>0 (aux,IB,p2,s2));

      set scb1 = (((s . cc) - (s . bb)) + 1);

      defpred P[ Nat] means ((SF . $1) . aux) > 0 implies $1 < scb1;

      assume

       A1: (s . ( intloc 0 )) = 1 & ProperForUpBody (a,bb,cc,I,s,p);

      

       A2: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A3: P[k] and

         A4: ((SF . (k + 1)) . aux) > 0 ;

        

         A5: ((SF . k) . aux) > 0

        proof

          assume

           A6: ((SF . k) . aux) <= 0 ;

          then ( DataPart (SF . (k + 1))) = ( DataPart (SF . k)) by SCMFSA9A: 31;

          hence contradiction by A4, A6, SCMFSA_M: 2;

        end;

        then

        reconsider scb1 as Element of NAT by A3, INT_1: 3;

        assume (k + 1) >= (((s . cc) - (s . bb)) + 1);

        then

         A7: (((SF . (k + 1)) . aux) + (k + 1)) > ( 0 + scb1) by A4, XREAL_1: 8;

        (k + 1) <= scb1 by A3, A5, NAT_1: 13;

        hence contradiction by A1, A7, Th17;

      end;

      let k;

      a in {a, bb, cc} by ENUMSET1:def 1;

      then a in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A8: aux <> a by SCMFSA_M: 25;

      

       A9: aux in ( dom s) by SCMFSA_2: 42;

      

       A10: P[ 0 ]

      proof

        (SW2 . 0 ) = s2 by SCMFSA_9:def 5;

        

        then

         A11: ((SF . 0 ) . aux) = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . aux) by A8, FUNCT_7: 32

        .= scb1 by A9, FUNCT_7: 31;

        assume ((SF . 0 ) . aux) > 0 ;

        hence thesis by A11;

      end;

      for k holds P[k] from NAT_1:sch 2( A10, A2);

      hence P[k];

      assume

       A12: k < scb1;

      then

       A13: (k - k) < (scb1 - k) by XREAL_1: 9;

      (((SF . k) . aux) + k) = scb1 by A1, A12, Th17;

      hence thesis by A13;

    end;

    theorem :: SFMASTR3:21

    

     Th19: for Ig be good really-closed MacroInstruction of SCM+FSA holds (s . ( intloc 0 )) = 1 & ProperForUpBody (a,bb,cc,Ig,s,p) & k < (((s . cc) - (s . bb)) + 1) implies ((( StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (( {a, bb, cc} \/ ( UsedILoc Ig)) \/ FinSeq-Locations )) = (( IExec ((Ig ";" ( AddTo (a,( intloc 0 )))),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc Ig))),((Ig ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc Ig))),( intloc 0 ))))))),(( StepForUp (a,bb,cc,Ig,p,s)) . k))) | (( {a, bb, cc} \/ ( UsedILoc Ig)) \/ FinSeq-Locations ))

    proof

      let Ig be good really-closed MacroInstruction of SCM+FSA ;

      assume that

       A1: (s . ( intloc 0 )) = 1 and

       A2: ProperForUpBody (a,bb,cc,Ig,s,p) and

       A3: k < (((s . cc) - (s . bb)) + 1);

      set FL = FinSeq-Locations ;

      set I = Ig;

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set SF = ( StepForUp (a,bb,cc,I,p,s));

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set s2 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))), p2 = p;

      set SW2 = ( StepWhile>0 (aux,IB,p2,s2));

      

       A4: ((SW2 . k) . ( intloc 0 )) = 1 by A1, A2, A3, Th17;

      set scb1 = (((s . cc) - (s . bb)) + 1);

      

       A5: (((SF . k) . aux) + k) = scb1 by A1, A2, A3, Th17;

      

       A6: ((SW2 . k) . aux) > 0

      proof

        assume ((SW2 . k) . aux) <= 0 ;

        then (((SW2 . k) . aux) + k) < ( 0 + scb1) by A3, XREAL_1: 8;

        hence contradiction by A5;

      end;

      set S2 = ( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k)));

      set IB1 = (I ";" ( AddTo (a,( intloc 0 ))));

      set Iloc = ( {a, bb, cc} \/ ( UsedILoc I));

      set S1 = ( IExec (IB1,(p +* ( while>0 (aux,IB))),(SW2 . k)));

      I is_halting_on ((SF . k),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 )))))))) by A2, A3;

      then

       A7: I is_halting_on (( Initialized (SW2 . k)),(p +* ( while>0 (aux,IB)))) by A4, SCMFSA8B: 42;

      ( Macro ( AddTo (a,( intloc 0 )))) is_halting_on (( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))),(p +* ( while>0 (aux,IB)))) by SCMFSA7B: 19;

      then

       A8: IB1 is_halting_on (( Initialized (SW2 . k)),(p +* ( while>0 (aux,IB)))) by A7, SFMASTR1: 3;

      now

        hereby

          let x be Int-Location;

          assume x in Iloc;

          then

           A9: x <> aux by SCMFSA_M: 25;

          (S2 . x) = (( Exec (( SubFrom (aux,( intloc 0 ))),S1)) . x) by A8, SFMASTR1: 11

          .= (S1 . x) by A9, SCMFSA_2: 65;

          hence (S1 . x) = (S2 . x);

        end;

        let x be FinSeq-Location;

        (S2 . x) = (( Exec (( SubFrom (aux,( intloc 0 ))),S1)) . x) by A8, SFMASTR1: 12

        .= (S1 . x) by SCMFSA_2: 65;

        hence (S1 . x) = (S2 . x);

      end;

      then

       A10: (S1 | (Iloc \/ FL)) = (( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k))) | (Iloc \/ FL)) by SCMFSA_M: 28;

      

       A11: IB = (I ";" (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 ))))) by SCMFSA6A: 28;

      (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 )))) is_halting_on (( IExec (I,(p +* ( while>0 (aux,IB))),(SW2 . k))),(p +* ( while>0 (aux,IB)))) by SCMFSA7B: 19;

      then ( DataPart (SW2 . (k + 1))) = ( DataPart ( IExec (IB,(p +* ( while>0 (aux,IB))),(SW2 . k)))) by A4, A6, A7, A11, SCMFSA9A: 32, SFMASTR1: 3;

      hence thesis by A10, RELAT_1: 153, SCMFSA_2: 100, XBOOLE_1: 9;

    end;

    definition

      let a,b,c be Int-Location, I be MacroInstruction of SCM+FSA ;

      :: SFMASTR3:def3

      func for-up (a,b,c,I) -> MacroInstruction of SCM+FSA equals ((((((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))) := c) ";" ( SubFrom ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),b))) ";" ( AddTo ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),( intloc 0 )))) ";" (a := b)) ";" ( while>0 ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, b, c} \/ ( UsedILoc I))),( intloc 0 )))))));

      coherence ;

    end

    registration

      let a,b,c be Int-Location, I be really-closed MacroInstruction of SCM+FSA ;

      cluster ( for-up (a,b,c,I)) -> really-closed;

      coherence ;

    end

    reserve I for MacroInstruction of SCM+FSA ;

    theorem :: SFMASTR3:22

    

     Th20: ( {aa, bb, cc} \/ ( UsedILoc I)) c= ( UsedILoc ( for-up (aa,bb,cc,I)))

    proof

      set aux = (1 -stRWNotIn ( {aa, bb, cc} \/ ( UsedILoc I)));

      set i0 = (aux := cc);

      set i1 = ( SubFrom (aux,bb));

      set i2 = ( AddTo (aux,( intloc 0 )));

      set i3 = (aa := bb);

      set I4 = ( while>0 (aux,((I ";" ( AddTo (aa,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))))));

      

       A1: ( UsedILoc (((i0 ";" i1) ";" i2) ";" i3)) = (( UsedILoc ((i0 ";" i1) ";" i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 30

      .= ((( UsedILoc (i0 ";" i1)) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 30

      .= (((( UsedIntLoc i0) \/ ( UsedIntLoc i1)) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 31

      .= ((( {aux, cc} \/ ( UsedIntLoc i1)) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 14

      .= ((( {aux, cc} \/ {aux, bb}) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 14

      .= ((( {aux, cc} \/ {aux, bb}) \/ {aux, ( intloc 0 )}) \/ ( UsedIntLoc i3)) by SF_MASTR: 14

      .= ((( {aux, cc} \/ {aux, bb}) \/ {aux, ( intloc 0 )}) \/ {aa, bb}) by SF_MASTR: 14;

      let x be object;

      

       A2: ( UsedILoc I4) = ( {aux} \/ ( UsedILoc ((I ";" ( AddTo (aa,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 )))))) by SCMFSA9A: 24

      .= ( {aux} \/ (( UsedILoc (I ";" ( AddTo (aa,( intloc 0 ))))) \/ ( UsedIntLoc ( SubFrom (aux,( intloc 0 )))))) by SF_MASTR: 30

      .= ( {aux} \/ ((( UsedILoc I) \/ ( UsedIntLoc ( AddTo (aa,( intloc 0 ))))) \/ ( UsedIntLoc ( SubFrom (aux,( intloc 0 )))))) by SF_MASTR: 30

      .= ( {aux} \/ (( UsedILoc I) \/ (( UsedIntLoc ( AddTo (aa,( intloc 0 )))) \/ ( UsedIntLoc ( SubFrom (aux,( intloc 0 ))))))) by XBOOLE_1: 4

      .= (( UsedILoc I) \/ ( {aux} \/ (( UsedIntLoc ( AddTo (aa,( intloc 0 )))) \/ ( UsedIntLoc ( SubFrom (aux,( intloc 0 ))))))) by XBOOLE_1: 4;

      assume x in ( {aa, bb, cc} \/ ( UsedILoc I));

      then

       A3: x in {aa, bb, cc} or x in ( UsedILoc I) by XBOOLE_0:def 3;

      

       A4: ( UsedILoc ( for-up (aa,bb,cc,I))) = (( UsedILoc (((i0 ";" i1) ";" i2) ";" i3)) \/ ( UsedILoc I4)) by SF_MASTR: 27;

      per cases by A3, ENUMSET1:def 1;

        suppose x = aa;

        then x in {aa, bb} by TARSKI:def 2;

        then x in ( UsedILoc (((i0 ";" i1) ";" i2) ";" i3)) by A1, XBOOLE_0:def 3;

        hence thesis by A4, XBOOLE_0:def 3;

      end;

        suppose x = bb;

        then x in {aa, bb} by TARSKI:def 2;

        then x in ( UsedILoc (((i0 ";" i1) ";" i2) ";" i3)) by A1, XBOOLE_0:def 3;

        hence thesis by A4, XBOOLE_0:def 3;

      end;

        suppose x = cc;

        then x in {aux, cc} by TARSKI:def 2;

        then x in ( {aux, cc} \/ {aux, bb}) by XBOOLE_0:def 3;

        then x in (( {aux, cc} \/ {aux, bb}) \/ {aux, ( intloc 0 )}) by XBOOLE_0:def 3;

        then x in ((( {aux, cc} \/ {aux, bb}) \/ {aux, ( intloc 0 )}) \/ {aa, bb}) by XBOOLE_0:def 3;

        hence thesis by A1, A4, XBOOLE_0:def 3;

      end;

        suppose x in ( UsedILoc I);

        then x in ( UsedILoc I4) by A2, XBOOLE_0:def 3;

        hence thesis by A4, XBOOLE_0:def 3;

      end;

    end;

    registration

      let a be read-write Int-Location, b,c be Int-Location, I be good MacroInstruction of SCM+FSA ;

      cluster ( for-up (a,b,c,I)) -> good;

      coherence ;

    end

    theorem :: SFMASTR3:23

    

     Th21: a <> aa & aa <> (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))) & not I destroys aa implies not ( for-up (a,bb,cc,I)) destroys aa

    proof

      assume that

       A1: a <> aa and

       A2: aa <> (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))) and

       A3: not I destroys aa;

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set i2 = ( AddTo (aux,( intloc 0 )));

      

       A4: not i2 destroys aa by A2, SCMFSA7B: 7;

      set i3 = (a := bb);

      set i1 = ( SubFrom (aux,bb));

      set i0 = (aux := cc);

      set I03 = (((i0 ";" i1) ";" i2) ";" i3);

       not i0 destroys aa & not i1 destroys aa by A2, SCMFSA7B: 6, SCMFSA7B: 8;

      then not ((i0 ";" i1) ";" i2) destroys aa by A4, SCMFSA8C: 54, SCMFSA8C: 55;

      then

       A5: not I03 destroys aa by A1, SCMFSA7B: 6, SCMFSA8C: 54;

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set I4 = ( while>0 (aux,IB));

       not (I ";" ( AddTo (a,( intloc 0 )))) destroys aa by A1, A3, SCMFSA7B: 7, SCMFSA8C: 54;

      then not IB destroys aa by A2, SCMFSA7B: 8, SCMFSA8C: 54;

      then not I4 destroys aa by SCMFSA8C: 92;

      hence thesis by A5, SCMFSA8C: 52;

    end;

    theorem :: SFMASTR3:24

    

     Th22: for I be really-closed MacroInstruction of SCM+FSA holds (s . ( intloc 0 )) = 1 & (s . bb) > (s . cc) implies (for x st x <> a & x in ( {bb, cc} \/ ( UsedILoc I)) holds (( IExec (( for-up (a,bb,cc,I)),p,s)) . x) = (s . x)) & for f holds (( IExec (( for-up (a,bb,cc,I)),p,s)) . f) = (s . f)

    proof

      let I be really-closed MacroInstruction of SCM+FSA ;

      assume that

       A1: (s . ( intloc 0 )) = 1 and

       A2: (s . bb) > (s . cc);

      cc = ( intloc 0 ) or cc is read-write by SCMFSA_M:def 2;

      then

       A3: (( Initialized s) . cc) = (s . cc) by A1, SCMFSA_M: 9, SCMFSA_M: 37;

      set MI = ( for-up (a,bb,cc,I));

      set i3 = (a := bb);

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set i0 = (aux := cc);

      set i1 = ( SubFrom (aux,bb));

      set i2 = ( AddTo (aux,( intloc 0 )));

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set I4 = ( while>0 (aux,IB));

      set I03 = (((i0 ";" i1) ";" i2) ";" i3);

      set s1 = ( IExec (I03,p,s)), p1 = p;

      set s2 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)));

      

       A4: (( IExec ((i0 ";" i1),p,s)) . ( intloc 0 )) = (( Exec (i1,( Exec (i0,( Initialized s))))) . ( intloc 0 )) by SCMFSA6C: 8

      .= (( Exec (i0,( Initialized s))) . ( intloc 0 )) by SCMFSA_2: 65

      .= (( Initialized s) . ( intloc 0 )) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      bb = ( intloc 0 ) or bb is read-write by SCMFSA_M:def 2;

      then

       A5: (( Initialized s) . bb) = (s . bb) by A1, SCMFSA_M: 9, SCMFSA_M: 37;

      

       A6: (s1 . ( intloc 0 )) = (( Exec (i3,( IExec (((i0 ";" i1) ";" i2),p,s)))) . ( intloc 0 )) by SCMFSA6C: 6

      .= (( IExec (((i0 ";" i1) ";" i2),p,s)) . ( intloc 0 )) by SCMFSA_2: 63

      .= (( Exec (i2,( IExec ((i0 ";" i1),p,s)))) . ( intloc 0 )) by SCMFSA6C: 6

      .= 1 by A4, SCMFSA_2: 64;

      ((s . bb) - (s . bb)) > ((s . cc) - (s . bb)) by A2, XREAL_1: 9;

      then ((s . cc) - (s . bb)) <= ( - 1) by INT_1: 8;

      then

       A7: (((s . cc) - (s . bb)) + 1) <= (( - 1) + 1) by XREAL_1: 6;

      set s3 = ( IExec (MI,p,s));

      a in {a, bb, cc} by ENUMSET1:def 1;

      then a in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A8: a <> aux by SCMFSA_M: 25;

      bb in {a, bb, cc} by ENUMSET1:def 1;

      then bb in ( {a, bb, cc} \/ ( UsedILoc I)) by XBOOLE_0:def 3;

      then

       A9: bb <> aux by SCMFSA_M: 25;

      

       A10: (s1 . aux) = (( Exec (i3,( IExec (((i0 ";" i1) ";" i2),p,s)))) . aux) by SCMFSA6C: 6

      .= (( IExec (((i0 ";" i1) ";" i2),p,s)) . aux) by A8, SCMFSA_2: 63

      .= (( Exec (i2,( IExec ((i0 ";" i1),p,s)))) . aux) by SCMFSA6C: 6

      .= ((( IExec ((i0 ";" i1),p,s)) . aux) + 1) by A4, SCMFSA_2: 64

      .= ((( Exec (i1,( Exec (i0,( Initialized s))))) . aux) + 1) by SCMFSA6C: 8

      .= (((( Exec (i0,( Initialized s))) . aux) - (( Exec (i0,( Initialized s))) . bb)) + 1) by SCMFSA_2: 65

      .= (((( Initialized s) . cc) - (( Exec (i0,( Initialized s))) . bb)) + 1) by SCMFSA_2: 63

      .= (((s . cc) - (s . bb)) + 1) by A9, A3, A5, SCMFSA_2: 63;

      then I4 is_halting_on (s1,p1) by A7, SCMFSA_9: 38;

      

      then

       A11: ( DataPart ( IExec (MI,p,s))) = ( DataPart ( IExec (I4,p1,s1))) by SFMASTR1: 9

      .= ( DataPart s1) by A10, A7, A6, SCMFSA9A: 35

      .= ( DataPart s2) by A1, Th14;

      hereby

        let x be Int-Location such that

         A12: x <> a and

         A13: x in ( {bb, cc} \/ ( UsedILoc I));

        x in ( {a, bb, cc} \/ ( UsedILoc I))

        proof

          per cases by A13, XBOOLE_0:def 3;

            suppose x in {bb, cc};

            then x = bb or x = cc by TARSKI:def 2;

            then x in {a, bb, cc} by ENUMSET1:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose x in ( UsedILoc I);

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        then

         A14: x <> aux by SCMFSA_M: 25;

        

        thus (s3 . x) = (s2 . x) by A11, SCMFSA_M: 2

        .= ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . x) by A12, FUNCT_7: 32

        .= (s . x) by A14, FUNCT_7: 32;

      end;

      let x be FinSeq-Location;

      

      thus (s3 . x) = (s2 . x) by A11, SCMFSA_M: 2

      .= ((s +* (aux,(((s . cc) - (s . bb)) + 1))) . x) by FUNCT_7: 32, SCMFSA_2: 58

      .= (s . x) by FUNCT_7: 32, SCMFSA_2: 58;

    end;

     Lm1:

    now

      let s, a, bb, cc, p;

      let I be good really-closed MacroInstruction of SCM+FSA such that

       A1: (s . ( intloc 0 )) = 1 and

       A2: ProperForUpBody (a,bb,cc,I,s,p) or I is parahalting;

      

       A3: ProperForUpBody (a,bb,cc,I,s,p) by A2, Th15;

      set scb1 = (((s . cc) - (s . bb)) + 1);

      set SF = ( StepForUp (a,bb,cc,I,p,s));

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set s2 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))), p2 = p;

      set IB2 = (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 ))));

      set SW2 = ( StepWhile>0 (aux,IB,p2,s2));

      

       A4: IB = (I ";" (( AddTo (a,( intloc 0 ))) ";" ( SubFrom (aux,( intloc 0 ))))) by SCMFSA6A: 28;

      

       A5: ProperBodyWhile>0 (aux,IB,s2,p2)

      proof

        let k be Nat;

        assume ((( StepWhile>0 (aux,IB,p2,s2)) . k) . aux) > 0 ;

        then

         A6: k < scb1 by A1, A3, Th18;

        

         A7: ((SF . k) . ( intloc 0 )) = 1 by A1, A3, A6, Th17;

        I is_halting_on ((SF . k),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 )))))))) by A3, A6;

        then

         A8: I is_halting_on (( Initialized (SF . k)),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 )))))))) by A7, SCMFSA8B: 42;

        IB2 is_halting_on (( IExec (I,(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 ))))))),(SF . k))),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 )))))))) by SCMFSA7B: 19;

        then IB is_halting_on (( Initialized (SF . k)),(p +* ( while>0 ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I))),( intloc 0 )))))))) by A4, A8, SFMASTR1: 3;

        hence thesis by A7, SCMFSA8B: 42;

      end;

      set i3 = (a := bb);

      set i2 = ( AddTo (aux,( intloc 0 )));

      set i1 = ( SubFrom (aux,bb));

      set i0 = (aux := cc);

      set s1 = ( IExec ((((i0 ";" i1) ";" i2) ";" i3),p,s)), p1 = p;

      set SW1 = ( StepWhile>0 (aux,IB,p1,s1));

      deffunc U( State of SCM+FSA ) = |.($1 . aux).|;

      consider f be Function of ( product ( the_Values_of SCM+FSA )), NAT such that

       A9: for x be Element of ( product ( the_Values_of SCM+FSA )) holds (f . x) = U(x) from FUNCT_2:sch 4;

      

       A10: for x be State of SCM+FSA holds (f . x) = U(x)

      proof

        let x be State of SCM+FSA ;

        reconsider x as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

        (f . x) = U(x) by A9;

        hence thesis;

      end;

      

       A11: ( DataPart s1) = ( DataPart s2) by A1, Th14;

      thus ProperBodyWhile>0 (aux,IB,s1,p1)

      proof

        let k be Nat;

        assume

         A12: ((( StepWhile>0 (aux,IB,p1,s1)) . k) . aux) > 0 ;

        

         A13: ( DataPart (SW2 . k)) = ( DataPart (SW1 . k)) by A11, A5, SCMFSA9A: 34;

        then

         A14: ((SW1 . k) . aux) = ((SW2 . k) . aux) by SCMFSA_M: 2;

        IB is_halting_on ((SW2 . k),(p2 +* ( while>0 (aux,IB)))) by A5, A12, A14;

        hence thesis by A13, SCMFSA8B: 5;

      end;

      

       A15: for k be Nat holds ((f . (SW1 . (k + 1))) < (f . (SW1 . k)) or ((SW1 . k) . aux) <= 0 )

      proof

        let k be Nat;

        

         A16: ( DataPart (SW1 . k)) = ( DataPart (SW2 . k)) by A11, A5, SCMFSA9A: 34;

        then

         A17: ((SW1 . k) . aux) = ((SW2 . k) . aux) by SCMFSA_M: 2;

        ( DataPart (SW2 . (k + 1))) = ( DataPart (SW1 . (k + 1))) by A11, A5, SCMFSA9A: 34;

        then

         A18: ((SW1 . (k + 1)) . aux) = ((SW2 . (k + 1)) . aux) by SCMFSA_M: 2;

        now

          assume

           A19: ((SW1 . k) . aux) > 0 ;

          then

           A20: k < scb1 by A1, A3, A17, Th18;

          k < scb1 by A1, A3, A17, A19, Th18;

          then

           A21: (((SW2 . k) . aux) + k) = (((s . cc) - (s . bb)) + 1) by A1, A3, Th17;

          reconsider scb1 as Element of NAT by A20, INT_1: 3;

          

           A22: (k + 1) <= scb1 by A20, NAT_1: 13;

          then

           A23: (((SW2 . (k + 1)) . aux) + (k + 1)) = (((s . cc) - (s . bb)) + 1) by A1, A3, Th17;

          

           A24: (f . (SW1 . k)) = |.((SW1 . k) . aux).| by A10

          .= ((SW2 . k) . aux) by A17, A19, ABSVALUE:def 1;

          per cases ;

            suppose

             A25: ((SW1 . (k + 1)) . aux) > 0 ;

            (f . (SW1 . (k + 1))) = |.((SW1 . (k + 1)) . aux).| by A10

            .= ((scb1 - k) - 1) by A18, A23, A25, ABSVALUE:def 1;

            hence (f . (SW1 . (k + 1))) < (f . (SW1 . k)) by A24, A21, XREAL_1: 146;

          end;

            suppose

             A26: ((SW1 . (k + 1)) . aux) <= 0 ;

            ((SW2 . (k + 1)) . aux) = (scb1 - (k + 1)) by A23;

            then

             A27: ((SW1 . (k + 1)) . aux) = 0 by A18, A22, A26, XREAL_1: 48;

            (f . (SW1 . (k + 1))) = |.((SW1 . (k + 1)) . aux).| by A10

            .= 0 by A27, ABSVALUE:def 1;

            hence (f . (SW1 . (k + 1))) < (f . (SW1 . k)) by A16, A19, A24, SCMFSA_M: 2;

          end;

        end;

        hence thesis;

      end;

      thus WithVariantWhile>0 (aux,IB,s1,p1) by A15;

    end;

    theorem :: SFMASTR3:25

    

     Th23: for Ig be good really-closed MacroInstruction of SCM+FSA holds (s . ( intloc 0 )) = 1 & k = (((s . cc) - (s . bb)) + 1) & ( ProperForUpBody (a,bb,cc,Ig,s,p) or Ig is parahalting) implies ( DataPart ( IExec (( for-up (a,bb,cc,Ig)),p,s))) = ( DataPart (( StepForUp (a,bb,cc,Ig,p,s)) . k))

    proof

      let Ig be good really-closed MacroInstruction of SCM+FSA ;

      set I = Ig;

      assume that

       A1: (s . ( intloc 0 )) = 1 and

       A2: k = (((s . cc) - (s . bb)) + 1) and

       A3: ProperForUpBody (a,bb,cc,I,s,p) or I is parahalting;

      set scb1 = (((s . cc) - (s . bb)) + 1);

      set SF = ( StepForUp (a,bb,cc,I,p,s));

      

       A4: ProperForUpBody (a,bb,cc,I,s,p) by A3, Th15;

      set i3 = (a := bb);

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set i0 = (aux := cc);

      set i1 = ( SubFrom (aux,bb));

      set i2 = ( AddTo (aux,( intloc 0 )));

      reconsider IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 )))) as really-closed MacroInstruction of SCM+FSA ;

      set I03 = (((i0 ";" i1) ";" i2) ";" i3);

      set s1 = ( IExec (I03,p,s)), p1 = p;

      

       A5: (s1 . ( intloc 0 )) = (( Exec (i3,( IExec (((i0 ";" i1) ";" i2),p,s)))) . ( intloc 0 )) by SCMFSA6C: 6

      .= (( IExec (((i0 ";" i1) ";" i2),p,s)) . ( intloc 0 )) by SCMFSA_2: 63

      .= (( Exec (i2,( IExec ((i0 ";" i1),p,s)))) . ( intloc 0 )) by SCMFSA6C: 6

      .= (( IExec ((i0 ";" i1),p,s)) . ( intloc 0 )) by SCMFSA_2: 64

      .= (( Exec (i1,( Exec (i0,( Initialized s))))) . ( intloc 0 )) by SCMFSA6C: 8

      .= (( Exec (i0,( Initialized s))) . ( intloc 0 )) by SCMFSA_2: 65

      .= (( Initialized s) . ( intloc 0 )) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      then

       A6: ( DataPart ( Initialized s1)) = ( DataPart s1) by SCMFSA_M: 19;

      set Ex1 = ( ExitsAtWhile>0 (aux,IB,p1,( Initialized s1)));

      set SW1 = ( StepWhile>0 (aux,IB,p1,( Initialized s1)));

      

       A7: ProperBodyWhile>0 (aux,IB,s1,p1) by A1, A3, Lm1;

      then

       A8: ProperBodyWhile>0 (aux,IB,( Initialized s1),p1) by A6, SCMFSA9A: 38;

      set s2 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))), p2 = p;

      set SW2 = ( StepWhile>0 (aux,IB,p2,s2));

      

       A9: ( DataPart s1) = ( DataPart s2) by A1, Th14;

      then ( DataPart (SW1 . k)) = ( DataPart (SW2 . k)) by A6, A8, SCMFSA9A: 34;

      then

       A10: ((SW1 . k) . aux) = ((SW2 . k) . aux) by SCMFSA_M: 2;

      

       A11: WithVariantWhile>0 (aux,IB,s1,p1) by A1, A3, Lm1;

      then

       A12: WithVariantWhile>0 (aux,IB,( Initialized s1),p1) by A5, A6, A7, SCMFSA9A: 41;

      consider K be Nat such that

       A13: ( ExitsAtWhile>0 (aux,IB,p1,( Initialized s1))) = K and

       A14: ((( StepWhile>0 (aux,IB,p1,( Initialized s1))) . K) . aux) <= 0 and

       A15: (for i be Nat st ((( StepWhile>0 (aux,IB,p1,( Initialized s1))) . i) . aux) <= 0 holds K <= i) & ( DataPart ( Comput ((p1 +* ( while>0 (aux,IB))),( Initialize ( Initialized s1)),( LifeSpan ((p1 +* ( while>0 (aux,IB))),( Initialize ( Initialized s1))))))) = ( DataPart (( StepWhile>0 (aux,IB,p1,( Initialized s1))) . K)) by A12, A8, SCMFSA9A:def 6;

      ( DataPart (SW1 . K)) = ( DataPart (SW2 . K)) by A6, A8, A9, SCMFSA9A: 34;

      then

       A16: ((SW1 . K) . aux) = ((SW2 . K) . aux) by SCMFSA_M: 2;

       A17:

      now

        assume

         A18: K < scb1;

        then (((SF . K) . aux) + K) < ( 0 + scb1) by A14, A16, XREAL_1: 8;

        hence contradiction by A1, A4, A18, Th17;

      end;

      (((SF . k) . aux) + k) = scb1 by A1, A2, A4, Th17;

      then K <= k by A2, A15, A10;

      then

       A19: Ex1 = k by A2, A13, A17, XXREAL_0: 1;

      set MI = ( for-up (a,bb,cc,I));

      set I4 = ( while>0 (aux,IB));

      I4 is_halting_on (s1,p1) by A7, A11, SCMFSA9A: 27;

      

      hence ( DataPart ( IExec (MI,p,s))) = ( DataPart ( IExec (I4,p1,s1))) by SFMASTR1: 9

      .= ( DataPart (SW1 . Ex1)) by A8, A12, SCMFSA9A: 36

      .= ( DataPart (( StepForUp (a,bb,cc,I,p,s)) . k)) by A6, A8, A9, A19, SCMFSA9A: 34;

    end;

    theorem :: SFMASTR3:26

    

     Th24: for Ig be good really-closed MacroInstruction of SCM+FSA holds (s . ( intloc 0 )) = 1 & ( ProperForUpBody (a,bb,cc,Ig,s,p) or Ig is parahalting) implies ( for-up (a,bb,cc,Ig)) is_halting_on (s,p)

    proof

      let Ig be good really-closed MacroInstruction of SCM+FSA ;

      set I = Ig;

      assume that

       A1: (s . ( intloc 0 )) = 1 and

       A2: ProperForUpBody (a,bb,cc,I,s,p) or I is parahalting;

      set i3 = (a := bb);

      set aux = (1 -stRWNotIn ( {a, bb, cc} \/ ( UsedILoc I)));

      set i0 = (aux := cc);

      set i1 = ( SubFrom (aux,bb));

      set i2 = ( AddTo (aux,( intloc 0 )));

      set IB = ((I ";" ( AddTo (a,( intloc 0 )))) ";" ( SubFrom (aux,( intloc 0 ))));

      set I4 = ( while>0 (aux,IB));

      set I03 = (((i0 ";" i1) ";" i2) ";" i3);

      set s1 = ( IExec (I03,p,s)), p1 = p;

      

       A3: ProperBodyWhile>0 (aux,IB,s1,p1) & WithVariantWhile>0 (aux,IB,s1,p1) by A1, A2, Lm1;

      reconsider I03 as parahalting Program of SCM+FSA ;

      set MI = ( for-up (a,bb,cc,I));

      

       A4: I03 is_halting_on (( Initialized s),p) by SCMFSA7B: 19;

      I4 is_halting_on (s1,p1) by A3, SCMFSA9A: 27;

      then MI is_halting_on (( Initialized s),p) by A4, SFMASTR1: 3;

      hence thesis by A1, SCMFSA8B: 42;

    end;

    begin

    definition

      let start,finish,minpos be Int-Location, f be FinSeq-Location;

      :: SFMASTR3:def4

      func FinSeqMin (f,start,finish,minpos) -> MacroInstruction of SCM+FSA equals ((minpos := start) ";" ( for-up ((3 -rdRWNotIn {start, finish, minpos}),start,finish,((((1 -stRWNotIn {start, finish, minpos}) := (f,(3 -rdRWNotIn {start, finish, minpos}))) ";" ((2 -ndRWNotIn {start, finish, minpos}) := (f,minpos))) ";" ( if>0 ((2 -ndRWNotIn {start, finish, minpos}),(1 -stRWNotIn {start, finish, minpos}),( Macro (minpos := (3 -rdRWNotIn {start, finish, minpos}))),( Stop SCM+FSA )))))));

      coherence ;

    end

    registration

      let start,finish be Int-Location, minpos be read-write Int-Location, f be FinSeq-Location;

      cluster ( FinSeqMin (f,start,finish,minpos)) -> good really-closed;

      coherence ;

    end

    theorem :: SFMASTR3:27

    

     Th25: c <> aa implies not ( FinSeqMin (f,aa,bb,c)) destroys aa

    proof

      set a = aa, b = bb;

      set aux1 = (1 -stRWNotIn {a, b, c});

      set aux2 = (2 -ndRWNotIn {a, b, c});

      set cv = (3 -rdRWNotIn {a, b, c});

      set i10 = (aux1 := (f,cv));

      set i11 = (aux2 := (f,c));

      reconsider I12 = ( if>0 (aux2,aux1,( Macro (c := cv)),( Stop SCM+FSA ))) as really-closed MacroInstruction of SCM+FSA ;

      set I1B = ((i10 ";" i11) ";" I12);

      set I1 = ( for-up (cv,a,b,I1B));

      

       A1: not ( Stop SCM+FSA ) destroys a by SCMFSA8C: 56;

      

       A2: a in {a, b, c} by ENUMSET1:def 1;

      then aux1 <> a by SCMFSA_M: 25;

      then

       A3: not i10 destroys a by SCMFSA7B: 14;

      

       A4: aux2 <> a by A2, SCMFSA_M: 25;

      then not i11 destroys a by SCMFSA7B: 14;

      then

       A5: not (i10 ";" i11) destroys a by A3, SCMFSA8C: 55;

      assume

       A6: c <> aa;

      then not ( Macro (c := cv)) destroys a by SCMFSA7B: 6, SCMFSA8C: 48;

      then not I12 destroys a by A4, A1, Th7;

      then

       A7: not I1B destroys a by A5, SCMFSA8C: 52;

      a in {cv, a, b} by ENUMSET1:def 1;

      then a in ( {cv, a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

      then

       A8: a <> (1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))) by SCMFSA_M: 25;

      cv <> a by A2, SCMFSA_M: 25;

      then not I1 destroys a by A7, A8, Th21;

      hence thesis by A6, SCMFSA7B: 6, SCMFSA8C: 53;

    end;

    theorem :: SFMASTR3:28

    

     Th26: {aa, bb, c} c= ( UsedILoc ( FinSeqMin (f,aa,bb,c)))

    proof

      set a = aa, b = bb;

      set aux1 = (1 -stRWNotIn {a, b, c});

      set aux2 = (2 -ndRWNotIn {a, b, c});

      set cv = (3 -rdRWNotIn {a, b, c});

      set i0 = (c := a);

      set i10 = (aux1 := (f,cv));

      set i11 = (aux2 := (f,c));

      set I12 = ( if>0 (aux2,aux1,( Macro (c := cv)),( Stop SCM+FSA )));

      set I1B = ((i10 ";" i11) ";" I12);

      set I1 = ( for-up (cv,a,b,I1B));

      

       A1: ( UsedILoc (i0 ";" I1)) = (( UsedIntLoc i0) \/ ( UsedILoc I1)) by SF_MASTR: 29;

      

       A2: ( {cv, a, b} \/ ( UsedILoc I1B)) c= ( UsedILoc I1) by Th20;

      let x be object;

      

       A3: ( UsedIntLoc i0) = {c, a} by SF_MASTR: 14;

      assume

       A4: x in {a, b, c};

      per cases by A4, ENUMSET1:def 1;

        suppose x = a;

        then x in {c, a} by TARSKI:def 2;

        hence thesis by A1, A3, XBOOLE_0:def 3;

      end;

        suppose x = b;

        then x in {cv, a, b} by ENUMSET1:def 1;

        then x in ( {cv, a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

        hence thesis by A1, A2, XBOOLE_0:def 3;

      end;

        suppose x = c;

        then x in {c, a} by TARSKI:def 2;

        hence thesis by A1, A3, XBOOLE_0:def 3;

      end;

    end;

    theorem :: SFMASTR3:29

    

     Th27: (s . ( intloc 0 )) = 1 implies ( FinSeqMin (f,aa,bb,c)) is_halting_on (s,p)

    proof

      assume

       A1: (s . ( intloc 0 )) = 1;

      set a = aa, b = bb;

      set aux1 = (1 -stRWNotIn {a, b, c});

      set aux2 = (2 -ndRWNotIn {a, b, c});

      set cv = (3 -rdRWNotIn {a, b, c});

      set i0 = (c := a);

      set i10 = (aux1 := (f,cv));

      set i11 = (aux2 := (f,c));

      set I12 = ( if>0 (aux2,aux1,( Macro (c := cv)),( Stop SCM+FSA )));

      set I1B = ((i10 ";" i11) ";" I12);

      set I1 = ( for-up (cv,a,b,I1B));

      set s1 = ( IExec (( Macro i0),p,s)), p1 = p;

      

       A2: (s1 . ( intloc 0 )) = (( Exec (i0,( Initialized s))) . ( intloc 0 )) by SCMFSA6C: 5

      .= (( Initialized s) . ( intloc 0 )) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      

       A3: ( Macro i0) is_halting_on (( Initialized s),p) by SCMFSA7B: 19;

      I1 is_halting_on (s1,p1) by A2, Th24;

      then ( FinSeqMin (f,aa,bb,c)) is_halting_on (( Initialized s),p) by A3, SFMASTR1: 3;

      hence thesis by A1, SCMFSA8B: 42;

    end;

    theorem :: SFMASTR3:30

    

     Th28: aa <> c & bb <> c & (s . ( intloc 0 )) = 1 implies (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . f) = (s . f) & (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . aa) = (s . aa) & (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . bb) = (s . bb)

    proof

      assume that

       A1: aa <> c and

       A2: bb <> c and

       A3: (s . ( intloc 0 )) = 1;

      set a = aa, b = bb;

      set i0 = (c := a);

      set s1 = ( Exec (i0,( Initialized s))), p1 = p;

      

       A4: a = ( intloc 0 ) or a is read-write by SCMFSA_M:def 2;

      

       A5: b = ( intloc 0 ) or b is read-write by SCMFSA_M:def 2;

      

       A6: (s1 . b) = (( Initialized s) . b) by A2, SCMFSA_2: 63

      .= (s . b) by A3, A5, SCMFSA_M: 9, SCMFSA_M: 37;

      set cv = (3 -rdRWNotIn {a, b, c});

      set aux2 = (2 -ndRWNotIn {a, b, c});

      set aux1 = (1 -stRWNotIn {a, b, c});

      set i10 = (aux1 := (f,cv));

      set i11 = (aux2 := (f,c));

      set I12 = ( if>0 (aux2,aux1,( Macro (c := cv)),( Stop SCM+FSA )));

      set I1B = ((i10 ";" i11) ";" I12);

      set I1 = ( for-up (cv,a,b,I1B));

      

       A7: aux2 <> cv by SCMFSA_M: 26;

      cv in {cv, a, b} by ENUMSET1:def 1;

      then

       A8: cv in ( {cv, a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

      

       A9: aux1 <> cv by SCMFSA_M: 26;

      

       A10: b in {a, b, c} by ENUMSET1:def 1;

      then

       A11: cv <> b by SCMFSA_M: 25;

      

       A12: aux1 <> b by A10, SCMFSA_M: 25;

      

       A13: aux2 <> b by A10, SCMFSA_M: 25;

      

       A14: (s1 . a) = (( Initialized s) . a) by A1, SCMFSA_2: 63

      .= (s . a) by A3, A4, SCMFSA_M: 9, SCMFSA_M: 37;

      b in {cv, a, b} by ENUMSET1:def 1;

      then

       A15: b in ( {cv, a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

      

       A16: a in {a, b, c} by ENUMSET1:def 1;

      then

       A17: cv <> a by SCMFSA_M: 25;

      

       A18: aux1 <> a by A16, SCMFSA_M: 25;

      

       A19: aux2 <> a by A16, SCMFSA_M: 25;

      

       A20: (s1 . f) = (( Initialized s) . f) by SCMFSA_2: 63

      .= (s . f) by SCMFSA_M: 37;

      a in {cv, a, b} by ENUMSET1:def 1;

      then

       A21: a in ( {cv, a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

      c in {a, b, c} by ENUMSET1:def 1;

      then

       A22: cv <> c by SCMFSA_M: 25;

      

       A23: (s1 . ( intloc 0 )) = (( Initialized s) . ( intloc 0 )) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      then

       A24: I1 is_halting_on (s1,p1) by Th24;

      per cases ;

        suppose

         A25: (s . aa) > (s . bb);

        

        thus (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . f) = (( IExec (I1,p1,s1)) . f) by A24, SFMASTR1: 15

        .= (s . f) by A23, A14, A6, A20, A25, Th22;

        a in {a, b} by TARSKI:def 2;

        then

         A26: a in ( {a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

        

        thus (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . aa) = (( IExec (I1,p1,s1)) . aa) by A24, SFMASTR1: 14

        .= (s . aa) by A17, A23, A14, A6, A25, A26, Th22;

        b in {a, b} by TARSKI:def 2;

        then

         A27: b in ( {a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

        

        thus (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . bb) = (( IExec (I1,p1,s1)) . bb) by A24, SFMASTR1: 14

        .= (s . bb) by A11, A23, A14, A6, A25, A27, Th22;

      end;

        suppose

         A28: (s . aa) <= (s . bb);

        set SF = ( StepForUp (cv,a,b,I1B,p1,s1));

        

         A29: ((s . a) - (s . a)) <= ((s . b) - (s . a)) by A28, XREAL_1: 9;

        then

        reconsider k = (((s . b) - (s . a)) + 1) as Element of NAT by INT_1: 3;

        defpred P[ Nat] means 0 < $1 & $1 <= k implies ((SF . $1) . ( intloc 0 )) = 1 & ((SF . $1) . cv) = ($1 + (s1 . a)) & ((SF . $1) . f) = (s1 . f) & ((SF . $1) . a) = (s1 . a) & ((SF . $1) . b) = (s1 . b);

        

         A30: ProperForUpBody (cv,a,b,I1B,s1,p1) by Th15;

        

         A31: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat such that

           A32: P[n] and 0 < (n + 1) and

           A33: (n + 1) <= k;

          

           A34: ((SF . n) . ( intloc 0 )) = 1 & ((SF . n) . cv) = (n + (s1 . a)) & ((SF . n) . cv) <= (s1 . b)

          proof

            per cases ;

              suppose

               A35: 0 = n;

              hence ((SF . n) . ( intloc 0 )) = 1 by A23, Th8;

              thus ((SF . n) . cv) = (n + (s1 . a)) by A35, Th9;

              thus thesis by A14, A6, A28, A35, Th9;

            end;

              suppose

               A36: 0 < n;

              hence ((SF . n) . ( intloc 0 )) = 1 by A32, A33, NAT_1: 13;

              thus ((SF . n) . cv) = (n + (s1 . a)) by A32, A33, A36, NAT_1: 13;

              ((n + 1) - 1) <= ((((s . b) - (s . a)) + 1) - 1) by A33, XREAL_1: 9;

              hence thesis by A14, A6, A32, A33, A36, NAT_1: 13, XREAL_1: 19;

            end;

          end;

          n < (n + 1) by XREAL_1: 29;

          then n < k by A33, XXREAL_0: 2;

          then

           A37: ((SF . (n + 1)) | (( {cv, a, b} \/ ( UsedILoc I1B)) \/ FinSeq-Locations )) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) | (( {cv, a, b} \/ ( UsedILoc I1B)) \/ FinSeq-Locations )) by A23, A14, A6, A30, Th19;

          

          then

           A38: ((SF . (n + 1)) . f) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . f) by SCMFSA_M: 28

          .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by SFMASTR1: 12

          .= (( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . f) by SCMFSA_2: 64

          .= (( IExec (I12,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by SFMASTR1: 8;

          

           A39: ((SF . (n + 1)) . b) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . b) by A15, A37, SCMFSA_M: 28

          .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . b) by SFMASTR1: 11

          .= (( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . b) by A11, SCMFSA_2: 64

          .= (( IExec (I12,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . b) by SFMASTR1: 7;

          

           A40: ((SF . (n + 1)) . a) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . a) by A21, A37, SCMFSA_M: 28

          .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . a) by SFMASTR1: 11

          .= (( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . a) by A17, SCMFSA_2: 64

          .= (( IExec (I12,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . a) by SFMASTR1: 7;

          

           A41: ((SF . (n + 1)) . cv) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) by A8, A37, SCMFSA_M: 28

          .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) by SFMASTR1: 11

          .= ((( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) + (( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . ( intloc 0 ))) by SCMFSA_2: 64

          .= ((( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) + 1) by SCMFSA6B: 11

          .= ((( IExec (I12,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) + 1) by SFMASTR1: 7;

          set ss = ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)));

          set S0 = ( Initialized (SF . n));

          set S1 = ( Exec (i10,S0));

          set S2 = ( Exec (i11,( Exec (i10,S0))));

          

           A42: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . f) = (S2 . f) by SCMFSA6C: 9

          .= (S1 . f) by SCMFSA_2: 72

          .= (S0 . f) by SCMFSA_2: 72;

          

           A43: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . ( intloc 0 )) = (S2 . ( intloc 0 )) by SCMFSA6C: 8

          .= (S1 . ( intloc 0 )) by SCMFSA_2: 72

          .= (S0 . ( intloc 0 )) by SCMFSA_2: 72

          .= 1 by SCMFSA_M: 9;

          then

           A44: ( DataPart ( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) = ( DataPart ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) by Th1;

          

           A45: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . b) = (S2 . b) by SCMFSA6C: 8

          .= (S1 . b) by A13, SCMFSA_2: 72

          .= (S0 . b) by A12, SCMFSA_2: 72;

          

           A46: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . a) = (S2 . a) by SCMFSA6C: 8

          .= (S1 . a) by A19, SCMFSA_2: 72

          .= (S0 . a) by A18, SCMFSA_2: 72;

          

           A47: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) = (S2 . cv) by SCMFSA6C: 8

          .= (S1 . cv) by A7, SCMFSA_2: 72

          .= (S0 . cv) by A9, SCMFSA_2: 72;

          

           A48: not ( Macro (c := cv)) refers aux2 & not ( Stop SCM+FSA ) refers aux2 by A7, Th2, Th3, SCMFSA8C: 51;

          per cases ;

            suppose

             A49: 0 = n;

            thus thesis

            proof

              thus ((SF . (n + 1)) . ( intloc 0 )) = 1 by A23, A14, A6, A30, A33, Th17;

              

               A50: (S0 . f) = ((SF . 0 ) . f) by A49, SCMFSA_M: 37

              .= (s . f) by A20, Th13;

              

               A51: (S0 . cv) = ((SF . 0 ) . cv) by A49, SCMFSA_M: 37

              .= (s . a) by A14, Th9;

              

               A52: (S0 . b) = ((SF . 0 ) . b) by A5, A34, A49, SCMFSA_M: 9, SCMFSA_M: 37

              .= (s1 . b) by A11, Th11;

              

               A53: (S0 . a) = ((SF . 0 ) . a) by A4, A34, A49, SCMFSA_M: 9, SCMFSA_M: 37

              .= (s1 . a) by A17, Th10;

              thus thesis

              proof

                per cases ;

                  suppose

                   A54: (ss . aux2) <= (ss . aux1);

                  

                  hence ((SF . (n + 1)) . cv) = ((( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) + 1) by A7, A48, A41, SCMFSA8B: 40

                  .= ((n + 1) + (s1 . a)) by A14, A44, A47, A49, A51, SCMFSA_M: 2;

                  

                  thus ((SF . (n + 1)) . f) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by A48, A38, A54, SCMFSA8B: 40

                  .= (s1 . f) by A20, A44, A42, A50, SCMFSA_M: 2;

                  

                  thus ((SF . (n + 1)) . a) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . a) by A19, A48, A40, A54, SCMFSA8B: 40

                  .= (s1 . a) by A44, A46, A53, SCMFSA_M: 2;

                  

                  thus ((SF . (n + 1)) . b) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . b) by A13, A48, A39, A54, SCMFSA8B: 40

                  .= (s1 . b) by A44, A45, A52, SCMFSA_M: 2;

                end;

                  suppose

                   A55: (ss . aux2) > (ss . aux1);

                  

                   A56: (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) = (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . cv) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . cv) by A22, SCMFSA_2: 63;

                  

                  thus ((SF . (n + 1)) . cv) = ((( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . cv) + 1) by A56, A7, A48, A41, A55, SCMFSA8B: 40

                  .= ((n + 1) + (s1 . a)) by A14, A47, A49, A51, SCMFSA_M: 37;

                  

                  thus ((SF . (n + 1)) . f) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by A48, A38, A55, SCMFSA8B: 40

                  .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . f) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . f) by SCMFSA_2: 63

                  .= (s1 . f) by A20, A42, A50, SCMFSA_M: 37;

                  

                  thus ((SF . (n + 1)) . a) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . a) by A19, A48, A40, A55, SCMFSA8B: 40

                  .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . a) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . a) by A1, SCMFSA_2: 63

                  .= (s1 . a) by A4, A43, A46, A53, SCMFSA_M: 9, SCMFSA_M: 37;

                  

                  thus ((SF . (n + 1)) . b) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . b) by A13, A48, A39, A55, SCMFSA8B: 40

                  .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . b) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . b) by A2, SCMFSA_2: 63

                  .= (s1 . b) by A5, A43, A45, A52, SCMFSA_M: 9, SCMFSA_M: 37;

                end;

              end;

            end;

          end;

            suppose

             A57: 0 < n;

            thus thesis

            proof

              thus ((SF . (n + 1)) . ( intloc 0 )) = 1 by A23, A14, A6, A30, A33, Th17;

              

               A58: (S0 . cv) = ((SF . n) . cv) by SCMFSA_M: 37;

              

               A59: (S0 . a) = (s1 . a) by A4, A32, A33, A57, NAT_1: 13, SCMFSA_M: 9, SCMFSA_M: 37;

              

               A60: (S0 . b) = (s1 . b) by A5, A32, A33, A57, NAT_1: 13, SCMFSA_M: 9, SCMFSA_M: 37;

              

               A61: (S0 . f) = (s . f) by A20, A32, A33, A57, NAT_1: 13, SCMFSA_M: 37;

              thus thesis

              proof

                per cases ;

                  suppose

                   A62: (ss . aux2) <= (ss . aux1);

                  

                  hence ((SF . (n + 1)) . cv) = ((( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) + 1) by A7, A48, A41, SCMFSA8B: 40

                  .= ((( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) + 1) by A44, SCMFSA_M: 2

                  .= ((n + 1) + (s1 . a)) by A34, A47, A58;

                  

                  thus ((SF . (n + 1)) . f) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by A48, A38, A62, SCMFSA8B: 40

                  .= (s1 . f) by A20, A44, A42, A61, SCMFSA_M: 2;

                  

                  thus ((SF . (n + 1)) . a) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . a) by A19, A48, A40, A62, SCMFSA8B: 40

                  .= (s1 . a) by A44, A46, A59, SCMFSA_M: 2;

                  

                  thus ((SF . (n + 1)) . b) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . b) by A13, A48, A39, A62, SCMFSA8B: 40

                  .= (s1 . b) by A44, A45, A60, SCMFSA_M: 2;

                end;

                  suppose

                   A63: (ss . aux2) > (ss . aux1);

                  

                   A64: (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) = (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . cv) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . cv) by A22, SCMFSA_2: 63

                  .= (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) by SCMFSA_M: 37;

                  

                  thus ((SF . (n + 1)) . cv) = ((( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) + 1) by A7, A48, A41, A63, SCMFSA8B: 40

                  .= ((n + 1) + (s1 . a)) by A34, A47, A58, A64;

                  

                  thus ((SF . (n + 1)) . f) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by A48, A38, A63, SCMFSA8B: 40

                  .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . f) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . f) by SCMFSA_2: 63

                  .= (s1 . f) by A20, A42, A61, SCMFSA_M: 37;

                  

                  thus ((SF . (n + 1)) . a) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . a) by A19, A48, A40, A63, SCMFSA8B: 40

                  .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . a) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . a) by A1, SCMFSA_2: 63

                  .= (s1 . a) by A4, A43, A46, A59, SCMFSA_M: 9, SCMFSA_M: 37;

                  

                  thus ((SF . (n + 1)) . b) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . b) by A13, A48, A39, A63, SCMFSA8B: 40

                  .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . b) by SCMFSA6C: 5

                  .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . b) by A2, SCMFSA_2: 63

                  .= (s1 . b) by A5, A43, A45, A60, SCMFSA_M: 9, SCMFSA_M: 37;

                end;

              end;

            end;

          end;

        end;

        

         A65: P[ 0 ];

        

         A66: for n be Nat holds P[n] from NAT_1:sch 2( A65, A31);

        

         A67: ( DataPart ( IExec (I1,p1,s1))) = ( DataPart (SF . k)) by A23, A14, A6, Th23;

        

        thus (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . f) = (( IExec (I1,p1,s1)) . f) by A24, SFMASTR1: 15

        .= ((SF . k) . f) by A67, SCMFSA_M: 2

        .= (s . f) by A20, A29, A66;

        

        thus (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . aa) = (( IExec (I1,p1,s1)) . a) by A24, SFMASTR1: 14

        .= ((SF . k) . a) by A67, SCMFSA_M: 2

        .= (s . aa) by A14, A29, A66;

        

        thus (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . bb) = (( IExec (I1,p1,s1)) . b) by A24, SFMASTR1: 14

        .= ((SF . k) . b) by A67, SCMFSA_M: 2

        .= (s . bb) by A6, A29, A66;

      end;

    end;

    theorem :: SFMASTR3:31

    

     Th29: 1 <= (s . aa) & (s . aa) <= (s . bb) & (s . bb) <= ( len (s . f)) & aa <> c & bb <> c & (s . ( intloc 0 )) = 1 implies (( IExec (( FinSeqMin (f,aa,bb,c)),p,s)) . c) = ( min_at ((s . f), |.(s . aa).|, |.(s . bb).|))

    proof

      set a = aa, b = bb;

      assume that

       A1: 1 <= (s . a) and

       A2: (s . a) <= (s . b) and

       A3: (s . b) <= ( len (s . f)) and

       A4: a <> c and

       A5: b <> c and

       A6: (s . ( intloc 0 )) = 1;

      

       A7: b = ( intloc 0 ) or b is read-write by SCMFSA_M:def 2;

      set i0 = (c := a);

      set s1 = ( Exec (i0,( Initialized s))), p1 = p;

      

       A8: a = ( intloc 0 ) or a is read-write by SCMFSA_M:def 2;

      reconsider sa = |.(s . a).| as Element of NAT ;

      

       A9: (s . a) = sa by A1, ABSVALUE:def 1;

      ((s . a) - (s . a)) <= ((s . b) - (s . a)) by A2, XREAL_1: 9;

      then

      reconsider sba = ((s . b) - (s . a)) as Element of NAT by INT_1: 3;

      

       A10: (s1 . f) = (( Initialized s) . f) by SCMFSA_2: 63

      .= (s . f) by SCMFSA_M: 37;

      set k = (sba + 1);

      set cv = (3 -rdRWNotIn {a, b, c});

      set aux2 = (2 -ndRWNotIn {a, b, c});

      set aux1 = (1 -stRWNotIn {a, b, c});

      

       A11: aux1 <> aux2 by SCMFSA_M: 26;

      set I12 = ( if>0 (aux2,aux1,( Macro (c := cv)),( Stop SCM+FSA )));

      set i10 = (aux1 := (f,cv));

      

       A12: aux2 <> cv by SCMFSA_M: 26;

      set i11 = (aux2 := (f,c));

      

       A13: aux1 <> cv by SCMFSA_M: 26;

      

       A14: c in {a, b, c} by ENUMSET1:def 1;

      then

       A15: cv <> c by SCMFSA_M: 25;

      set I1B = ((i10 ";" i11) ";" I12);

      set I1 = ( for-up (cv,a,b,I1B));

      set SF = ( StepForUp (cv,a,b,I1B,p1,s1));

      defpred P[ Nat] means 0 < $1 & $1 <= k implies ((SF . $1) . ( intloc 0 )) = 1 & ((SF . $1) . cv) = ($1 + (s1 . a)) & ((SF . $1) . f) = (s1 . f) & ex sa1 be Element of NAT st sa1 = (($1 + sa) - 1) & ((SF . $1) . c) = ( min_at ((s . f),sa,sa1));

      cv in {cv, a, b} by ENUMSET1:def 1;

      then

       A16: cv in ( {cv, a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

      

       A17: ProperForUpBody (cv,a,b,I1B,s1,p1) by Th15;

      

       A18: aux1 <> c by A14, SCMFSA_M: 25;

      

       A19: aux2 <> c by A14, SCMFSA_M: 25;

      

       A20: (s1 . c) = (( Initialized s) . a) by SCMFSA_2: 63

      .= (s . a) by A6, A8, SCMFSA_M: 9, SCMFSA_M: 37;

      

       A21: (s1 . a) = (( Initialized s) . a) by A4, SCMFSA_2: 63

      .= (s . a) by A6, A8, SCMFSA_M: 9, SCMFSA_M: 37;

      

       A22: (s . a) <= ( len (s . f)) by A2, A3, XXREAL_0: 2;

      then

       A23: sa in ( dom (s . f)) by A1, A9, FINSEQ_3: 25;

      

       A24: (s1 . b) = (( Initialized s) . b) by A5, SCMFSA_2: 63

      .= (s . b) by A6, A7, SCMFSA_M: 9, SCMFSA_M: 37;

      

       A25: (s1 . ( intloc 0 )) = (( Initialized s) . ( intloc 0 )) by SCMFSA_2: 63

      .= 1 by SCMFSA_M: 9;

      then

       A26: ( DataPart ( IExec (I1,p1,s1))) = ( DataPart (SF . k)) by A21, A24, Th23;

      c in {c, cv} by TARSKI:def 2;

      then c in ( UsedIntLoc (c := cv)) by SF_MASTR: 14;

      then c in ( UsedILoc ( Macro (c := cv))) by SF_MASTR: 28;

      then c in ( {aux2, aux1} \/ ( UsedILoc ( Macro (c := cv)))) by XBOOLE_0:def 3;

      then c in (( {aux2, aux1} \/ ( UsedILoc ( Macro (c := cv)))) \/ ( UsedILoc ( Stop SCM+FSA ))) by XBOOLE_0:def 3;

      then c in ( UsedILoc I12) by Th6;

      then c in (( UsedILoc (i10 ";" i11)) \/ ( UsedILoc I12)) by XBOOLE_0:def 3;

      then

       A27: c in ( UsedILoc I1B) by SF_MASTR: 27;

      then

       A28: c in ( {cv, a, b} \/ ( UsedILoc I1B)) by XBOOLE_0:def 3;

      

       A29: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A30: P[n] and 0 < (n + 1) and

         A31: (n + 1) <= k;

        

         A32: ((SF . n) . ( intloc 0 )) = 1 & ((SF . n) . cv) = (n + (s1 . a)) & ((SF . n) . cv) <= (s1 . b)

        proof

          per cases ;

            suppose

             A33: 0 = n;

            hence ((SF . n) . ( intloc 0 )) = 1 by A25, Th8;

            thus ((SF . n) . cv) = (n + (s1 . a)) by A33, Th9;

            thus thesis by A2, A21, A24, A33, Th9;

          end;

            suppose

             A34: 0 < n;

            hence ((SF . n) . ( intloc 0 )) = 1 by A30, A31, NAT_1: 13;

            thus ((SF . n) . cv) = (n + (s1 . a)) by A30, A31, A34, NAT_1: 13;

            ((n + 1) - 1) <= ((((s . b) - (s . a)) + 1) - 1) by A31, XREAL_1: 9;

            hence thesis by A21, A24, A30, A34, NAT_1: 13, XREAL_1: 19;

          end;

        end;

        set S0 = ( Initialized (SF . n));

        set S1 = ( Exec (i10,S0));

        set S2 = ( Exec (i11,( Exec (i10,S0))));

        

         A35: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . f) = (S2 . f) by SCMFSA6C: 9

        .= (S1 . f) by SCMFSA_2: 72

        .= (S0 . f) by SCMFSA_2: 72;

        (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . ( intloc 0 )) = (S2 . ( intloc 0 )) by SCMFSA6C: 8

        .= (S1 . ( intloc 0 )) by SCMFSA_2: 72

        .= (S0 . ( intloc 0 )) by SCMFSA_2: 72

        .= 1 by SCMFSA_M: 9;

        then

         A36: ( DataPart ( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) = ( DataPart ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) by Th1;

        n < (n + 1) by XREAL_1: 29;

        then n < k by A31, XXREAL_0: 2;

        then

         A37: ((SF . (n + 1)) | (( {cv, a, b} \/ ( UsedILoc I1B)) \/ FinSeq-Locations )) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) | (( {cv, a, b} \/ ( UsedILoc I1B)) \/ FinSeq-Locations )) by A25, A21, A24, A17, Th19;

        

        then

         A38: ((SF . (n + 1)) . f) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . f) by SCMFSA_M: 28

        .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by SFMASTR1: 12

        .= (( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . f) by SCMFSA_2: 64

        .= (( IExec (I12,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by SFMASTR1: 8;

        

         A39: ((SF . (n + 1)) . c) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . c) by A28, A37, SCMFSA_M: 28

        .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . c) by SFMASTR1: 11

        .= (( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . c) by A15, SCMFSA_2: 64

        .= (( IExec (I12,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . c) by SFMASTR1: 7;

        

         A40: ((SF . (n + 1)) . cv) = (( IExec ((I1B ";" ( AddTo (cv,( intloc 0 )))),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) by A16, A37, SCMFSA_M: 28

        .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) by SFMASTR1: 11

        .= ((( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) + (( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . ( intloc 0 ))) by SCMFSA_2: 64

        .= ((( IExec (I1B,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) + 1) by SCMFSA6B: 11

        .= ((( IExec (I12,(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) + 1) by SFMASTR1: 7;

        

         A41: not ( Macro (c := cv)) refers aux2 & not ( Stop SCM+FSA ) refers aux2 by A12, Th2, Th3, SCMFSA8C: 51;

        

         A42: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . c) = (S2 . c) by SCMFSA6C: 8

        .= (S1 . c) by A19, SCMFSA_2: 72

        .= (S0 . c) by A18, SCMFSA_2: 72

        .= ((SF . n) . c) by SCMFSA_M: 37;

        

         A43: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) = (S2 . cv) by SCMFSA6C: 8

        .= (S1 . cv) by A12, SCMFSA_2: 72

        .= (S0 . cv) by A13, SCMFSA_2: 72;

        per cases ;

          suppose

           A44: 0 = n;

          thus thesis

          proof

            reconsider sa1 = (((n + 1) + sa) - 1) as Element of NAT by A44;

            

             A45: ((SF . 0 ) . c) = (s1 . c) by A15, A27, Th12;

            

             A46: (S1 . c) = (S0 . c) by A18, SCMFSA_2: 72

            .= (s . a) by A20, A44, A45, SCMFSA_M: 37;

            thus ((SF . (n + 1)) . ( intloc 0 )) = 1 by A25, A21, A24, A17, A31, Th17;

            

             A47: (S0 . f) = ((SF . 0 ) . f) by A44, SCMFSA_M: 37

            .= (s . f) by A10, Th13;

            then

             A48: (S1 . f) = (s . f) by SCMFSA_2: 72;

            

             A49: (S0 . cv) = ((SF . 0 ) . cv) by A44, SCMFSA_M: 37

            .= (s . a) by A21, Th9;

            then

            reconsider S0cv = (S0 . cv) as Element of NAT by A1, INT_1: 3;

            

             A50: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . aux1) = (S2 . aux1) by SCMFSA6C: 8

            .= (S1 . aux1) by A11, SCMFSA_2: 72

            .= ((S0 . f) /. |.(S0 . cv).|) by Th4

            .= ((s . f) . S0cv) by A9, A23, A47, A49, PARTFUN1:def 6;

            

             A51: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . aux2) = (S2 . aux2) by SCMFSA6C: 8

            .= ((S1 . f) /. |.(S1 . c).|) by Th4

            .= ((s . f) . S0cv) by A9, A23, A49, A48, A46, PARTFUN1:def 6;

            

            hence ((SF . (n + 1)) . cv) = ((( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) + 1) by A12, A41, A40, A50, SCMFSA8B: 40

            .= ((n + 1) + (s1 . a)) by A21, A36, A43, A44, A49, SCMFSA_M: 2;

            

            thus ((SF . (n + 1)) . f) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by A41, A38, A50, A51, SCMFSA8B: 40

            .= (s1 . f) by A10, A36, A35, A47, SCMFSA_M: 2;

            take sa1;

            thus sa1 = (((n + 1) + sa) - 1);

            ((SF . (n + 1)) . c) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . c) by A19, A41, A39, A50, A51, SCMFSA8B: 40

            .= (s . a) by A20, A36, A42, A44, A45, SCMFSA_M: 2;

            hence thesis by A1, A22, A9, A44, FINSEQ_6: 162;

          end;

        end;

          suppose

           A52: 0 < n;

          thus thesis

          proof

            

             A53: (S0 . cv) = ((SF . n) . cv) by SCMFSA_M: 37;

            then

            reconsider S0cv = (S0 . cv) as Element of NAT by A1, A21, A32, INT_1: 3;

            1 <= S0cv & S0cv <= ( len (s . f)) by A1, A3, A9, A21, A24, A32, A53, NAT_1: 12, XXREAL_0: 2;

            then

             A54: S0cv in ( dom (s . f)) by FINSEQ_3: 25;

            

             A55: (S0 . f) = (s . f) by A10, A30, A31, A52, NAT_1: 13, SCMFSA_M: 37;

            then

             A56: (S1 . f) = (s . f) by SCMFSA_2: 72;

            

             A57: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . aux1) = (S2 . aux1) by SCMFSA6C: 8

            .= (S1 . aux1) by A11, SCMFSA_2: 72

            .= ((S0 . f) /. |.(S0 . cv).|) by Th4

            .= ((S0 . f) /. S0cv) by ABSVALUE:def 1

            .= ((s . f) . S0cv) by A55, A54, PARTFUN1:def 6;

            (n + (s . a)) <= ( len (s . f)) by A3, A21, A24, A32, XXREAL_0: 2;

            then ((n + (s . a)) - 1) <= (( len (s . f)) - 1) by XREAL_1: 9;

            then

             A58: (((n + (s . a)) - 1) + 0 ) <= ((( len (s . f)) - 1) + 1) by XREAL_1: 7;

            thus ((SF . (n + 1)) . ( intloc 0 )) = 1 by A25, A21, A24, A17, A31, Th17;

            consider sa1 be Nat such that

             A59: sa1 = ((n + sa) - 1) and

             A60: ((SF . n) . c) = ( min_at ((s . f),sa,sa1)) by A30, A31, A52, NAT_1: 13;

            reconsider SFnc = ((SF . n) . c) as Element of NAT by A60, ORDINAL1:def 12;

            ( 0 + 1) <= n by A52, NAT_1: 13;

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

            then

             A61: ( 0 + (s . a)) <= ((n - 1) + (s . a)) by XREAL_1: 6;

            then

             A62: sa <= SFnc by A1, A9, A59, A60, A58, FINSEQ_6: 161;

            then

             A63: 1 <= SFnc by A1, A9, XXREAL_0: 2;

            

             A64: SFnc <= sa1 by A1, A9, A59, A60, A61, A58, FINSEQ_6: 161;

            then SFnc <= ( len (s . f)) by A9, A59, A58, XXREAL_0: 2;

            then

             A65: SFnc in ( dom (s . f)) by A63, FINSEQ_3: 25;

            

             A66: (( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . aux2) = (S2 . aux2) by SCMFSA6C: 8

            .= ((S1 . f) /. |.(S1 . c).|) by Th4

            .= ((S1 . f) /. |.(S0 . c).|) by A18, SCMFSA_2: 72

            .= ((S1 . f) /. |.((SF . n) . c).|) by SCMFSA_M: 37

            .= ((S1 . f) /. SFnc) by ABSVALUE:def 1

            .= ((s . f) . SFnc) by A56, A65, PARTFUN1:def 6;

            

             A67: for i st sa <= i & i < ((SF . n) . c) holds ((s . f) . i) > ((s . f) . SFnc) by A1, A9, A59, A60, A61, A58, FINSEQ_6: 161;

            thus thesis

            proof

              

               A68: (((n + 1) + (s . a)) - 1) <= ( len (s . f)) by A3, A21, A24, A32, XXREAL_0: 2;

              

               A69: (((n + 1) + (s . a)) - 1) = (((n + (s . a)) + 1) - 1)

              .= (n + sa) by A1, ABSVALUE:def 1;

              then

               A70: (s . a) <= (((n + 1) + (s . a)) - 1) by NAT_1: 12;

              per cases ;

                suppose

                 A71: ((s . f) . S0cv) < ((s . f) . SFnc);

                

                 A72: (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) = (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . cv) by SCMFSA6C: 5

                .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . cv) by A15, SCMFSA_2: 63;

                

                thus ((SF . (n + 1)) . cv) = ((( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . cv) + 1) by A72, A12, A41, A40, A57, A66, A71, SCMFSA8B: 40

                .= ((( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) + 1) by SCMFSA_M: 37

                .= ((n + 1) + (s1 . a)) by A32, A43, A53;

                

                thus ((SF . (n + 1)) . f) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by A41, A38, A57, A66, A71, SCMFSA8B: 40

                .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . f) by SCMFSA6C: 5

                .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . f) by SCMFSA_2: 63

                .= (s1 . f) by A10, A35, A55, SCMFSA_M: 37;

                reconsider sa11 = (((n + 1) + sa) - 1) as Element of NAT by A69;

                take sa11;

                thus sa11 = (((n + 1) + sa) - 1);

                

                 A73: for i st (s . a) <= i & i <= (((n + 1) + (s . a)) - 1) holds ((s . f) . S0cv) <= ((s . f) . i)

                proof

                  let i such that

                   A74: (s . a) <= i and

                   A75: i <= (((n + 1) + (s . a)) - 1);

                  per cases by A75, XXREAL_0: 1;

                    suppose i < (((n + 1) + (s . a)) - 1);

                    then (i + 1) <= (n + (s . a)) by A69, NAT_1: 13;

                    then ((i + 1) - 1) <= ((n + (s . a)) - 1) by XREAL_1: 9;

                    then ((s . f) . SFnc) <= ((s . f) . i) by A1, A9, A59, A60, A61, A58, A74, FINSEQ_6: 161;

                    hence thesis by A71, XXREAL_0: 2;

                  end;

                    suppose i = (((n + 1) + (s . a)) - 1);

                    hence thesis by A21, A32, SCMFSA_M: 37;

                  end;

                end;

                

                 A76: for i st (s . a) <= i & i < S0cv holds ((s . f) . i) > ((s . f) . S0cv)

                proof

                  let i;

                  assume that

                   A77: (s . a) <= i and

                   A78: i < S0cv;

                  (i + 1) <= S0cv by A78, NAT_1: 13;

                  then ((i + 1) - 1) <= (S0cv - 1) by XREAL_1: 9;

                  then ((s . f) . SFnc) <= ((s . f) . i) by A1, A9, A21, A32, A53, A59, A60, A61, A58, A77, FINSEQ_6: 161;

                  hence thesis by A71, XXREAL_0: 2;

                end;

                ((SF . (n + 1)) . c) = (( IExec (( Macro (c := cv)),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . c) by A19, A41, A39, A57, A66, A71, SCMFSA8B: 40

                .= (( Exec ((c := cv),( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))))) . c) by SCMFSA6C: 5

                .= (( Initialized ( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n)))) . cv) by SCMFSA_2: 63

                .= S0cv by A43, SCMFSA_M: 37;

                hence thesis by A1, A9, A21, A32, A53, A70, A68, A73, A76, FINSEQ_6: 161;

              end;

                suppose

                 A79: ((s . f) . SFnc) <= ((s . f) . S0cv);

                thus thesis

                proof

                  

                   A80: for i st (s . a) <= i & i <= (((n + 1) + (s . a)) - 1) holds ((s . f) . SFnc) <= ((s . f) . i)

                  proof

                    let i such that

                     A81: (s . a) <= i and

                     A82: i <= (((n + 1) + (s . a)) - 1);

                    per cases by A82, XXREAL_0: 1;

                      suppose i < (((n + 1) + (s . a)) - 1);

                      then (i + 1) <= (n + (s . a)) by A69, NAT_1: 13;

                      then ((i + 1) - 1) <= ((n + (s . a)) - 1) by XREAL_1: 9;

                      hence thesis by A1, A9, A59, A60, A61, A58, A81, FINSEQ_6: 161;

                    end;

                      suppose i = (((n + 1) + (s . a)) - 1);

                      hence thesis by A21, A32, A79, SCMFSA_M: 37;

                    end;

                  end;

                  

                  thus ((SF . (n + 1)) . cv) = ((( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . cv) + 1) by A12, A41, A40, A57, A66, A79, SCMFSA8B: 40

                  .= ((( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))) . cv) + 1) by A36, SCMFSA_M: 2

                  .= ((n + 1) + (s1 . a)) by A32, A43, A53;

                  

                  thus ((SF . (n + 1)) . f) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . f) by A41, A38, A57, A66, A79, SCMFSA8B: 40

                  .= (s1 . f) by A10, A36, A35, A55, SCMFSA_M: 2;

                  reconsider sa11 = (((n + 1) + sa) - 1) as Element of NAT by A69;

                  take sa11;

                  thus sa11 = (((n + 1) + sa) - 1);

                  ((n + (s . a)) - 1) <= (((n + (s . a)) - 1) + 1) by XREAL_1: 29;

                  then

                   A83: SFnc <= (((n + 1) + (s . a)) - 1) by A9, A59, A64, XXREAL_0: 2;

                  ((SF . (n + 1)) . c) = (( IExec (( Stop SCM+FSA ),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),( IExec ((i10 ";" i11),(p1 +* ( while>0 ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),((I1B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, a, b} \/ ( UsedILoc I1B))),( intloc 0 ))))))),(SF . n))))) . c) by A19, A41, A39, A57, A66, A79, SCMFSA8B: 40

                  .= ((SF . n) . c) by A36, A42, SCMFSA_M: 2;

                  hence thesis by A1, A9, A62, A67, A70, A68, A83, A80, FINSEQ_6: 161;

                end;

              end;

            end;

          end;

        end;

      end;

      reconsider sb = |.(s . b).| as Element of NAT ;

      

       A84: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A84, A29);

      then

      consider sab be Element of NAT such that

       A85: sab = ((k + sa) - 1) and

       A86: ((SF . k) . c) = ( min_at ((s . f),sa,sab));

      

       A87: sab = sb by A9, A85, ABSVALUE:def 1;

      I1 is_halting_on (s1,p1) by A25, Th24;

      

      hence (( IExec (( FinSeqMin (f,a,b,c)),p,s)) . c) = (( IExec (I1,p1,s1)) . c) by SFMASTR1: 14

      .= ( min_at ((s . f), |.(s . a).|, |.(s . b).|)) by A26, A86, A87, SCMFSA_M: 2;

    end;

    begin

    definition

      let f be FinSeq-Location, a,b be Int-Location;

      :: SFMASTR3:def5

      func swap (f,a,b) -> MacroInstruction of SCM+FSA equals (((((1 -stRWNotIn {a, b}) := (f,a)) ";" ((2 -ndRWNotIn {a, b}) := (f,b))) ";" ((f,a) := (2 -ndRWNotIn {a, b}))) ";" ((f,b) := (1 -stRWNotIn {a, b})));

      coherence ;

    end

    registration

      let f be FinSeq-Location, a,b be Int-Location;

      cluster ( swap (f,a,b)) -> good parahalting;

      coherence ;

    end

    theorem :: SFMASTR3:32

    

     Th30: cc <> (1 -stRWNotIn {aa, bb}) & cc <> (2 -ndRWNotIn {aa, bb}) implies not ( swap (f,aa,bb)) destroys cc

    proof

      set a = aa, b = bb;

      set aux1 = (1 -stRWNotIn {a, b});

      set aux2 = (2 -ndRWNotIn {a, b});

      assume cc <> (1 -stRWNotIn {aa, bb}) & cc <> (2 -ndRWNotIn {aa, bb});

      then

       A1: not (aux1 := (f,a)) destroys cc & not (aux2 := (f,b)) destroys cc by SCMFSA7B: 14;

       not ((f,a) := aux2) destroys cc by SCMFSA7B: 15;

      then not (((aux1 := (f,a)) ";" (aux2 := (f,b))) ";" ((f,a) := aux2)) destroys cc by A1, SCMFSA8C: 54, SCMFSA8C: 55;

      hence thesis by SCMFSA7B: 15, SCMFSA8C: 54;

    end;

    theorem :: SFMASTR3:33

    

     Th31: 1 <= (s . aa) & (s . aa) <= ( len (s . f)) & 1 <= (s . bb) & (s . bb) <= ( len (s . f)) & (s . ( intloc 0 )) = 1 implies (( IExec (( swap (f,aa,bb)),p,s)) . f) = (((s . f) +* ((s . aa),((s . f) . (s . bb)))) +* ((s . bb),((s . f) . (s . aa))))

    proof

      set a = aa, b = bb;

      assume that

       A1: 1 <= (s . a) and

       A2: (s . a) <= ( len (s . f)) and

       A3: 1 <= (s . b) and

       A4: (s . b) <= ( len (s . f)) and

       A5: (s . ( intloc 0 )) = 1;

      set aux1 = (1 -stRWNotIn {a, b}), aux2 = (2 -ndRWNotIn {a, b});

      set i0 = (aux1 := (f,a)), i1 = (aux2 := (f,b)), i2 = ((f,a) := aux2);

      set s0 = ( Initialized s), s1 = ( Exec (i0,s0)), s2 = ( IExec ((i0 ";" i1),p,s));

      

       A6: b = ( intloc 0 ) or b is read-write by SCMFSA_M:def 2;

      reconsider sa = (s . a) as Element of NAT by A1, INT_1: 3;

      set s0a = |.(s0 . a).|, s2a = |.(s2 . a).|;

      

       A7: a = ( intloc 0 ) or a is read-write by SCMFSA_M:def 2;

      

       A8: sa = |.(s . a).| by ABSVALUE:def 1;

      then

       A9: (s0 . f) = (s . f) & sa = s0a by A5, A7, SCMFSA_M: 9, SCMFSA_M: 37;

      reconsider sb = (s . b) as Element of NAT by A3, INT_1: 3;

      

       A10: sb = |.(s . b).| by ABSVALUE:def 1;

      set s3 = ( IExec (((i0 ";" i1) ";" i2),p,s));

      

       A11: aux1 <> aux2 by SCMFSA_M: 26;

      

       A12: (s3 . aux1) = (( Exec (i2,s2)) . aux1) by SCMFSA6C: 6

      .= (s2 . aux1) by SCMFSA_2: 73

      .= (( Exec (i1,s1)) . aux1) by SCMFSA6C: 8

      .= (s1 . aux1) by A11, SCMFSA_2: 72

      .= ((s0 . f) /. s0a) by Th4

      .= ((s . f) . sa) by A1, A2, A9, FINSEQ_4: 15;

      set i3 = ((f,b) := aux1);

      

       A13: (s2 . f) = (( Exec (i1,s1)) . f) by SCMFSA6C: 9

      .= (s1 . f) by SCMFSA_2: 72;

      

       A14: (s3 . f) = (( Exec (i2,s2)) . f) by SCMFSA6C: 7

      .= ((s2 . f) +* (s2a,(s2 . aux2))) by Th5;

      

       A15: b in {a, b} by TARSKI:def 2;

      then

       A16: b <> aux2 by SCMFSA_M: 25;

      b <> aux1 by A15, SCMFSA_M: 25;

      

      then

       A17: (s1 . b) = (s0 . b) by SCMFSA_2: 72

      .= (s . b) by A5, A6, SCMFSA_M: 9, SCMFSA_M: 37;

      

       A18: a in {a, b} by TARSKI:def 2;

      then

       A19: a <> aux2 by SCMFSA_M: 25;

      

       A20: a <> aux1 by A18, SCMFSA_M: 25;

      (s2 . a) = (( Exec (i1,s1)) . a) by SCMFSA6C: 8

      .= (s1 . a) by A19, SCMFSA_2: 72

      .= (s0 . a) by A20, SCMFSA_2: 72;

      then

       A21: sa = s2a by A5, A8, A7, SCMFSA_M: 9, SCMFSA_M: 37;

      set s1b = |.(s1 . b).|;

      

       A22: (s1 . f) = (s0 . f) by SCMFSA_2: 72

      .= (s . f) by SCMFSA_M: 37;

      

       A23: (s3 . b) = (( Exec (i2,s2)) . b) by SCMFSA6C: 6

      .= (s2 . b) by SCMFSA_2: 73

      .= (( Exec (i1,s1)) . b) by SCMFSA6C: 8

      .= (s1 . b) by A16, SCMFSA_2: 72;

      

       A24: (s2 . aux2) = (( Exec (i1,s1)) . aux2) by SCMFSA6C: 8

      .= ((s1 . f) /. s1b) by Th4

      .= ((s . f) . sb) by A3, A4, A10, A22, A17, FINSEQ_4: 15;

      

      thus (( IExec (( swap (f,a,b)),p,s)) . f) = (( Exec (i3,s3)) . f) by SCMFSA6C: 7

      .= (((s . f) +* ((s . a),((s . f) . (s . b)))) +* ((s . b),((s . f) . (s . a)))) by A10, A22, A13, A14, A21, A17, A23, A24, A12, Th5;

    end;

    theorem :: SFMASTR3:34

    1 <= (s . aa) & (s . aa) <= ( len (s . f)) & 1 <= (s . bb) & (s . bb) <= ( len (s . f)) & (s . ( intloc 0 )) = 1 implies ((( IExec (( swap (f,aa,bb)),p,s)) . f) . (s . aa)) = ((s . f) . (s . bb)) & ((( IExec (( swap (f,aa,bb)),p,s)) . f) . (s . bb)) = ((s . f) . (s . aa))

    proof

      set a = aa, b = bb;

      assume that

       A1: 1 <= (s . a) and

       A2: (s . a) <= ( len (s . f)) and

       A3: 1 <= (s . b) and

       A4: (s . b) <= ( len (s . f)) and

       A5: (s . ( intloc 0 )) = 1;

      

       A6: (( IExec (( swap (f,a,b)),p,s)) . f) = (((s . f) +* ((s . a),((s . f) . (s . b)))) +* ((s . b),((s . f) . (s . a)))) by A1, A2, A3, A4, A5, Th31;

      reconsider sa = (s . a) as Element of NAT by A1, INT_1: 3;

      

       A7: sa in ( dom (s . f)) by A1, A2, FINSEQ_3: 25;

      

       A8: ( dom ((s . f) +* ((s . a),((s . f) . (s . b))))) = ( dom (s . f)) by FUNCT_7: 30;

      reconsider sb = (s . b) as Element of NAT by A3, INT_1: 3;

      

       A9: sb in ( dom (s . f)) by A3, A4, FINSEQ_3: 25;

      per cases ;

        suppose sa <> sb;

        

        hence ((( IExec (( swap (f,a,b)),p,s)) . f) . (s . a)) = (((s . f) +* ((s . a),((s . f) . (s . b)))) . (s . a)) by A6, FUNCT_7: 32

        .= ((s . f) . (s . b)) by A7, FUNCT_7: 31;

        thus thesis by A9, A6, A8, FUNCT_7: 31;

      end;

        suppose sa = sb;

        hence ((( IExec (( swap (f,a,b)),p,s)) . f) . (s . a)) = ((s . f) . (s . b)) by A7, A6, A8, FUNCT_7: 31;

        thus thesis by A9, A6, A8, FUNCT_7: 31;

      end;

    end;

    theorem :: SFMASTR3:35

    

     Th33: {aa, bb} c= ( UsedILoc ( swap (f,aa,bb)))

    proof

      set a = aa, b = bb;

      set aux1 = (1 -stRWNotIn {a, b}), aux2 = (2 -ndRWNotIn {a, b});

      set i0 = (aux1 := (f,a)), i1 = (aux2 := (f,b)), i2 = ((f,a) := aux2);

      set i3 = ((f,b) := aux1);

      

       A1: ( UsedILoc ( swap (f,a,b))) = (( UsedILoc ((i0 ";" i1) ";" i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 30

      .= ((( UsedILoc (i0 ";" i1)) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 30

      .= (((( UsedIntLoc i0) \/ ( UsedIntLoc i1)) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 31

      .= ((( {aux1, a} \/ ( UsedIntLoc i1)) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 17

      .= ((( {aux1, a} \/ {aux2, b}) \/ ( UsedIntLoc i2)) \/ ( UsedIntLoc i3)) by SF_MASTR: 17

      .= ((( {aux1, a} \/ {aux2, b}) \/ {aux2, a}) \/ ( UsedIntLoc i3)) by SF_MASTR: 17

      .= ((( {aux1, a} \/ {aux2, b}) \/ {aux2, a}) \/ {aux1, b}) by SF_MASTR: 17;

      let x be object;

      assume

       A2: x in {a, b};

      per cases by A2, TARSKI:def 2;

        suppose x = a;

        then x in {aux2, a} by TARSKI:def 2;

        then x in (( {aux1, a} \/ {aux2, b}) \/ {aux2, a}) by XBOOLE_0:def 3;

        hence thesis by A1, XBOOLE_0:def 3;

      end;

        suppose x = b;

        then x in {aux1, b} by TARSKI:def 2;

        hence thesis by A1, XBOOLE_0:def 3;

      end;

    end;

    theorem :: SFMASTR3:36

    ( UsedI*Loc ( swap (f,aa,bb))) = {f}

    proof

      set a = aa, b = bb;

      set aux1 = (1 -stRWNotIn {a, b});

      set aux2 = (2 -ndRWNotIn {a, b});

      

      thus ( UsedI*Loc ( swap (f,a,b))) = (( UsedI*Loc (((aux1 := (f,a)) ";" (aux2 := (f,b))) ";" ((f,a) := aux2))) \/ ( UsedInt*Loc ((f,b) := aux1))) by SF_MASTR: 46

      .= (( UsedI*Loc (((aux1 := (f,a)) ";" (aux2 := (f,b))) ";" ((f,a) := aux2))) \/ {f}) by SF_MASTR: 33

      .= ((( UsedI*Loc ((aux1 := (f,a)) ";" (aux2 := (f,b)))) \/ ( UsedInt*Loc ((f,a) := aux2))) \/ {f}) by SF_MASTR: 46

      .= ((( UsedI*Loc ((aux1 := (f,a)) ";" (aux2 := (f,b)))) \/ {f}) \/ {f}) by SF_MASTR: 33

      .= (((( UsedInt*Loc (aux1 := (f,a))) \/ ( UsedInt*Loc (aux2 := (f,b)))) \/ {f}) \/ {f}) by SF_MASTR: 47

      .= ((( {f} \/ ( UsedInt*Loc (aux2 := (f,b)))) \/ {f}) \/ {f}) by SF_MASTR: 33

      .= (( {f} \/ {f}) \/ {f}) by SF_MASTR: 33

      .= {f};

    end;

    begin

    definition

      let f be FinSeq-Location;

      :: SFMASTR3:def6

      func Selection-sort f -> Program of SCM+FSA equals (((1 -stNotUsed ( swap (f,(1 -stRWNotIn ( {} Int-Locations )),(2 -ndRWNotIn ( {} Int-Locations ))))) :=len f) ";" ( for-up ((1 -stRWNotIn ( {} Int-Locations )),( intloc 0 ),(1 -stNotUsed ( swap (f,(1 -stRWNotIn ( {} Int-Locations )),(2 -ndRWNotIn ( {} Int-Locations ))))),(( FinSeqMin (f,(1 -stRWNotIn ( {} Int-Locations )),(1 -stNotUsed ( swap (f,(1 -stRWNotIn ( {} Int-Locations )),(2 -ndRWNotIn ( {} Int-Locations ))))),(2 -ndRWNotIn ( {} Int-Locations )))) ";" ( swap (f,(1 -stRWNotIn ( {} Int-Locations )),(2 -ndRWNotIn ( {} Int-Locations ))))))));

      coherence ;

    end

    theorem :: SFMASTR3:37

    for S be State of SCM+FSA st S = ( IExec (( Selection-sort f),p,s)) holds (S . f) is_non_decreasing_on (1,( len (S . f))) & ex p be Permutation of ( dom (s . f)) st (S . f) = ((s . f) * p)

    proof

      set minpos = (2 -ndRWNotIn ( {} Int-Locations ));

      set cv = (1 -stRWNotIn ( {} Int-Locations ));

      let S be State of SCM+FSA such that

       A1: S = ( IExec (( Selection-sort f),p,s));

      set I22 = ( swap (f,cv,minpos));

      set finish = (1 -stNotUsed ( swap (f,cv,minpos)));

      set i1 = (finish :=len f);

      set I21 = ( FinSeqMin (f,cv,finish,minpos));

      set I2B = (I21 ";" I22);

      set I2 = ( for-up (cv,( intloc 0 ),finish,I2B));

      set s1 = ( Exec (i1,( Initialized s))), p1 = p;

      

       A2: (s1 . ( intloc 0 )) = (( Initialized s) . ( intloc 0 )) by SCMFSA_2: 74

      .= 1 by SCMFSA_M: 9;

      cv in {cv, minpos} by TARSKI:def 2;

      then cv <> (1 -stRWNotIn {cv, minpos}) & cv <> (2 -ndRWNotIn {cv, minpos}) by SCMFSA_M: 25;

      then

       A3: not ( swap (f,cv,minpos)) destroys cv by Th30;

      set SF = ( StepForUp (cv,( intloc 0 ),finish,I2B,p1,s1));

      

       A4: (s1 . finish) = ( len (( Initialized s) . f)) by SCMFSA_2: 74

      .= ( len (s . f)) by SCMFSA_M: 37;

      then

      reconsider n = (((s1 . finish) - (s1 . ( intloc 0 ))) + 1) as Element of NAT by A2;

      defpred P[ Nat] means $1 <= n implies ((SF . $1) . cv) = ($1 + (s1 . ( intloc 0 ))) & ((SF . $1) . finish) = (s1 . finish) & ((SF . $1) . f) is_split_at $1 & ((SF . $1) . f) is_non_decreasing_on (1,$1) & ex p be Permutation of ( dom (s . f)) st ((SF . $1) . f) = ((s . f) * p);

      defpred Q[ Nat] means $1 < n implies ((SF . $1) . ( intloc 0 )) = 1 & I2B is_halting_on ((SF . $1),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))));

      

       A5: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat such that

         A6: Q[k];

        assume (k + 1) < n;

        hence

         A7: ((SF . (k + 1)) . ( intloc 0 )) = 1 by A6, Th16, NAT_1: 13;

        (( Initialized (SF . (k + 1))) . ( intloc 0 )) = 1 by SCMFSA_M: 9;

        then

         A8: I21 is_halting_on (( Initialized (SF . (k + 1))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by Th27;

        I22 is_halting_on (( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . (k + 1)))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by SCMFSA7B: 19;

        then I2B is_halting_on (( Initialized (SF . (k + 1))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by SFMASTR1: 3, A8;

        hence thesis by A7, SCMFSA8B: 42;

      end;

      

       A9: Q[ 0 ]

      proof

        (( Initialized (SF . 0 )) . ( intloc 0 )) = 1 by SCMFSA_M: 9;

        then

         A10: I21 is_halting_on (( Initialized (SF . 0 )),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by Th27;

        assume 0 < n;

        thus

         A11: ((SF . 0 ) . ( intloc 0 )) = 1 by A2, Th8;

        I22 is_halting_on (( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . 0 ))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by SCMFSA7B: 19;

        then I2B is_halting_on (( Initialized (SF . 0 )),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by SFMASTR1: 3, A10;

        hence thesis by A11, SCMFSA8B: 42;

      end;

      

       A12: for k be Nat holds Q[k] from NAT_1:sch 2( A9, A5);

      

       A13: ProperForUpBody (cv,( intloc 0 ),finish,I2B,s1,p1) by A12;

      then

       A14: ( DataPart ( IExec (I2,p1,s1))) = ( DataPart (SF . n)) by A2, Th23;

      I2 is_halting_on (s1,p1) by A2, A13, Th24;

      

      then

       A15: (S . f) = (( IExec (I2,p1,s1)) . f) by A1, SFMASTR1: 15

      .= ((SF . n) . f) by A14, SCMFSA_M: 2;

       not ( FinSeqMin (f,cv,finish,minpos)) destroys cv by Th25, SCMFSA_M: 26;

      then

       A16: not I2B destroys cv by A3, SCMFSA8C: 52;

      

       A17: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A18: P[k];

         A19:

        now

          assume

           A20: k < n;

          hence

           A21: ((SF . k) . ( intloc 0 )) = 1 by A12;

          I2B is_halting_on ((SF . k),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by A12, A20;

          hence I2B is_halting_on (( Initialized (SF . k)),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by A21, SCMFSA8B: 42;

          thus ((SF . k) . cv) = (k + (s1 . ( intloc 0 ))) by A18, A20;

          thus ((SF . k) . finish) = (s1 . finish) by A18, A20;

          thus ((SF . k) . cv) <= (s1 . finish) by A2, A18, A20, NAT_1: 13;

          thus ((SF . (k + 1)) | (( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B)) \/ FinSeq-Locations )) = (( IExec ((I2B ";" ( AddTo (cv,( intloc 0 )))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))) | (( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B)) \/ FinSeq-Locations )) by A2, A13, A20, Th19;

        end;

        set F = ((SF . k) . f), F1 = ((SF . (k + 1)) . f);

        assume

         A22: (k + 1) <= n;

        then

        consider pp be Permutation of ( dom (s . f)) such that

         A23: F = ((s . f) * pp) by A18, NAT_1: 13;

        thus ((SF . (k + 1)) . cv) = ((k + 1) + (s1 . ( intloc 0 ))) by A16, A2, A13, A22, Th17;

        

         A24: I22 is_halting_on (( Initialized ( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k)))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by SCMFSA7B: 19;

        

         A25: finish = (1 -stRWNotIn ( UsedILoc I22)) by SFMASTR1:def 4;

        set ma = ( min_at (F,(k + 1),( len F)));

        

         A26: ( dom (s . f)) = ( Seg ( len (s . f))) by FINSEQ_1:def 3;

        then

         A27: ( len F) = ( len (s . f)) by A23, FINSEQ_2: 43;

        

         A28: 1 <= (k + 1) by NAT_1: 12;

        then

         A29: (k + 1) <= ma by A2, A4, A22, A27, FINSEQ_6: 161;

        then

         A30: 1 <= ma by A28, XXREAL_0: 2;

        ma <= ( len F) by A2, A4, A22, A27, A28, FINSEQ_6: 161;

        then

         A31: ma in ( dom F) by A30, FINSEQ_3: 25;

        

         A32: {cv, minpos} c= ( UsedILoc I22) by Th33;

        minpos in {cv, minpos} by TARSKI:def 2;

        then

         A33: finish <> minpos by A25, A32, SCMFSA_M: 25;

        cv in {cv, minpos} by TARSKI:def 2;

        then

         A34: cv <> finish by A25, A32, SCMFSA_M: 25;

        

         A35: cv <> minpos by SCMFSA_M: 26;

        (( Initialized (SF . k)) . ( intloc 0 )) = 1 by SCMFSA_M: 9;

        then

         A36: I21 is_halting_on (( Initialized (SF . k)),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 )))))))) by Th27;

        

         A37: F1 = ((F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))))

        proof

          set S2 = ( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k)));

          

           A38: ( len F) = |.( len F).| by ABSVALUE:def 1;

          ((SF . k) . finish) = ( len F) & (k + 1) = |.(k + 1).| by A4, A19, A22, A23, A26, ABSVALUE:def 1, FINSEQ_2: 43, NAT_1: 13;

          then

           A39: (S2 . minpos) = ma by A2, A19, A22, A33, A35, A28, A38, Th29, NAT_1: 13;

          then

           A40: 1 <= (S2 . minpos) by A28, A29, XXREAL_0: 2;

          

           A41: (S2 . f) = F by A19, A22, A33, A35, Th28, NAT_1: 13;

          then

           A42: (S2 . minpos) <= ( len (S2 . f)) by A2, A4, A22, A27, A28, A39, FINSEQ_6: 161;

          

           A43: (S2 . cv) = (k + 1) & (S2 . ( intloc 0 )) = 1 by A2, A19, A22, A36, A33, A35, Th28, NAT_1: 13, SCMFSA8C: 67;

          

          thus F1 = (( IExec ((I2B ";" ( AddTo (cv,( intloc 0 )))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))) . f) by A19, A22, NAT_1: 13, SCMFSA_M: 28

          .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I2B,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))))) . f) by A19, A22, NAT_1: 13, SFMASTR1: 12

          .= (( IExec (I2B,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))) . f) by SCMFSA_2: 64

          .= (( IExec (I22,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))))) . f) by A36, SFMASTR1: 8

          .= ((F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1)))) by A2, A4, A22, A27, A28, A41, A39, A40, A42, A43, Th31;

        end;

        (k + 1) in ( dom F) by A2, A4, A22, A27, A28, FINSEQ_3: 25;

        then

        consider p1 be Permutation of ( dom F) such that

         A44: F1 = (F * p1) by A31, A37, FUNCT_7: 111;

         {cv, finish, minpos} c= ( UsedILoc I21) & finish in {cv, finish, minpos} by Th26, ENUMSET1:def 1;

        then finish in (( UsedILoc I21) \/ ( UsedILoc I22)) by XBOOLE_0:def 3;

        then finish in ( UsedILoc I2B) by SF_MASTR: 27;

        then finish in ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B)) by XBOOLE_0:def 3;

        

        hence ((SF . (k + 1)) . finish) = (( IExec ((I2B ";" ( AddTo (cv,( intloc 0 )))),(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))) . finish) by A19, A22, NAT_1: 13, SCMFSA_M: 28

        .= (( Exec (( AddTo (cv,( intloc 0 ))),( IExec (I2B,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))))) . finish) by A19, A22, NAT_1: 13, SFMASTR1: 11

        .= (( IExec (I2B,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))) . finish) by A34, SCMFSA_2: 64

        .= (( IExec (I22,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))))) . finish) by A36, SFMASTR1: 7

        .= (( Initialized ( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k)))) . finish) by A25, A24, SCMFSA_M: 25, SFMASTR2: 1

        .= (( IExec (I21,(p +* ( while>0 ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),((I2B ";" ( AddTo (cv,( intloc 0 )))) ";" ( SubFrom ((1 -stRWNotIn ( {cv, ( intloc 0 ), finish} \/ ( UsedILoc I2B))),( intloc 0 ))))))),(SF . k))) . finish) by SCMFSA_M: 37

        .= (s1 . finish) by A19, A22, A33, A35, Th28, NAT_1: 13;

        thus ((SF . (k + 1)) . f) is_split_at (k + 1) by A2, A4, A18, A22, A27, A37, FINSEQ_6: 164, NAT_1: 13;

        thus ((SF . (k + 1)) . f) is_non_decreasing_on (1,(k + 1)) by A2, A4, A18, A22, A27, A37, FINSEQ_6: 163, NAT_1: 13;

        ( dom F) = ( dom (s . f)) by A27, FINSEQ_3: 29;

        then

        reconsider p1 as Permutation of ( dom (s . f));

        reconsider ppp = (pp * p1) as Permutation of ( dom (s . f));

        take ppp;

        thus thesis by A23, A44, RELAT_1: 36;

      end;

      

       A45: ( dom (s . f)) = ( Seg ( len (s . f))) by FINSEQ_1:def 3;

      

       A46: cv in {cv, minpos} by TARSKI:def 2;

      finish = (1 -stRWNotIn ( UsedILoc I22)) & {cv, minpos} c= ( UsedILoc I22) by Th33, SFMASTR1:def 4;

      then

       A47: cv <> finish by A46, SCMFSA_M: 25;

      

       A48: P[ 0 ]

      proof

        assume 0 <= n;

        thus ((SF . 0 ) . cv) = ( 0 + (s1 . ( intloc 0 ))) by Th9;

        thus ((SF . 0 ) . finish) = (s1 . finish) by A47, Th11;

        thus ((SF . 0 ) . f) is_split_at 0 ;

        thus ((SF . 0 ) . f) is_non_decreasing_on (1, 0 );

        ( dom (s . f)) = ( Seg ( len (s . f))) by FINSEQ_1:def 3;

        then

        reconsider p = ( idseq ( len (s . f))) as Permutation of ( dom (s . f)) by FINSEQ_2: 55;

        take p;

        ((SF . 0 ) . f) = (s1 . f) by Th13

        .= (( Initialized s) . f) by SCMFSA_2: 74

        .= (s . f) by SCMFSA_M: 37;

        hence thesis by FINSEQ_2: 54;

      end;

      

       A49: for k be Nat holds P[k] from NAT_1:sch 2( A48, A17);

      then ex p be Permutation of ( dom (s . f)) st ((SF . n) . f) = ((s . f) * p);

      then ( len (S . f)) = n by A2, A4, A15, A45, FINSEQ_2: 43;

      hence (S . f) is_non_decreasing_on (1,( len (S . f))) by A49, A15;

      thus thesis by A49, A15;

    end;