aofa_i00.miz

    begin

    theorem :: AOFA_I00:1



     Th1: for x,y,z,a,b,c be set st a <> b & b <> c & c <> a holds ex f be Function st (f . a) = x & (f . b) = y & (f . c) = z

    proof

      let x,y,z,a,b,c be set such that

       A1: a <> b and

       A2: b <> c and

       A3: c <> a;

      set fb = (b .--> y);



       A5: a nin ( dom fb) by A1, TARSKI:def 1;



       A6: b in ( dom fb) by TARSKI:def 1;

      set fc = (c .--> z);

      set fa = (a .--> x);

      take f = ((fa +* fb) +* fc);

      a nin ( dom fc) by A3, TARSKI:def 1;



      hence (f . a) = ((fa +* fb) . a) by FUNCT_4: 11

      .= (fa . a) by A5, FUNCT_4: 11

      .= x by FUNCOP_1: 72;

      b nin ( dom fc) by A2, TARSKI:def 1;



      hence (f . b) = ((fa +* fb) . b) by FUNCT_4: 11

      .= (fb . b) by A6, FUNCT_4: 13

      .= y by FUNCOP_1: 72;

      c in ( dom fc) by TARSKI:def 1;



      hence (f . c) = (fc . c) by FUNCT_4: 13

      .= z by FUNCOP_1: 72;

    end;

    definition

      let F be non empty functional set;

      let x be set;

      let f be set;

      :: AOFA_I00:def1

      func F \ (x,f) -> Subset of F equals { g where g be Element of F : (g . x) <> f };

      coherence

      proof

        set X = { g where g be Element of F : (g . x) <> f };

        X c= F

        proof

          let a be object;

          assume a in X;

          then ex g be Element of F st g = a & (g . x) <> f;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: AOFA_I00:2



     Th2: for F be non empty functional set, x,y be set, g be Element of F holds g in (F \ (x,y)) iff (g . x) <> y

    proof

      let F be non empty functional set;

      let x,y be set;

      let g be Element of F;

      g in (F \ (x,y)) iff ex f be Element of F st g = f & (f . x) <> y;

      hence thesis;

    end;

    definition

      let X be set;

      let Y,Z be set;

      let f be Function of [:( Funcs (X, INT )), Y:], Z;

      :: AOFA_I00:def2

      mode Variable of f -> Element of X means

      : Def2: not contradiction;

      existence ;

    end

    notation

      let f be real-valued Function;

      let x be Real;

      synonym f * x for x (#) f;

    end

    definition

      let t1,t2 be INT -valued Function;

      :: AOFA_I00:def3

      func t1 div t2 -> INT -valued Function means

      : Def3: ( dom it ) = (( dom t1) /\ ( dom t2)) & for s be object st s in ( dom it ) holds (it . s) = ((t1 . s) div (t2 . s));

      correctness

      proof

        deffunc F( object) = ((t1 . $1) div (t2 . $1));

        consider f be Function such that

         A1: ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in (( dom t1) /\ ( dom t2)) holds (f . x) = F(x) from FUNCT_1:sch 3;

        f is INT -valued

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A2: x in ( dom f) and

           A3: (f . x) = y by FUNCT_1:def 3;

          (f . x) = F(x) by A1, A2;

          hence thesis by A3, INT_1:def 2;

        end;

        hence ex f be INT -valued Function st ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in ( dom f) holds (f . x) = F(x) by A1;

        let f1,f2 be INT -valued Function such that

         A4: ( dom f1) = (( dom t1) /\ ( dom t2)) and

         A5: for s be object st s in ( dom f1) holds (f1 . s) = F(s) and

         A6: ( dom f2) = (( dom t1) /\ ( dom t2)) and

         A7: for s be object st s in ( dom f2) holds (f2 . s) = F(s);

        now

          let s be object;

          assume

           A8: s in (( dom t1) /\ ( dom t2));



          hence (f1 . s) = F(s) by A4, A5

          .= (f2 . s) by A6, A7, A8;

        end;

        hence thesis by A4, A6;

      end;

      :: AOFA_I00:def4

      func t1 mod t2 -> INT -valued Function means

      : Def4: ( dom it ) = (( dom t1) /\ ( dom t2)) & for s be object st s in ( dom it ) holds (it . s) = ((t1 . s) mod (t2 . s));

      correctness

      proof

        deffunc F( object) = ((t1 . $1) mod (t2 . $1));

        consider f be Function such that

         A9: ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in (( dom t1) /\ ( dom t2)) holds (f . x) = F(x) from FUNCT_1:sch 3;

        f is INT -valued

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A10: x in ( dom f) and

           A11: (f . x) = y by FUNCT_1:def 3;

          (f . x) = F(x) by A9, A10;

          hence thesis by A11, INT_1:def 2;

        end;

        hence ex f be INT -valued Function st ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in ( dom f) holds (f . x) = F(x) by A9;

        let f1,f2 be INT -valued Function such that

         A12: ( dom f1) = (( dom t1) /\ ( dom t2)) and

         A13: for s be object st s in ( dom f1) holds (f1 . s) = F(s) and

         A14: ( dom f2) = (( dom t1) /\ ( dom t2)) and

         A15: for s be object st s in ( dom f2) holds (f2 . s) = F(s);

        now

          let s be object;

          assume

           A16: s in (( dom t1) /\ ( dom t2));



          hence (f1 . s) = F(s) by A12, A13

          .= (f2 . s) by A14, A15, A16;

        end;

        hence thesis by A12, A14;

      end;

      :: AOFA_I00:def5

      func leq (t1,t2) -> INT -valued Function means

      : Def5: ( dom it ) = (( dom t1) /\ ( dom t2)) & for s be object st s in ( dom it ) holds (it . s) = ( IFGT ((t1 . s),(t2 . s), 0 ,1));

      correctness

      proof

        deffunc F( object) = ( IFGT ((t1 . $1),(t2 . $1), 0 ,1));

        consider f be Function such that

         A17: ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in (( dom t1) /\ ( dom t2)) holds (f . x) = F(x) from FUNCT_1:sch 3;

        f is INT -valued

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A18: x in ( dom f) and

           A19: (f . x) = y by FUNCT_1:def 3;

          (f . x) = F(x) by A17, A18;

          hence thesis by A19, INT_1:def 2;

        end;

        hence ex f be INT -valued Function st ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in ( dom f) holds (f . x) = F(x) by A17;

        let f1,f2 be INT -valued Function such that

         A20: ( dom f1) = (( dom t1) /\ ( dom t2)) and

         A21: for s be object st s in ( dom f1) holds (f1 . s) = F(s) and

         A22: ( dom f2) = (( dom t1) /\ ( dom t2)) and

         A23: for s be object st s in ( dom f2) holds (f2 . s) = F(s);

        now

          let s be object;

          assume

           A24: s in (( dom t1) /\ ( dom t2));



          hence (f1 . s) = F(s) by A20, A21

          .= (f2 . s) by A22, A23, A24;

        end;

        hence thesis by A20, A22;

      end;

      :: AOFA_I00:def6

      func gt (t1,t2) -> INT -valued Function means

      : Def6: ( dom it ) = (( dom t1) /\ ( dom t2)) & for s be object st s in ( dom it ) holds (it . s) = ( IFGT ((t1 . s),(t2 . s),1, 0 ));

      correctness

      proof

        deffunc F( object) = ( IFGT ((t1 . $1),(t2 . $1),1, 0 ));

        consider f be Function such that

         A25: ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in (( dom t1) /\ ( dom t2)) holds (f . x) = F(x) from FUNCT_1:sch 3;

        f is INT -valued

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A26: x in ( dom f) and

           A27: (f . x) = y by FUNCT_1:def 3;

          (f . x) = F(x) by A25, A26;

          hence thesis by A27, INT_1:def 2;

        end;

        hence ex f be INT -valued Function st ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in ( dom f) holds (f . x) = F(x) by A25;

        let f1,f2 be INT -valued Function such that

         A28: ( dom f1) = (( dom t1) /\ ( dom t2)) and

         A29: for s be object st s in ( dom f1) holds (f1 . s) = F(s) and

         A30: ( dom f2) = (( dom t1) /\ ( dom t2)) and

         A31: for s be object st s in ( dom f2) holds (f2 . s) = F(s);

        now

          let s be object;

          assume

           A32: s in (( dom t1) /\ ( dom t2));



          hence (f1 . s) = F(s) by A28, A29

          .= (f2 . s) by A30, A31, A32;

        end;

        hence thesis by A28, A30;

      end;

      :: AOFA_I00:def7

      func eq (t1,t2) -> INT -valued Function means

      : Def7: ( dom it ) = (( dom t1) /\ ( dom t2)) & for s be object st s in ( dom it ) holds (it . s) = ( IFEQ ((t1 . s),(t2 . s),1, 0 ));

      correctness

      proof

        deffunc F( object) = ( IFEQ ((t1 . $1),(t2 . $1),1, 0 ));

        consider f be Function such that

         A33: ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in (( dom t1) /\ ( dom t2)) holds (f . x) = F(x) from FUNCT_1:sch 3;

        f is INT -valued

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A34: x in ( dom f) and

           A35: (f . x) = y by FUNCT_1:def 3;

          (f . x) = F(x) by A33, A34;

          hence thesis by A35, INT_1:def 2;

        end;

        hence ex f be INT -valued Function st ( dom f) = (( dom t1) /\ ( dom t2)) & for x be object st x in ( dom f) holds (f . x) = F(x) by A33;

        let f1,f2 be INT -valued Function such that

         A36: ( dom f1) = (( dom t1) /\ ( dom t2)) and

         A37: for s be object st s in ( dom f1) holds (f1 . s) = F(s) and

         A38: ( dom f2) = (( dom t1) /\ ( dom t2)) and

         A39: for s be object st s in ( dom f2) holds (f2 . s) = F(s);

        now

          let s be object;

          assume

           A40: s in (( dom t1) /\ ( dom t2));



          hence (f1 . s) = F(s) by A36, A37

          .= (f2 . s) by A38, A39, A40;

        end;

        hence thesis by A36, A38;

      end;

    end

    definition

      let X be non empty set;

      let f be Function of X, INT ;

      let x be Integer;

      :: original: +

      redefine

      :: AOFA_I00:def8

      func f + x -> Function of X, INT means

      : Def8: for s be Element of X holds (it . s) = ((f . s) + x);

      compatibility

      proof

        let ti be Function of X, INT ;



         A1: ( dom f) = X by FUNCT_2:def 1;

        ( dom (f + x)) = ( dom f) by VALUED_1:def 2;

        hence ti = (f + x) implies for s be Element of X holds (ti . s) = ((f . s) + x) by A1, VALUED_1:def 2;



         A2: ( dom ti) = X by FUNCT_2:def 1;

        assume for s be Element of X holds (ti . s) = ((f . s) + x);

        then for s be object st s in X holds (ti . s) = (x + (f . s));

        hence thesis by A1, A2, VALUED_1:def 2;

      end;

      coherence

      proof

        (x + f) is Function of X, INT ;

        hence thesis;

      end;

      :: original: -

      redefine

      :: AOFA_I00:def9

      func f - x -> Function of X, INT means for s be Element of X holds (it . s) = ((f . s) - x);

      compatibility

      proof

        let ti be Function of X, INT ;



         A3: ( dom ti) = X by FUNCT_2:def 1;



         A4: ( dom f) = X by FUNCT_2:def 1;

        hence ti = (f - x) implies for s be Element of X holds (ti . s) = ((f . s) - x) by VALUED_1: 3;

        assume

         A5: for s be Element of X holds (ti . s) = ((f . s) - x);

         A6:

        now

          let s be object;

          assume

           A7: s in ( dom ti);



          hence (ti . s) = ((f . s) - x) by A5

          .= ((f - x) . s) by A4, A7, VALUED_1: 3;

        end;

        thus ti = (f - x) by A3, A6;

      end;

      coherence

      proof

        thus (f - x) is Function of X, INT ;

      end;

      :: original: *

      redefine

      :: AOFA_I00:def10

      func f * x -> Function of X, INT means

      : Def10: for s be Element of X holds (it . s) = ((f . s) * x);

      compatibility

      proof

        let ti be Function of X, INT ;



         A8: ( dom (f * x)) = ( dom f) by VALUED_1:def 5;



         A9: ( dom f) = X by FUNCT_2:def 1;

        hence ti = (f * x) implies for s be Element of X holds (ti . s) = ((f . s) * x) by A8, VALUED_1:def 5;



         A10: ( dom ti) = X by FUNCT_2:def 1;

        assume for s be Element of X holds (ti . s) = ((f . s) * x);

        then for s be object st s in ( dom (f * x)) holds (ti . s) = (x * (f . s));

        hence thesis by A8, A9, A10, VALUED_1:def 5;

      end;

      coherence

      proof

        (x (#) f) is Function of X, INT ;

        hence thesis;

      end;

    end

    definition

      let X be set;

      let f,g be Function of X, INT ;

      :: original: div

      redefine

      func f div g -> Function of X, INT ;

      coherence

      proof



         A1: ( dom g) = X by FUNCT_2:def 1;



         A2: ( dom (f div g)) = (( dom f) /\ ( dom g)) by Def3;



         A3: ( dom f) = X by FUNCT_2:def 1;

        ( rng (f div g)) c= INT ;

        hence thesis by A2, A3, A1, FUNCT_2: 2;

      end;

      :: original: mod

      redefine

      func f mod g -> Function of X, INT ;

      coherence

      proof



         A4: ( dom g) = X by FUNCT_2:def 1;



         A5: ( dom (f mod g)) = (( dom f) /\ ( dom g)) by Def4;



         A6: ( dom f) = X by FUNCT_2:def 1;

        ( rng (f mod g)) c= INT ;

        hence thesis by A5, A6, A4, FUNCT_2: 2;

      end;

      :: original: leq

      redefine

      func leq (f,g) -> Function of X, INT ;

      coherence

      proof



         A7: ( dom g) = X by FUNCT_2:def 1;



         A8: ( dom ( leq (f,g))) = (( dom f) /\ ( dom g)) by Def5;



         A9: ( dom f) = X by FUNCT_2:def 1;

        ( rng ( leq (f,g))) c= INT ;

        hence thesis by A8, A9, A7, FUNCT_2: 2;

      end;

      :: original: gt

      redefine

      func gt (f,g) -> Function of X, INT ;

      coherence

      proof



         A10: ( dom g) = X by FUNCT_2:def 1;



         A11: ( dom ( gt (f,g))) = (( dom f) /\ ( dom g)) by Def6;



         A12: ( dom f) = X by FUNCT_2:def 1;

        ( rng ( gt (f,g))) c= INT ;

        hence thesis by A11, A12, A10, FUNCT_2: 2;

      end;

      :: original: eq

      redefine

      func eq (f,g) -> Function of X, INT ;

      coherence

      proof



         A13: ( dom g) = X by FUNCT_2:def 1;



         A14: ( dom ( eq (f,g))) = (( dom f) /\ ( dom g)) by Def7;



         A15: ( dom f) = X by FUNCT_2:def 1;

        ( rng ( eq (f,g))) c= INT ;

        hence thesis by A14, A15, A13, FUNCT_2: 2;

      end;

    end

    definition

      let X be non empty set;

      let t1,t2 be Function of X, INT ;

      :: original: -

      redefine

      :: AOFA_I00:def11

      func t1 - t2 -> Function of X, INT means

      : Def11: for s be Element of X holds (it . s) = ((t1 . s) - (t2 . s));

      compatibility

      proof

        let ti be Function of X, INT ;

        thus ti = (t1 - t2) implies for s be Element of X holds (ti . s) = ((t1 . s) - (t2 . s)) by VALUED_1: 15;

        assume

         A1: for s be Element of X holds (ti . s) = ((t1 . s) - (t2 . s));

         A2:

        now

          let s be object;

          assume

           A3: s in X;



          hence (ti . s) = ((t1 . s) - (t2 . s)) by A1

          .= ((t1 - t2) . s) by A3, VALUED_1: 15;

        end;

        thus ti = (t1 - t2) by A2;

      end;

      coherence

      proof

        thus (t1 - t2) is Function of X, INT ;

      end;

      :: original: +

      redefine

      :: AOFA_I00:def12

      func t1 + t2 -> Function of X, INT means for s be Element of X holds (it . s) = ((t1 . s) + (t2 . s));

      compatibility

      proof

        let ti be Function of X, INT ;



         A4: ( dom t1) = X by FUNCT_2:def 1;



         A5: ( dom t2) = X by FUNCT_2:def 1;



         A6: ( dom (t1 + t2)) = (( dom t1) /\ ( dom t2)) by VALUED_1:def 1;

        hence ti = (t1 + t2) implies for s be Element of X holds (ti . s) = ((t1 . s) + (t2 . s)) by A4, A5, VALUED_1:def 1;



         A7: ( dom ti) = X by FUNCT_2:def 1;

        assume for s be Element of X holds (ti . s) = ((t1 . s) + (t2 . s));

        then for s be object st s in X holds (ti . s) = ((t1 . s) + (t2 . s));

        hence ti = (t1 + t2) by A6, A4, A5, A7, VALUED_1:def 1;

      end;

      coherence

      proof

        thus (t1 + t2) is Function of X, INT ;

      end;

    end

    registration

      let A be non empty set;

      let B be infinite set;

      cluster ( Funcs (A,B)) -> infinite;

      coherence

      proof



         A1: ( card ( card B)) = ( card B);

        ( card A) = ( card ( card A));

        then

         A2: ( card ( Funcs (A,B))) = ( exp (( card B),( card A))) by A1, FUNCT_5: 61;

        set a = the Element of A;



         A3: ( card {a}) = 1 by CARD_1: 30;

         {a} c= A by ZFMISC_1: 31;

        then 1 c= ( card A) by A3, CARD_1: 11;

        then ( exp (( card B),1)) c= ( card ( Funcs (A,B))) by A2, CARD_2: 93;

        hence thesis by CARD_2: 27;

      end;

    end

    definition

      let N be set;

      let v be Function;

      let f be Function;

      :: AOFA_I00:def13

      func v ** (f,N) -> Function means

      : Def13: (ex Y be set st (for y be set holds y in Y iff ex h be Function st h in ( dom v) & y in ( rng h)) & for a be set holds a in ( dom it ) iff a in ( Funcs (N,Y)) & ex g be Function st a = g & (g * f) in ( dom v)) & for g be Function st g in ( dom it ) holds (it . g) = (v . (g * f));

      uniqueness

      proof

        let F1,F2 be Function;

        given Y1 be set such that

         A1: for y be set holds y in Y1 iff ex h be Function st h in ( dom v) & y in ( rng h) and

         A2: for a be set holds a in ( dom F1) iff a in ( Funcs (N,Y1)) & ex g be Function st a = g & (g * f) in ( dom v);

        assume

         A3: for g be Function st g in ( dom F1) holds (F1 . g) = (v . (g * f));

        given Y2 be set such that

         A4: for y be set holds y in Y2 iff ex h be Function st h in ( dom v) & y in ( rng h) and

         A5: for a be set holds a in ( dom F2) iff a in ( Funcs (N,Y2)) & ex g be Function st a = g & (g * f) in ( dom v);

        now

          let a be object;

          a in Y1 iff ex h be Function st h in ( dom v) & a in ( rng h) by A1;

          hence a in Y1 iff a in Y2 by A4;

        end;

        then

         A6: Y1 = Y2 by TARSKI: 2;

        now

          let a be object;

          a in ( dom F1) iff a in ( Funcs (N,Y1)) & ex g be Function st a = g & (g * f) in ( dom v) by A2;

          hence a in ( dom F1) iff a in ( dom F2) by A5, A6;

        end;

        then

         A7: ( dom F1) = ( dom F2) by TARSKI: 2;

        assume

         A8: for g be Function st g in ( dom F2) holds (F2 . g) = (v . (g * f));

        now

          let a be object;

          assume

           A9: a in ( dom F1);

          then

          consider g be Function such that

           A10: a = g and (g * f) in ( dom v) by A2;



          thus (F1 . a) = (v . (g * f)) by A3, A9, A10

          .= (F2 . a) by A8, A7, A9, A10;

        end;

        hence thesis by A7;

      end;

      existence

      proof

        defpred F[ object, object] means ex g be Function st g = $1 & $2 = (v . (g * f));

        defpred R[ object] means ex g be Function st g = $1 & (g * f) in ( dom v);

        defpred P[ object, object] means ex g be Function st $1 = g & $2 = ( rng g);



         A11: for x,y,z be object st P[x, y] & P[x, z] holds y = z;

        consider X be set such that

         A12: for x be object holds x in X iff ex y be object st y in ( dom v) & P[y, x] from TARSKI:sch 1( A11);

        set Y = ( union X);

        consider D be set such that

         A13: for x be object holds x in D iff x in ( Funcs (N,Y)) & R[x] from XBOOLE_0:sch 1;



         A14: for x be object st x in D holds ex y be object st F[x, y]

        proof

          let x be object;

          assume x in D;

          then

          consider y be Function such that

           A15: y = x and (y * f) in ( dom v) by A13;

          take (v . (y * f));

          thus thesis by A15;

        end;

        consider F be Function such that

         A16: ( dom F) = D & for g be object st g in D holds F[g, (F . g)] from CLASSES1:sch 1( A14);

        take F;

        hereby

          take Y;

          hereby

            let y be set;

            hereby

              assume y in Y;

              then

              consider a be set such that

               A17: y in a and

               A18: a in X by TARSKI:def 4;

              ex z be object st z in ( dom v) & P[z, a] by A12, A18;

              hence ex h be Function st h in ( dom v) & y in ( rng h) by A17;

            end;

            given h be Function such that

             A19: h in ( dom v) and

             A20: y in ( rng h);

            ( rng h) in X by A12, A19;

            hence y in Y by A20, TARSKI:def 4;

          end;

          let a be set;

          thus a in ( dom F) iff a in ( Funcs (N,Y)) & ex g be Function st a = g & (g * f) in ( dom v) by A13, A16;

        end;

        let g be Function;

        assume g in ( dom F);

        then F[g, (F . g)] by A16;

        hence thesis;

      end;

    end

    definition

      let X,Y,Z,N be non empty set;

      let v be Element of ( Funcs (( Funcs (X,Y)),Z));

      let f be Function of X, N;

      :: original: **

      redefine

      func v ** (f,N) -> Element of ( Funcs (( Funcs (N,Y)),Z)) ;

      coherence

      proof

        consider Y0 be set such that

         A1: for y be set holds y in Y0 iff ex h be Function st h in ( dom v) & y in ( rng h) and

         A2: for a be set holds a in ( dom (v ** (f,N))) iff a in ( Funcs (N,Y0)) & ex g be Function st a = g & (g * f) in ( dom v) by Def13;



         A3: ( dom v) = ( Funcs (X,Y)) by FUNCT_2:def 1;



         A4: Y0 = Y

        proof

          thus Y0 c= Y

          proof

            let y be object;

            assume y in Y0;

            then

            consider h be Function such that

             A5: h in ( dom v) and

             A6: y in ( rng h) by A1;

            ( rng h) c= Y by A5, FUNCT_2: 92;

            hence thesis by A6;

          end;

          let y be object;

          assume y in Y;

          then

          reconsider y as Element of Y;

          reconsider h = (X --> y) as Function of X, Y;



           A7: ( rng h) = {y} by FUNCOP_1: 8;



           A8: h in ( Funcs (X,Y)) by FUNCT_2: 8;

          y in {y} by TARSKI:def 1;

          hence thesis by A3, A1, A7, A8;

        end;



         A9: ( dom (v ** (f,N))) = ( Funcs (N,Y))

        proof

          thus ( dom (v ** (f,N))) c= ( Funcs (N,Y)) by A2, A4;

          let a be object;

          assume

           A10: a in ( Funcs (N,Y));

          then

          reconsider g = a as Function of N, Y by FUNCT_2: 66;

          (g * f) in ( Funcs (X,Y)) by FUNCT_2: 8;

          hence thesis by A3, A2, A4, A10;

        end;

        ( rng (v ** (f,N))) c= Z

        proof

          let a be object;

          assume a in ( rng (v ** (f,N)));

          then

          consider g be object such that

           A11: g in ( dom (v ** (f,N))) and

           A12: a = ((v ** (f,N)) . g) by FUNCT_1:def 3;

          reconsider g as Element of ( Funcs (N,Y)) by A9, A11;

          reconsider gf = (g * f) as Element of ( Funcs (X,Y)) by FUNCT_2: 8;

          a = (v . gf) by A11, A12, Def13;

          hence thesis;

        end;

        hence thesis by A9, FUNCT_2:def 2;

      end;

    end

    theorem :: AOFA_I00:3



     Th3: for f1,f2,g be Function st ( rng g) c= ( dom f2) holds ((f1 +* f2) * g) = (f2 * g)

    proof

      let f1,f2,g be Function;

      assume

       A1: ( rng g) c= ( dom f2);

       A2:

      now

        let x be object;

        assume

         A3: x in ( dom g);

        then

         A4: ((f2 * g) . x) = (f2 . (g . x)) by FUNCT_1: 13;



         A5: (g . x) in ( rng g) by A3, FUNCT_1: 3;

        (((f1 +* f2) * g) . x) = ((f1 +* f2) . (g . x)) by A3, FUNCT_1: 13;

        hence (((f1 +* f2) * g) . x) = ((f2 * g) . x) by A1, A4, A5, FUNCT_4: 13;

      end;

      ( dom (f1 +* f2)) = (( dom f1) \/ ( dom f2)) by FUNCT_4:def 1;

      then

       A6: ( dom ((f1 +* f2) * g)) = ( dom g) by A1, RELAT_1: 27, XBOOLE_1: 10;

      ( dom (f2 * g)) = ( dom g) by A1, RELAT_1: 27;

      hence thesis by A6, A2;

    end;

    theorem :: AOFA_I00:4



     Th4: for X,N,I be non empty set holds for s be Function of X, I holds for c be Function of X, N st c is one-to-one holds for n be Element of I holds ((N --> n) +* (s * (c " ))) is Function of N, I

    proof

      let X,N,I be non empty set;

      let s be Function of X, I;

      let c be Function of X, N;

      assume c is one-to-one;

      then

       A1: ( dom (c " )) = ( rng c) by FUNCT_1: 33;

      let n be Element of I;

      set f = (N --> n), g = (s * (c " ));



       A2: ( dom g) c= ( dom (c " )) by RELAT_1: 25;

      ( rng g) c= ( rng s) by RELAT_1: 26;

      then ( rng g) c= I by XBOOLE_1: 1;

      then

       A3: (( rng f) \/ ( rng g)) c= I by XBOOLE_1: 8;



       A5: ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

      ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

      then ( dom (f +* g)) = N by A2, A1, XBOOLE_1: 1, XBOOLE_1: 12;

      hence thesis by A5, A3, FUNCT_2: 2, XBOOLE_1: 1;

    end;

    theorem :: AOFA_I00:5



     Th5: for N,X,I be non empty set holds for v1,v2 be Function st ( dom v1) = ( dom v2) & ( dom v1) = ( Funcs (X,I)) holds for f be Function of X, N st f is one-to-one & (v1 ** (f,N)) = (v2 ** (f,N)) holds v1 = v2

    proof

      let N,X,I be non empty set;

      let v1,v2 be Function such that

       A1: ( dom v1) = ( dom v2) and

       A2: ( dom v1) = ( Funcs (X,I));

      reconsider rv1 = ( rng v1), rv2 = ( rng v2) as non empty set by A1, A2, RELAT_1: 42;

      reconsider Z = (rv1 \/ rv2) as non empty set;



       A3: ( rng v2) c= Z by XBOOLE_1: 7;

      ( rng v1) c= Z by XBOOLE_1: 7;

      then

      reconsider f1 = v1, f2 = v2 as Element of ( Funcs (( Funcs (X,I)),Z)) by A1, A2, A3, FUNCT_2:def 2;

      let f be Function of X, N such that

       A4: f is one-to-one and

       A5: (v1 ** (f,N)) = (v2 ** (f,N));



       A6: ( dom (f2 ** (f,N))) = ( Funcs (N,I)) by FUNCT_2:def 1;



       A7: ( dom (f1 ** (f,N))) = ( Funcs (N,I)) by FUNCT_2:def 1;

      now

        set i = the Element of I;

        let a be object;



         A8: ( dom f) = X by FUNCT_2:def 1;

        assume a in ( Funcs (X,I));

        then

        reconsider h = a as Element of ( Funcs (X,I));

        set g = ((N --> i) +* (h * (f " )));



         A9: ( dom h) = X by FUNCT_2:def 1;

        ( rng (f " )) = ( dom f) by A4, FUNCT_1: 33;



        then ( dom (h * (f " ))) = ( dom (f " )) by A9, RELAT_1: 27

        .= ( rng f) by A4, FUNCT_1: 33;



        then

         A10: (g * f) = ((h * (f " )) * f) by Th3

        .= (h * ((f " ) * f)) by RELAT_1: 36

        .= (h * ( id X)) by A4, A8, FUNCT_1: 39

        .= a by A9, RELAT_1: 52;

        g is Function of N, I by A4, Th4;

        then

         A11: g in ( Funcs (N,I)) by FUNCT_2: 8;

        then ((v1 ** (f,N)) . g) = (v1 . a) by A7, A10, Def13;

        hence (v1 . a) = (v2 . a) by A5, A6, A11, A10, Def13;

      end;

      hence thesis by A1, A2;

    end;

    registration

      let X be set;

      cluster one-to-one onto for Function of X, ( card X);

      existence

      proof

        (X,( card X)) are_equipotent by CARD_1:def 2;

        then

        consider f be Function such that

         A1: f is one-to-one and

         A2: ( dom f) = X and

         A3: ( rng f) = ( card X) by WELLORD2:def 4;

        reconsider f as Function of X, ( card X) by A2, A3, FUNCT_2: 2;

        take f;

        thus f is one-to-one by A1;

        thus ( rng f) = ( card X) by A3;

      end;

      cluster one-to-one onto for Function of ( card X), X;

      existence

      proof

        (X,( card X)) are_equipotent by CARD_1:def 2;

        then

        consider f be Function such that

         A4: f is one-to-one and

         A5: ( dom f) = ( card X) and

         A6: ( rng f) = X by WELLORD2:def 4;

        reconsider f as Function of ( card X), X by A5, A6, FUNCT_2: 2;

        take f;

        thus f is one-to-one by A4;

        thus ( rng f) = X by A6;

      end;

    end

    definition

      let X be set;

      mode Enumeration of X is one-to-one onto Function of X, ( card X);

      mode Denumeration of X is one-to-one onto Function of ( card X), X;

    end

    theorem :: AOFA_I00:6



     Th6: for X be set, f be Function holds f is Enumeration of X iff ( dom f) = X & ( rng f) = ( card X) & f is one-to-one

    proof

      let X be set, f be Function;

      ( card X) = {} implies X = {} ;

      hence thesis by FUNCT_2: 2, FUNCT_2:def 1, FUNCT_2:def 3;

    end;

    theorem :: AOFA_I00:7



     Th7: for X be set, f be Function holds f is Denumeration of X iff ( dom f) = ( card X) & ( rng f) = X & f is one-to-one

    proof

      let X be set, f be Function;

      X = {} implies ( card X) = {} ;

      hence thesis by FUNCT_2: 2, FUNCT_2:def 1, FUNCT_2:def 3;

    end;

    theorem :: AOFA_I00:8



     Th8: for X be non empty set, x,y be Element of X holds for f be Enumeration of X holds ((f +* (x,(f . y))) +* (y,(f . x))) is Enumeration of X

    proof

      let X be non empty set, x,y be Element of X;

      let f be Enumeration of X;

      set g = ((f +* (x,(f . y))) +* (y,(f . x)));

      set A = ( dom g);



       A1: ( dom (f +* (x,(f . y)))) = ( dom f) by FUNCT_7: 30;



       A2: A = ( dom (f +* (x,(f . y)))) by FUNCT_7: 30;



       A3: ( dom f) = X by Th6;



       A4: ( rng f) = ( card X) by Th6;



       A5: ( rng ((f +* (x,(f . y))) +* (y,(f . x)))) = ( rng f)

      proof

         {(f . x)} c= ( rng f) by A4, ZFMISC_1: 31;

        then

         A6: (( rng f) \/ {(f . x)}) = ( rng f) by XBOOLE_1: 12;



         A7: ( rng g) c= (( rng (f +* (x,(f . y)))) \/ {(f . x)}) by FUNCT_7: 100;

         {(f . y)} c= ( rng f) by A4, ZFMISC_1: 31;

        then (( rng f) \/ {(f . y)}) = ( rng f) by XBOOLE_1: 12;

        then (( rng (f +* (x,(f . y)))) \/ {(f . x)}) c= ( rng f) by A6, FUNCT_7: 100, XBOOLE_1: 9;

        hence ( rng g) c= ( rng f) by A7;

        let z be object;

        assume z in ( rng f);

        then

        consider a be object such that

         A8: a in ( dom f) and

         A9: z = (f . a) by FUNCT_1:def 3;

        per cases ;

          suppose

           A10: a <> x & a <> y;

          then

           A11: (g . a) = ((f +* (x,(f . y))) . a) by FUNCT_7: 32;

          ((f +* (x,(f . y))) . a) = z by A9, A10, FUNCT_7: 32;

          hence thesis by A1, A2, A8, A11, FUNCT_1:def 3;

        end;

          suppose a = x;

          then (g . y) = z by A1, A3, A9, FUNCT_7: 31;

          hence thesis by A1, A2, A3, FUNCT_1:def 3;

        end;

          suppose

           A12: a = y;

          then

           A13: x <> y implies (g . x) = ((f +* (x,z)) . x) by A9, FUNCT_7: 32;



           A14: ((f +* (x,z)) . x) = z by A3, FUNCT_7: 31;

          x = y implies (g . x) = z by A1, A3, A9, A12, FUNCT_7: 31;

          hence thesis by A1, A2, A3, A14, A13, FUNCT_1:def 3;

        end;

      end;

      ((f +* (x,(f . y))) +* (y,(f . x))) is one-to-one

      proof

        let a,b be object;



         A15: a <> y implies (g . a) = ((f +* (x,(f . y))) . a) by FUNCT_7: 32;



         A16: a <> x implies ((f +* (x,(f . y))) . a) = (f . a) by FUNCT_7: 32;



         A17: b = y implies (g . b) = (f . x) by A1, A3, FUNCT_7: 31;



         A18: b <> y implies (g . b) = ((f +* (x,(f . y))) . b) by FUNCT_7: 32;



         A19: b = x implies ((f +* (x,(f . y))) . b) = (f . y) by A3, FUNCT_7: 31;



         A20: a = x implies ((f +* (x,(f . y))) . a) = (f . y) by A3, FUNCT_7: 31;



         A21: b <> x implies ((f +* (x,(f . y))) . b) = (f . b) by FUNCT_7: 32;

        a = y implies (g . a) = (f . x) by A1, A3, FUNCT_7: 31;

        hence thesis by A2, A3, A15, A20, A16, A17, A18, A19, A21, FUNCT_1:def 4;

      end;

      hence thesis by A1, A2, A3, A4, A5, Th6;

    end;

    theorem :: AOFA_I00:9

    for X be non empty set, x be Element of X holds ex f be Enumeration of X st (f . x) = 0

    proof

      let X be non empty set, x be Element of X;

      set f = the Enumeration of X;



       A1: 0 in ( card X) by ORDINAL3: 8;



       A2: ( rng f) = ( card X) by Th6;

      ( dom f) = X by Th6;

      then

      consider y be object such that

       A3: y in X and

       A4: 0 = (f . y) by A1, A2, FUNCT_1:def 3;

      reconsider y as Element of X by A3;

      reconsider g = ((f +* (y,(f . x))) +* (x, 0 )) as Enumeration of X by A4, Th8;

      take g;

      ( dom f) = X by Th6;

      then ( dom (f +* (y,(f . x)))) = X by FUNCT_7: 30;

      hence thesis by FUNCT_7: 31;

    end;

    theorem :: AOFA_I00:10

    for X be non empty set, f be Denumeration of X holds (f . 0 ) in X by FUNCT_2: 5, ORDINAL3: 8;

    theorem :: AOFA_I00:11



     Th11: for X be countable set, f be Enumeration of X holds ( rng f) c= NAT

    proof

      let X be countable set, f be Enumeration of X;

      ( card X) c= NAT by CARD_3:def 14;

      hence thesis;

    end;

    definition

      let X be set;

      let f be Enumeration of X;

      :: original: "

      redefine

      func f " -> Denumeration of X ;

      coherence

      proof

        ( rng f) = ( card X) by Th6;

        then

         A1: ( dom (f " )) = ( card X) by FUNCT_1: 33;

        ( dom f) = X by Th6;

        then ( rng (f " )) = X by FUNCT_1: 33;

        hence thesis by A1, Th7;

      end;

    end

    definition

      let X be set;

      let f be Denumeration of X;

      :: original: "

      redefine

      func f " -> Enumeration of X ;

      coherence

      proof

        ( rng f) = X by Th7;

        then

         A1: ( dom (f " )) = X by FUNCT_1: 33;

        ( dom f) = ( card X) by Th7;

        then ( rng (f " )) = ( card X) by FUNCT_1: 33;

        hence thesis by A1, Th6;

      end;

    end

    theorem :: AOFA_I00:12

    for n,m be Nat holds ( 0 to_power (n + m)) = (( 0 to_power n) * ( 0 to_power m))

    proof

      let n,m be Nat;

      per cases ;

        suppose

         A1: n > 0 or m > 0 ;

        then ( 0 to_power n) = 0 or ( 0 to_power m) = 0 by POWER:def 2;

        hence thesis by A1, POWER:def 2;

      end;

        suppose

         A2: n = 0 & m = 0 ;

        then ( 0 to_power (n + m)) = 1 by POWER: 24;

        hence thesis by A2;

      end;

    end;

    theorem :: AOFA_I00:13

    for x be Real holds for n,m be Nat holds ((x to_power n) to_power m) = (x to_power (n * m)) by NEWTON: 9;

    begin

    definition

      let X be non empty set;

      mode INT-Variable of X is Function of ( Funcs (X, INT )), X;

      mode INT-Expression of X is Function of ( Funcs (X, INT )), INT ;

      mode INT-Array of X is Function of INT , X;

    end

    reserve A for preIfWhileAlgebra;

    definition

      let A;

      let I be Element of A;

      let X be non empty set;

      let T be Subset of ( Funcs (X, INT ));

      let f be ExecutionFunction of A, ( Funcs (X, INT )), T;

      :: AOFA_I00:def14

      pred I is_assignment_wrt A,X,f means I in ( ElementaryInstructions A) & ex v be INT-Variable of X, t be INT-Expression of X st for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s)));

    end

    definition

      let A;

      let X be non empty set;

      let T be Subset of ( Funcs (X, INT ));

      let f be ExecutionFunction of A, ( Funcs (X, INT )), T;

      let v be INT-Variable of X;

      let t be INT-Expression of X;

      :: AOFA_I00:def15

      pred v,t form_assignment_wrt f means ex I be Element of A st I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s)));

    end

    definition

      let A;

      let X be non empty set;

      let T be Subset of ( Funcs (X, INT ));

      let f be ExecutionFunction of A, ( Funcs (X, INT )), T;

      :: AOFA_I00:def16

      mode INT-Variable of A,f -> INT-Variable of X means ex t be INT-Expression of X st (it ,t) form_assignment_wrt f;

      existence

      proof

        consider I be Element of A such that

         A2: I is_assignment_wrt (A,X,f) by A1;

        consider v be INT-Variable of X, t be INT-Expression of X such that

         A3: for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s))) by A2;

        take v, t, I;

        thus thesis by A2, A3;

      end;

    end

    definition

      let A;

      let X be non empty set;

      let T be Subset of ( Funcs (X, INT ));

      let f be ExecutionFunction of A, ( Funcs (X, INT )), T;

      :: AOFA_I00:def17

      mode INT-Expression of A,f -> INT-Expression of X means ex v be INT-Variable of X st (v,it ) form_assignment_wrt f;

      existence

      proof

        consider I be Element of A such that

         A2: I is_assignment_wrt (A,X,f) by A1;

        consider v be INT-Variable of X, t be INT-Expression of X such that

         A3: for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s))) by A2;

        take t, v, I;

        thus thesis by A2, A3;

      end;

    end

    definition

      let X,Y be non empty set;

      let f be Element of ( Funcs (X,Y));

      let x be Element of X;

      :: original: .

      redefine

      func f . x -> Element of Y ;

      coherence

      proof

        (f . x) in ( rng f) by FUNCT_2: 4;

        hence thesis;

      end;

    end

    definition

      let X be non empty set;

      let x be Element of X;

      :: AOFA_I00:def18

      func . x -> INT-Expression of X means

      : Def18: for s be Element of ( Funcs (X, INT )) holds (it . s) = (s . x);

      correctness

      proof

        deffunc F( Element of ( Funcs (X, INT ))) = ($1 . x);

        thus ex f be Function of ( Funcs (X, INT )), INT st for x be Element of ( Funcs (X, INT )) holds (f . x) = F(x) from FUNCT_2:sch 4;

        let f1,f2 be INT-Expression of X such that

         A1: for s be Element of ( Funcs (X, INT )) holds (f1 . s) = (s . x) and

         A2: for s be Element of ( Funcs (X, INT )) holds (f2 . s) = (s . x);

        now

          let s be Element of ( Funcs (X, INT ));



          thus (f1 . s) = (s . x) by A1

          .= (f2 . s) by A2;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty set;

      let v be INT-Variable of X;

      :: AOFA_I00:def19

      func . v -> INT-Expression of X means

      : Def19: for s be Element of ( Funcs (X, INT )) holds (it . s) = (s . (v . s));

      correctness

      proof

        deffunc F( Element of ( Funcs (X, INT ))) = ($1 . (v . $1));

        thus ex f be Function of ( Funcs (X, INT )), INT st for x be Element of ( Funcs (X, INT )) holds (f . x) = F(x) from FUNCT_2:sch 4;

        let f1,f2 be INT-Expression of X such that

         A1: for s be Element of ( Funcs (X, INT )) holds (f1 . s) = (s . (v . s)) and

         A2: for s be Element of ( Funcs (X, INT )) holds (f2 . s) = (s . (v . s));

        now

          let s be Element of ( Funcs (X, INT ));



          thus (f1 . s) = (s . (v . s)) by A1

          .= (f2 . s) by A2;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty set;

      let x be Element of X;

      :: AOFA_I00:def20

      func ^ x -> INT-Variable of X equals (( Funcs (X, INT )) --> x);

      correctness ;

    end

    theorem :: AOFA_I00:14

    for X be non empty set holds for x be Element of X holds ( . x) = ( . ( ^ x))

    proof

      let X be non empty set;

      let x be Element of X;

      for s be Element of ( Funcs (X, INT )) holds (( . ( ^ x)) . s) = (s . x)

      proof

        let s be Element of ( Funcs (X, INT ));



        thus (( . ( ^ x)) . s) = (s . (( ^ x) . s)) by Def19

        .= (s . x);

      end;

      hence thesis by Def18;

    end;

    definition

      let X be non empty set;

      let i be Integer;

      :: AOFA_I00:def21

      func . (i,X) -> INT-Expression of X equals (( Funcs (X, INT )) --> i);

      correctness

      proof

        i in INT by INT_1:def 2;

        hence thesis by FUNCOP_1: 45;

      end;

    end

    theorem :: AOFA_I00:15

    for X be non empty set, t be INT-Expression of X holds (t + ( . ( 0 ,X))) = t & (t (#) ( . (1,X))) = t

    proof

      let X be non empty set;

      let t be INT-Expression of X;

      now

        let s be Element of ( Funcs (X, INT ));

        ( dom (t + ( . ( 0 ,X)))) = ( Funcs (X, INT )) by FUNCT_2:def 1;



        hence ((t + ( . ( 0 ,X))) . s) = ((t . s) + (( . ( 0 ,X)) . s)) by VALUED_1:def 1

        .= (t . s);

      end;

      hence (t + ( . ( 0 ,X))) = t;

      now

        let s be Element of ( Funcs (X, INT ));

        ( dom (t (#) ( . (1,X)))) = ( Funcs (X, INT )) by FUNCT_2:def 1;



        hence ((t (#) ( . (1,X))) . s) = ((t . s) * (( . (1,X)) . s)) by VALUED_1:def 4

        .= ((t . s) * 1)

        .= (t . s);

      end;

      hence thesis;

    end;

    definition

      let A;

      let X be non empty set;

      let T be Subset of ( Funcs (X, INT ));

      let f be ExecutionFunction of A, ( Funcs (X, INT )), T;

      :: AOFA_I00:def22

      attr f is Euclidean means

      : Def22: (for v be INT-Variable of A, f, t be INT-Expression of A, f holds (v,t) form_assignment_wrt f) & (for i be Integer holds ( . (i,X)) is INT-Expression of A, f) & (for v be INT-Variable of A, f holds ( . v) is INT-Expression of A, f) & (for x be Element of X holds ( ^ x) is INT-Variable of A, f) & (ex a be INT-Array of X st (a | ( card X)) is one-to-one & for t be INT-Expression of A, f holds (a * t) is INT-Variable of A, f) & (for t be INT-Expression of A, f holds ( - t) is INT-Expression of A, f) & for t1,t2 be INT-Expression of A, f holds (t1 (#) t2) is INT-Expression of A, f & (t1 + t2) is INT-Expression of A, f & (t1 div t2) is INT-Expression of A, f & (t1 mod t2) is INT-Expression of A, f & ( leq (t1,t2)) is INT-Expression of A, f & ( gt (t1,t2)) is INT-Expression of A, f;

    end

    definition

      let A;

      :: AOFA_I00:def23

      attr A is Euclidean means

      : Def23: for X be non empty countable set, T be Subset of ( Funcs (X, INT )) holds ex f be ExecutionFunction of A, ( Funcs (X, INT )), T st f is Euclidean;

    end

    definition

      :: AOFA_I00:def24

      func INT-ElemIns -> infinite disjoint_with_NAT set equals [:( Funcs (( Funcs ( NAT , INT )), NAT )), ( Funcs (( Funcs ( NAT , INT )), INT )):];

      coherence ;

    end

    definition

      :: AOFA_I00:def25

      mode INT-Exec -> ExecutionFunction of ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns )), ( Funcs ( NAT , INT )), (( Funcs ( NAT , INT )) \ ( 0 , 0 )) means

      : Def25: for s be Element of ( Funcs ( NAT , INT )) holds for v be Element of ( Funcs (( Funcs ( NAT , INT )), NAT )) holds for e be Element of ( Funcs (( Funcs ( NAT , INT )), INT )) holds (it . (s,( root-tree [v, e]))) = (s +* ((v . s),(e . s)));

      existence

      proof

        reconsider i0 = 0 as Element of INT by INT_1:def 1;

        set Q = ( Funcs ( NAT , INT )), T = (Q \ ( 0 , 0 ));

        set S = ECIW-signature , G = INT-ElemIns ;

        set A = ( FreeUnivAlgNSG (S,G));



         A1: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;

        reconsider q0 = ( NAT --> i0) as Element of Q by FUNCT_2: 8;

        defpred P[ object, object] means ex s be Element of Q, v be Element of ( Funcs (Q, NAT )), e be Element of ( Funcs (Q, INT )) st $1 = [s, ( root-tree [v, e])] & $2 = (s +* ((v . s),(e . s)));



         A2: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;



         A3: for x be object st x in [:Q, ( ElementaryInstructions A):] holds ex y be object st y in Q & P[x, y]

        proof

          let x be object;

          assume x in [:Q, ( ElementaryInstructions A):];

          then

          consider s,I be object such that

           A4: s in Q and

           A5: I in ( ElementaryInstructions A) and

           A6: x = [s, I] by ZFMISC_1:def 2;

          reconsider s as Element of Q by A4;

          consider a be Symbol of ( DTConUA (S,G)) such that

           A7: I = ( root-tree a) and

           A8: a in ( Terminals ( DTConUA (S,G))) by A2, A5;

          consider v,e be object such that

           A9: v in ( Funcs (( Funcs ( NAT , INT )), NAT )) and

           A10: e in ( Funcs (( Funcs ( NAT , INT )), INT )) and

           A11: a = [v, e] by A1, A8, ZFMISC_1:def 2;

          reconsider e as Element of ( Funcs (Q, INT )) by A10;

          reconsider v as Element of ( Funcs (Q, NAT )) by A9;

          take y = (s +* ((v . s),(e . s)));

          thus y in Q by FUNCT_2: 8;

          take s, v, e;

          thus x = [s, ( root-tree [v, e])] & y = (s +* ((v . s),(e . s))) by A6, A7, A11;

        end;

        consider g be Function such that

         A12: ( dom g) = [:Q, ( ElementaryInstructions A):] & ( rng g) c= Q and

         A13: for x be object st x in [:Q, ( ElementaryInstructions A):] holds P[x, (g . x)] from FUNCT_1:sch 6( A3);

        reconsider g as Function of [:Q, ( ElementaryInstructions A):], Q by A12, FUNCT_2: 2;

        consider f be ExecutionFunction of A, Q, T such that

         A14: (f | [:Q, ( ElementaryInstructions A):]) = g and for s be Element of Q holds for C,I be Element of A st not f iteration_terminates_for ((I \; C),(f . (s,C))) holds (f . (s,( while (C,I)))) = q0 by AOFA_000: 91;

        take f;

        let s be Element of ( Funcs ( NAT , INT ));

        let v be Element of ( Funcs (( Funcs ( NAT , INT )), NAT ));

        let e be Element of ( Funcs (( Funcs ( NAT , INT )), INT ));

        set I = ( root-tree [v, e]);

         [v, e] in G by ZFMISC_1: 87;

        then I in ( ElementaryInstructions A) by A2, A1;

        then

         A15: [s, I] in [:Q, ( ElementaryInstructions A):] by ZFMISC_1: 87;

        then

        consider s9 be Element of Q, v9 be Element of ( Funcs (Q, NAT )), e9 be Element of ( Funcs (Q, INT )) such that

         A16: [s, I] = [s9, ( root-tree [v9, e9])] and

         A17: (g . [s, I]) = (s9 +* ((v9 . s9),(e9 . s9))) by A13;

        I = ( root-tree [v9, e9]) by A16, XTUPLE_0: 1;

        then

         A18: [v, e] = [v9, e9] by TREES_4: 4;

        then

         A19: v = v9 by XTUPLE_0: 1;



         A20: e = e9 by A18, XTUPLE_0: 1;

        s = s9 by A16, XTUPLE_0: 1;

        hence thesis by A14, A15, A17, A19, A20, FUNCT_1: 49;

      end;

    end

    definition

      let X be non empty set;

      :: AOFA_I00:def26

      func INT-ElemIns X -> infinite disjoint_with_NAT set equals [:( Funcs (( Funcs (X, INT )),X)), ( Funcs (( Funcs (X, INT )), INT )):];

      coherence ;

    end

    definition

      let X be non empty set;

      let x be Element of X;

      :: AOFA_I00:def27

      mode INT-Exec of x -> ExecutionFunction of ( FreeUnivAlgNSG ( ECIW-signature ,( INT-ElemIns X))), ( Funcs (X, INT )), (( Funcs (X, INT )) \ (x, 0 )) means for s be Element of ( Funcs (X, INT )) holds for v be Element of ( Funcs (( Funcs (X, INT )),X)) holds for e be Element of ( Funcs (( Funcs (X, INT )), INT )) holds (it . (s,( root-tree [v, e]))) = (s +* ((v . s),(e . s)));

      existence

      proof

        reconsider i0 = 0 as Element of INT by INT_1:def 1;

        set Q = ( Funcs (X, INT )), T = (Q \ (x, 0 ));

        set S = ECIW-signature , G = ( INT-ElemIns X);

        set A = ( FreeUnivAlgNSG (S,G));



         A1: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;

        reconsider q0 = (X --> i0) as Element of Q by FUNCT_2: 8;

        defpred P[ object, object] means ex s be Element of Q, v be Element of ( Funcs (Q,X)), e be Element of ( Funcs (Q, INT )) st $1 = [s, ( root-tree [v, e])] & $2 = (s +* ((v . s),(e . s)));



         A2: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;



         A3: for x be object st x in [:Q, ( ElementaryInstructions A):] holds ex y be object st y in Q & P[x, y]

        proof

          let x be object;

          assume x in [:Q, ( ElementaryInstructions A):];

          then

          consider s,I be object such that

           A4: s in Q and

           A5: I in ( ElementaryInstructions A) and

           A6: x = [s, I] by ZFMISC_1:def 2;

          reconsider s as Element of Q by A4;

          consider a be Symbol of ( DTConUA (S,G)) such that

           A7: I = ( root-tree a) and

           A8: a in ( Terminals ( DTConUA (S,G))) by A2, A5;

          consider v,e be object such that

           A9: v in ( Funcs (( Funcs (X, INT )),X)) and

           A10: e in ( Funcs (( Funcs (X, INT )), INT )) and

           A11: a = [v, e] by A1, A8, ZFMISC_1:def 2;

          reconsider e as Element of ( Funcs (Q, INT )) by A10;

          reconsider v as Element of ( Funcs (Q,X)) by A9;

          take y = (s +* ((v . s),(e . s)));

          thus y in Q by FUNCT_2: 8;

          take s, v, e;

          thus x = [s, ( root-tree [v, e])] & y = (s +* ((v . s),(e . s))) by A6, A7, A11;

        end;

        consider g be Function such that

         A12: ( dom g) = [:Q, ( ElementaryInstructions A):] & ( rng g) c= Q and

         A13: for x be object st x in [:Q, ( ElementaryInstructions A):] holds P[x, (g . x)] from FUNCT_1:sch 6( A3);

        reconsider g as Function of [:Q, ( ElementaryInstructions A):], Q by A12, FUNCT_2: 2;

        consider f be ExecutionFunction of A, Q, T such that

         A14: (f | [:Q, ( ElementaryInstructions A):]) = g and for s be Element of Q holds for C,I be Element of A st not f iteration_terminates_for ((I \; C),(f . (s,C))) holds (f . (s,( while (C,I)))) = q0 by AOFA_000: 91;

        take f;

        let s be Element of ( Funcs (X, INT ));

        let v be Element of ( Funcs (( Funcs (X, INT )),X));

        let e be Element of ( Funcs (( Funcs (X, INT )), INT ));

        set I = ( root-tree [v, e]);

         [v, e] in G by ZFMISC_1: 87;

        then I in ( ElementaryInstructions A) by A2, A1;

        then

         A15: [s, I] in [:Q, ( ElementaryInstructions A):] by ZFMISC_1: 87;

        then

        consider s9 be Element of Q, v9 be Element of ( Funcs (Q,X)), e9 be Element of ( Funcs (Q, INT )) such that

         A16: [s, I] = [s9, ( root-tree [v9, e9])] and

         A17: (g . [s, I]) = (s9 +* ((v9 . s9),(e9 . s9))) by A13;

        I = ( root-tree [v9, e9]) by A16, XTUPLE_0: 1;

        then

         A18: [v, e] = [v9, e9] by TREES_4: 4;

        then

         A19: v = v9 by XTUPLE_0: 1;



         A20: e = e9 by A18, XTUPLE_0: 1;

        s = s9 by A16, XTUPLE_0: 1;

        hence thesis by A14, A15, A17, A19, A20, FUNCT_1: 49;

      end;

    end

    definition

      let X be non empty set;

      let T be Subset of ( Funcs (X, INT ));

      let c be Enumeration of X;

      :: AOFA_I00:def28

      mode INT-Exec of c,T -> ExecutionFunction of ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns )), ( Funcs (X, INT )), T means

      : Def28: for s be Element of ( Funcs (X, INT )) holds for v be Element of ( Funcs (( Funcs (X, INT )),X)) holds for e be Element of ( Funcs (( Funcs (X, INT )), INT )) holds (it . (s,( root-tree [((c * v) ** (c, NAT )), (e ** (c, NAT ))]))) = (s +* ((v . s),(e . s)));

      existence

      proof

        ( dom c) = X by Th6;

        then

        reconsider c9 = c as Function of X, NAT by A1, FUNCT_2: 2;

        reconsider i0 = 0 as Element of INT by INT_1:def 1;

        set Q = ( Funcs (X, INT ));

        set S = ECIW-signature , G = INT-ElemIns ;

        set A = ( FreeUnivAlgNSG (S,G));

        reconsider q0 = (X --> i0) as Element of Q by FUNCT_2: 8;



         A2: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;

        defpred P[ object, object] means ex s be Element of Q st ($1 `1 ) = s & (($2 = s & not ex v be Element of ( Funcs (Q,X)), e be Element of ( Funcs (Q, INT )) st ($1 `2 ) = ( root-tree [((c * v) ** (c9, NAT )), (e ** (c9, NAT ))])) or ex v be Element of ( Funcs (Q,X)), e be Element of ( Funcs (Q, INT )) st ($1 `2 ) = ( root-tree [((c * v) ** (c9, NAT )), (e ** (c9, NAT ))]) & $2 = (s +* ((v . s),(e . s))));



         A3: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;



         A4: for x be object st x in [:Q, ( ElementaryInstructions A):] holds ex y be object st y in Q & P[x, y]

        proof

          let x be object;

          assume x in [:Q, ( ElementaryInstructions A):];

          then

          consider s,I be object such that

           A5: s in Q and

           A6: I in ( ElementaryInstructions A) and

           A7: x = [s, I] by ZFMISC_1:def 2;



           A8: (x `1 ) = s by A7;

          reconsider s as Element of Q by A5;



           A9: (x `2 ) = I by A7;

          consider a be Symbol of ( DTConUA (S,G)) such that

           A10: I = ( root-tree a) and a in ( Terminals ( DTConUA (S,G))) by A3, A6;

          per cases ;

            suppose ex v be Element of ( Funcs (Q,X)), e be Element of ( Funcs (Q, INT )) st a = [((c * v) ** (c9, NAT )), (e ** (c9, NAT ))];

            then

            consider v be Element of ( Funcs (Q,X)), e be Element of ( Funcs (Q, INT )) such that

             A11: a = [((c * v) ** (c9, NAT )), (e ** (c9, NAT ))];

            take y = (s +* ((v . s),(e . s)));

            thus y in Q by FUNCT_2: 8;

            thus thesis by A8, A9, A10, A11;

          end;

            suppose

             A12: not ex v be Element of ( Funcs (Q,X)), e be Element of ( Funcs (Q, INT )) st a = [((c * v) ** (c9, NAT )), (e ** (c9, NAT ))];

            take y = s;

            thus y in Q;

             not ex v be Element of ( Funcs (Q,X)), e be Element of ( Funcs (Q, INT )) st (x `2 ) = ( root-tree [((c * v) ** (c9, NAT )), (e ** (c9, NAT ))]) by A9, A10, A12, TREES_4: 4;

            hence thesis by A8;

          end;

        end;

        consider g be Function such that

         A13: ( dom g) = [:Q, ( ElementaryInstructions A):] & ( rng g) c= Q and

         A14: for x be object st x in [:Q, ( ElementaryInstructions A):] holds P[x, (g . x)] from FUNCT_1:sch 6( A4);

        reconsider g as Function of [:Q, ( ElementaryInstructions A):], Q by A13, FUNCT_2: 2;

        consider f be ExecutionFunction of A, Q, T such that

         A15: (f | [:Q, ( ElementaryInstructions A):]) = g and for s be Element of Q holds for C,I be Element of A st not f iteration_terminates_for ((I \; C),(f . (s,C))) holds (f . (s,( while (C,I)))) = q0 by AOFA_000: 91;

        take f;

        let s be Element of ( Funcs (X, INT ));

        let v be Element of ( Funcs (( Funcs (X, INT )),X));

        let e be Element of ( Funcs (( Funcs (X, INT )), INT ));

        reconsider vv = v as Function of ( Funcs (X, INT )), X;

        reconsider cv = (c9 * vv) as Element of ( Funcs (( Funcs (X, INT )), NAT )) by FUNCT_2: 8;

        set v0 = (cv ** (c9, NAT )), e0 = (e ** (c9, NAT ));

        set I = ( root-tree [v0, e0]);

         [v0, e0] in G by ZFMISC_1: 87;

        then I in ( ElementaryInstructions A) by A3, A2;

        then

         A16: [s, I] in [:Q, ( ElementaryInstructions A):] by ZFMISC_1: 87;

        then P[ [s, I], (g . [s, I])] by A14;

        then

        consider v9 be Element of ( Funcs (Q,X)), e9 be Element of ( Funcs (Q, INT )) such that

         A17: ( [s, I] `2 ) = ( root-tree [((c * v9) ** (c9, NAT )), (e9 ** (c9, NAT ))]) and

         A18: (g . [s, I]) = (s +* ((v9 . s),(e9 . s)));



         A19: ( dom (c9 * v9)) = Q by FUNCT_2:def 1;



         A20: ( dom e) = Q by FUNCT_2:def 1;



         A21: ( dom v) = Q by FUNCT_2:def 1;



         A22: ( dom cv) = Q by FUNCT_2:def 1;



         A23: ( dom c9) = X by FUNCT_2:def 1;



         A24: ( rng v) c= X;



         A25: ( dom e9) = Q by FUNCT_2:def 1;



         A26: ( dom v9) = Q by FUNCT_2:def 1;



         A27: [v0, e0] = [((c * v9) ** (c9, NAT )), (e9 ** (c9, NAT ))] by A17, TREES_4: 4;

        then v0 = ((c * v9) ** (c9, NAT )) by XTUPLE_0: 1;

        then

         A28: cv = (c * v9) by A22, A19, Th5;

        e0 = (e9 ** (c9, NAT )) by A27, XTUPLE_0: 1;

        then

         A29: e = e9 by A20, A25, Th5;

        ( rng v9) c= X;

        then v = v9 by A24, A23, A26, A21, A28, FUNCT_1: 27;

        hence thesis by A15, A16, A18, A29, FUNCT_1: 49;

      end;

    end

    theorem :: AOFA_I00:16



     Th16: for f be INT-Exec holds for v be INT-Variable of NAT holds for t be INT-Expression of NAT holds (v,t) form_assignment_wrt f

    proof

      let f be INT-Exec;

      set S = ECIW-signature , G = INT-ElemIns ;

      set X = NAT ;

      set A = ( FreeUnivAlgNSG (S,G));

      let v be INT-Variable of NAT ;

      let t be INT-Expression of NAT ;

      reconsider v9 = v as Element of ( Funcs (( Funcs (X, INT )),X)) by FUNCT_2: 8;

      reconsider t9 = t as Element of ( Funcs (( Funcs (X, INT )), INT )) by FUNCT_2: 8;



       A1: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;



       A2: [v9, t9] in G by ZFMISC_1: 87;



       A3: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;

      then ( root-tree [v9, t9]) in ( ElementaryInstructions A) by A1, A2;

      then

      reconsider I = ( root-tree [v9, t9]) as Element of A;

      take I;

      thus I in ( ElementaryInstructions A) by A3, A1, A2;

      thus thesis by Def25;

    end;

    theorem :: AOFA_I00:17



     Th17: for f be INT-Exec holds for v be INT-Variable of NAT holds v is INT-Variable of ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns )), f

    proof

      set t = the INT-Expression of NAT ;

      let f be INT-Exec;

      set S = ECIW-signature , G = INT-ElemIns ;

      set X = NAT ;

      set A = ( FreeUnivAlgNSG (S,G));

      let v be INT-Variable of NAT ;



       A1: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;

      reconsider t9 = t as Element of ( Funcs (( Funcs (X, INT )), INT )) by FUNCT_2: 8;

      reconsider v9 = v as Element of ( Funcs (( Funcs (X, INT )),X)) by FUNCT_2: 8;



       A2: [v9, t9] in G by ZFMISC_1: 87;



       A3: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;

      then ( root-tree [v9, t9]) in ( ElementaryInstructions A) by A1, A2;

      then

      reconsider I = ( root-tree [v9, t9]) as Element of A;

      hereby

        take I;

        thus I is_assignment_wrt (A,X,f)

        proof

          thus I in ( ElementaryInstructions A) by A3, A1, A2;

          take v, t;

          thus thesis by Def25;

        end;

      end;

      take t;

      thus thesis by Th16;

    end;

    theorem :: AOFA_I00:18



     Th18: for f be INT-Exec holds for t be INT-Expression of NAT holds t is INT-Expression of ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns )), f

    proof

      set v = the INT-Variable of NAT ;

      let f be INT-Exec;

      set S = ECIW-signature , G = INT-ElemIns ;

      set X = NAT ;

      set A = ( FreeUnivAlgNSG (S,G));

      let t be INT-Expression of NAT ;



       A1: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;

      reconsider t9 = t as Element of ( Funcs (( Funcs (X, INT )), INT )) by FUNCT_2: 8;

      reconsider v9 = v as Element of ( Funcs (( Funcs (X, INT )),X)) by FUNCT_2: 8;



       A2: [v9, t9] in G by ZFMISC_1: 87;



       A3: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;

      then ( root-tree [v9, t9]) in ( ElementaryInstructions A) by A1, A2;

      then

      reconsider I = ( root-tree [v9, t9]) as Element of A;

      hereby

        take I;

        thus I is_assignment_wrt (A,X,f)

        proof

          thus I in ( ElementaryInstructions A) by A3, A1, A2;

          take v, t;

          thus thesis by Def25;

        end;

      end;

      take v;

      thus thesis by Th16;

    end;

    registration

      cluster -> Euclidean for INT-Exec;

      coherence

      proof

        set X = NAT ;

        set a = (( INT --> 0 ) +* ( id X));



         A1: ( dom ( id X)) = X by RELAT_1: 45;



         A2: ( INT \/ X) = INT by NUMBERS: 17, XBOOLE_1: 12;

        ( dom ( INT --> 0 )) = INT ;

        then

         A3: ( dom a) = INT by A1, A2, FUNCT_4:def 1;



         A4: ( rng ( id X)) = X by RELAT_1: 45;

         { 0 } c= X by ZFMISC_1: 31;

        then

         A5: ( { 0 } \/ X) = X by XBOOLE_1: 12;

        ( rng ( INT --> 0 )) = { 0 } by FUNCOP_1: 8;

        then ( rng a) c= NAT by A4, A5, FUNCT_4: 17;

        then

        reconsider a as INT-Array of X by A3, FUNCT_2: 2;

        let f be INT-Exec;

        set S = ECIW-signature , G = INT-ElemIns ;

        set A = ( FreeUnivAlgNSG (S,G));

        thus for v be INT-Variable of A, f, t be INT-Expression of A, f holds (v,t) form_assignment_wrt f by Th16;

        thus for i be Integer holds ( . (i,X)) is INT-Expression of A, f by Th18;

        thus for v be INT-Variable of A, f holds ( . v) is INT-Expression of A, f by Th18;

        thus for x be Element of X holds ( ^ x) is INT-Variable of A, f by Th17;

        hereby

          take a;

          ( dom ( id X)) = X by RELAT_1: 45;

          hence (a | ( card X)) is one-to-one by FUNCT_4: 23;

          thus for t be INT-Expression of A, f holds (a * t) is INT-Variable of A, f by Th17;

        end;

        thus thesis by Th18;

      end;

    end

    theorem :: AOFA_I00:19



     Th19: for X be non empty countable set holds for T be Subset of ( Funcs (X, INT )) holds for c be Enumeration of X holds for f be INT-Exec of c, T holds for v be INT-Variable of X holds for t be INT-Expression of X holds (v,t) form_assignment_wrt f

    proof

      set S = ECIW-signature , G = INT-ElemIns ;

      let X be non empty countable set;

      let T be Subset of ( Funcs (X, INT ));

      let c be Enumeration of X;

      set A = ( FreeUnivAlgNSG (S,G));

      let f be INT-Exec of c, T;

      let v be INT-Variable of X;

      let t be INT-Expression of X;

      reconsider v9 = v as Element of ( Funcs (( Funcs (X, INT )),X)) by FUNCT_2: 8;

      reconsider t9 = t as Element of ( Funcs (( Funcs (X, INT )), INT )) by FUNCT_2: 8;



       A1: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;



       A2: ( rng c) c= NAT by Th11;

      ( dom c) = X by Th6;

      then

      reconsider c9 = c as Function of X, NAT by A2, FUNCT_2: 2;

      reconsider cv = (c9 * v) as Element of ( Funcs (( Funcs (X, INT )), NAT )) by FUNCT_2: 8;

      set v1 = (cv ** (c9, NAT )), t1 = (t9 ** (c9, NAT ));



       A3: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;



       A4: [v1, t1] in G by ZFMISC_1: 87;

      then ( root-tree [v1, t1]) in ( ElementaryInstructions A) by A1, A3;

      then

      reconsider I = ( root-tree [v1, t1]) as Element of A;

      take I;

      for s be Element of ( Funcs (X, INT )) holds (f . (s,( root-tree [((c * v9) ** (c, NAT )), (t9 ** (c, NAT ))]))) = (s +* ((v9 . s),(t9 . s))) by A2, Def28;

      hence thesis by A1, A3, A4;

    end;

    theorem :: AOFA_I00:20



     Th20: for X be non empty countable set holds for T be Subset of ( Funcs (X, INT )) holds for c be Enumeration of X holds for f be INT-Exec of c, T holds for v be INT-Variable of X holds v is INT-Variable of ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns )), f

    proof

      set S = ECIW-signature , G = INT-ElemIns ;

      let X be non empty countable set;

      let T be Subset of ( Funcs (X, INT ));

      let c be Enumeration of X;

      set A = ( FreeUnivAlgNSG (S,G));

      let f be INT-Exec of c, T;

      let v be INT-Variable of X;

      set t = the INT-Expression of X;



       A1: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;



       A2: ( rng c) c= NAT by Th11;

      ( dom c) = X by Th6;

      then

      reconsider c9 = c as Function of X, NAT by A2, FUNCT_2: 2;

      reconsider cv = (c9 * v) as Element of ( Funcs (( Funcs (X, INT )), NAT )) by FUNCT_2: 8;

      reconsider v9 = v as Element of ( Funcs (( Funcs (X, INT )),X)) by FUNCT_2: 8;

      reconsider t9 = t as Element of ( Funcs (( Funcs (X, INT )), INT )) by FUNCT_2: 8;



       A3: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;

      set v1 = (cv ** (c9, NAT )), t1 = (t9 ** (c9, NAT ));



       A4: [v1, t1] in G by ZFMISC_1: 87;

      then ( root-tree [v1, t1]) in ( ElementaryInstructions A) by A1, A3;

      then

      reconsider I = ( root-tree [v1, t1]) as Element of A;

      hereby

        take I;

        thus I is_assignment_wrt (A,X,f)

        proof

          thus I in ( ElementaryInstructions A) by A1, A3, A4;

          take v, t;

          for s be Element of ( Funcs (X, INT )) holds (f . (s,( root-tree [((c * v9) ** (c, NAT )), (t9 ** (c, NAT ))]))) = (s +* ((v9 . s),(t9 . s))) by A2, Def28;

          hence thesis;

        end;

      end;

      take t;

      thus thesis by Th19;

    end;

    theorem :: AOFA_I00:21



     Th21: for X be non empty countable set holds for T be Subset of ( Funcs (X, INT )) holds for c be Enumeration of X holds for f be INT-Exec of c, T holds for t be INT-Expression of X holds t is INT-Expression of ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns )), f

    proof

      set S = ECIW-signature , G = INT-ElemIns ;

      let X be non empty countable set;

      let T be Subset of ( Funcs (X, INT ));

      let c be Enumeration of X;

      set A = ( FreeUnivAlgNSG (S,G));

      let f be INT-Exec of c, T;

      set v = the INT-Variable of X;

      let t be INT-Expression of X;



       A1: ( ElementaryInstructions A) = ( FreeGenSetNSG (S,G)) by AOFA_000: 70;



       A2: ( rng c) c= NAT by Th11;

      ( dom c) = X by Th6;

      then

      reconsider c9 = c as Function of X, NAT by A2, FUNCT_2: 2;

      reconsider cv = (c9 * v) as Element of ( Funcs (( Funcs (X, INT )), NAT )) by FUNCT_2: 8;

      reconsider v9 = v as Element of ( Funcs (( Funcs (X, INT )),X)) by FUNCT_2: 8;

      reconsider t9 = t as Element of ( Funcs (( Funcs (X, INT )), INT )) by FUNCT_2: 8;



       A3: ( Terminals ( DTConUA (S,G))) = G by FREEALG: 3;

      set v1 = (cv ** (c9, NAT )), t1 = (t9 ** (c9, NAT ));



       A4: [v1, t1] in G by ZFMISC_1: 87;

      then ( root-tree [v1, t1]) in ( ElementaryInstructions A) by A1, A3;

      then

      reconsider I = ( root-tree [v1, t1]) as Element of A;

      hereby

        take I;

        thus I is_assignment_wrt (A,X,f)

        proof

          thus I in ( ElementaryInstructions A) by A1, A3, A4;

          take v, t;

          for s be Element of ( Funcs (X, INT )) holds (f . (s,( root-tree [((c * v9) ** (c, NAT )), (t9 ** (c, NAT ))]))) = (s +* ((v9 . s),(t9 . s))) by A2, Def28;

          hence thesis;

        end;

      end;

      take v;

      thus thesis by Th19;

    end;

    registration

      let X be countable non empty set;

      let T be Subset of ( Funcs (X, INT ));

      let c be Enumeration of X;

      cluster -> Euclidean for INT-Exec of c, T;

      coherence

      proof



         A1: ( rng c) c= NAT by Th11;

        ( card X) = ( rng c) by Th6;

        then

         A2: ( INT \/ ( card X)) = INT by A1, NUMBERS: 17, XBOOLE_1: 1, XBOOLE_1: 12;

        set x = ((c " ) . 0 );

        set a = (( INT --> x) +* (c " ));



         A3: ( dom ( INT --> x)) = INT ;



         A4: ( rng ( INT --> x)) = {x} by FUNCOP_1: 8;

        x in X by FUNCT_2: 5, ORDINAL3: 8;

        then {x} c= X by ZFMISC_1: 31;

        then

         A5: ( {x} \/ X) = X by XBOOLE_1: 12;

        ( rng (c " )) = X by Th7;

        then

         A6: ( rng a) c= X by A4, A5, FUNCT_4: 17;

        ( dom (c " )) = ( card X) by Th7;

        then ( dom a) = INT by A3, A2, FUNCT_4:def 1;

        then

        reconsider a as INT-Array of X by A6, FUNCT_2: 2;

        let f be INT-Exec of c, T;

        set S = ECIW-signature , G = INT-ElemIns ;

        set A = ( FreeUnivAlgNSG (S,G));

        thus for v be INT-Variable of A, f, t be INT-Expression of A, f holds (v,t) form_assignment_wrt f by Th19;

        thus for i be Integer holds ( . (i,X)) is INT-Expression of A, f by Th21;

        thus for v be INT-Variable of A, f holds ( . v) is INT-Expression of A, f by Th21;

        thus for x be Element of X holds ( ^ x) is INT-Variable of A, f by Th20;

        hereby

          take a;

          ( dom (c " )) = ( card X) by Th7;

          hence (a | ( card X)) is one-to-one by FUNCT_4: 23;

          thus for t be INT-Expression of A, f holds (a * t) is INT-Variable of A, f by Th20;

        end;

        thus thesis by Th21;

      end;

    end

    registration

      cluster ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns )) -> Euclidean;

      coherence

      proof

        let X be non empty countable set, T be Subset of ( Funcs (X, INT ));

        set c = the Enumeration of X;

        set f = the INT-Exec of c, T;

        take f;

        thus thesis;

      end;

    end

    registration

      cluster Euclidean non degenerated for preIfWhileAlgebra;

      existence

      proof

        take ( FreeUnivAlgNSG ( ECIW-signature , INT-ElemIns ));

        thus thesis;

      end;

    end

    registration

      let A be Euclidean preIfWhileAlgebra;

      let X be non empty countable set;

      let T be Subset of ( Funcs (X, INT ));

      cluster Euclidean for ExecutionFunction of A, ( Funcs (X, INT )), T;

      existence by Def23;

    end

    reserve A for Euclidean preIfWhileAlgebra;

    reserve X for non empty countable set;

    reserve T for Subset of ( Funcs (X, INT ));

    reserve f for Euclidean ExecutionFunction of A, ( Funcs (X, INT )), T;

    definition

      let A, X, T, f;

      let t be INT-Expression of A, f;

      :: original: -

      redefine

      func - t -> INT-Expression of A, f ;

      coherence by Def22;

    end

    definition

      let A, X, T, f;

      let t be INT-Expression of A, f;

      let i be Integer;

      :: original: +

      redefine

      func t + i -> INT-Expression of A, f ;

      coherence

      proof



         A1: ( dom (t + ( . (i,X)))) = ( Funcs (X, INT )) by FUNCT_2:def 1;

         A2:

        now

          let a be object;

          assume a in ( Funcs (X, INT ));

          then

          reconsider s = a as Element of ( Funcs (X, INT ));



          thus ((t + ( . (i,X))) . a) = ((t . s) + (( . (i,X)) . s)) by A1, VALUED_1:def 1

          .= (i + (t . a));

        end;

        ( . (i,X)) is INT-Expression of A, f by Def22;

        then

         A3: (t + ( . (i,X))) is INT-Expression of A, f by Def22;

        ( dom t) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        hence thesis by A3, A1, A2, VALUED_1:def 2;

      end;

      :: original: -

      redefine

      func t - i -> INT-Expression of A, f ;

      coherence

      proof

        ( . (i,X)) is INT-Expression of A, f by Def22;

        then ( - ( . (i,X))) is INT-Expression of A, f by Def22;

        then

         A4: (t + ( - ( . (i,X)))) is INT-Expression of A, f by Def22;



         A5: ( dom t) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A6: ( dom (t + ( - ( . (i,X))))) = ( Funcs (X, INT )) by FUNCT_2:def 1;

         A7:

        now

          let a be object;

          assume a in ( Funcs (X, INT ));

          then

          reconsider s = a as Element of ( Funcs (X, INT ));



          thus ((t + ( - ( . (i,X)))) . a) = ((t . s) + (( - ( . (i,X))) . s)) by A6, VALUED_1:def 1

          .= ((t . s) + ( - (( . (i,X)) . s))) by VALUED_1: 8

          .= ((t . s) - i)

          .= ((t - i) . a) by A5, VALUED_1: 3;

        end;

        ( dom (t - i)) = ( dom t) by VALUED_1: 3;

        hence thesis by A4, A6, A5, A7, FUNCT_1: 2;

      end;

      :: original: *

      redefine

      func t * i -> INT-Expression of A, f ;

      coherence

      proof



         A8: ( dom (t (#) ( . (i,X)))) = ( Funcs (X, INT )) by FUNCT_2:def 1;

         A9:

        now

          let a be object;

          assume a in ( Funcs (X, INT ));

          then

          reconsider s = a as Element of ( Funcs (X, INT ));



          thus ((t (#) ( . (i,X))) . a) = ((t . s) * (( . (i,X)) . s)) by A8, VALUED_1:def 4

          .= (i * (t . a));

        end;

        ( . (i,X)) is INT-Expression of A, f by Def22;

        then

         A10: (t (#) ( . (i,X))) is INT-Expression of A, f by Def22;

        ( dom t) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        hence thesis by A10, A8, A9, VALUED_1:def 5;

      end;

    end

    definition

      let A, X, T, f;

      let t1,t2 be INT-Expression of A, f;

      :: original: -

      redefine

      func t1 - t2 -> INT-Expression of A, f ;

      coherence

      proof

        ( - t2) is INT-Expression of A, f;

        hence thesis by Def22;

      end;

      :: original: +

      redefine

      func t1 + t2 -> INT-Expression of A, f ;

      coherence by Def22;

      :: original: (#)

      redefine

      func t1 (#) t2 -> INT-Expression of A, f ;

      coherence by Def22;

    end

    definition

      let A, X, T, f;

      let t1,t2 be INT-Expression of A, f;

      :: original: div

      redefine

      :: AOFA_I00:def29

      func t1 div t2 -> INT-Expression of A, f means

      : Def29: for s be Element of ( Funcs (X, INT )) holds (it . s) = ((t1 . s) div (t2 . s));

      coherence by Def22;

      compatibility

      proof

        let ti be INT-Expression of A, f;



         A1: ( dom t1) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A2: ( dom t2) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A3: ( dom (t1 div t2)) = (( dom t1) /\ ( dom t2)) by Def3;

        hence ti = (t1 div t2) implies for s be Element of ( Funcs (X, INT )) holds (ti . s) = ((t1 . s) div (t2 . s)) by A1, A2, Def3;



         A4: ( dom ti) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        assume for s be Element of ( Funcs (X, INT )) holds (ti . s) = ((t1 . s) div (t2 . s));

        then for s be object st s in ( Funcs (X, INT )) holds (ti . s) = ((t1 . s) div (t2 . s));

        hence ti = (t1 div t2) by A3, A1, A2, A4, Def3;

      end;

      :: original: mod

      redefine

      :: AOFA_I00:def30

      func t1 mod t2 -> INT-Expression of A, f means

      : Def30: for s be Element of ( Funcs (X, INT )) holds (it . s) = ((t1 . s) mod (t2 . s));

      coherence by Def22;

      compatibility

      proof

        let ti be INT-Expression of A, f;



         A5: ( dom t1) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A6: ( dom t2) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A7: ( dom (t1 mod t2)) = (( dom t1) /\ ( dom t2)) by Def4;

        hence ti = (t1 mod t2) implies for s be Element of ( Funcs (X, INT )) holds (ti . s) = ((t1 . s) mod (t2 . s)) by A5, A6, Def4;



         A8: ( dom ti) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        assume for s be Element of ( Funcs (X, INT )) holds (ti . s) = ((t1 . s) mod (t2 . s));

        then for s be object st s in ( Funcs (X, INT )) holds (ti . s) = ((t1 . s) mod (t2 . s));

        hence ti = (t1 mod t2) by A7, A5, A6, A8, Def4;

      end;

      :: original: leq

      redefine

      :: AOFA_I00:def31

      func leq (t1,t2) -> INT-Expression of A, f means

      : Def31: for s be Element of ( Funcs (X, INT )) holds (it . s) = ( IFGT ((t1 . s),(t2 . s), 0 ,1));

      compatibility

      proof

        let ti be INT-Expression of A, f;



         A9: ( dom t1) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A10: ( dom t2) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A11: ( dom ( leq (t1,t2))) = (( dom t1) /\ ( dom t2)) by Def5;

        hence ti = ( leq (t1,t2)) implies for s be Element of ( Funcs (X, INT )) holds (ti . s) = ( IFGT ((t1 . s),(t2 . s), 0 ,1)) by A9, A10, Def5;



         A12: ( dom ti) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        assume for s be Element of ( Funcs (X, INT )) holds (ti . s) = ( IFGT ((t1 . s),(t2 . s), 0 ,1));

        then for s be object st s in ( Funcs (X, INT )) holds (ti . s) = ( IFGT ((t1 . s),(t2 . s), 0 ,1));

        hence ti = ( leq (t1,t2)) by A11, A9, A10, A12, Def5;

      end;

      coherence by Def22;

      :: original: gt

      redefine

      :: AOFA_I00:def32

      func gt (t1,t2) -> INT-Expression of A, f means

      : Def32: for s be Element of ( Funcs (X, INT )) holds (it . s) = ( IFGT ((t1 . s),(t2 . s),1, 0 ));

      coherence by Def22;

      compatibility

      proof

        let ti be INT-Expression of A, f;



         A13: ( dom t1) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A14: ( dom t2) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A15: ( dom ( gt (t1,t2))) = (( dom t1) /\ ( dom t2)) by Def6;

        hence ti = ( gt (t1,t2)) implies for s be Element of ( Funcs (X, INT )) holds (ti . s) = ( IFGT ((t1 . s),(t2 . s),1, 0 )) by A13, A14, Def6;



         A16: ( dom ti) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        assume for s be Element of ( Funcs (X, INT )) holds (ti . s) = ( IFGT ((t1 . s),(t2 . s),1, 0 ));

        then for s be object st s in ( Funcs (X, INT )) holds (ti . s) = ( IFGT ((t1 . s),(t2 . s),1, 0 ));

        hence ti = ( gt (t1,t2)) by A15, A13, A14, A16, Def6;

      end;

    end

    definition

      let A, X, T, f;

      let t1,t2 be INT-Expression of A, f;

      :: original: eq

      redefine

      :: AOFA_I00:def33

      func eq (t1,t2) -> INT-Expression of A, f means for s be Element of ( Funcs (X, INT )) holds (it . s) = ( IFEQ ((t1 . s),(t2 . s),1, 0 ));

      compatibility

      proof

        let ti be INT-Expression of A, f;



         A1: ( dom t1) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A2: ( dom t2) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A3: ( dom ( eq (t1,t2))) = (( dom t1) /\ ( dom t2)) by Def7;

        hence ti = ( eq (t1,t2)) implies for s be Element of ( Funcs (X, INT )) holds (ti . s) = ( IFEQ ((t1 . s),(t2 . s),1, 0 )) by A1, A2, Def7;



         A4: ( dom ti) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        assume for s be Element of ( Funcs (X, INT )) holds (ti . s) = ( IFEQ ((t1 . s),(t2 . s),1, 0 ));

        then for s be object st s in ( Funcs (X, INT )) holds (ti . s) = ( IFEQ ((t1 . s),(t2 . s),1, 0 ));

        hence ti = ( eq (t1,t2)) by A3, A1, A2, A4, Def7;

      end;

      coherence

      proof

        reconsider l1 = ( leq (t1,t2)), l2 = ( leq (t2,t1)) as INT-Expression of A, f;



         A5: ( dom (l1 (#) l2)) = ( Funcs (X, INT )) by FUNCT_2:def 1;



         A6: ( dom ( eq (t1,t2))) = ( Funcs (X, INT )) by FUNCT_2:def 1;

        now

          let a be object;

          assume a in ( Funcs (X, INT ));

          then

          reconsider s = a as Element of ( Funcs (X, INT ));



           A7: (t1 . s) = (t2 . s) or (t1 . s) < (t2 . s) or (t2 . s) < (t1 . s) by XXREAL_0: 1;



           A8: (l2 . s) = ( IFGT ((t2 . s),(t1 . s), 0 ,1)) by Def31;



           A9: ((l1 (#) l2) . s) = ((l1 . s) * (l2 . s)) by A5, VALUED_1:def 4;



           A10: (l1 . s) = ( IFGT ((t1 . s),(t2 . s), 0 ,1)) by Def31;

          (( eq (t1,t2)) . s) = ( IFEQ ((t1 . s),(t2 . s),1, 0 )) by A6, Def7;

          then (( eq (t1,t2)) . s) = 1 & (l1 . s) = 1 & (l2 . s) = 1 or (( eq (t1,t2)) . s) = 0 & (l1 . s) = 0 & (l2 . s) = 1 or (( eq (t1,t2)) . s) = 0 & (l1 . s) = 1 & (l2 . s) = 0 by A8, A10, A7, FUNCOP_1:def 8, XXREAL_0:def 11;

          hence (( eq (t1,t2)) . a) = ((l1 (#) l2) . a) by A9;

        end;

        hence thesis by A6, A5, FUNCT_1: 2;

      end;

    end

    definition

      let A, X, T, f;

      let v be INT-Variable of A, f;

      :: AOFA_I00:def34

      func . v -> INT-Expression of A, f equals ( . v);

      coherence by Def22;

    end

    definition

      let A, X, T, f;

      let x be Element of X;

      :: AOFA_I00:def35

      func x ^ (A,f) -> INT-Variable of A, f equals ( ^ x);

      coherence by Def22;

    end

    notation

      let A, X, T, f;

      let x be Variable of f;

      synonym ^ x for x ^ (A,f);

    end

    definition

      let A, X, T, f;

      let x be Variable of f;

      :: AOFA_I00:def36

      func . x -> INT-Expression of A, f equals ( . ( ^ x));

      coherence ;

    end

    theorem :: AOFA_I00:22



     Th22: for x be Variable of f holds for s be Element of ( Funcs (X, INT )) holds (( . x) . s) = (s . x)

    proof

      let x be Variable of f;

      let s be Element of ( Funcs (X, INT ));



      thus (( . x) . s) = (s . ((x ^ (A,f)) . s)) by Def19

      .= (s . x);

    end;

    definition

      let A, X, T, f;

      let i be Integer;

      :: AOFA_I00:def37

      func . (i,A,f) -> INT-Expression of A, f equals ( . (i,X));

      coherence by Def22;

    end

    definition

      let A, X, T, f;

      let v be INT-Variable of A, f;

      let t be INT-Expression of A, f;

      :: AOFA_I00:def38

      func v := t -> Element of A equals the Element of { I where I be Element of A : I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s))) };

      coherence

      proof

        set Y = { I where I be Element of A : I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s))) };



         A1: Y c= the carrier of A

        proof

          let i be object;

          assume i in Y;

          then ex I be Element of A st i = I & I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s)));

          hence thesis;

        end;

        (v,t) form_assignment_wrt f by Def22;

        then

        consider I0 be Element of A such that

         A2: I0 in ( ElementaryInstructions A) and

         A3: for s be Element of ( Funcs (X, INT )) holds (f . (s,I0)) = (s +* ((v . s),(t . s)));

        I0 in Y by A2, A3;

        then the Element of Y in Y;

        hence thesis by A1;

      end;

    end

    theorem :: AOFA_I00:23



     Th23: for v be INT-Variable of A, f holds for t be INT-Expression of A, f holds (v := t) in ( ElementaryInstructions A)

    proof

      let v be INT-Variable of A, f;

      let t be INT-Expression of A, f;

      set Y = { I where I be Element of A : I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s))) };

      (v,t) form_assignment_wrt f by Def22;

      then

      consider I0 be Element of A such that

       A1: I0 in ( ElementaryInstructions A) and

       A2: for s be Element of ( Funcs (X, INT )) holds (f . (s,I0)) = (s +* ((v . s),(t . s)));

      I0 in Y by A1, A2;

      then (v := t) in Y;

      then ex I be Element of A st (v := t) = I & I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s)));

      hence thesis;

    end;

    registration

      let A, X, T, f;

      let v be INT-Variable of A, f;

      let t be INT-Expression of A, f;

      cluster (v := t) -> absolutely-terminating;

      coherence by Th23, AOFA_000: 95;

    end

    definition

      let A, X, T, f;

      let v be INT-Variable of A, f;

      let t be INT-Expression of A, f;

      :: AOFA_I00:def39

      func v += t -> absolutely-terminating Element of A equals (v := (( . v) + t));

      coherence ;

      :: AOFA_I00:def40

      func v *= t -> absolutely-terminating Element of A equals (v := (( . v) (#) t));

      coherence ;

    end

    definition

      let A, X, T, f;

      let x be Element of X;

      let t be INT-Expression of A, f;

      :: AOFA_I00:def41

      func x := t -> absolutely-terminating Element of A equals ((x ^ (A,f)) := t);

      correctness ;

    end

    definition

      let A, X, T, f;

      let x be Element of X;

      let y be Variable of f;

      :: AOFA_I00:def42

      func x := y -> absolutely-terminating Element of A equals (x := ( . y));

      correctness ;

    end

    definition

      let A, X, T, f;

      let x be Element of X;

      let v be INT-Variable of A, f;

      :: AOFA_I00:def43

      func x := v -> absolutely-terminating Element of A equals (x := ( . v));

      correctness ;

    end

    definition

      let A, X, T, f;

      let v,w be INT-Variable of A, f;

      :: AOFA_I00:def44

      func v := w -> absolutely-terminating Element of A equals (v := ( . w));

      correctness ;

    end

    definition

      let A, X, T, f;

      let x be Variable of f;

      let i be Integer;

      :: AOFA_I00:def45

      func x := i -> absolutely-terminating Element of A equals (x := ( . (i,A,f)));

      correctness ;

    end

    definition

      let A, X, T, f;

      let v1,v2 be INT-Variable of A, f;

      let x be Variable of f;

      :: AOFA_I00:def46

      func swap (v1,x,v2) -> absolutely-terminating Element of A equals (((x := v1) \; (v1 := v2)) \; (v2 := ( . x)));

      coherence ;

    end

    definition

      let A, X, T, f;

      let x be Variable of f;

      let t be INT-Expression of A, f;

      :: AOFA_I00:def47

      func x += t -> absolutely-terminating Element of A equals (x := (( . x) + t));

      correctness ;

      :: AOFA_I00:def48

      func x *= t -> absolutely-terminating Element of A equals (x := (( . x) (#) t));

      correctness ;

      :: AOFA_I00:def49

      func x %= t -> absolutely-terminating Element of A equals (x := (( . x) mod t));

      correctness ;

      :: AOFA_I00:def50

      func x /= t -> absolutely-terminating Element of A equals (x := (( . x) div t));

      correctness ;

    end

    definition

      let A, X, T, f;

      let x be Variable of f;

      let i be Integer;

      :: AOFA_I00:def51

      func x += i -> absolutely-terminating Element of A equals (x := (( . x) + i));

      correctness ;

      :: AOFA_I00:def52

      func x *= i -> absolutely-terminating Element of A equals (x := (( . x) * i));

      correctness ;

      :: AOFA_I00:def53

      func x %= i -> absolutely-terminating Element of A equals (x := (( . x) mod ( . (i,A,f))));

      correctness ;

      :: AOFA_I00:def54

      func x /= i -> absolutely-terminating Element of A equals (x := (( . x) div ( . (i,A,f))));

      correctness ;

      :: AOFA_I00:def55

      func x div i -> INT-Expression of A, f equals (( . x) div ( . (i,A,f)));

      correctness ;

    end

    definition

      let A, X, T, f;

      let v be INT-Variable of A, f;

      let i be Integer;

      :: AOFA_I00:def56

      func v := i -> absolutely-terminating Element of A equals (v := ( . (i,A,f)));

      correctness ;

    end

    definition

      let A, X, T, f;

      let v be INT-Variable of A, f;

      let i be Integer;

      :: AOFA_I00:def57

      func v += i -> absolutely-terminating Element of A equals (v := (( . v) + i));

      correctness ;

      :: AOFA_I00:def58

      func v *= i -> absolutely-terminating Element of A equals (v := (( . v) * i));

      correctness ;

    end

    definition

      let A, X;

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let t1 be INT-Expression of A, g;

      :: AOFA_I00:def59

      func t1 is_odd -> absolutely-terminating Element of A equals (b := (t1 mod ( . (2,A,g))));

      coherence ;

      :: AOFA_I00:def60

      func t1 is_even -> absolutely-terminating Element of A equals (b := ((t1 + 1) mod ( . (2,A,g))));

      coherence ;

      let t2 be INT-Expression of A, g;

      :: AOFA_I00:def61

      func t1 leq t2 -> absolutely-terminating Element of A equals (b := ( leq (t1,t2)));

      coherence ;

      :: AOFA_I00:def62

      func t1 gt t2 -> absolutely-terminating Element of A equals (b := ( gt (t1,t2)));

      coherence ;

      :: AOFA_I00:def63

      func t1 eq t2 -> absolutely-terminating Element of A equals (b := ( eq (t1,t2)));

      coherence ;

    end

    notation

      let A, X;

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let t1,t2 be INT-Expression of A, g;

      synonym t2 geq t1 for t1 leq t2;

      synonym t2 lt t1 for t1 gt t2;

    end

    definition

      let A, X;

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let v1,v2 be INT-Variable of A, g;

      :: AOFA_I00:def64

      func v1 leq v2 -> absolutely-terminating Element of A equals (( . v1) leq ( . v2));

      coherence ;

      :: AOFA_I00:def65

      func v1 gt v2 -> absolutely-terminating Element of A equals (( . v1) gt ( . v2));

      coherence ;

    end

    notation

      let A, X;

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let v1,v2 be INT-Variable of A, g;

      synonym v2 geq v1 for v1 leq v2;

      synonym v2 lt v1 for v1 gt v2;

    end

    definition

      let A, X;

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x1 be Variable of g;

      :: AOFA_I00:def66

      func x1 is_odd -> absolutely-terminating Element of A equals (( . x1) is_odd );

      coherence ;

      :: AOFA_I00:def67

      func x1 is_even -> absolutely-terminating Element of A equals (( . x1) is_even );

      coherence ;

      let x2 be Variable of g;

      :: AOFA_I00:def68

      func x1 leq x2 -> absolutely-terminating Element of A equals (( . x1) leq ( . x2));

      coherence ;

      :: AOFA_I00:def69

      func x1 gt x2 -> absolutely-terminating Element of A equals (( . x1) gt ( . x2));

      coherence ;

    end

    notation

      let A, X;

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x1,x2 be Variable of g;

      synonym x2 geq x1 for x1 leq x2;

      synonym x2 lt x1 for x1 gt x2;

    end

    definition

      let A, X;

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x be Variable of g;

      let i be Integer;

      :: AOFA_I00:def70

      func x leq i -> absolutely-terminating Element of A equals (( . x) leq ( . (i,A,g)));

      coherence ;

      :: AOFA_I00:def71

      func x geq i -> absolutely-terminating Element of A equals (( . x) geq ( . (i,A,g)));

      coherence ;

      :: AOFA_I00:def72

      func x gt i -> absolutely-terminating Element of A equals (( . x) gt ( . (i,A,g)));

      coherence ;

      :: AOFA_I00:def73

      func x lt i -> absolutely-terminating Element of A equals (( . x) lt ( . (i,A,g)));

      coherence ;

      :: AOFA_I00:def74

      func x / i -> INT-Expression of A, g equals (( . x) div ( . (i,A,g)));

      coherence ;

    end

    definition

      let A, X, T, f;

      let x1,x2 be Variable of f;

      :: AOFA_I00:def75

      func x1 += x2 -> absolutely-terminating Element of A equals (x1 += ( . x2));

      coherence ;

      :: AOFA_I00:def76

      func x1 *= x2 -> absolutely-terminating Element of A equals (x1 *= ( . x2));

      coherence ;

      :: AOFA_I00:def77

      func x1 %= x2 -> absolutely-terminating Element of A equals (x1 := (( . x1) mod ( . x2)));

      coherence ;

      :: AOFA_I00:def78

      func x1 /= x2 -> absolutely-terminating Element of A equals (x1 := (( . x1) div ( . x2)));

      coherence ;

      :: AOFA_I00:def79

      func x1 + x2 -> INT-Expression of A, f equals (( . x1) + ( . x2));

      coherence ;

      :: AOFA_I00:def80

      func x1 * x2 -> INT-Expression of A, f equals (( . x1) (#) ( . x2));

      coherence ;

      :: AOFA_I00:def81

      func x1 mod x2 -> INT-Expression of A, f equals (( . x1) mod ( . x2));

      coherence ;

      :: AOFA_I00:def82

      func x1 div x2 -> INT-Expression of A, f equals (( . x1) div ( . x2));

      coherence ;

    end

    reserve A for Euclidean preIfWhileAlgebra,

X for non empty countable set,

z for Element of X,

s,s9 for Element of ( Funcs (X, INT )),

T for Subset of ( Funcs (X, INT )),

f for Euclidean ExecutionFunction of A, ( Funcs (X, INT )), T,

v for INT-Variable of A, f,

t for INT-Expression of A, f;

    reserve i for Integer;

    theorem :: AOFA_I00:24



     Th24: ((f . (s,(v := t))) . (v . s)) = (t . s) & for z st z <> (v . s) holds ((f . (s,(v := t))) . z) = (s . z)

    proof

      set Y = { I where I be Element of A : I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s))) };

      (v,t) form_assignment_wrt f by Def22;

      then

      consider I0 be Element of A such that

       A1: I0 in ( ElementaryInstructions A) and

       A2: for s be Element of ( Funcs (X, INT )) holds (f . (s,I0)) = (s +* ((v . s),(t . s)));

      I0 in Y by A1, A2;

      then (v := t) in Y;

      then ex I be Element of A st (v := t) = I & I in ( ElementaryInstructions A) & for s be Element of ( Funcs (X, INT )) holds (f . (s,I)) = (s +* ((v . s),(t . s)));

      then

       A3: (f . (s,(v := t))) = (s +* ((v . s),(t . s)));

      ( dom s) = X by FUNCT_2:def 1;

      hence thesis by A3, FUNCT_7: 31, FUNCT_7: 32;

    end;

    theorem :: AOFA_I00:25



     Th25: for x be Variable of f holds for i be Integer holds ((f . (s,(x := i))) . x) = i & for z st z <> x holds ((f . (s,(x := i))) . z) = (s . z)

    proof

      let x be Variable of f;

      let i be Integer;



       A1: (( . (i,A,f)) . s) = i;

      (( ^ x) . s) = x;

      hence thesis by A1, Th24;

    end;

    theorem :: AOFA_I00:26



     Th26: for x be Variable of f holds for t be INT-Expression of A, f holds ((f . (s,(x := t))) . x) = (t . s) & for z st z <> x holds ((f . (s,(x := t))) . z) = (s . z)

    proof

      let x be Variable of f;

      let t be INT-Expression of A, f;

      (( ^ x) . s) = x;

      hence thesis by Th24;

    end;

    theorem :: AOFA_I00:27



     Th27: for x,y be Variable of f holds ((f . (s,(x := y))) . x) = (s . y) & for z st z <> x holds ((f . (s,(x := y))) . z) = (s . z)

    proof

      let x,y be Variable of f;

      (( . y) . s) = (s . y) by Th22;

      hence thesis by Th26;

    end;

    theorem :: AOFA_I00:28



     Th28: for x be Variable of f holds ((f . (s,(x += i))) . x) = ((s . x) + i) & for z st z <> x holds ((f . (s,(x += i))) . z) = (s . z)

    proof

      let x be Variable of f;



       A2: (( . ( ^ x qua Element of X)) . s) = (s . (( ^ x qua Element of X) . s)) by Def19;

      ((( . x) + i) . s) = ((( . x) . s) + i) by Def8;

      hence thesis by A2, Th24;

    end;

    theorem :: AOFA_I00:29



     Th29: for x be Variable of f holds for t be INT-Expression of A, f holds ((f . (s,(x += t))) . x) = ((s . x) + (t . s)) & for z st z <> x holds ((f . (s,(x += t))) . z) = (s . z)

    proof

      let x be Variable of f;

      let t be INT-Expression of A, f;



       A1: (( ^ x) . s) = x;

      ( dom (( . x) + t)) = ( Funcs (X, INT )) by FUNCT_2:def 1;

      then

       A2: ((( . x) + t) . s) = ((( . x) . s) + (t . s)) by VALUED_1:def 1;

      (( . x) . s) = (s . x) by Th22;

      hence thesis by A1, A2, Th24;

    end;

    theorem :: AOFA_I00:30



     Th30: for x,y be Variable of f holds ((f . (s,(x += y))) . x) = ((s . x) + (s . y)) & for z st z <> x holds ((f . (s,(x += y))) . z) = (s . z)

    proof

      let x,y be Variable of f;

      (( . y) . s) = (s . y) by Th22;

      hence thesis by Th29;

    end;

    theorem :: AOFA_I00:31



     Th31: for x be Variable of f holds ((f . (s,(x *= i))) . x) = ((s . x) * i) & for z st z <> x holds ((f . (s,(x *= i))) . z) = (s . z)

    proof

      let x be Variable of f;



       A2: (( . ( ^ x qua Element of X)) . s) = (s . (( ^ x qua Element of X) . s)) by Def19;

      ((( . x) * i) . s) = ((( . x) . s) * i) by Def10;

      hence thesis by A2, Th24;

    end;

    theorem :: AOFA_I00:32



     Th32: for x be Variable of f holds for t be INT-Expression of A, f holds ((f . (s,(x *= t))) . x) = ((s . x) * (t . s)) & for z st z <> x holds ((f . (s,(x *= t))) . z) = (s . z)

    proof

      let x be Variable of f;

      let t be INT-Expression of A, f;



       A1: (( ^ x) . s) = x;

      ( dom (( . x) (#) t)) = ( Funcs (X, INT )) by FUNCT_2:def 1;

      then

       A2: ((( . x) (#) t) . s) = ((( . x) . s) * (t . s)) by VALUED_1:def 4;

      (( . x) . s) = (s . x) by Th22;

      hence thesis by A1, A2, Th24;

    end;

    theorem :: AOFA_I00:33



     Th33: for x,y be Variable of f holds ((f . (s,(x *= y))) . x) = ((s . x) * (s . y)) & for z st z <> x holds ((f . (s,(x *= y))) . z) = (s . z)

    proof

      let x,y be Variable of f;



       A1: ( dom (( . x) (#) ( . y))) = ( Funcs (X, INT )) by FUNCT_2:def 1;

      (( ^ x) . s) = x;



      hence ((f . (s,(x *= y))) . x) = ((( . x) (#) ( . y)) . s) by Th24

      .= ((( . x) . s) * (( . y) . s)) by A1, VALUED_1:def 4

      .= ((s . x) * (( . y) . s)) by Th22

      .= ((s . x) * (s . y)) by Th22;

      thus thesis by Th26;

    end;

    theorem :: AOFA_I00:34



     Th34: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x be Variable of g holds for i be Integer holds ((s . x) <= i implies ((g . (s,(x leq i))) . b) = 1) & ((s . x) > i implies ((g . (s,(x leq i))) . b) = 0 ) & ((s . x) >= i implies ((g . (s,(x geq i))) . b) = 1) & ((s . x) < i implies ((g . (s,(x geq i))) . b) = 0 ) & for z st z <> b holds ((g . (s,(x leq i))) . z) = (s . z) & ((g . (s,(x geq i))) . z) = (s . z)

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      reconsider b9 = b as Variable of f by Def2;

      let x be Variable of f;

      let i be Integer;

      set v = ( ^ b9);



       A2: (v . s) = b;



       A3: (( . x) . s) < i implies ( IFGT (i,(( . x) . s), 0 ,1)) = 0 by XXREAL_0:def 11;



       A4: (( . x) . s) >= i implies ( IFGT (i,(( . x) . s), 0 ,1)) = 1 by XXREAL_0:def 11;



       A5: (( leq (( . (i,A,f)),( . x))) . s) = ( IFGT ((( . (i,A,f)) . s),(( . x) . s), 0 ,1)) by Def31;



       A6: (( . x) . s) > i implies ( IFGT ((( . x) . s),i, 0 ,1)) = 0 by XXREAL_0:def 11;



       A7: (( leq (( . x),( . (i,A,f)))) . s) = ( IFGT ((( . x) . s),(( . (i,A,f)) . s), 0 ,1)) by Def31;



       A8: (( . x) . s) <= i implies ( IFGT ((( . x) . s),i, 0 ,1)) = 1 by XXREAL_0:def 11;

      (( . x) . s) = (s . (( ^ x) . s)) by Def19;

      hence thesis by A2, A8, A6, A4, A3, A7, A5, Th24;

    end;

    theorem :: AOFA_I00:35



     Th35: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x,y be Variable of g holds ((s . x) <= (s . y) implies ((g . (s,(x leq y))) . b) = 1) & ((s . x) > (s . y) implies ((g . (s,(x leq y))) . b) = 0 ) & for z st z <> b holds ((g . (s,(x leq y))) . z) = (s . z)

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      reconsider b9 = b as Variable of f by Def2;

      let x,y be Variable of f;

      set v = ( ^ b9);



       A1: (v . s) = b;



       A2: (( . x) . s) <= (( . y) . s) implies ( IFGT ((( . x) . s),(( . y) . s), 0 ,1)) = 1 by XXREAL_0:def 11;

      (( . x) . s) = (s . (( ^ x) . s)) by Def19;

      then

       A3: (s . x) = (( . x) . s);



       A4: (( . x) . s) > (( . y) . s) implies ( IFGT ((( . x) . s),(( . y) . s), 0 ,1)) = 0 by XXREAL_0:def 11;



       A5: (( leq (( . x),( . y))) . s) = ( IFGT ((( . x) . s),(( . y) . s), 0 ,1)) by Def31;

      (( . y) . s) = (s . (( ^ y) . s)) by Def19;

      hence thesis by A3, A1, A2, A4, A5, Th24;

    end;

    theorem :: AOFA_I00:36

    for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x be Variable of g holds for i be Integer holds ((s . x) <= i iff (g . (s,(x leq i))) in (( Funcs (X, INT )) \ (b, 0 ))) & ((s . x) >= i iff (g . (s,(x geq i))) in (( Funcs (X, INT )) \ (b, 0 )))

    proof

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x be Variable of g;

      let i be Integer;

      (g . (s,(x leq i))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x leq i))) . b) <> 0 by Th2;

      hence (s . x) <= i iff (g . (s,(x leq i))) in (( Funcs (X, INT )) \ (b, 0 )) by Th34;

      (g . (s,(x geq i))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x geq i))) . b) <> 0 by Th2;

      hence thesis by Th34;

    end;

    theorem :: AOFA_I00:37

    for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x,y be Variable of g holds ((s . x) <= (s . y) iff (g . (s,(x leq y))) in (( Funcs (X, INT )) \ (b, 0 ))) & ((s . x) >= (s . y) iff (g . (s,(x geq y))) in (( Funcs (X, INT )) \ (b, 0 )))

    proof

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x,y be Variable of g;

      (g . (s,(x leq y))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x leq y))) . b) <> 0 by Th2;

      hence (s . x) <= (s . y) iff (g . (s,(x leq y))) in (( Funcs (X, INT )) \ (b, 0 )) by Th35;

      (g . (s,(x geq y))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x geq y))) . b) <> 0 by Th2;

      hence thesis by Th35;

    end;

    theorem :: AOFA_I00:38



     Th38: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x be Variable of g holds for i be Integer holds ((s . x) > i implies ((g . (s,(x gt i))) . b) = 1) & ((s . x) <= i implies ((g . (s,(x gt i))) . b) = 0 ) & ((s . x) < i implies ((g . (s,(x lt i))) . b) = 1) & ((s . x) >= i implies ((g . (s,(x lt i))) . b) = 0 ) & for z st z <> b holds ((g . (s,(x gt i))) . z) = (s . z) & ((g . (s,(x lt i))) . z) = (s . z)

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      reconsider b9 = b as Variable of f by Def2;

      let x be Variable of f;

      let i be Integer;

      set v = ( ^ b9);



       A2: (v . s) = b;



       A3: (( . x) . s) >= i implies ( IFGT (i,(( . x) . s),1, 0 )) = 0 by XXREAL_0:def 11;



       A4: (( . x) . s) < i implies ( IFGT (i,(( . x) . s),1, 0 )) = 1 by XXREAL_0:def 11;



       A5: (( gt (( . (i,A,f)),( . x))) . s) = ( IFGT ((( . (i,A,f)) . s),(( . x) . s),1, 0 )) by Def32;



       A6: (( . x) . s) <= i implies ( IFGT ((( . x) . s),i,1, 0 )) = 0 by XXREAL_0:def 11;



       A7: (( gt (( . x),( . (i,A,f)))) . s) = ( IFGT ((( . x) . s),(( . (i,A,f)) . s),1, 0 )) by Def32;



       A8: (( . x) . s) > i implies ( IFGT ((( . x) . s),i,1, 0 )) = 1 by XXREAL_0:def 11;

      (( . x) . s) = (s . (( ^ x) . s)) by Def19;

      hence thesis by A2, A8, A6, A4, A3, A7, A5, Th24;

    end;

    theorem :: AOFA_I00:39



     Th39: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x,y be Variable of g holds ((s . x) > (s . y) implies ((g . (s,(x gt y))) . b) = 1) & ((s . x) <= (s . y) implies ((g . (s,(x gt y))) . b) = 0 ) & ((s . x) < (s . y) implies ((g . (s,(x lt y))) . b) = 1) & ((s . x) >= (s . y) implies ((g . (s,(x lt y))) . b) = 0 ) & for z st z <> b holds ((g . (s,(x gt y))) . z) = (s . z) & ((g . (s,(x lt y))) . z) = (s . z)

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      reconsider b9 = b as Variable of f by Def2;

      let x,y be Variable of f;

      set v = ( ^ b9);



       A1: (v . s) = b;



       A2: (( . x) . s) > (( . y) . s) implies ( IFGT ((( . x) . s),(( . y) . s),1, 0 )) = 1 by XXREAL_0:def 11;



       A3: (( gt (( . x),( . y))) . s) = ( IFGT ((( . x) . s),(( . y) . s),1, 0 )) by Def32;



       A4: (( . x) . s) < (( . y) . s) implies ( IFGT ((( . y) . s),(( . x) . s),1, 0 )) = 1 by XXREAL_0:def 11;

      (( . x) . s) = (s . (( ^ x) . s)) by Def19;

      then

       A5: (s . x) = (( . x) . s);



       A6: (( . x) . s) <= (( . y) . s) implies ( IFGT ((( . x) . s),(( . y) . s),1, 0 )) = 0 by XXREAL_0:def 11;



       A7: (( gt (( . y),( . x))) . s) = ( IFGT ((( . y) . s),(( . x) . s),1, 0 )) by Def32;



       A8: (( . x) . s) >= (( . y) . s) implies ( IFGT ((( . y) . s),(( . x) . s),1, 0 )) = 0 by XXREAL_0:def 11;

      (( . y) . s) = (s . (( ^ y) . s)) by Def19;

      hence thesis by A5, A1, A2, A6, A4, A8, A3, A7, Th24;

    end;

    theorem :: AOFA_I00:40



     Th40: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x be Variable of g holds for i be Integer holds ((s . x) > i iff (g . (s,(x gt i))) in (( Funcs (X, INT )) \ (b, 0 ))) & ((s . x) < i iff (g . (s,(x lt i))) in (( Funcs (X, INT )) \ (b, 0 )))

    proof

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x be Variable of g;

      let i be Integer;

      (g . (s,(x gt i))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x gt i))) . b) <> 0 by Th2;

      hence (s . x) > i iff (g . (s,(x gt i))) in (( Funcs (X, INT )) \ (b, 0 )) by Th38;

      (g . (s,(x lt i))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x lt i))) . b) <> 0 by Th2;

      hence thesis by Th38;

    end;

    theorem :: AOFA_I00:41

    for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x,y be Variable of g holds ((s . x) > (s . y) iff (g . (s,(x gt y))) in (( Funcs (X, INT )) \ (b, 0 ))) & ((s . x) < (s . y) iff (g . (s,(x lt y))) in (( Funcs (X, INT )) \ (b, 0 )))

    proof

      let b be Element of X;

      let g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x,y be Variable of g;

      (g . (s,(x gt y))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x gt y))) . b) <> 0 by Th2;

      hence (s . x) > (s . y) iff (g . (s,(x gt y))) in (( Funcs (X, INT )) \ (b, 0 )) by Th39;

      (g . (s,(x lt y))) in (( Funcs (X, INT )) \ (b, 0 )) iff ((g . (s,(x lt y))) . b) <> 0 by Th2;

      hence thesis by Th39;

    end;

    theorem :: AOFA_I00:42

    for x be Variable of f holds ((f . (s,(x %= i))) . x) = ((s . x) mod i) & for z st z <> x holds ((f . (s,(x %= i))) . z) = (s . z)

    proof

      let x be Variable of f;



       A3: (( . ( ^ x qua Element of X)) . s) = (s . (( ^ x qua Element of X) . s)) by Def19;

      ((( . x) mod ( . (i,A,f))) . s) = ((( . x) . s) mod (( . (i,A,f)) . s)) by Def30;

      hence thesis by A3, Th24;

    end;

    theorem :: AOFA_I00:43



     Th43: for x be Variable of f holds for t be INT-Expression of A, f holds ((f . (s,(x %= t))) . x) = ((s . x) mod (t . s)) & for z st z <> x holds ((f . (s,(x %= t))) . z) = (s . z)

    proof

      let x be Variable of f;

      let t be INT-Expression of A, f;



       A1: (( ^ x) . s) = x;



       A2: (( . x) . s) = (s . x) by Th22;

      ((( . x) mod t) . s) = ((( . x) . s) mod (t . s)) by Def30;

      hence thesis by A1, A2, Th24;

    end;

    theorem :: AOFA_I00:44



     Th44: for x,y be Variable of f holds ((f . (s,(x %= y))) . x) = ((s . x) mod (s . y)) & for z st z <> x holds ((f . (s,(x %= y))) . z) = (s . z)

    proof

      let x,y be Variable of f;



       A1: (x %= y) = (x %= ( . y));

      (( . y) . s) = (s . y) by Th22;

      hence thesis by A1, Th43;

    end;

    theorem :: AOFA_I00:45



     Th45: for x be Variable of f holds ((f . (s,(x /= i))) . x) = ((s . x) div i) & for z st z <> x holds ((f . (s,(x /= i))) . z) = (s . z)

    proof

      let x be Variable of f;



       A3: (( . ( ^ x qua Element of X)) . s) = (s . (( ^ x qua Element of X) . s)) by Def19;

      ((( . x) div ( . (i,A,f))) . s) = ((( . x) . s) div (( . (i,A,f)) . s)) by Def29;

      hence thesis by A3, Th24;

    end;

    theorem :: AOFA_I00:46



     Th46: for x be Variable of f holds for t be INT-Expression of A, f holds ((f . (s,(x /= t))) . x) = ((s . x) div (t . s)) & for z st z <> x holds ((f . (s,(x /= t))) . z) = (s . z)

    proof

      let x be Variable of f;

      let t be INT-Expression of A, f;



       A1: (( ^ x) . s) = x;



       A2: (( . x) . s) = (s . x) by Th22;

      ((( . x) div t) . s) = ((( . x) . s) div (t . s)) by Def29;

      hence thesis by A1, A2, Th24;

    end;

    theorem :: AOFA_I00:47

    for x,y be Variable of f holds ((f . (s,(x /= y))) . x) = ((s . x) div (s . y)) & for z st z <> x holds ((f . (s,(x /= y))) . z) = (s . z)

    proof

      let x,y be Variable of f;



       A1: (x /= y) = (x /= ( . y));

      (( . y) . s) = (s . y) by Th22;

      hence thesis by A1, Th46;

    end;

    theorem :: AOFA_I00:48



     Th48: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for t be INT-Expression of A, g holds ((g . (s,(t is_odd ))) . b) = ((t . s) mod 2) & ((g . (s,(t is_even ))) . b) = (((t . s) + 1) mod 2) & for z st z <> b holds ((g . (s,(t is_odd ))) . z) = (s . z) & ((g . (s,(t is_even ))) . z) = (s . z)

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let t be INT-Expression of A, f;

      reconsider y = b as Variable of f by Def2;



       A1: (t is_odd ) = (y := (t mod ( . (2,A,f))));

      ( dom (t + 1)) = ( Funcs (X, INT )) by FUNCT_2:def 1;

      then

       A2: ((t + 1) . s) = (1 + (t . s)) by VALUED_1:def 2;



       A3: (( . (2,A,f)) . s) = 2;

      then

       A4: (((t + 1) mod ( . (2,A,f))) . s) = (((t + 1) . s) mod 2) by Def30;

      ((t mod ( . (2,A,f))) . s) = ((t . s) mod 2) by A3, Def30;

      hence thesis by A1, A2, A4, Th26;

    end;

    theorem :: AOFA_I00:49



     Th49: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x be Variable of g holds ((g . (s,(x is_odd ))) . b) = ((s . x) mod 2) & ((g . (s,(x is_even ))) . b) = (((s . x) + 1) mod 2) & for z st z <> b holds ((g . (s,(x is_odd ))) . z) = (s . z)

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x be Variable of f;

      (( . x) . s) = (s . x) by Th22;

      hence thesis by Th48;

    end;

    theorem :: AOFA_I00:50



     Th50: for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for t be INT-Expression of A, g holds ((t . s) is odd iff (g . (s,(t is_odd ))) in (( Funcs (X, INT )) \ (b, 0 ))) & ((t . s) is even iff (g . (s,(t is_even ))) in (( Funcs (X, INT )) \ (b, 0 )))

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let t be INT-Expression of A, f;



       A1: ((t . s) mod 2) = 0 or ((t . s) mod 2) = 1 by PRE_FF: 6;



       A2: (t . s) = ((((t . s) div 2) * 2) + ((t . s) mod 2)) by INT_1: 59;

      ((f . (s,(t is_odd ))) . b) = ((t . s) mod 2) by Th48;

      hence (t . s) is odd iff (f . (s,(t is_odd ))) in (( Funcs (X, INT )) \ (b, 0 )) by A1, A2, Th2;



       A3: (((t . s) + 1) mod 2) = 0 or (((t . s) + 1) mod 2) = 1 by PRE_FF: 6;



       A4: ((t . s) + 1) = (((((t . s) + 1) div 2) * 2) + (((t . s) + 1) mod 2)) by INT_1: 59;

      ((f . (s,(t is_even ))) . b) = (((t . s) + 1) mod 2) by Th48;

      hence thesis by A3, A4, Th2;

    end;

    theorem :: AOFA_I00:51

    for b be Element of X holds for g be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 )) holds for x be Variable of g holds ((s . x) is odd iff (g . (s,(x is_odd ))) in (( Funcs (X, INT )) \ (b, 0 ))) & ((s . x) is even iff (g . (s,(x is_even ))) in (( Funcs (X, INT )) \ (b, 0 )))

    proof

      let b be Element of X;

      let f be Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

      let x be Variable of f;

      (( . x) . s) = (s . x) by Th22;

      hence thesis by Th50;

    end;

    scheme :: AOFA_I00:sch1

    ForToIteration { A() -> Euclidean preIfWhileAlgebra , X() -> countable non empty set , b() -> Element of X() , I,F() -> Element of A() , g() -> Euclidean ExecutionFunction of A(), ( Funcs (X(), INT )), (( Funcs (X(), INT )) \ (b(), 0 )) , i,n() -> Variable of g() , s() -> Element of ( Funcs (X(), INT )) , a() -> INT-Expression of A(), g() , P[ set] } :

P[(g() . (s(),F()))] & ((a() . s()) <= (s() . n()) implies ((g() . (s(),F())) . i()) = ((s() . n()) + 1)) & ((a() . s()) > (s() . n()) implies ((g() . (s(),F())) . i()) = (a() . s())) & ((g() . (s(),F())) . n()) = (s() . n())

      provided

       A1: F() = ( for-do ((i() := a()),(i() leq n()),(i() += 1),I()))

       and

       A2: P[(g() . (s(),(i() := a())))]

       and

       A3: for s be Element of ( Funcs (X(), INT )) st P[s] holds P[(g() . (s,(I() \; (i() += 1))))] & P[(g() . (s,(i() leq n())))]

       and

       A4: for s be Element of ( Funcs (X(), INT )) st P[s] holds ((g() . (s,I())) . i()) = (s . i()) & ((g() . (s,I())) . n()) = (s . n())

       and

       A5: n() <> i() & n() <> b() & i() <> b();

      set C = (i() leq n());

      set S = ( Funcs (X(), INT ));

      reconsider s1 = (g() . (s(),(i() := a()))) as Element of S;

      reconsider s2 = (g() . (s1,C)) as Element of S;



       A6: P[s2] by A2, A3;

      defpred Q[ Element of S] means P[$1] & ((a() . s()) <= (s() . n()) implies (($1 . i()) - 1) <= (s() . n())) & ($1 . n()) = (s() . n());



       A7: (s1 . i()) = (a() . s()) by Th26;

      then

       A8: (s2 . i()) = (a() . s()) by A5, Th35;

      defpred R[ Element of S] means ($1 . i()) <= ($1 . n());

      set T = (S \ (b(), 0 ));



       A9: g() complies_with_while_wrt T by AOFA_000:def 32;

      set II = (I() \; (i() += 1));



       A10: (g() . (s(),F())) = (g() . (s1,( while (C,II)))) by A1, AOFA_000:def 29;

      ((a() . s()) - 1) < (a() . s()) by XREAL_1: 44;

      then

       A11: Q[s1] by A2, A5, A7, Th26, XXREAL_0: 2;



       A12: (s1 . n()) = (s() . n()) by A5, Th26;

      then

       A13: (s2 . n()) = (s() . n()) by A5, Th35;

      per cases ;

        suppose

         A14: (a() . s()) <= (s() . n());

        deffunc F( Element of S) = ( In (((($1 . n()) + 1) - ($1 . i())), NAT ));

        defpred PR[ Element of S] means P[$1] & R[$1];



         A15: for s be Element of S st Q[s] & s in T & R[s] holds Q[(g() . (s,II)) qua Element of S]

        proof

          let s be Element of S;

          assume that

           A16: Q[s] and s in T and

           A17: R[s];

          thus P[(g() . (s,II))] by A3, A16;

          reconsider s9 = (g() . (s,I())) as Element of S;

          reconsider s99 = (g() . (s9,(i() += 1))) as Element of S;



           A18: s99 = (g() . (s,II)) by AOFA_000:def 29;



           A19: (s99 . i()) = ((s9 . i()) + 1) by Th28;

          (s9 . n()) = (s . n()) by A4, A16;

          hence thesis by A4, A5, A16, A17, A19, A18, Th28;

        end;



         A20: for s be Element of S st PR[s] holds ( PR[(g() . (s,(II \; C))) qua Element of S] iff (g() . (s,(II \; C))) in T) & F() < F(s)

        proof

          let s be Element of S;

          reconsider s9 = (g() . (s,I())) as Element of S;

          reconsider s99 = (g() . (s9,(i() += 1))) as Element of S;

          reconsider s999 = (g() . (s99,C)) as Element of S;



           A21: (g() . (s,(II \; C))) = (g() . ((g() . (s,II)),C)) by AOFA_000:def 29;



           A22: (s99 . n()) = (s9 . n()) by A5, Th28;



           A23: (s99 . i()) <= (s99 . n()) implies (s999 . b()) = 1 by Th35;



           A24: (s99 . i()) > (s99 . n()) implies (s999 . b()) = 0 by Th35;

          assume

           A25: PR[s];

          then

          reconsider j = ((s . n()) - (s . i())) as Element of NAT by INT_1: 5;



           A26: (s999 . i()) = (s99 . i()) by A5, Th35;



           A27: s99 = (g() . (s,II)) by AOFA_000:def 29;

          then P[s99] by A3, A25;

          hence PR[(g() . (s,(II \; C))) qua Element of S] iff (g() . (s,(II \; C))) in T by A3, A5, A21, A27, A26, A24, A23, Th2, Th35;



           A28: (s99 . i()) = ((s9 . i()) + 1) by Th28;



           A29: (s9 . n()) = (s . n()) by A4, A25;



           A30: (s9 . i()) = (s . i()) by A4, A25;

          (s999 . n()) = (s99 . n()) by A5, Th35;

          then F(s999) = j by A26, A30, A29, A28, A22;

          then ( F(s999) + 1) = F(s);

          hence thesis by A21, A27, NAT_1: 13;

        end;



         A31: for s be Element of S st Q[s] holds Q[(g() . (s,C)) qua Element of S] & ((g() . (s,C)) in T iff R[(g() . (s,C)) qua Element of S])

        proof

          let s be Element of S;



           A32: (s . i()) > (s . n()) implies ((g() . (s,C)) . b()) = 0 by Th35;

          assume

           A33: Q[s];

          hence P[(g() . (s,C))] by A3;



           A34: (s . i()) <= (s . n()) implies ((g() . (s,C)) . b()) = 1 by Th35;

          ((g() . (s,C)) . i()) = (s . i()) by A5, Th35;

          hence thesis by A5, A33, A32, A34, Th2, Th35;

        end;

        (s2 . b()) = 1 by A7, A12, A14, Th35;

        then

         A35: (g() . (s1,C)) in T iff PR[(g() . (s1,C)) qua Element of S] by A2, A3, A5, A12, A8, A14, Th35;



         A36: g() iteration_terminates_for ((II \; C),(g() . (s1,C))) from AOFA_000:sch 3( A35, A20);



         A37: Q[(g() . (s1,( while (C,II)))) qua Element of S] & not R[(g() . (s1,( while (C,II)))) qua Element of S] from AOFA_000:sch 5( A11, A36, A15, A31);

        then ((g() . (s(),F())) qua Element of S . i()) >= ((s() . n()) + 1) by A10, INT_1: 7;

        then (((g() . (s(),F())) qua Element of S . i()) - 1) >= (((s() . n()) + 1) - 1) by XREAL_1: 13;

        then (((g() . (s(),F())) qua Element of S . i()) - 1) = (s() . n()) by A10, A14, A37, XXREAL_0: 1;

        hence thesis by A1, A14, A37, AOFA_000:def 29;

      end;

        suppose

         A38: (a() . s()) > (s() . n());

        then (s2 . b()) = 0 by A7, A12, Th35;

        then s2 nin T by Th2;

        hence thesis by A9, A8, A13, A10, A6, A38;

      end;

    end;

    scheme :: AOFA_I00:sch2

    ForDowntoIteration { A() -> Euclidean preIfWhileAlgebra , X() -> countable non empty set , b() -> Element of X() , I,F() -> Element of A() , f() -> Euclidean ExecutionFunction of A(), ( Funcs (X(), INT )), (( Funcs (X(), INT )) \ (b(), 0 )) , i,n() -> Variable of f() , s() -> Element of ( Funcs (X(), INT )) , a() -> INT-Expression of A(), f() , P[ set] } :

P[(f() . (s(),F()))] & ((a() . s()) >= (s() . n()) implies ((f() . (s(),F())) . i()) = ((s() . n()) - 1)) & ((a() . s()) < (s() . n()) implies ((f() . (s(),F())) . i()) = (a() . s())) & ((f() . (s(),F())) . n()) = (s() . n())

      provided

       A1: F() = ( for-do ((i() := a()),(( . n()) leq ( . i())),(i() += ( - 1)),I()))

       and

       A2: P[(f() . (s(),(i() := a())))]

       and

       A3: for s be Element of ( Funcs (X(), INT )) st P[s] holds P[(f() . (s,(I() \; (i() += ( - 1)))))] & P[(f() . (s,(n() leq i())))]

       and

       A4: for s be Element of ( Funcs (X(), INT )) st P[s] holds ((f() . (s,I())) . i()) = (s . i()) & ((f() . (s,I())) . n()) = (s . n())

       and

       A5: n() <> i() & n() <> b() & i() <> b();

      set S = ( Funcs (X(), INT ));

      reconsider s1 = (f() . (s(),(i() := a()))) as Element of S;

      set C = (n() leq i());

      reconsider s2 = (f() . (s1,C)) as Element of S;



       A6: P[s2] by A2, A3;

      defpred Q[ Element of S] means P[$1] & ((a() . s()) >= (s() . n()) implies (($1 . i()) + 1) >= (s() . n())) & ($1 . n()) = (s() . n());



       A7: (s1 . i()) = (a() . s()) by Th26;

      then

       A8: Q[s1] by A2, A5, Th26, XREAL_1: 39;



       A9: (s2 . i()) = (a() . s()) by A5, A7, Th35;

      defpred R[ Element of S] means ($1 . i()) >= ($1 . n());

      set T = (S \ (b(), 0 ));



       A10: f() complies_with_while_wrt T by AOFA_000:def 32;

      set II = (I() \; (i() += ( - 1)));



       A11: (f() . (s(),F())) = (f() . (s1,( while (C,II)))) by A1, AOFA_000:def 29;



       A12: (s1 . n()) = (s() . n()) by A5, Th26;

      then

       A13: (s2 . n()) = (s() . n()) by A5, Th35;

      per cases ;

        suppose

         A14: (a() . s()) >= (s() . n());

        deffunc F( Element of S) = ( In (((($1 . i()) + 1) - ($1 . n())), NAT ));

        defpred PR[ Element of S] means P[$1] & R[$1];



         A15: for s be Element of S st Q[s] & s in T & R[s] holds Q[(f() . (s,II)) qua Element of S]

        proof

          let s be Element of S;

          assume that

           A16: Q[s] and s in T and

           A17: R[s];

          thus P[(f() . (s,II))] by A3, A16;

          reconsider s99 = (f() . (s,I())) as Element of S;

          reconsider s999 = (f() . (s99,(i() += ( - 1)))) as Element of S;



           A18: s999 = (f() . (s,II)) by AOFA_000:def 29;



           A19: (s999 . i()) = ((s99 . i()) - 1) by Th28;

          (s99 . n()) = (s . n()) by A4, A16;

          hence thesis by A4, A5, A16, A17, A19, A18, Th28;

        end;



         A20: for s be Element of S st PR[s] holds ( PR[(f() . (s,(II \; C))) qua Element of S] iff (f() . (s,(II \; C))) in T) & F() < F(s)

        proof

          let s be Element of S;

          reconsider s9 = (f() . (s,I())) as Element of S;

          reconsider s99 = (f() . (s9,(i() += ( - 1)))) as Element of S;

          reconsider s999 = (f() . (s99,C)) as Element of S;



           A21: (f() . (s,(II \; C))) = (f() . ((f() . (s,II)),C)) by AOFA_000:def 29;



           A22: (s99 . n()) = (s9 . n()) by A5, Th28;



           A23: (s99 . i()) >= (s99 . n()) implies (s999 . b()) = 1 by Th35;



           A24: (s99 . i()) < (s99 . n()) implies (s999 . b()) = 0 by Th35;

          assume

           A25: PR[s];

          then

          reconsider j = ((s . i()) - (s . n())) as Element of NAT by INT_1: 5;



           A26: (s999 . i()) = (s99 . i()) by A5, Th35;



           A27: s99 = (f() . (s,II)) by AOFA_000:def 29;

          then P[s99] by A3, A25;

          hence PR[(f() . (s,(II \; C))) qua Element of S] iff (f() . (s,(II \; C))) in T by A3, A5, A21, A27, A26, A24, A23, Th2, Th35;



           A28: (s99 . i()) = ((s9 . i()) - 1) by Th28;



           A29: (s9 . n()) = (s . n()) by A4, A25;



           A30: (s9 . i()) = (s . i()) by A4, A25;

          (s999 . n()) = (s99 . n()) by A5, Th35;

          then F(s999) = j by A26, A30, A29, A28, A22;

          then ( F(s999) + 1) = F(s);

          hence thesis by A21, A27, NAT_1: 13;

        end;



         A31: for s be Element of S st Q[s] holds Q[(f() . (s,C)) qua Element of S] & ((f() . (s,C)) in T iff R[(f() . (s,C)) qua Element of S])

        proof

          let s be Element of S;



           A32: (s . i()) < (s . n()) implies ((f() . (s,C)) . b()) = 0 by Th35;

          assume

           A33: Q[s];

          hence P[(f() . (s,C))] by A3;



           A34: (s . i()) >= (s . n()) implies ((f() . (s,C)) . b()) = 1 by Th35;

          ((f() . (s,C)) . i()) = (s . i()) by A5, Th35;

          hence thesis by A5, A33, A32, A34, Th2, Th35;

        end;

        (s2 . b()) = 1 by A7, A12, A14, Th35;

        then

         A35: (f() . (s1,C)) in T iff PR[(f() . (s1,C)) qua Element of S] by A2, A3, A5, A12, A9, A14, Th35;



         A36: f() iteration_terminates_for ((II \; C),(f() . (s1,C))) from AOFA_000:sch 3( A35, A20);



         A37: Q[(f() . (s1,( while (C,II)))) qua Element of S] & not R[(f() . (s1,( while (C,II)))) qua Element of S] from AOFA_000:sch 5( A8, A36, A15, A31);

        then (((f() . (s(),F())) qua Element of S . i()) + 1) <= (((s() . n()) + 1) - 1) by A11, INT_1: 7;

        then (((f() . (s(),F())) qua Element of S . i()) + 1) = (s() . n()) by A11, A14, A37, XXREAL_0: 1;

        hence thesis by A1, A14, A37, AOFA_000:def 29;

      end;

        suppose

         A38: (a() . s()) < (s() . n());

        then (s2 . b()) = 0 by A7, A12, Th35;

        then s2 nin T by Th2;

        hence thesis by A10, A9, A13, A11, A6, A38;

      end;

    end;

    begin

    reserve b for Element of X,

g for Euclidean ExecutionFunction of A, ( Funcs (X, INT )), (( Funcs (X, INT )) \ (b, 0 ));

    theorem :: AOFA_I00:52



     Th52: for I be Element of A holds for i,n be Variable of g st (ex d be Function st (d . b) = 0 & (d . n) = 1 & (d . i) = 2) & for s holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i) holds g iteration_terminates_for (((I \; (i += 1)) \; (i leq n)),(g . (s,(i leq n))))

    proof

      let I be Element of A;

      let i,n be Variable of g;

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . n) = 1 and

       A3: (d . i) = 2;

      set J = (i += 1);

      set C = (i leq n);

      set S = ( Funcs (X, INT ));

      set h = g;

      assume

       A4: for s holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i);

      deffunc F( Element of S) = ( In (((($1 . n) + 1) - ($1 . i)), NAT ));

      defpred R[ Element of S] means ($1 . i) <= ($1 . n);

      set T = (S \ (b, 0 ));



       A5: i <> n by A2, A3;



       A6: for s be Element of S st R[s] holds ( R[(h . (s,((I \; J) \; C))) qua Element of S] iff (h . (s,((I \; J) \; C))) in T) & F() < F(s)

      proof

        let s be Element of S;

        set s1 = (h . (s,I));

        set q = (h . (s,(I \; J)));

        set q1 = (h . (q,C));



         A7: q = (h . (s1,J)) by AOFA_000:def 29;

        (s1 . i) = (s . i) by A4;

        then (q . i) = ((s . i) + 1) by A7, Th28;

        then

         A8: (q1 . i) = ((s . i) + 1) by A1, A3, Th35;



         A9: (q . i) > (q . n) implies (q1 . b) = 0 by Th35;

        assume R[s];

        then

        reconsider ni = ((s . n) - (s . i)) as Element of NAT by INT_1: 3, XREAL_1: 48;



         A10: q1 = (h . (s,((I \; J) \; C))) by AOFA_000:def 29;



         A11: (q . i) <= (q . n) implies (q1 . b) = 1 by Th35;

        (q1 . i) = (q . i) by A1, A3, Th35;

        hence R[(h . (s,((I \; J) \; C))) qua Element of S] iff (h . (s,((I \; J) \; C))) in T by A1, A2, A9, A11, A10, Th2, Th35;



         A12: F(s) = (ni + 1);

        (s1 . n) = (s . n) by A4;

        then (q . n) = (s . n) by A5, A7, Th28;

        then (q1 . n) = (s . n) by A1, A2, Th35;

        then F() = ni by A8;

        hence thesis by A10, A12, NAT_1: 13;

      end;

      reconsider s1 = (h . (s,C)) as Element of S;



       A13: (s . i) > (s . n) implies (s1 . b) = 0 by Th35;



       A14: (s . i) <= (s . n) implies (s1 . b) = 1 by Th35;

      (s1 . i) = (s . i) by A1, A3, Th35;

      then

       A15: s1 in T iff R[s1] by A1, A2, A13, A14, Th2, Th35;

      h iteration_terminates_for (((I \; J) \; C),s1) from AOFA_000:sch 3( A15, A6);

      hence thesis;

    end;

    theorem :: AOFA_I00:53



     Th53: for P be set holds for I be Element of A holds for i,n be Variable of g st (ex d be Function st (d . b) = 0 & (d . n) = 1 & (d . i) = 2) & for s st s in P holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i) & (g . (s,I)) in P & (g . (s,(i leq n))) in P & (g . (s,(i += 1))) in P holds s in P implies g iteration_terminates_for (((I \; (i += 1)) \; (i leq n)),(g . (s,(i leq n))))

    proof

      let P be set;

      let I be Element of A;

      let i,n be Variable of g;

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . n) = 1 and

       A3: (d . i) = 2;

      set J = (i += 1);

      set C = (i leq n);

      set S = ( Funcs (X, INT ));

      set h = g;

      assume that

       A4: for s st s in P holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i) & (g . (s,I)) in P & (g . (s,(i leq n))) in P & (g . (s,(i += 1))) in P and

       A5: s in P;

      defpred P[ Element of S] means $1 in P;

      reconsider s1 = (h . (s,C)) as Element of S;



       A6: P[s1] by A4, A5;

      deffunc F( Element of S) = ( In (((($1 . n) + 1) - ($1 . i)), NAT ));

      defpred R[ Element of S] means ($1 . i) <= ($1 . n);

      set T = (S \ (b, 0 ));



       A7: i <> n by A2, A3;



       A8: for s be Element of S st P[s] & s in T & R[s] holds P[(h . (s,((I \; J) \; C))) qua Element of S] & ( R[(h . (s,((I \; J) \; C))) qua Element of S] iff (h . (s,((I \; J) \; C))) in T) & F() < F(s)

      proof

        let s be Element of S;

        assume that

         A9: P[s] and s in T and

         A10: R[s];

        set q = (h . (s,(I \; J)));

        set s1 = (h . (s,I));

        set q1 = (h . (q,C));



         A11: q = (h . (s1,J)) by AOFA_000:def 29;

        (s1 . i) = (s . i) by A4, A9;

        then (q . i) = ((s . i) + 1) by A11, Th28;

        then

         A12: (q1 . i) = ((s . i) + 1) by A1, A3, Th35;

        reconsider ni = ((s . n) - (s . i)) as Element of NAT by A10, INT_1: 3, XREAL_1: 48;



         A13: F(s) = (ni + 1);



         A14: (q . i) <= (q . n) implies (q1 . b) = 1 by Th35;



         A15: q1 = (h . (s,((I \; J) \; C))) by AOFA_000:def 29;

         P[s1 qua Element of S] by A4, A9;

        then P[q qua Element of S] by A4, A11;

        hence P[(h . (s,((I \; J) \; C))) qua Element of S] by A4, A15;



         A16: (q . i) > (q . n) implies (q1 . b) = 0 by Th35;

        (q1 . i) = (q . i) by A1, A3, Th35;

        hence R[(h . (s,((I \; J) \; C))) qua Element of S] iff (h . (s,((I \; J) \; C))) in T by A1, A2, A16, A14, A15, Th2, Th35;

        (s1 . n) = (s . n) by A4, A9;

        then (q . n) = (s . n) by A7, A11, Th28;

        then (q1 . n) = (s . n) by A1, A2, Th35;

        then F() = ni by A12;

        hence thesis by A15, A13, NAT_1: 13;

      end;



       A17: (s . i) > (s . n) implies (s1 . b) = 0 by Th35;



       A18: (s . i) <= (s . n) implies (s1 . b) = 1 by Th35;

      (s1 . i) = (s . i) by A1, A3, Th35;

      then

       A19: s1 in T iff R[s1] by A1, A2, A17, A18, Th2, Th35;

      h iteration_terminates_for (((I \; J) \; C),s1) from AOFA_000:sch 4( A6, A19, A8);

      hence thesis;

    end;

    theorem :: AOFA_I00:54



     Th54: for I be Element of A st I is_terminating_wrt g holds for i,n be Variable of g st (ex d be Function st (d . b) = 0 & (d . n) = 1 & (d . i) = 2) & for s holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i) holds ( for-do ((i := t),(i leq n),(i += 1),I)) is_terminating_wrt g

    proof

      set S = ( Funcs (X, INT ));

      set T = (( Funcs (X, INT )) \ (b, 0 ));

      let I be Element of A such that

       A1: I is_terminating_wrt g;

      let i,n be Variable of g;

      (i += 1) is_terminating_wrt g by AOFA_000: 104;

      then

       A2: (I \; (i += 1)) is_terminating_wrt g by A1, AOFA_000: 110;

      set Q = ( while ((i leq n),(I \; (i += 1))));

      given d be Function such that

       A3: (d . b) = 0 and

       A4: (d . n) = 1 and

       A5: (d . i) = 2;

      assume

       A6: for s holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i);

      let s;



       A7: [s, (i := t)] in ( TerminatingPrograms (A,S,T,g)) by AOFA_000:def 36;



       A8: (i leq n) is_terminating_wrt g by AOFA_000: 104;

      g iteration_terminates_for (((I \; (i += 1)) \; (i leq n)),(g . ((g . (s,(i := t))),(i leq n)))) by A3, A4, A5, A6, Th52;

      then [(g . (s,(i := t))), Q] in ( TerminatingPrograms (A,S,T,g)) by A8, A2, AOFA_000: 114;

      hence thesis by A7, AOFA_000:def 35;

    end;

    theorem :: AOFA_I00:55

    for P be set holds for I be Element of A st I is_terminating_wrt (g,P) holds for i,n be Variable of g st (ex d be Function st (d . b) = 0 & (d . n) = 1 & (d . i) = 2) & (for s st s in P holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i)) & P is_invariant_wrt ((i := t),g) & P is_invariant_wrt (I,g) & P is_invariant_wrt ((i leq n),g) & P is_invariant_wrt ((i += 1),g) holds ( for-do ((i := t),(i leq n),(i += 1),I)) is_terminating_wrt (g,P)

    proof

      set Z = ( Funcs (X, INT ));

      set T = (( Funcs (X, INT )) \ (b, 0 ));

      let S be set;

      let I be Element of A;

      assume

       A1: I is_terminating_wrt (g,S);

      let i,n be Variable of g;

      given d be Function such that

       A2: (d . b) = 0 and

       A3: (d . n) = 1 and

       A4: (d . i) = 2;

      set C = (i leq n), J = (I \; (i += 1));

      assume that

       A5: for s st s in S holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i) and

       A6: S is_invariant_wrt ((i := t),g) and

       A7: S is_invariant_wrt (I,g) and

       A8: S is_invariant_wrt ((i leq n),g) and

       A9: S is_invariant_wrt ((i += 1),g);

      let s;

      assume s in S;

      then

       A10: (g . (s,(i := t))) in S by A6;

      for s be Element of Z st s in S holds ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . i) = (s . i) & (g . (s,I)) in S & (g . (s,(i leq n))) in S & (g . (s,(i += 1))) in S by A5, A7, A8, A9;

      then

       A11: g iteration_terminates_for ((J \; C),(g . ((g . (s,(i := t))),C))) by A2, A3, A4, A10, Th53;

      set Q = ( while (C,J));



       A12: C is_terminating_wrt g by AOFA_000: 104;



       A13: [s, (i := t)] in ( TerminatingPrograms (A,Z,T,g)) by AOFA_000:def 36;

      S is_invariant_wrt (J,g) by A7, A9, AOFA_000: 109;

      then

       A14: for s st s in S & (g . ((g . (s,J)),C)) in T holds (g . (s,J)) in S;

      (i += 1) is_terminating_wrt (g,S) by AOFA_000: 107;

      then [(g . (s,(i := t))), Q] in ( TerminatingPrograms (A,Z,T,g)) by A1, A7, A8, A10, A11, A12, A14, AOFA_000: 111, AOFA_000: 116;

      hence thesis by A13, AOFA_000:def 35;

    end;

    begin

    definition

      let X, A, T, f, s;

      let I be Element of A;

      :: original: .

      redefine

      func f . (s,I) -> Element of ( Funcs (X, INT )) ;

      coherence

      proof

        (f . (s,I)) is Element of ( Funcs (X, INT ));

        hence thesis;

      end;

    end

    theorem :: AOFA_I00:56

    for n,s,i be Variable of g st ex d be Function st (d . n) = 1 & (d . s) = 2 & (d . i) = 3 & (d . b) = 4 holds ((s := 1) \; ( for-do ((i := 2),(i leq n),(i += 1),(s *= i)))) is_terminating_wrt g

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let n,s,i be Variable of g;

      given d be Function such that

       A1: (d . n) = 1 and

       A2: (d . s) = 2 and

       A3: (d . i) = 3 and

       A4: (d . b) = 4;



       A5: s <> n by A1, A2;

      s <> i by A2, A3;

      then

       A6: for q be Element of S holds ((g . (q,(s *= i))) . n) = (q . n) & ((g . (q,(s *= i))) . i) = (q . i) by A5, Th33;



       A7: n <> b by A1, A4;



       A8: b <> i by A3, A4;

      let q be Element of S;

      set t = ( . (2,A,g));

      i <> n by A1, A3;

      then ex d9 be Function st (d9 . b) = 0 & (d9 . n) = 1 & (d9 . i) = 2 by A8, A7, Th1;

      then ( for-do ((i := t),(i leq n),(i += 1),(s *= i))) is_terminating_wrt g by A6, Th54, AOFA_000: 104;

      then

       A9: [(g . (q,(s := 1))) qua Element of S, ( for-do ((i := t),(i leq n),(i += 1),(s *= i)))] in ( TerminatingPrograms (A,S,T,g));

       [q, (s := 1)] in ( TerminatingPrograms (A,S,T,g)) by AOFA_000:def 36;

      hence thesis by A9, AOFA_000:def 35;

    end;

    theorem :: AOFA_I00:57

    for n,s,i be Variable of g st ex d be Function st (d . n) = 1 & (d . s) = 2 & (d . i) = 3 & (d . b) = 4 holds for q be Element of ( Funcs (X, INT )) holds for N be Nat st N = (q . n) holds ((g . (q,((s := 1) \; ( for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s) = (N ! )

    proof

      set f = g;

      let n,s,i be Variable of f;

      given d be Function such that

       A1: (d . n) = 1 and

       A2: (d . s) = 2 and

       A3: (d . i) = 3 and

       A4: (d . b) = 4;



       A5: n <> i & n <> b & i <> b by A1, A3, A4;

      set S = ( Funcs (X, INT ));

      let q be Element of ( Funcs (X, INT ));

      reconsider q1 = (f . (q,(s := 1))) as Element of S;

      defpred P[ Element of S] means ex K be Nat st K = (($1 . i) - 1) & ($1 . s) = (K ! );

      reconsider a = ( . (2,A,f)) as INT-Expression of A, g;

      reconsider q2 = (f . (q1,(i := 2))) as Element of S;



       A6: (q2 . i) = 2 by Th25;



       A7: s <> i by A2, A3;

      then (q2 . s) = (q1 . s) by Th25;

      then

       A8: P[(f . (q1,(i := a)))] by A6, Th25, NEWTON: 13;

      set I = (s *= i);



       A10: s <> b by A2, A4;



       A11: for q be Element of ( Funcs (X, INT )) st P[q] holds P[(f . (q,(I \; (i += 1))))] & P[(f . (q,(i leq n)))]

      proof

        let q be Element of ( Funcs (X, INT ));

        given Ki be Nat such that

         A12: Ki = ((q . i) - 1) and

         A13: (q . s) = (Ki ! );

        reconsider q3 = (f . (q,I)) as Element of S;

        reconsider q4 = (f . (q3,(i += 1))) as Element of S;



         A14: (q3 . s) = ((q . s) * (q . i)) by Th33;

        (q4 . s) = (q3 . s) by A7, Th28;

        then

         A15: (q4 . s) = ((Ki + 1) ! ) by A12, A13, A14, NEWTON: 15;



         A16: q4 = (f . (q,(I \; (i += 1)))) by AOFA_000:def 29;

        (q4 . i) = ((q3 . i) + 1) by Th28;

        then (Ki + 1) = ((q4 . i) - 1) by A7, A12, Th33;

        hence P[(f . (q,(I \; (i += 1)))) qua Element of S] by A16, A15;

        reconsider q9 = (f . (q,(i leq n))) as Element of S;

        (q9 . i) = (q . i) by A5, Th35;

        hence thesis by A12, A13, A10, Th35;

      end;

      reconsider F = ( for-do ((i := a),(i leq n),(i += 1),I)) as Element of A;

      let N be Nat;

      assume

       A17: N = (q . n);



       A18: F = ( for-do ((i := a),(i leq n),(i += 1),I));



       A19: s <> n by A1, A2;



       A20: for q be Element of ( Funcs (X, INT )) st P[q] holds ((f . (q,I)) . i) = (q . i) & ((f . (q,I)) . n) = (q . n) by A19, A7, Th32;



       A21: P[(f . (q1,F))] & ((a . q1) <= (q1 . n) implies ((f . (q1,F)) . i) = ((q1 . n) + 1)) & ((a . q1) > (q1 . n) implies ((f . (q1,F)) . i) = (a . q1)) & ((f . (q1,F)) . n) = (q1 . n) from ForToIteration( A18, A8, A11, A20, A5);

      consider K be Nat such that

       A22: K = (((f . (q1,F)) . i) - 1) and

       A23: ((f . (q1,F)) . s) = (K ! ) by A21;

      per cases ;

        suppose

         A24: (a . q1) <= (q1 . n);



        thus ((f . (q,((s := 1) \; ( for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s) = (K ! ) by A23, AOFA_000:def 29

        .= (N ! ) by A17, A24, A21, A22, A19, Th25;

      end;

        suppose

         A25: (a . q1) > (q1 . n);

        then (1 + 1) > N by A19, A17, Th25;

        then

         A26: 1 >= N by NAT_1: 13;



        thus ((f . (q,((s := 1) \; ( for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s) = (K ! ) by A23, AOFA_000:def 29

        .= (N ! ) by A25, A21, A22, A26, NAT_1: 25, NEWTON: 12, NEWTON: 13;

      end;

    end;

    theorem :: AOFA_I00:58

    for x,n,s,i be Variable of g st ex d be Function st (d . n) = 1 & (d . s) = 2 & (d . i) = 3 & (d . b) = 4 holds ((s := 1) \; ( for-do ((i := 1),(i leq n),(i += 1),(s *= x)))) is_terminating_wrt g

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let x,n,s,i be Variable of g;

      given d be Function such that

       A1: (d . n) = 1 and

       A2: (d . s) = 2 and

       A3: (d . i) = 3 and

       A4: (d . b) = 4;



       A5: s <> n by A1, A2;

      s <> i by A2, A3;

      then

       A6: for q be Element of S holds ((g . (q,(s *= x))) . n) = (q . n) & ((g . (q,(s *= x))) . i) = (q . i) by A5, Th33;



       A7: n <> b by A1, A4;



       A8: b <> i by A3, A4;

      let q be Element of S;

      set t = ( . (1,A,g));

      i <> n by A1, A3;

      then ex d9 be Function st (d9 . b) = 0 & (d9 . n) = 1 & (d9 . i) = 2 by A8, A7, Th1;

      then ( for-do ((i := t),(i leq n),(i += 1),(s *= x))) is_terminating_wrt g by A6, Th54, AOFA_000: 104;

      then

       A9: [(g . (q,(s := 1))) qua Element of S, ( for-do ((i := t),(i leq n),(i += 1),(s *= x)))] in ( TerminatingPrograms (A,S,T,g));

       [q, (s := 1)] in ( TerminatingPrograms (A,S,T,g)) by AOFA_000:def 36;

      hence thesis by A9, AOFA_000:def 35;

    end;

    theorem :: AOFA_I00:59

    for x,n,s,i be Variable of g st ex d be Function st (d . x) = 0 & (d . n) = 1 & (d . s) = 2 & (d . i) = 3 & (d . b) = 4 holds for q be Element of ( Funcs (X, INT )) holds for N be Nat st N = (q . n) holds ((g . (q,((s := 1) \; ( for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s) = ((q . x) |^ N)

    proof

      set f = g;

      let x,n,s,i be Variable of f;

      given d be Function such that

       A1: (d . x) = 0 and

       A2: (d . n) = 1 and

       A3: (d . s) = 2 and

       A4: (d . i) = 3 and

       A5: (d . b) = 4;



       A6: n <> i & n <> b & i <> b by A2, A4, A5;

      set S = ( Funcs (X, INT ));

      let q be Element of ( Funcs (X, INT ));

      reconsider q1 = (f . (q,(s := 1))) as Element of S;

      reconsider q2 = (f . (q1,(i := 1))) as Element of S;



       A7: s <> i by A3, A4;

      then

       A8: (q2 . s) = (q1 . s) by Th25;

      defpred P[ Element of S] means ex K be Nat st K = (($1 . i) - 1) & ($1 . s) = ((q . x) |^ K) & ($1 . x) = (q . x);

      set I = (s *= x);

      set q0 = q;



       A9: ((q . x) |^ 0 ) = 1 by NEWTON: 4;



       A10: s <> n by A2, A3;

      then

       A11: for q be Element of ( Funcs (X, INT )) st P[q] holds ((f . (q,I)) . i) = (q . i) & ((f . (q,I)) . n) = (q . n) by A7, Th32;



       A12: s <> b by A3, A5;



       A13: for q be Element of ( Funcs (X, INT )) st P[q] holds P[(f . (q,(I \; (i += 1))))] & P[(f . (q,(i leq n)))]

      proof

        let q be Element of ( Funcs (X, INT ));

        given Ki be Nat such that

         A14: Ki = ((q . i) - 1) and

         A15: (q . s) = ((q0 . x) |^ Ki) and

         A16: (q . x) = (q0 . x);

        reconsider q3 = (f . (q,I)) as Element of S;

        reconsider q4 = (f . (q3,(i += 1))) as Element of S;



         A17: (q3 . s) = ((q . s) * (q . x)) by Th33;

        (q4 . s) = (q3 . s) by A7, Th28;

        then

         A18: (q4 . s) = ((q0 . x) |^ (Ki + 1)) by A15, A16, A17, NEWTON: 6;



         A19: q4 = (f . (q,(I \; (i += 1)))) by AOFA_000:def 29;



         A20: (q3 . x) = (q . x) by A1, A3, Th33;

        (q4 . i) = ((q3 . i) + 1) by Th28;

        then (Ki + 1) = ((q4 . i) - 1) by A7, A14, Th33;

        hence P[(f . (q,(I \; (i += 1)))) qua Element of S] by A1, A4, A16, A19, A20, A18, Th28;

        reconsider q9 = (f . (q,(i leq n))) as Element of S;



         A21: (q9 . s) = (q . s) by A12, Th35;



         A22: (q9 . i) = (q . i) by A6, Th35;

        (q9 . x) = (q . x) by A1, A5, Th35;

        hence thesis by A14, A15, A16, A21, A22;

      end;

      reconsider a = ( . (1,A,f)) as INT-Expression of A, g;

      reconsider F = ( for-do ((i := a),(i leq n),(i += 1),I)) as Element of A;



       A23: F = ( for-do ((i := a),(i leq n),(i += 1),I));



       A24: (q2 . i) = 1 by Th25;



       A25: (q2 . x) = (q1 . x) by A1, A4, Th25;



       A26: (q1 . s) = 1 by Th25;

      (q1 . x) = (q . x) by A1, A3, Th25;

      then

       A27: P[(f . (q1,(i := a)))] by A26, A8, A24, A25, A9;



       A28: P[(f . (q1,F))] & ((a . q1) <= (q1 . n) implies ((f . (q1,F)) . i) = ((q1 . n) + 1)) & ((a . q1) > (q1 . n) implies ((f . (q1,F)) . i) = (a . q1)) & ((f . (q1,F)) . n) = (q1 . n) from ForToIteration( A23, A27, A13, A11, A6);



       A30: (q1 . n) = (q . n) by A10, Th25;

      let N be Nat;

      assume

       A31: N = (q . n);



       A32: N = 0 or N >= 1 by NAT_1: 25;



      thus ((f . (q,((s := 1) \; ( for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s) = ((f . (q1,F)) . s) by AOFA_000:def 29

      .= ((q . x) |^ N) by A31, A30, A28, A32;

    end;

    theorem :: AOFA_I00:60

    for n,x,y,z,i be Variable of g st ex d be Function st (d . b) = 0 & (d . n) = 1 & (d . x) = 2 & (d . y) = 3 & (d . z) = 4 & (d . i) = 5 holds (((x := 0 ) \; (y := 1)) \; ( for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) is_terminating_wrt g

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let n,x,y,z,i be Variable of g;

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . n) = 1 and

       A3: (d . x) = 2 and

       A4: (d . y) = 3 and

       A5: (d . z) = 4 and

       A6: (d . i) = 5;



       A7: i <> y by A4, A6;



       A8: n <> z by A2, A5;



       A9: n <> y by A2, A4;



       A10: n <> x by A2, A3;



       A11: i <> z by A5, A6;

      set I = (((z := x) \; (x := y)) \; (y += z));

      set I1 = (z := x), I2 = (x := y), I3 = (y += z);



       A12: i <> x by A3, A6;



       A13: for q be Element of S holds ((g . (q,I)) . n) = (q . n) & ((g . (q,I)) . i) = (q . i)

      proof

        let q be Element of S;



        thus ((g . (q,I)) . n) = ((g . ((g . (q,(I1 \; I2))),I3)) . n) by AOFA_000:def 29

        .= ((g . (q,(I1 \; I2))) . n) by A9, Th30

        .= ((g . ((g . (q,I1)),I2)) . n) by AOFA_000:def 29

        .= ((g . (q,I1)) . n) by A10, Th27

        .= (q . n) by A8, Th27;



        thus ((g . (q,I)) . i) = ((g . ((g . (q,(I1 \; I2))),I3)) . i) by AOFA_000:def 29

        .= ((g . (q,(I1 \; I2))) . i) by A7, Th30

        .= ((g . ((g . (q,I1)),I2)) . i) by AOFA_000:def 29

        .= ((g . (q,I1)) . i) by A12, Th27

        .= (q . i) by A11, Th27;

      end;

      let s;

      set s2 = (g . (s,((x := 0 ) \; (y := 1))));

      i <> n by A2, A6;

      then ex d9 be Function st (d9 . b) = 0 & (d9 . n) = 1 & (d9 . i) = 2 by A1, A2, A6, Th1;

      then ( for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)))) is_terminating_wrt g by A13, Th54, AOFA_000: 104;

      then

       A14: [s2, ( for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))] in ( TerminatingPrograms (A,S,T,g));

       [s, ((x := 0 ) \; (y := 1))] in ( TerminatingPrograms (A,S,T,g)) by AOFA_000:def 36;

      hence thesis by A14, AOFA_000:def 35;

    end;

    theorem :: AOFA_I00:61

    for n,x,y,z,i be Variable of g st ex d be Function st (d . b) = 0 & (d . n) = 1 & (d . x) = 2 & (d . y) = 3 & (d . z) = 4 & (d . i) = 5 holds for s be Element of ( Funcs (X, INT )) holds for N be Element of NAT st N = (s . n) holds ((g . (s,(((x := 0 ) \; (y := 1)) \; ( for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))))) . x) = ( Fib N)

    proof



       A1: ( 0 qua Element of NAT + 1) = 1;

      set S = ( Funcs (X, INT ));

      let n,x,y,z,i be Variable of g;

      given d be Function such that

       A2: (d . b) = 0 and

       A3: (d . n) = 1 and

       A4: (d . x) = 2 and

       A5: (d . y) = 3 and

       A6: (d . z) = 4 and

       A7: (d . i) = 5;



       A8: n <> x by A3, A4;



       A9: y <> z by A5, A6;



       A10: x <> z by A4, A6;



       A11: i <> z by A6, A7;



       A12: n <> y by A3, A5;

      let s be Element of ( Funcs (X, INT ));

      reconsider s1 = (g . (s,(x := 0 ))) as Element of S;

      reconsider s2 = (g . (s1,(y := 1))) as Element of S;

      reconsider s4 = (g . (s2,(i := 1))) as Element of S;



       A13: (s4 . i) = 1 by Th25;



       A14: i <> y by A5, A7;

      then

       A15: (s4 . y) = (s2 . y) by Th25;

      set I = (((z := x) \; (x := y)) \; (y += z));



       A16: (s2 . y) = 1 by Th25;



       A17: i <> x by A4, A7;

      then

       A18: (s4 . x) = (s2 . x) by Th25;

      defpred P[ Element of S] means ex N be Element of NAT st N = (($1 . i) - 1) & ($1 . x) = ( Fib N) & ($1 . y) = ( Fib (N + 1));

      reconsider a = ( . (1,A,g)) as INT-Expression of A, g;



       A19: (s1 . x) = 0 by Th25;



       A20: x <> y by A4, A5;

      then (s2 . x) = (s1 . x) by Th25;

      then

       A21: P[(g . (s2,(i := a)))] by A19, A16, A15, A18, A13, A1, PRE_FF: 1;



       A22: n <> z by A3, A6;

       A23:

      now

        let s be Element of S;

        reconsider s1 = (g . (s,(z := x))) as Element of S;

        reconsider s2 = (g . (s1,(x := y))) as Element of S;

        reconsider s3 = (g . (s2,(y += z))) as Element of S;



         A24: (g . (s,I)) = (g . ((g . (s,((z := x) \; (x := y)))),(y += z))) by AOFA_000:def 29

        .= s3 by AOFA_000:def 29;



         A25: (s1 . z) = (s . x) by Th27;



         A26: (s2 . n) = (s1 . n) by A8, Th27;



         A27: (s1 . i) = (s . i) by A11, Th27;



         A28: (s2 . z) = (s1 . z) by A10, Th27;



         A29: (s2 . y) = (s1 . y) by A20, Th27;



         A30: (s2 . i) = (s1 . i) by A17, Th27;



         A31: (s1 . y) = (s . y) by A9, Th27;



         A32: (s2 . x) = (s1 . y) by Th27;

        (s1 . n) = (s . n) by A22, Th27;

        hence ((g . (s,I)) . i) = (s . i) & ((g . (s,I)) . n) = (s . n) & ((g . (s,I)) . x) = (s . y) & ((g . (s,I)) . y) = ((s . x) + (s . y)) by A12, A14, A20, A31, A25, A27, A26, A32, A29, A28, A30, A24, Th30;

      end;



       A33: for s be Element of ( Funcs (X, INT )) st P[s] holds P[(g . (s,(I \; (i += 1))))] & P[(g . (s,(i leq n)))]

      proof

        let s be Element of ( Funcs (X, INT ));

        given N be Element of NAT such that

         A34: N = ((s . i) - 1) and

         A35: (s . x) = ( Fib N) and

         A36: (s . y) = ( Fib (N + 1));

        reconsider s1 = (g . (s,I)) as Element of S;

        reconsider s2 = (g . (s1,(i += 1))) as Element of S;



         A37: (s1 . x) = (s . y) by A23;



         A38: (s2 . i) = ((s1 . i) + 1) by Th28;



         A39: (s1 . y) = ((s . x) + (s . y)) by A23;



         A40: (s2 . y) = (s1 . y) by A14, Th28;

        thus P[(g . (s,(I \; (i += 1)))) qua Element of S]

        proof

          take (N + 1);

          (g . (s,(I \; (i += 1)))) = s2 by AOFA_000:def 29;

          hence thesis by A17, A23, A34, A35, A36, A37, A39, A40, A38, Th28, PRE_FF: 1;

        end;

        take N;

        thus thesis by A2, A4, A5, A7, A34, A35, A36, Th35;

      end;

      reconsider F = ( for-do ((i := a),(i leq n),(i += 1),I)) as Element of A;

      reconsider s3 = (g . (s2,( for-do ((i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)))))) as Element of S;

      let N be Element of NAT ;

      assume

       A41: N = (s . n);



       A42: F = ( for-do ((i := a),(i leq n),(i += 1),I));

      (g . (s,((x := 0 ) \; (y := 1)))) = s2 by AOFA_000:def 29;

      then

       A43: (g . (s,(((x := 0 ) \; (y := 1)) \; F))) = s3 by AOFA_000:def 29;



       A44: 0 <= N & N <= 0 or N >= ( 0 qua Element of NAT + 1) by NAT_1: 13;



       A45: n <> i & n <> b & i <> b by A2, A3, A7;



       A47: for s be Element of ( Funcs (X, INT )) st P[s] holds ((g . (s,I)) . i) = (s . i) & ((g . (s,I)) . n) = (s . n) by A23;



       A48: P[(g . (s2,F))] & ((a . s2) <= (s2 . n) implies ((g . (s2,F)) . i) = ((s2 . n) + 1)) & ((a . s2) > (s2 . n) implies ((g . (s2,F)) . i) = (a . s2)) & ((g . (s2,F)) . n) = (s2 . n) from ForToIteration( A42, A21, A33, A47, A45);

      (s2 . n) = (s1 . n) by A12, Th25;

      hence thesis by A41, A43, A8, A48, A44, Th25;

    end;



     Lm1: for x,y,z be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . z) = 3 holds for s be Element of ( Funcs (X, INT )) holds ((g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x) = (s . y) & ((g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y) = ((s . x) mod (s . y)) & for n,m be Element of NAT st m = (s . y) & (s in (( Funcs (X, INT )) \ (b, 0 )) iff m > 0 ) holds g iteration_terminates_for ((((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )),s)

    proof

      set h = g;

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let x,y,z be Variable of h;

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . x) = 1 and

       A3: (d . y) = 2 and

       A4: (d . z) = 3;



       A5: z <> x by A2, A4;

      let s be Element of ( Funcs (X, INT ));

      set I = ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z));



       A6: y <> z by A3, A4;



       A7: x <> y by A2, A3;

       A8:

      now

        let s be Element of S;

        reconsider s1 = (h . (s,(z := x))) as Element of S;

        reconsider s2 = (h . (s1,(z %= y))) as Element of S;

        reconsider s3 = (h . (s2,(x := y))) as Element of S;

        reconsider s4 = (h . (s3,(y := z))) as Element of S;



         A9: (h . (s,I)) = (h . ((h . (s,(((z := x) \; (z %= y)) \; (x := y)))),(y := z))) by AOFA_000:def 29

        .= (h . ((h . ((h . (s,((z := x) \; (z %= y)))),(x := y))),(y := z))) by AOFA_000:def 29

        .= s4 by AOFA_000:def 29;



         A10: (s1 . z) = (s . x) by Th27;



         A11: (s2 . y) = (s1 . y) by A6, Th44;



         A12: (s2 . z) = ((s1 . z) mod (s1 . y)) by Th44;



         A13: (s3 . z) = (s2 . z) by A5, Th27;



         A14: (s3 . x) = (s2 . y) by Th27;

        (s1 . y) = (s . y) by A6, Th27;

        hence ((h . (s,I)) . x) = (s . y) & ((h . (s,I)) . y) = ((s . x) mod (s . y)) by A7, A9, A10, A11, A12, A14, A13, Th27;

      end;

      hence ((g . (s,I)) . x) = (s . y) & ((h . (s,I)) . y) = ((s . x) mod (s . y));

      deffunc F( Element of S) = ( In (($1 . y), NAT ));

      defpred R[ Element of S] means ($1 . y) > 0 ;

      set C = (y gt 0 );



       A15: for s be Element of S st R[s] holds ( R[(h . (s,(I \; C))) qua Element of S] iff (h . (s,(I \; C))) in T) & F() < F(s)

      proof

        let s be Element of S;

        assume

         A16: (s . y) > 0 ;

        reconsider s9 = (h . (s,I)) as Element of S;



         A17: (s9 . y) = ((s . x) mod (s . y)) by A8;

        then

         A18: 0 <= (s9 . y) by A16, NEWTON: 64;

        reconsider s99 = (h . (s9,C)) as Element of S;



         A19: (h . (s,(I \; C))) = s99 by AOFA_000:def 29;



         A20: (s9 . y) <= 0 implies (s99 . b) = 0 by Th38;

        (s9 . y) > 0 implies (s99 . b) = 1 by Th38;

        hence R[(h . (s,(I \; C))) qua Element of S] iff (h . (s,(I \; C))) in T by A19, A20, Th2, Th38;

        (s99 . y) = (s9 . y) by A1, A3, Th38;

        then

         A21: F(s99) = (s9 . y) by A18, INT_1: 3, SUBSET_1:def 8;



         A22: (s9 . y) < (s . y) by A16, A17, NEWTON: 65;

        then F(s) = (s . y) by A18, INT_1: 3, SUBSET_1:def 8;

        hence thesis by A22, A21, AOFA_000:def 29;

      end;

      let n,m be Element of NAT ;

      assume that

       A23: m = (s . y);

      assume s in T iff m > 0 ;

      then

       A24: s in T iff R[s] by A23;

      h iteration_terminates_for ((I \; C),s) from AOFA_000:sch 3( A24, A15);

      hence thesis;

    end;

    theorem :: AOFA_I00:62

    for x,y,z be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . z) = 3 holds ( while ((y gt 0 ),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) is_terminating_wrt (g,{ s : (s . x) > (s . y) & (s . y) >= 0 })

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let x,y,z be Variable of g;

      set P = { s : (s . x) > (s . y) & (s . y) >= 0 };

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . x) = 1 and

       A3: (d . y) = 2 and

       A4: (d . z) = 3;

      set C = (y gt 0 ), I = ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z));



       A5: P is_invariant_wrt (C,g)

      proof

        let s;

        set s1 = (g . (s,C));

        assume s in P;

        then

         A6: ex s9 st s9 = s & (s9 . x) > (s9 . y) & (s9 . y) >= 0 ;



         A7: (s1 . y) = (s . y) by A1, A3, Th38;

        (s1 . x) = (s . x) by A1, A2, Th38;

        hence thesis by A6, A7;

      end;

       A8:

      now

        let s;

        assume s in P;

        then ex s9 st s9 = s & (s9 . x) > (s9 . y) & (s9 . y) >= 0 ;

        then

        reconsider m = (s . y) as Element of NAT by INT_1: 3;

        assume (g . ((g . (s,I)),C)) in T;

        then ((g . ((g . (s,I)),C)) . b) <> 0 by Th2;

        then

         A9: ((g . (s,I)) . y) > 0 by Th38;



         A10: ((g . (s,I)) . x) = (s . y) by A1, A2, A3, A4, Lm1;



         A11: ((g . (s,I)) . y) = ((s . x) mod (s . y)) by A1, A2, A3, A4, Lm1;

        then m <> 0 by A9, INT_1:def 10;

        then ((g . (s,I)) . x) > ((g . (s,I)) . y) by A11, A10, NEWTON: 65;

        hence (g . (s,I)) in P by A9;

      end;

       A12:

      now

        let s;

        set s1 = (g . (s,C));



         A13: (s . y) <= 0 implies (s1 . b) = 0 by Th38;

        assume (g . (s,C)) in P;

        then ex s9 st s9 = (g . (s,C)) & (s9 . x) > (s9 . y) & (s9 . y) >= 0 ;

        then

        reconsider m = (s1 . y) as Element of NAT by INT_1: 3;

        (s . y) > 0 implies (s1 . b) = 1 by Th38;

        then s1 in T iff m > 0 by A13, Th2, Th38;

        hence g iteration_terminates_for ((I \; C),(g . (s,C))) by A1, A2, A3, A4, Lm1;

      end;

      C is_terminating_wrt g by AOFA_000: 104;

      hence thesis by A5, A8, A12, AOFA_000: 107, AOFA_000: 118;

    end;

    theorem :: AOFA_I00:63

    for x,y,z be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . z) = 3 holds for s be Element of ( Funcs (X, INT )) holds for n,m be Element of NAT st n = (s . x) & m = (s . y) & n > m holds ((g . (s,( while ((y gt 0 ),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x) = (n gcd m)

    proof

      set h = g;

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let x,y,z be Variable of h;

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . x) = 1 and

       A3: (d . y) = 2 and

       A4: (d . z) = 3;

      set C = (y gt 0 );

      set I = ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z));

      let s be Element of ( Funcs (X, INT ));

      reconsider fin = (h . (s,( while (C,I)))) as Element of S;

      defpred Q[ Element of S] means (fin . x) divides ($1 . x) & (fin . x) divides ($1 . y);



       A5: for s be Element of S st Q[(h . (s,C)) qua Element of S] holds Q[s] by A1, A2, A3, Th38;



       A6: for s be Element of S st Q[(h . ((h . (s,C)),I)) qua Element of S] & (h . (s,C)) in T holds Q[(h . (s,C)) qua Element of S]

      proof

        let s be Element of S;

        assume

         A7: Q[(h . ((h . (s,C)),I)) qua Element of S];

        reconsider s1 = (h . (s,C)) as Element of S;

        reconsider s2 = (h . (s1,I)) as Element of S;



         A8: (s . y) <= 0 implies (s1 . b) = 0 by Th38;



         A9: (s1 . x) = (s . x) by A1, A2, Th38;



         A10: (s2 . y) = ((s1 . x) mod (s1 . y)) by A1, A2, A3, A4, Lm1;



         A11: (s2 . x) = (s1 . y) by A1, A2, A3, A4, Lm1;



         A12: (s1 . y) = (s . y) by A1, A3, Th38;

        assume (h . (s,C)) in T;

        then (s . x) = ((((s . x) div (s . y)) * (s2 . x)) + ((s2 . y) * 1)) by A9, A12, A8, A11, A10, Th2, NEWTON: 66;

        hence thesis by A1, A2, A3, A4, A7, A9, Lm1, WSIERP_1: 5;

      end;

      reconsider s1 = (h . (s,C)) as Element of S;



       A13: (s1 . y) = (s . y) by A1, A3, Th38;



       A14: (s . y) <= 0 implies (s1 . b) = 0 by Th38;

      let n,m be Element of NAT ;

      defpred P[ Element of S] means (n gcd m) divides ($1 . x) & (n gcd m) divides ($1 . y) & ($1 . x) > ($1 . y) & ($1 . y) >= 0 ;

      defpred R[ Element of S] means ($1 . y) > 0 ;

      assume that

       A15: n = (s . x) and

       A16: m = (s . y) and

       A17: n > m;

      (s . y) > 0 implies (s1 . b) = 1 by Th38;

      then s1 in T iff m > 0 by A16, A14, Th2;

      then

       A18: h iteration_terminates_for ((I \; C),(h . (s,C))) by A1, A2, A3, A4, A16, A13, Lm1;



       A19: for s be Element of S st P[s] & s in T & R[s] holds P[(h . (s,I))]

      proof

        let s be Element of S;

        reconsider s99 = (h . (s,I)) as Element of S;

        assume

         A20: P[s];

        then

        reconsider n9 = (s . x), m9 = (s . y) as Element of NAT by INT_1: 3;

        assume that s in T and

         A21: R[s];



         A22: (s99 . x) = (s . y) by A1, A2, A3, A4, Lm1;



         A23: (s99 . y) = ((s . x) mod (s . y)) by A1, A2, A3, A4, Lm1;

        (n gcd m) divides (n9 mod m9) by A20, NAT_D: 11;

        hence thesis by A20, A21, A22, A23, NEWTON: 65;

      end;



       A24: for s be Element of S st P[s] holds P[(h . (s,C)) qua Element of S] & ((h . (s,C)) in T iff R[(h . (s,C)) qua Element of S])

      proof

        let s be Element of S;

        assume

         A25: P[s];

        reconsider s9 = (h . (s,C)) as Element of S;

        (s9 . y) = (s . y) by A1, A3, Th38;

        hence P[(h . (s,C)) qua Element of S] by A1, A2, A25, Th38;



         A26: (s . y) <= 0 implies (s9 . b) = 0 by Th38;

        (s . y) > 0 implies (s9 . b) = 1 by Th38;

        hence thesis by A26, Th2, Th38;

      end;



       A27: P[s] by A15, A16, A17, NAT_D:def 5;



       A28: P[(h . (s,( while (C,I)))) qua Element of S] & not R[(h . (s,( while (C,I)))) qua Element of S] from AOFA_000:sch 5( A27, A18, A19, A24);

      then (fin . y) = 0 ;

      then

       A29: Q[(h . (s,( while (C,I)))) qua Element of S] by INT_2: 12;

       Q[s] from AOFA_000:sch 6( A29, A18, A6, A5);

      then (fin . x) divides (n gcd m) by A15, A16, INT_2: 22;

      then (fin . x) = (n gcd m) or (fin . x) = ( - (n gcd m)) by A28, INT_2: 11;

      hence thesis by A28;

    end;



     Lm2: for x,y,z be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . z) = 3 holds for s be Element of ( Funcs (X, INT )) holds ((g . (s,((((z := (( . x) - ( . y))) \; ( if-then ((z lt 0 ),(z *= ( - 1))))) \; (x := y)) \; (y := z)))) . x) = (s . y) & ((g . (s,((((z := (( . x) - ( . y))) \; ( if-then ((z lt 0 ),(z *= ( - 1))))) \; (x := y)) \; (y := z)))) . y) = |.((s . x) - (s . y)).| & for n,m be Element of NAT st n = (s . x) & m = (s . y) & (s in (( Funcs (X, INT )) \ (b, 0 )) iff m > 0 ) holds g iteration_terminates_for ((((((z := (( . x) - ( . y))) \; ( if-then ((z lt 0 ),(z *= ( - 1))))) \; (x := y)) \; (y := z)) \; (y gt 0 )),s)

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let x,y,z be Variable of g;

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . x) = 1 and

       A3: (d . y) = 2 and

       A4: (d . z) = 3;



       A5: y <> z by A3, A4;

      let s be Element of ( Funcs (X, INT ));

      set J = ( if-then ((z lt 0 ),(z *= ( - 1))));



       A6: g complies_with_if_wrt T by AOFA_000:def 32;



       A7: z <> x by A2, A4;

      set I = ((((z := (( . x) - ( . y))) \; J) \; (x := y)) \; (y := z));



       A8: x <> y by A2, A3;

       A9:

      now

        let s be Element of S;

        set s1 = (g . (s,(z := (( . x) - ( . y)))));

        set s2 = (g . (s1,(z lt 0 )));

        set q = (g . (s1,J));

        set qz = (g . (s2,(z *= ( - 1))));



         A10: ((s2 . z) * ( - 1)) = ( - (s2 . z));

        set s3 = (g . (q,(x := y)));

        set s4 = (g . (s3,(y := z)));



         A11: (g . (s,I)) = (g . ((g . (s,(((z := (( . x) - ( . y))) \; J) \; (x := y)))),(y := z))) by AOFA_000:def 29

        .= (g . ((g . ((g . (s,((z := (( . x) - ( . y))) \; J))),(x := y))),(y := z))) by AOFA_000:def 29

        .= s4 by AOFA_000:def 29;

        (s2 . b) = 1 implies s2 in T;

        then

         A12: (s2 . b) = 1 implies q = qz by A6;



         A13: (( . x) . s) = (s . x) by Th22;



         A14: (qz . y) = (s2 . y) by A5, Th31;



         A15: (( . y) . s) = (s . y) by Th22;

        ((( . x) - ( . y)) . s) = ((( . x) . s) - (( . y) . s)) by Def11;

        then

         A16: (s1 . z) = ((s . x) - (s . y)) by A13, A15, Th26;



         A17: (s1 . z) < 0 implies (s2 . b) = 1 by Th38;



         A18: (s2 . z) = (s1 . z) by A1, A4, Th38;



         A19: (qz . z) = ((s2 . z) * ( - 1)) by Th31;



         A20: (s3 . z) = (q . z) by A7, Th27;



         A21: (s4 . y) = (s3 . z) by Th27;

        (s2 . b) = 0 implies s2 nin T by Th2;

        then

         A22: (s2 . b) = 0 implies q = s2 by A6, AOFA_000: 80;



         A23: (s1 . z) >= 0 implies (s2 . b) = 0 by Th38;



         A24: (s1 . y) = (s . y) by A5, Th26;



         A25: (s3 . x) = (q . y) by Th27;

        (s2 . y) = (s1 . y) by A1, A3, Th38;

        hence ((g . (s,I)) . x) = (s . y) & ((g . (s,I)) . y) = |.((s . x) - (s . y)).| by A8, A22, A12, A18, A17, A23, A14, A19, A10, A11, A24, A16, A25, A20, A21, Th27, ABSVALUE:def 1;

      end;

      hence ((g . (s,I)) . x) = (s . y) & ((g . (s,I)) . y) = |.((s . x) - (s . y)).|;

      deffunc F( Element of S) = ( IFEQ (($1 . y), 0 , 0 ,( IFEQ (($1 . x), 0 ,2,( IFEQ (($1 . x),($1 . y),1,( In (( max ((2 * ($1 . x)),((2 * ($1 . y)) + 1))), NAT ))))))));

      defpred R[ Element of S] means ($1 . x) >= 0 & ($1 . y) > 0 ;

      set C = (y gt 0 );



       A26: for s be Element of S st R[s] holds ( R[(g . (s,(I \; C))) qua Element of S] iff (g . (s,(I \; C))) in T) & F() < F(s)

      proof

        let s be Element of S;

        assume that

         A27: (s . x) >= 0 and

         A28: (s . y) > 0 ;

        reconsider s9 = (g . (s,I)) as Element of S;

        reconsider s99 = (g . (s9,C)) as Element of S;



         A29: (s9 . y) = |.((s . x) - (s . y)).| by A9;

        then

        reconsider nx = (s . x), ny = (s . y), nn = (s99 . y) as Element of NAT by A1, A3, A27, A28, Th38, INT_1: 3;



         A30: (g . (s,(I \; C))) = s99 by AOFA_000:def 29;



         A31: (s99 . x) = (s9 . x) by A1, A2, Th38;



         A32: (s9 . y) <= 0 implies (s99 . b) = 0 by Th38;



         A33: (s9 . y) > 0 implies (s99 . b) = 1 by Th38;

        hence R[(g . (s,(I \; C))) qua Element of S] iff (g . (s,(I \; C))) in T by A9, A28, A30, A31, A32, Th2, Th38;



         A34: (s9 . x) = (s . y) by A9;



         A35: F(s99) = ( IFEQ (nn, 0 , 0 ,( IFEQ (ny, 0 ,2,( IFEQ (ny,nn,1,( max ((2 * ny),((2 * nn) + 1))))))))) by A31, A34;

        ((2 * ny) + 1) > (2 * ny) by NAT_1: 13;

        then

         A36: ( max ((2 * nx),((2 * ny) + 1))) > (2 * ny) by XXREAL_0: 30;



         A37: (s99 . y) = (s9 . y) by A1, A3, Th38;



         A38: F(s) = ( IFEQ (ny, 0 , 0 ,( IFEQ (nx, 0 ,2,( IFEQ (nx,ny,1,( max ((2 * nx),((2 * ny) + 1)))))))))

        .= ( IFEQ (nx, 0 ,2,( IFEQ (nx,ny,1,( max ((2 * nx),((2 * ny) + 1))))))) by A28, FUNCOP_1:def 8;

        per cases by XXREAL_0: 1;

          suppose

           A39: nx = ny;

          then

           A40: ( IFEQ (nx,ny,1,( max ((2 * nx),((2 * ny) + 1))))) = 1 by FUNCOP_1:def 8;



           A41: nn = 0 by A37, A29, A39, ABSVALUE: 2;

           F(s) = ( IFEQ (nx,ny,1,( max ((2 * nx),((2 * ny) + 1))))) by A28, A38, A39, FUNCOP_1:def 8;

          hence thesis by A30, A40, A41, FUNCOP_1:def 8;

        end;

          suppose

           A42: nx > ny;

          then ( IFEQ (nx,ny,1,( max ((2 * nx),((2 * ny) + 1))))) = ( max ((2 * nx),((2 * ny) + 1))) by FUNCOP_1:def 8;

          then

           A43: F(s) = ( max ((2 * nx),((2 * ny) + 1))) by A38, A42, FUNCOP_1:def 8;



           A44: (nx - ny) > 0 by A42, XREAL_1: 50;



          then

           A45: F(s99) = ( IFEQ (ny, 0 ,2,( IFEQ (ny,nn,1,( max ((2 * ny),((2 * nn) + 1))))))) by A37, A33, A32, A29, A35, ABSVALUE:def 1, FUNCOP_1:def 8

          .= ( IFEQ (ny,nn,1,( max ((2 * ny),((2 * nn) + 1))))) by A28, FUNCOP_1:def 8;

          then

           A46: ny = nn implies F(s99) = 1 by FUNCOP_1:def 8;

          nn = (nx - ny) by A37, A29, A44, ABSVALUE:def 1;

          then nn < nx by A28, XREAL_1: 44;

          then (nn + 1) <= nx by NAT_1: 13;

          then

           A47: (2 * (nn + 1)) <= (2 * nx) by XREAL_1: 64;



           A48: 1 <= ((2 * nn) + 1) by NAT_1: 11;



           A49: ny <> nn implies F(s99) = ( max ((2 * ny),((2 * nn) + 1))) by A45, FUNCOP_1:def 8;

          ((2 * nn) + 2) = (((2 * nn) + 1) + 1);

          then ((2 * nn) + 1) < (2 * nx) by A47, NAT_1: 13;

          then ((2 * nn) + 1) < F(s) by A43, XXREAL_0: 30;

          hence thesis by A30, A36, A43, A46, A49, A48, XXREAL_0: 2, XXREAL_0: 29;

        end;

          suppose

           A50: nx < ny & nx > 0 ;



           A51: ( - (nx - ny)) = (ny - nx);



           A52: (nx - ny) < 0 by A50, XREAL_1: 49;

          then

           A53: nn = ( - (nx - ny)) by A37, A29, ABSVALUE:def 1;

          then

           A54: nn < ny by A50, A51, XREAL_1: 44;

          (2 * nn) < (2 * ny) by A50, A53, A51, XREAL_1: 44, XREAL_1: 68;

          then ((2 * nn) + 1) < ((2 * ny) + 1) by XREAL_1: 6;

          then

           A55: ((2 * nn) + 1) < ( max ((2 * nx),((2 * ny) + 1))) by XXREAL_0: 30;

          nn > 0 by A37, A29, A52, A51, ABSVALUE:def 1;



          then

           A56: F(s99) = ( IFEQ (ny, 0 ,2,( IFEQ (ny,nn,1,( max ((2 * ny),((2 * nn) + 1))))))) by A35, FUNCOP_1:def 8

          .= ( IFEQ (ny,nn,1,( max ((2 * ny),((2 * nn) + 1))))) by A28, FUNCOP_1:def 8

          .= ( max ((2 * ny),((2 * nn) + 1))) by A54, FUNCOP_1:def 8;

           F(s) = ( IFEQ (nx,ny,1,( max ((2 * nx),((2 * ny) + 1))))) by A38, A50, FUNCOP_1:def 8

          .= ( max ((2 * nx),((2 * ny) + 1))) by A50, FUNCOP_1:def 8;

          hence thesis by A30, A36, A55, A56, XXREAL_0: 29;

        end;

          suppose

           A57: nx = 0 ;

          then

           A58: F(s) = 2 by A38, FUNCOP_1:def 8;



           A59: nn = ( - (nx - ny)) by A28, A37, A29, A57, ABSVALUE:def 1

          .= ny by A57;



          then F(s99) = ( IFEQ (ny, 0 ,2,( IFEQ (ny,nn,1,( max ((2 * ny),((2 * nn) + 1))))))) by A28, A35, FUNCOP_1:def 8

          .= ( IFEQ (ny,nn,1,( max ((2 * ny),((2 * nn) + 1))))) by A28, FUNCOP_1:def 8

          .= 1 by A59, FUNCOP_1:def 8;

          hence thesis by A30, A58;

        end;

      end;

      let n,m be Element of NAT ;

      assume that

       A60: n = (s . x) and

       A61: m = (s . y);

      assume s in T iff m > 0 ;

      then

       A62: s in T iff R[s] by A60, A61;

      g iteration_terminates_for ((I \; C),s) from AOFA_000:sch 3( A62, A26);

      hence thesis;

    end;

    theorem :: AOFA_I00:64

    for x,y,z be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . z) = 3 holds ( while ((y gt 0 ),((((z := (( . x) - ( . y))) \; ( if-then ((z lt 0 ),(z *= ( - 1))))) \; (x := y)) \; (y := z)))) is_terminating_wrt (g,{ s : (s . x) >= 0 & (s . y) >= 0 })

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let x,y,z be Variable of g;

      set P = { s : (s . x) >= 0 & (s . y) >= 0 };

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . x) = 1 and

       A3: (d . y) = 2 and

       A4: (d . z) = 3;

      set C = (y gt 0 ), I = ((((z := (( . x) - ( . y))) \; ( if-then ((z lt 0 ),(z *= ( - 1))))) \; (x := y)) \; (y := z));

       A5:

      now

        let s;

        assume s in P;

        then ex s9 st s9 = s & (s9 . x) >= 0 & (s9 . y) >= 0 ;

        then

        reconsider m = (s . y) as Element of NAT by INT_1: 3;

        assume (g . ((g . (s,I)),C)) in T;



         A6: ((g . (s,I)) . x) = m by A1, A2, A3, A4, Lm2;

        ((g . (s,I)) . y) = |.((s . x) - (s . y)).| by A1, A2, A3, A4, Lm2;

        hence (g . (s,I)) in P by A6;

      end;

       A7:

      now

        let s;

        set s1 = (g . (s,C));



         A8: (s . y) <= 0 implies (s1 . b) = 0 by Th38;

        assume (g . (s,C)) in P;

        then ex s9 st s9 = (g . (s,C)) & (s9 . x) >= 0 & (s9 . y) >= 0 ;

        then

        reconsider n = (s1 . x), m = (s1 . y) as Element of NAT by INT_1: 3;



         A9: n = n;

        (s . y) > 0 implies (s1 . b) = 1 by Th38;

        then s1 in T iff m > 0 by A8, Th2, Th38;

        hence g iteration_terminates_for ((I \; C),(g . (s,C))) by A1, A2, A3, A4, A9, Lm2;

      end;



       A10: P is_invariant_wrt (C,g)

      proof

        let s;

        set s1 = (g . (s,C));

        assume s in P;

        then

         A11: ex s9 st s9 = s & (s9 . x) >= 0 & (s9 . y) >= 0 ;



         A12: (s1 . y) = (s . y) by A1, A3, Th38;

        (s1 . x) = (s . x) by A1, A2, Th38;

        hence thesis by A11, A12;

      end;

      C is_terminating_wrt g by AOFA_000: 104;

      hence thesis by A10, A5, A7, AOFA_000: 107, AOFA_000: 118;

    end;

    theorem :: AOFA_I00:65

    for x,y,z be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . z) = 3 holds for s be Element of ( Funcs (X, INT )) holds for n,m be Element of NAT st n = (s . x) & m = (s . y) & n > 0 holds ((g . (s,( while ((y gt 0 ),((((z := (( . x) - ( . y))) \; ( if-then ((z lt 0 ),(z *= ( - 1))))) \; (x := y)) \; (y := z)))))) . x) = (n gcd m)

    proof

      set h = g;

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));



       A1: h complies_with_if_wrt T by AOFA_000:def 32;

      let x,y,z be Variable of h;

      given d be Function such that

       A2: (d . b) = 0 and

       A3: (d . x) = 1 and

       A4: (d . y) = 2 and

       A5: (d . z) = 3;

      set C = (y gt 0 );

      let s be Element of ( Funcs (X, INT ));



       A6: y <> z by A4, A5;

      reconsider s1 = (h . (s,C)) as Element of S;



       A7: (s1 . x) = (s . x) by A2, A3, Th38;



       A8: (s1 . y) = (s . y) by A2, A4, Th38;



       A9: (s . y) <= 0 implies (s1 . b) = 0 by Th38;

      defpred R[ Element of S] means ($1 . x) > 0 & ($1 . y) > 0 ;

      let n,m be Element of NAT ;

      defpred P[ Element of S] means (n gcd m) divides ($1 . x) & (n gcd m) divides ($1 . y) & ($1 . x) > 0 & ($1 . y) >= 0 & for c be Nat st c divides ($1 . x) & c divides ($1 . y) holds c divides (n gcd m);

      set J = ( if-then ((z lt 0 ),(z *= ( - 1))));

      set I = ((((z := (( . x) - ( . y))) \; J) \; (x := y)) \; (y := z));

      assume that

       A10: n = (s . x) and

       A11: m = (s . y) and

       A12: n > 0 ;

      (s . y) > 0 implies (s1 . b) = 1 by Th38;

      then s1 in T iff R[s1] by A10, A12, A9, Th2, Th38;

      then

       A13: h iteration_terminates_for ((I \; C),(h . (s,C))) by A2, A3, A4, A5, A10, A11, A12, A7, A8, Lm2;



       A14: z <> x by A3, A5;



       A15: x <> y by A3, A4;

       A16:

      now

        let s be Element of S;

        set s1 = (h . (s,(z := (( . x) - ( . y)))));

        set s2 = (h . (s1,(z lt 0 )));

        set q = (h . (s1,J));

        set qz = (h . (s2,(z *= ( - 1))));



         A17: ((s2 . z) * ( - 1)) = ( - (s2 . z));

        set s3 = (h . (q,(x := y)));

        set s4 = (h . (s3,(y := z)));



         A18: (h . (s,I)) = (h . ((h . (s,(((z := (( . x) - ( . y))) \; J) \; (x := y)))),(y := z))) by AOFA_000:def 29

        .= (h . ((h . ((h . (s,((z := (( . x) - ( . y))) \; J))),(x := y))),(y := z))) by AOFA_000:def 29

        .= s4 by AOFA_000:def 29;

        (s2 . b) = 1 implies s2 in T;

        then

         A19: (s2 . b) = 1 implies q = qz by A1;



         A20: (( . x) . s) = (s . x) by Th22;



         A21: (qz . y) = (s2 . y) by A6, Th31;



         A22: (( . y) . s) = (s . y) by Th22;

        ((( . x) - ( . y)) . s) = ((( . x) . s) - (( . y) . s)) by Def11;

        then

         A23: (s1 . z) = ((s . x) - (s . y)) by A20, A22, Th26;



         A24: (s1 . z) < 0 implies (s2 . b) = 1 by Th38;



         A25: (s2 . z) = (s1 . z) by A2, A5, Th38;



         A26: (qz . z) = ((s2 . z) * ( - 1)) by Th31;



         A27: (s3 . z) = (q . z) by A14, Th27;



         A28: (s4 . y) = (s3 . z) by Th27;

        (s2 . b) = 0 implies s2 nin T by Th2;

        then

         A29: (s2 . b) = 0 implies q = s2 by A1, AOFA_000: 80;



         A30: (s1 . z) >= 0 implies (s2 . b) = 0 by Th38;



         A31: (s1 . y) = (s . y) by A6, Th26;



         A32: (s3 . x) = (q . y) by Th27;

        (s2 . y) = (s1 . y) by A2, A4, Th38;

        hence ((h . (s,I)) . x) = (s . y) & ((h . (s,I)) . y) = |.((s . x) - (s . y)).| by A15, A29, A19, A25, A24, A30, A21, A26, A17, A18, A31, A23, A32, A27, A28, Th27, ABSVALUE:def 1;

      end;



       A33: for s be Element of S st P[s] & s in T & R[s] holds P[(h . (s,I))]

      proof

        let s be Element of S;

        reconsider s99 = (h . (s,I)) as Element of S;



         A34: |.(n gcd m).| = (n gcd m) by ABSVALUE:def 1;



         A35: (s99 . y) = |.((s . x) - (s . y)).| by A16;

        assume

         A36: P[s];

        then

        reconsider n9 = (s . x), m9 = (s . y) as Element of NAT by INT_1: 3;

        assume that s in T and

         A37: R[s];

        (n gcd m) divides (n9 - m9) by A36, PREPOWER: 94;

        hence (n gcd m) divides ((h . (s,I)) . x) & (n gcd m) divides ((h . (s,I)) . y) & ((h . (s,I)) . x) > 0 & ((h . (s,I)) . y) >= 0 by A16, A36, A37, A35, A34, INT_2: 16;

        let c be Nat;

        reconsider c9 = c as Element of NAT by ORDINAL1:def 12;

        assume that

         A38: c divides ((h . (s,I)) . x) and

         A39: c divides ((h . (s,I)) . y);



         A40: |.c.| = c by ABSVALUE:def 1;



         A41: (s99 . x) = (s . y) by A16;

        c9 divides |.(n9 - m9).| by A16, A39;

        then

         A42: c divides (n9 - m9) by A40, INT_2: 16;

        c qua Integer divides m9 by A16, A38;

        then c divides ((n9 - m9) + m9) by A42, WSIERP_1: 4;

        hence thesis by A36, A41, A38;

      end;



       A43: for s be Element of S st P[s] holds P[(h . (s,C)) qua Element of S] & ((h . (s,C)) in T iff R[(h . (s,C)) qua Element of S])

      proof

        let s be Element of S;

        assume

         A44: P[s];

        reconsider s9 = (h . (s,C)) as Element of S;



         A45: (s9 . y) = (s . y) by A2, A4, Th38;

        (s9 . x) = (s . x) by A2, A3, Th38;

        hence P[(h . (s,C)) qua Element of S] by A44, A45;



         A46: (s . y) <= 0 implies (s9 . b) = 0 by Th38;

        (s . y) > 0 implies (s9 . b) = 1 by Th38;

        hence thesis by A44, A46, Th2, Th38;

      end;

      reconsider fin = (h . (s,( while (C,I)))) as Element of S;



       A47: P[s] by A10, A11, A12, NAT_D:def 5;



       A48: P[(h . (s,( while (C,I)))) qua Element of S] & not R[(h . (s,( while (C,I)))) qua Element of S] from AOFA_000:sch 5( A47, A13, A33, A43);

      then

      reconsider fn = (fin . x) as Element of NAT by INT_1: 3;



       A49: fn divides 0 by NAT_D: 6;

      (fin . y) = 0 by A48;

      then fn divides (n gcd m) by A48, A49;

      hence thesis by A48, NAT_D: 5;

    end;

    theorem :: AOFA_I00:66

    for x,y,m be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . m) = 3 holds ((y := 1) \; ( while ((m gt 0 ),((( if-then ((m is_odd ),(y *= x))) \; (m /= 2)) \; (x *= x))))) is_terminating_wrt (g,{ s : (s . m) >= 0 })

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));

      let x,y,m be Variable of g;

      set P = { s : (s . m) >= 0 };

      given d be Function such that

       A1: (d . b) = 0 and

       A2: (d . x) = 1 and

       A3: (d . y) = 2 and

       A4: (d . m) = 3;

      set C = (m gt 0 );



       A5: (y := 1) is_terminating_wrt (g,P) by AOFA_000: 107;

      deffunc F( Element of S) = ( In (($1 . m), NAT ));

      defpred R[ Element of S] means ($1 . m) > 0 ;

      set I = ( if-then ((m is_odd ),(y *= x)));

      set J = ((I \; (m /= 2)) \; (x *= x));



       A6: g complies_with_if_wrt T by AOFA_000:def 32;



       A7: P is_invariant_wrt (C,g)

      proof

        let s;

        assume s in P;

        then

         A8: ex s9 st s = s9 & (s9 . m) >= 0 ;

        ((g . (s,C)) . m) = (s . m) by A1, A4, Th38;

        hence (g . (s,C)) in P by A8;

      end;



       A9: for s st s in P & (g . ((g . (s,J)),C)) in T holds (g . (s,J)) in P

      proof

        let s such that s in P;

        assume (g . ((g . (s,J)),C)) in T;

        then ((g . (s,J)) . m) > 0 by Th40;

        hence thesis;

      end;



       A10: m <> y by A3, A4;



       A11: P is_invariant_wrt ((y := 1),g)

      proof

        let s;

        assume s in P;

        then

         A12: ex s9 st s = s9 & (s9 . m) >= 0 ;

        ((g . (s,(y := 1))) . m) = (s . m) by A10, Th25;

        hence (g . (s,(y := 1))) in P by A12;

      end;



       A13: m <> x by A2, A4;



       A14: for s st (g . (s,C)) in P holds g iteration_terminates_for ((J \; C),(g . (s,C)))

      proof



         A15: for s be Element of S st R[s] holds ( R[(g . (s,(J \; C)))] iff (g . (s,(J \; C))) in T) & F(.) < F(s)

        proof

          let s be Element of S such that

           A16: (s . m) > 0 ;



           A17: F(s) = (s . m) by A16, INT_1: 3, SUBSET_1:def 8;

          set q1 = (g . (s,I));

          set q0 = (g . (s,(m is_odd )));

          set sJ = (g . (s,J));

          set sC = (g . (sJ,C));



           A18: (g . (s,(J \; C))) = sC by AOFA_000:def 29;



           A19: (sJ . m) <= 0 implies (sC . b) = 0 by Th38;

          (sJ . m) > 0 implies (sC . b) = 1 by Th38;

          hence R[(g . (s,(J \; C)))] iff (g . (s,(J \; C))) in T by A19, A18, Th2, Th38;

          set q2 = (g . (q1,(m /= 2)));

          set q3 = (g . (q2,(x *= x)));



           A20: q1 = (g . (q0,(y *= x))) or q1 = (g . (q0,( EmptyIns A))) by A6;

          q2 = (g . (s,(I \; (m /= 2)))) by AOFA_000:def 29;

          then q3 = (g . (s,J)) by AOFA_000:def 29;



          then

           A21: (sJ . m) = (q2 . m) by A13, Th33

          .= ((q1 . m) div 2) by Th45

          .= ((q0 . m) div 2) by A10, A20, Th33, AOFA_000:def 28

          .= ((s . m) div 2) by A1, A4, Th49;



           A22: (sC . m) = (sJ . m) by A1, A4, Th38;

          then (sC . m) in NAT by A16, A21, INT_1: 3, INT_1: 61;

          then F(sC) = (sC . m) by SUBSET_1:def 8;

          hence thesis by A16, A22, A18, A21, A17, INT_1: 56;

        end;

        let s0 be Element of S such that (g . (s0,C)) in P;

        set s1 = (g . (s0,C));



         A23: (s0 . m) <= 0 implies (s1 . b) = 0 by Th38;

        (s0 . m) > 0 implies (s1 . b) = 1 by Th38;

        then

         A24: (g . (s0,C)) in T iff R[(g . (s0,C))] by A23, Th2, Th38;

        thus g iteration_terminates_for ((J \; C),(g . (s0,C))) from AOFA_000:sch 3( A24, A15);

      end;

      J is_terminating_wrt (g,P) by AOFA_000: 107;

      then ( while ((m gt 0 ),((( if-then ((m is_odd ),(y *= x))) \; (m /= 2)) \; (x *= x)))) is_terminating_wrt (g,P) by A7, A9, A14, AOFA_000: 104, AOFA_000: 118;

      hence thesis by A5, A11, AOFA_000: 111;

    end;

    ::$Notion-Name

    theorem :: AOFA_I00:67

    for x,y,m be Variable of g st ex d be Function st (d . b) = 0 & (d . x) = 1 & (d . y) = 2 & (d . m) = 3 holds for s be Element of ( Funcs (X, INT )) holds for n be Nat st n = (s . m) holds ((g . (s,((y := 1) \; ( while ((m gt 0 ),((( if-then ((m is_odd ),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y) = ((s . x) |^ n)

    proof

      set S = ( Funcs (X, INT ));

      set T = (S \ (b, 0 ));



       A1: g complies_with_if_wrt T by AOFA_000:def 32;

      let x,y,m be Variable of g;

      given d be Function such that

       A2: (d . b) = 0 and

       A3: (d . x) = 1 and

       A4: (d . y) = 2 and

       A5: (d . m) = 3;

      defpred R[ Element of S] means ($1 . m) > 0 ;

      set C = (m gt 0 );

      let s be Element of ( Funcs (X, INT ));

      let n be Nat;

      defpred P[ Element of S] means ((s . x) |^ n) = (($1 . y) * (($1 . x) to_power ($1 . m))) & ($1 . m) >= 0 ;

      deffunc F( Element of S) = ( In (($1 . m), NAT ));

      set I = ( if-then ((m is_odd ),(y *= x)));

      set J = ((I \; (m /= 2)) \; (x *= x));

      set s0 = (g . (s,(y := 1)));



       A6: m <> y by A4, A5;

      then

       A7: (s0 . m) = (s . m) by Th25;



       A8: for s be Element of S st P[s] holds P[(g . (s,C))] & ((g . (s,C)) in T iff R[(g . (s,C))])

      proof

        let s be Element of S such that

         A9: P[s];

        set s1 = (g . (s,C));



         A10: (s1 . x) = (s . x) by A2, A3, Th38;

        (s1 . m) = (s . m) by A2, A5, Th38;

        hence P[(g . (s,C))] by A2, A4, A9, A10, Th38;



         A11: (s . m) <= 0 implies (s1 . b) = 0 by Th38;

        (s . m) > 0 implies (s1 . b) = 1 by Th38;

        hence thesis by A11, Th2, Th38;

      end;



       A12: (s0 . y) = 1 by Th25;

      set fs = (g . (s0,( while (C,J))));

      set s1 = (g . (s0,C));

      assume

       A13: n = (s . m);



       A14: ((fs . x) to_power 0 ) = 1 by POWER: 24;



       A15: m <> x by A3, A5;



       A16: for s be Element of S st R[s] holds ( R[(g . (s,(J \; C)))] iff (g . (s,(J \; C))) in T) & F(.) < F(s)

      proof

        let s be Element of S such that

         A17: (s . m) > 0 ;



         A18: F(s) = (s . m) by A17, INT_1: 3, SUBSET_1:def 8;

        set q1 = (g . (s,I));

        set q0 = (g . (s,(m is_odd )));

        set sJ = (g . (s,J));

        set sC = (g . (sJ,C));



         A19: (g . (s,(J \; C))) = sC by AOFA_000:def 29;



         A20: (sJ . m) <= 0 implies (sC . b) = 0 by Th38;

        (sJ . m) > 0 implies (sC . b) = 1 by Th38;

        hence R[(g . (s,(J \; C)))] iff (g . (s,(J \; C))) in T by A20, A19, Th2, Th38;

        set q2 = (g . (q1,(m /= 2)));

        set q3 = (g . (q2,(x *= x)));



         A21: q1 = (g . (q0,(y *= x))) or q1 = (g . (q0,( EmptyIns A))) by A1;

        q2 = (g . (s,(I \; (m /= 2)))) by AOFA_000:def 29;

        then q3 = (g . (s,J)) by AOFA_000:def 29;



        then

         A22: (sJ . m) = (q2 . m) by A15, Th33

        .= ((q1 . m) div 2) by Th45

        .= ((q0 . m) div 2) by A6, A21, Th33, AOFA_000:def 28

        .= ((s . m) div 2) by A2, A5, Th49;



         A23: (sC . m) = (sJ . m) by A2, A5, Th38;

        then (sC . m) in NAT by A17, A22, INT_1: 3, INT_1: 61;

        then F(sC) = (sC . m) by SUBSET_1:def 8;

        hence thesis by A17, A23, A19, A22, A18, INT_1: 56;

      end;

      set q = s;



       A24: x <> y by A3, A4;



       A25: for s be Element of S st P[s] & s in T & R[s] holds P[(g . (s,J))]

      proof

        let s be Element of S such that

         A26: P[s] and s in T and R[s];

        reconsider sm = (s . m) as Element of NAT by A26, INT_1: 3;

        (s . m) = ((((s . m) div 2) * 2) + ((s . m) mod 2)) by NEWTON: 66;



        then

         A27: ((q . x) |^ n) = ((s . y) * (((s . x) to_power ((sm div 2) * 2)) * ((s . x) to_power (sm mod 2)))) by A26, FIB_NUM2: 5

        .= (((s . y) * ((s . x) to_power (sm mod 2))) * ((s . x) to_power ((sm div 2) * 2)))

        .= (((s . y) * ((s . x) to_power (sm mod 2))) * (((s . x) to_power 2) to_power (sm div 2))) by NEWTON: 9

        .= (((s . y) * ((s . x) to_power (sm mod 2))) * (((s . x) * (s . x)) to_power (sm div 2))) by NEWTON: 81;

        set q1 = (g . (s,I));

        set q0 = (g . (s,(m is_odd )));

        set sJ = (g . (s,J));

        set q2 = (g . (q1,(m /= 2)));

        set q3 = (g . (q2,(x *= x)));



         A28: q1 = (g . (q0,(y *= x))) or q1 = (g . (q0,( EmptyIns A))) by A1;



         A29: (q2 . x) = (q1 . x) by A15, Th45

        .= (q0 . x) by A24, A28, Th33, AOFA_000:def 28;



         A30: (q2 . y) = (q1 . y) by A6, Th45;



         A31: (q0 . y) = (s . y) by A2, A4, Th49;



         A32: (q0 . x) = (s . x) by A2, A3, Th49;

        q2 = (g . (s,(I \; (m /= 2)))) by AOFA_000:def 29;

        then

         A33: q3 = (g . (s,J)) by AOFA_000:def 29;

        then

         A34: (sJ . y) = (q2 . y) by A24, Th33;



         A35: (sm div 2) = ((s . m) div 2);

         A36:

        now



           A37: (q0 . b) = ((s . m) mod 2) by Th49;

          per cases by A35, A37, NAT_D: 12;

            suppose

             A38: (q0 . b) = 0 ;

            then q0 nin T by Th2;

            then q1 = (g . (q0,( EmptyIns A))) by A1;

            then

             A39: (q1 . y) = (q0 . y) by AOFA_000:def 28;



             A40: ((s . y) * 1) = (s . y);

            ((s . x) to_power 0 ) = 1 by POWER: 24;

            hence ((s . y) * ((s . x) to_power (sm mod 2))) = (sJ . y) by A34, A30, A31, A38, A39, A40, Th49;

          end;

            suppose

             A41: (q0 . b) = 1;

            then q0 in T;

            then q1 = (g . (q0,(y *= x))) by A1;

            then

             A42: (q1 . y) = ((q0 . y) * (q0 . x)) by Th33;

            ((s . x) to_power 1) = (s . x) by POWER: 25;

            hence ((s . y) * ((s . x) to_power (sm mod 2))) = (sJ . y) by A32, A34, A30, A31, A41, A42, Th49;

          end;

        end;

        (sJ . m) = (q2 . m) by A15, A33, Th33

        .= ((q1 . m) div 2) by Th45

        .= ((q0 . m) div 2) by A6, A28, Th33, AOFA_000:def 28

        .= ((s . m) div 2) by A2, A5, Th49;

        hence thesis by A33, A29, A32, A36, A27, Th33;

      end;



       A43: (s0 . m) <= 0 implies (s1 . b) = 0 by Th38;

      (s0 . m) > 0 implies (s1 . b) = 1 by Th38;

      then

       A44: (g . (s0,C)) in T iff R[(g . (s0,C))] by A43, Th2, Th38;



       A45: g iteration_terminates_for ((J \; C),(g . (s0,C))) from AOFA_000:sch 3( A44, A16);

      (s0 . x) = (s . x) by A24, Th25;

      then

       A46: P[s0] by A13, A7, A12, POWER: 41;



       A47: P[(g . (s0,( while (C,J))))] & not R[(g . (s0,( while (C,J))))] from AOFA_000:sch 5( A46, A45, A25, A8);

      then (fs . m) = 0 ;

      hence thesis by A47, A14, AOFA_000:def 29;

    end;