:: by Grzegorz Bancerek

::

:: Received November 9, 2012

:: Copyright (c) 2012-2019 Association of Mizar Users

theorem Th2: :: AOFA_A01:2

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for B being MSSubAlgebra of A

for s being SortSymbol of S

for a being set st a in the Sorts of B . s holds

a in the Sorts of A . s

for A being MSAlgebra over S

for B being MSSubAlgebra of A

for s being SortSymbol of S

for a being set st a in the Sorts of B . s holds

a in the Sorts of A . s

proof end;

theorem Th3: :: AOFA_A01:3

for I being non empty set

for a, b, c being set

for i being Element of I holds

( c in (i -singleton a) . b iff ( b = i & c = a ) )

for a, b, c being set

for i being Element of I holds

( c in (i -singleton a) . b iff ( b = i & c = a ) )

proof end;

theorem Th4: :: AOFA_A01:4

for I being non empty set

for a, b, c, d being set

for i, j being Element of I holds

( c in ((i -singleton a) (\/) (j -singleton d)) . b iff ( ( b = i & c = a ) or ( b = j & c = d ) ) )

for a, b, c, d being set

for i, j being Element of I holds

( c in ((i -singleton a) (\/) (j -singleton d)) . b iff ( ( b = i & c = a ) or ( b = j & c = d ) ) )

proof end;

definition

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let A be non-empty MSAlgebra over S;

end;
let A be non-empty MSAlgebra over S;

attr A is integer means :Def1: :: AOFA_A01:def 1

ex C being image of A st C is bool-correct 4,1 integer MSAlgebra over S;

ex C being image of A st C is bool-correct 4,1 integer MSAlgebra over S;

:: deftheorem Def1 defines integer AOFA_A01:def 1 :

for S being non empty non void bool-correct 4,1 integer BoolSignature

for A being non-empty MSAlgebra over S holds

( A is integer iff ex C being image of A st C is bool-correct 4,1 integer MSAlgebra over S );

for S being non empty non void bool-correct 4,1 integer BoolSignature

for A being non-empty MSAlgebra over S holds

( A is integer iff ex C being image of A st C is bool-correct 4,1 integer MSAlgebra over S );

theorem Th5: :: AOFA_A01:5

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S holds Image (id the Sorts of A) = MSAlgebra(# the Sorts of A, the Charact of A #)

for A being non-empty MSAlgebra over S holds Image (id the Sorts of A) = MSAlgebra(# the Sorts of A, the Charact of A #)

proof end;

theorem Th6: :: AOFA_A01:6

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S holds A is image of A

for A being non-empty MSAlgebra over S holds A is image of A

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

existence

ex b_{1} being non-empty MSAlgebra over S st b_{1} is integer

end;
existence

ex b

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let A be non-empty integer MSAlgebra over S;

existence

ex b_{1} being image of A st b_{1} is bool-correct

end;
let A be non-empty integer MSAlgebra over S;

existence

ex b

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let A be non-empty integer MSAlgebra over S;

ex b_{1} being bool-correct image of A st b_{1} is 4,1 integer

end;
let A be non-empty integer MSAlgebra over S;

cluster non-empty A -Image Equations (S,A) -satisfying bool-correct 4,1 integer for MSAlgebra over S;

existence ex b

proof end;

theorem Th7: :: AOFA_A01:7

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for o being OperSymbol of S

for a being set

for r being SortSymbol of S st o is_of_type a,r holds

( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )

for A being non-empty MSAlgebra over S

for o being OperSymbol of S

for a being set

for r being SortSymbol of S st o is_of_type a,r holds

( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )

proof end;

registration

let S be non empty non void bool-correct BoolSignature ;

let A be non-empty bool-correct MSAlgebra over S;

coherence

for b_{1} being non-empty MSSubAlgebra of A holds b_{1} is bool-correct

end;
let A be non-empty bool-correct MSAlgebra over S;

coherence

for b

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let A be non-empty bool-correct 4,1 integer MSAlgebra over S;

coherence

for b_{1} being non-empty MSSubAlgebra of A holds b_{1} is 4,1 integer

end;
let A be non-empty bool-correct 4,1 integer MSAlgebra over S;

coherence

for b

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

coherence

for b_{1} being non-empty MSAlgebra over S st b_{1} = Free (S,X) holds

b_{1} is integer

end;
let X be V3() ManySortedSet of the carrier of S;

coherence

for b

b

proof end;

theorem Th8: :: AOFA_A01:8

for S being non empty non void ManySortedSign

for A1, A2, B1 being MSAlgebra over S

for B2 being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds

for h1 being ManySortedFunction of A1,B1

for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_epimorphism A1,B1 holds

h2 is_epimorphism A2,B2 by MSAFREE4:30;

for A1, A2, B1 being MSAlgebra over S

for B2 being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds

for h1 being ManySortedFunction of A1,B1

for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_epimorphism A1,B1 holds

h2 is_epimorphism A2,B2 by MSAFREE4:30;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

ex b_{1} being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( b_{1} is vf-free & b_{1} is integer )

end;
let X be V3() ManySortedSet of the carrier of S;

cluster non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free disjoint_valued integer for VarMSAlgebra over S;

existence ex b

( b

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

coherence

FreeGen X is V3() GeneratorSet of T by MSAFREE4:45;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

coherence

FreeGen X is V3() GeneratorSet of T by MSAFREE4:45;

:: deftheorem defines FreeGen AOFA_A01:def 2 :

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen T = FreeGen X;

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b

registration

let S be non empty non void ManySortedSign ;

let X0 be V3() countable ManySortedSet of the carrier of S;

let T be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

coherence

( FreeGen T is Equations (S,T) -free & FreeGen T is non-empty ) by MSAFREE4:75;

end;
let X0 be V3() countable ManySortedSet of the carrier of S;

let T be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

coherence

( FreeGen T is Equations (S,T) -free & FreeGen T is non-empty ) by MSAFREE4:75;

definition

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

let G be GeneratorSet of T;

let s be SortSymbol of S;

let x be Element of G . s;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

let G be GeneratorSet of T;

let s be SortSymbol of S;

let x be Element of G . s;

:: deftheorem Def3 defines basic AOFA_A01:def 3 :

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations MSAlgebra over S

for G being GeneratorSet of T holds

( G is basic iff FreeGen T c= G );

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being GeneratorSet of T holds

( G is basic iff FreeGen T c= G );

:: deftheorem Def4 defines pure AOFA_A01:def 4 :

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations MSAlgebra over S

for G being GeneratorSet of T

for s being SortSymbol of S

for x being Element of G . s holds

( x is pure iff x in (FreeGen T) . s );

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being GeneratorSet of T

for s being SortSymbol of S

for x being Element of G . s holds

( x is pure iff x in (FreeGen T) . s );

registration

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

coherence

FreeGen T is basic ;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

coherence

FreeGen T is basic ;

registration

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

ex b_{1} being V3() GeneratorSet of T st b_{1} is basic

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

cluster non empty Relation-like V3() non empty-yielding the carrier of S -defined Function-like total basic for GeneratorSet of T;

existence ex b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

let G be basic GeneratorSet of T;

let s be SortSymbol of S;

existence

ex b_{1} being Element of G . s st b_{1} is pure

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S;

let G be basic GeneratorSet of T;

let s be SortSymbol of S;

existence

ex b

proof end;

theorem :: AOFA_A01:9

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations MSAlgebra over S

for G being basic GeneratorSet of T

for s being SortSymbol of S

for a being set holds

( a is pure Element of G . s iff a in (FreeGen T) . s )

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being basic GeneratorSet of T

for s being SortSymbol of S

for a being set holds

( a is pure Element of G . s iff a in (FreeGen T) . s )

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let G be GeneratorSystem over S,X,T;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let G be GeneratorSystem over S,X,T;

:: deftheorem Def5 defines basic AOFA_A01:def 5 :

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for G being GeneratorSystem over S,X,T holds

( G is basic iff the generators of G is basic );

for S being non empty non void ManySortedSign

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being GeneratorSystem over S,X,T holds

( G is basic iff the generators of G is basic );

registration

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

existence

ex b_{1} being GeneratorSystem over S,X,T st b_{1} is basic

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

existence

ex b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

coherence

the generators of G is basic by Def5;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

coherence

the generators of G is basic by Def5;

definition

let S be non empty non void bool-correct BoolSignature ;

let A be non-empty MSAlgebra over S;

coherence

\not (\true A) is Element of A, the bool-sort of S ;

end;
let A be non-empty MSAlgebra over S;

coherence

\not (\true A) is Element of A, the bool-sort of S ;

:: deftheorem defines \false AOFA_A01:def 6 :

for S being non empty non void bool-correct BoolSignature

for A being non-empty MSAlgebra over S holds \false A = \not (\true A);

for S being non empty non void bool-correct BoolSignature

for A being non-empty MSAlgebra over S holds \false A = \not (\true A);

theorem Th10: :: AOFA_A01:10

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T holds \false C = FALSE

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T holds \false C = FALSE

proof end;

definition

let S be non empty non void bool-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let G be GeneratorSystem over S,X,T;

let b be Element of the generators of G . the bool-sort of S;

let C be image of T;

let A be preIfWhileAlgebra;

let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b);

let s be Element of C -States the generators of G;

let P be Algorithm of A;

:: original: .

redefine func f . (s,P) -> Element of C -States the generators of G;

coherence

f . (s,P) is Element of C -States the generators of G

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let G be GeneratorSystem over S,X,T;

let b be Element of the generators of G . the bool-sort of S;

let C be image of T;

let A be preIfWhileAlgebra;

let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b);

let s be Element of C -States the generators of G;

let P be Algorithm of A;

:: original: .

redefine func f . (s,P) -> Element of C -States the generators of G;

coherence

f . (s,P) is Element of C -States the generators of G

proof end;

definition

let S be non empty non void ManySortedSign ;

let T be non-empty MSAlgebra over S;

let G be V3() GeneratorSet of T;

let s be SortSymbol of S;

let x be Element of G . s;

coherence

x is Element of T,s

end;
let T be non-empty MSAlgebra over S;

let G be V3() GeneratorSet of T;

let s be SortSymbol of S;

let x be Element of G . s;

coherence

x is Element of T,s

proof end;

:: deftheorem defines @ AOFA_A01:def 7 :

for S being non empty non void ManySortedSign

for T being non-empty MSAlgebra over S

for G being V3() GeneratorSet of T

for s being SortSymbol of S

for x being Element of G . s holds @ x = x;

for S being non empty non void ManySortedSign

for T being non-empty MSAlgebra over S

for G being V3() GeneratorSet of T

for s being SortSymbol of S

for x being Element of G . s holds @ x = x;

definition

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be IfWhileAlgebra of the generators of G;

let b be pure Element of the generators of G . the bool-sort of S;

let I be integer SortSymbol of S;

let t1, t2 be Element of T,I;

coherence

b := ((leq (t1,t2)),A) is Algorithm of A ;

coherence

b := ((\not (leq (t1,t2))),A) is Algorithm of A ;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be IfWhileAlgebra of the generators of G;

let b be pure Element of the generators of G . the bool-sort of S;

let I be integer SortSymbol of S;

let t1, t2 be Element of T,I;

coherence

b := ((leq (t1,t2)),A) is Algorithm of A ;

coherence

b := ((\not (leq (t1,t2))),A) is Algorithm of A ;

:: deftheorem defines leq AOFA_A01:def 8 :

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t1, t2 being Element of T,I holds b leq (t1,t2,A) = b := ((leq (t1,t2)),A);

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t1, t2 being Element of T,I holds b leq (t1,t2,A) = b := ((leq (t1,t2)),A);

:: deftheorem defines gt AOFA_A01:def 9 :

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t1, t2 being Element of T,I holds b gt (t1,t2,A) = b := ((\not (leq (t1,t2))),A);

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t1, t2 being Element of T,I holds b gt (t1,t2,A) = b := ((\not (leq (t1,t2))),A);

definition

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let I be integer SortSymbol of S;

coherence

(\1 (T,I)) + (\1 (T,I)) is Element of T,I ;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let I be integer SortSymbol of S;

coherence

(\1 (T,I)) + (\1 (T,I)) is Element of T,I ;

:: deftheorem defines \2 AOFA_A01:def 10 :

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for I being integer SortSymbol of S holds \2 (T,I) = (\1 (T,I)) + (\1 (T,I));

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b

for I being integer SortSymbol of S holds \2 (T,I) = (\1 (T,I)) + (\1 (T,I));

definition

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be IfWhileAlgebra of the generators of G;

let b be pure Element of the generators of G . the bool-sort of S;

let I be integer SortSymbol of S;

let t be Element of T,I;

b gt ((t mod (\2 (T,I))),(\0 (T,I)),A) is Algorithm of A ;

b leq ((t mod (\2 (T,I))),(\0 (T,I)),A) is Algorithm of A ;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be IfWhileAlgebra of the generators of G;

let b be pure Element of the generators of G . the bool-sort of S;

let I be integer SortSymbol of S;

let t be Element of T,I;

func t is_odd (b,A) -> Algorithm of A equals :: AOFA_A01:def 11

b gt ((t mod (\2 (T,I))),(\0 (T,I)),A);

coherence b gt ((t mod (\2 (T,I))),(\0 (T,I)),A);

b gt ((t mod (\2 (T,I))),(\0 (T,I)),A) is Algorithm of A ;

func t is_even (b,A) -> Algorithm of A equals :: AOFA_A01:def 12

b leq ((t mod (\2 (T,I))),(\0 (T,I)),A);

coherence b leq ((t mod (\2 (T,I))),(\0 (T,I)),A);

b leq ((t mod (\2 (T,I))),(\0 (T,I)),A) is Algorithm of A ;

:: deftheorem defines is_odd AOFA_A01:def 11 :

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t being Element of T,I holds t is_odd (b,A) = b gt ((t mod (\2 (T,I))),(\0 (T,I)),A);

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t being Element of T,I holds t is_odd (b,A) = b gt ((t mod (\2 (T,I))),(\0 (T,I)),A);

:: deftheorem defines is_even AOFA_A01:def 12 :

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t being Element of T,I holds t is_even (b,A) = b leq ((t mod (\2 (T,I))),(\0 (T,I)),A);

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for I being integer SortSymbol of S

for t being Element of T,I holds t is_even (b,A) = b leq ((t mod (\2 (T,I))),(\0 (T,I)),A);

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer image of T;

let I be integer SortSymbol of S;

let s be Element of C -States the generators of G;

let x be Element of the generators of G . I;

coherence

(s . I) . x is integer

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer image of T;

let I be integer SortSymbol of S;

let s be Element of C -States the generators of G;

let x be Element of the generators of G . I;

coherence

(s . I) . x is integer

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer image of T;

let I be integer SortSymbol of S;

let s be Element of C -States the generators of G;

let t be Element of T,I;

coherence

t value_at (C,s) is integer

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer image of T;

let I be integer SortSymbol of S;

let s be Element of C -States the generators of G;

let t be Element of T,I;

coherence

t value_at (C,s) is integer

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let C be bool-correct 4,1 integer image of T;

let I be integer SortSymbol of S;

let u be ManySortedFunction of FreeGen T, the Sorts of C;

let t be Element of T,I;

coherence

t value_at (C,u) is integer

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let C be bool-correct 4,1 integer image of T;

let I be integer SortSymbol of S;

let u be ManySortedFunction of FreeGen T, the Sorts of C;

let t be Element of T,I;

coherence

t value_at (C,u) is integer

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer image of T;

let s be Element of C -States the generators of G;

let t be Element of T, the bool-sort of S;

coherence

t value_at (C,s) is boolean

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer image of T;

let s be Element of C -States the generators of G;

let t be Element of T, the bool-sort of S;

coherence

t value_at (C,s) is boolean

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let C be bool-correct 4,1 integer image of T;

let u be ManySortedFunction of FreeGen T, the Sorts of C;

let t be Element of T, the bool-sort of S;

coherence

t value_at (C,u) is boolean

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let C be bool-correct 4,1 integer image of T;

let u be ManySortedFunction of FreeGen T, the Sorts of C;

let t be Element of T, the bool-sort of S;

coherence

t value_at (C,u) is boolean

proof end;

theorem Th11: :: AOFA_A01:11

for S being non empty non void bool-correct 4,1 integer BoolSignature

for o being OperSymbol of S st o = In (( the connectives of S . 1), the carrier' of S) holds

( o = the connectives of S . 1 & the_arity_of o = {} & the_result_sort_of o = the bool-sort of S )

for o being OperSymbol of S st o = In (( the connectives of S . 1), the carrier' of S) holds

( o = the connectives of S . 1 & the_arity_of o = {} & the_result_sort_of o = the bool-sort of S )

proof end;

theorem Th12: :: AOFA_A01:12

for S being non empty non void bool-correct 4,1 integer BoolSignature

for o being OperSymbol of S st o = In (( the connectives of S . 2), the carrier' of S) holds

( o = the connectives of S . 2 & the_arity_of o = <* the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )

for o being OperSymbol of S st o = In (( the connectives of S . 2), the carrier' of S) holds

( o = the connectives of S . 2 & the_arity_of o = <* the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )

proof end;

theorem Th13: :: AOFA_A01:13

for S being non empty non void bool-correct 4,1 integer BoolSignature

for o being OperSymbol of S st o = In (( the connectives of S . 3), the carrier' of S) holds

( o = the connectives of S . 3 & the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )

for o being OperSymbol of S st o = In (( the connectives of S . 3), the carrier' of S) holds

( o = the connectives of S . 3 & the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )

proof end;

theorem Th14: :: AOFA_A01:14

for S being non empty non void bool-correct 4,1 integer BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 4), the carrier' of S) holds

( the_arity_of o = {} & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 4), the carrier' of S) holds

( the_arity_of o = {} & the_result_sort_of o = I )

proof end;

theorem Th15: :: AOFA_A01:15

for S being non empty non void bool-correct 4,1 integer BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 5), the carrier' of S) holds

( the_arity_of o = {} & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 5), the carrier' of S) holds

( the_arity_of o = {} & the_result_sort_of o = I )

proof end;

theorem Th16: :: AOFA_A01:16

for S being non empty non void bool-correct 4,1 integer BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 6), the carrier' of S) holds

( the_arity_of o = <*I*> & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 6), the carrier' of S) holds

( the_arity_of o = <*I*> & the_result_sort_of o = I )

proof end;

theorem Th17: :: AOFA_A01:17

for S being non empty non void bool-correct 4,1 integer BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 7), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 7), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = I )

proof end;

theorem Th18: :: AOFA_A01:18

for S being non empty non void bool-correct 4,1 integer BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 8), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 8), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = I )

proof end;

theorem Th19: :: AOFA_A01:19

for S being non empty non void bool-correct 4,1 integer BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 9), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 9), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = I )

proof end;

theorem Th20: :: AOFA_A01:20

for S being non empty non void bool-correct 4,1 integer BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 10), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = the bool-sort of S )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 10), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = the bool-sort of S )

proof end;

theorem Th21: :: AOFA_A01:21

for S being non empty non void ManySortedSign

for o being OperSymbol of S st the_arity_of o = {} holds

for A being MSAlgebra over S holds Args (o,A) = {{}}

for o being OperSymbol of S st the_arity_of o = {} holds

for A being MSAlgebra over S holds Args (o,A) = {{}}

proof end;

theorem Th22: :: AOFA_A01:22

for S being non empty non void ManySortedSign

for a being SortSymbol of S

for o being OperSymbol of S st the_arity_of o = <*a*> holds

for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a)*>

for a being SortSymbol of S

for o being OperSymbol of S st the_arity_of o = <*a*> holds

for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a)*>

proof end;

theorem Th23: :: AOFA_A01:23

for S being non empty non void ManySortedSign

for a, b being SortSymbol of S

for o being OperSymbol of S st the_arity_of o = <*a,b*> holds

for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*>

for a, b being SortSymbol of S

for o being OperSymbol of S st the_arity_of o = <*a,b*> holds

for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*>

proof end;

theorem Th24: :: AOFA_A01:24

for S being non empty non void ManySortedSign

for a, b, c being SortSymbol of S

for o being OperSymbol of S st the_arity_of o = <*a,b,c*> holds

for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b),( the Sorts of A . c)*>

for a, b, c being SortSymbol of S

for o being OperSymbol of S st the_arity_of o = <*a,b,c*> holds

for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b),( the Sorts of A . c)*>

proof end;

theorem Th25: :: AOFA_A01:25

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for s being SortSymbol of S

for a being Element of A,s

for h being ManySortedFunction of A,B

for o being OperSymbol of S st the_arity_of o = <*s*> holds

for p being Element of Args (o,A) st p = <*a*> holds

h # p = <*((h . s) . a)*>

for A, B being non-empty MSAlgebra over S

for s being SortSymbol of S

for a being Element of A,s

for h being ManySortedFunction of A,B

for o being OperSymbol of S st the_arity_of o = <*s*> holds

for p being Element of Args (o,A) st p = <*a*> holds

h # p = <*((h . s) . a)*>

proof end;

theorem Th26: :: AOFA_A01:26

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S

for a being Element of A,s1

for b being Element of A,s2

for h being ManySortedFunction of A,B

for o being OperSymbol of S st the_arity_of o = <*s1,s2*> holds

for p being Element of Args (o,A) st p = <*a,b*> holds

h # p = <*((h . s1) . a),((h . s2) . b)*>

for A, B being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S

for a being Element of A,s1

for b being Element of A,s2

for h being ManySortedFunction of A,B

for o being OperSymbol of S st the_arity_of o = <*s1,s2*> holds

for p being Element of Args (o,A) st p = <*a,b*> holds

h # p = <*((h . s1) . a),((h . s2) . b)*>

proof end;

theorem Th27: :: AOFA_A01:27

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for s1, s2, s3 being SortSymbol of S

for a being Element of A,s1

for b being Element of A,s2

for c being Element of A,s3

for h being ManySortedFunction of A,B

for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds

for p being Element of Args (o,A) st p = <*a,b,c*> holds

h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>

for A, B being non-empty MSAlgebra over S

for s1, s2, s3 being SortSymbol of S

for a being Element of A,s1

for b being Element of A,s2

for c being Element of A,s3

for h being ManySortedFunction of A,B

for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds

for p being Element of Args (o,A) st p = <*a,b,c*> holds

h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>

proof end;

theorem Th28: :: AOFA_A01:28

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for h being ManySortedFunction of T,C st h is_homomorphism T,C holds

for a being SortSymbol of S

for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for h being ManySortedFunction of T,C st h is_homomorphism T,C holds

for a being SortSymbol of S

for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t

proof end;

theorem Th29: :: AOFA_A01:29

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds

for a being SortSymbol of S

for t being Element of T,a holds t value_at (C,s) = (h . a) . t

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds

for a being SortSymbol of S

for t being Element of T,a holds t value_at (C,s) = (h . a) . t

proof end;

theorem Th30: :: AOFA_A01:30

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G holds (\true T) value_at (C,s) = TRUE

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G holds (\true T) value_at (C,s) = TRUE

proof end;

theorem Th31: :: AOFA_A01:31

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for t being Element of T, the bool-sort of S holds (\not t) value_at (C,s) = \not (t value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for t being Element of T, the bool-sort of S holds (\not t) value_at (C,s) = \not (t value_at (C,s))

proof end;

theorem :: AOFA_A01:32

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for a being boolean object

for t being Element of T, the bool-sort of S holds

( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for a being boolean object

for t being Element of T, the bool-sort of S holds

( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )

proof end;

theorem Th33: :: AOFA_A01:33

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for a being Element of C, the bool-sort of S

for x being boolean object holds

( \not a = 'not' x iff a = x )

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for a being Element of C, the bool-sort of S

for x being boolean object holds

( \not a = 'not' x iff a = x )

proof end;

theorem :: AOFA_A01:34

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G holds (\false T) value_at (C,s) = FALSE

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G holds (\false T) value_at (C,s) = FALSE

proof end;

theorem :: AOFA_A01:35

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))

proof end;

theorem Th36: :: AOFA_A01:36

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0

proof end;

theorem Th37: :: AOFA_A01:37

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G holds (\1 (T,I)) value_at (C,s) = 1

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G holds (\1 (T,I)) value_at (C,s) = 1

proof end;

theorem Th38: :: AOFA_A01:38

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t being Element of T,I

for s being Element of C -States the generators of G holds (- t) value_at (C,s) = - (t value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t being Element of T,I

for s being Element of C -States the generators of G holds (- t) value_at (C,s) = - (t value_at (C,s))

proof end;

theorem Th39: :: AOFA_A01:39

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 + t2) value_at (C,s) = (t1 value_at (C,s)) + (t2 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 + t2) value_at (C,s) = (t1 value_at (C,s)) + (t2 value_at (C,s))

proof end;

theorem Th40: :: AOFA_A01:40

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G holds (\2 (T,I)) value_at (C,s) = 2

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G holds (\2 (T,I)) value_at (C,s) = 2

proof end;

theorem Th41: :: AOFA_A01:41

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 - t2) value_at (C,s) = (t1 value_at (C,s)) - (t2 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 - t2) value_at (C,s) = (t1 value_at (C,s)) - (t2 value_at (C,s))

proof end;

theorem Th42: :: AOFA_A01:42

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 * t2) value_at (C,s) = (t1 value_at (C,s)) * (t2 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 * t2) value_at (C,s) = (t1 value_at (C,s)) * (t2 value_at (C,s))

proof end;

theorem Th43: :: AOFA_A01:43

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 div t2) value_at (C,s) = (t1 value_at (C,s)) div (t2 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 div t2) value_at (C,s) = (t1 value_at (C,s)) div (t2 value_at (C,s))

proof end;

theorem Th44: :: AOFA_A01:44

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))

proof end;

theorem Th45: :: AOFA_A01:45

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))

proof end;

theorem Th46: :: AOFA_A01:46

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\true T) value_at (C,u) = TRUE

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\true T) value_at (C,u) = TRUE

proof end;

theorem Th47: :: AOFA_A01:47

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T, the bool-sort of S holds (\not t) value_at (C,u) = \not (t value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T, the bool-sort of S holds (\not t) value_at (C,u) = \not (t value_at (C,u))

proof end;

theorem :: AOFA_A01:48

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C

for a being boolean object

for t being Element of T, the bool-sort of S holds

( (\not t) value_at (C,u) = 'not' a iff t value_at (C,u) = a )

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C

for a being boolean object

for t being Element of T, the bool-sort of S holds

( (\not t) value_at (C,u) = 'not' a iff t value_at (C,u) = a )

proof end;

theorem :: AOFA_A01:49

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\false T) value_at (C,u) = FALSE

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\false T) value_at (C,u) = FALSE

proof end;

theorem :: AOFA_A01:50

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 value_at (C,u))

proof end;

theorem :: AOFA_A01:51

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\0 (T,I)) value_at (C,u) = 0

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\0 (T,I)) value_at (C,u) = 0

proof end;

theorem Th52: :: AOFA_A01:52

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\1 (T,I)) value_at (C,u) = 1

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\1 (T,I)) value_at (C,u) = 1

proof end;

theorem Th53: :: AOFA_A01:53

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))

proof end;

theorem Th54: :: AOFA_A01:54

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 + t2) value_at (C,u) = (t1 value_at (C,u)) + (t2 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 + t2) value_at (C,u) = (t1 value_at (C,u)) + (t2 value_at (C,u))

proof end;

theorem :: AOFA_A01:55

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\2 (T,I)) value_at (C,u) = 2

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\2 (T,I)) value_at (C,u) = 2

proof end;

theorem Th56: :: AOFA_A01:56

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 - t2) value_at (C,u) = (t1 value_at (C,u)) - (t2 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 - t2) value_at (C,u) = (t1 value_at (C,u)) - (t2 value_at (C,u))

proof end;

theorem Th57: :: AOFA_A01:57

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 * t2) value_at (C,u) = (t1 value_at (C,u)) * (t2 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 * t2) value_at (C,u) = (t1 value_at (C,u)) * (t2 value_at (C,u))

proof end;

theorem Th58: :: AOFA_A01:58

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 div t2) value_at (C,u) = (t1 value_at (C,u)) div (t2 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 div t2) value_at (C,u) = (t1 value_at (C,u)) div (t2 value_at (C,u))

proof end;

theorem :: AOFA_A01:59

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 mod t2) value_at (C,u) = (t1 value_at (C,u)) mod (t2 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (t1 mod t2) value_at (C,u) = (t1 value_at (C,u)) mod (t2 value_at (C,u))

proof end;

theorem :: AOFA_A01:60

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (leq (t1,t2)) value_at (C,u) = leq ((t1 value_at (C,u)),(t2 value_at (C,u)))

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for t1, t2 being Element of T,I

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (leq (t1,t2)) value_at (C,u) = leq ((t1 value_at (C,u)),(t2 value_at (C,u)))

proof end;

theorem Th61: :: AOFA_A01:61

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for a being SortSymbol of S

for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for s being Element of C -States the generators of G

for a being SortSymbol of S

for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x

proof end;

theorem Th62: :: AOFA_A01:62

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for a being SortSymbol of S

for x being pure Element of the generators of G . a

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for a being SortSymbol of S

for x being pure Element of the generators of G . a

for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x

proof end;

theorem Th63: :: AOFA_A01:63

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for i, j being Integer

for a, b being Element of C,I st a = i & b = j holds

a - b = i - j

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for i, j being Integer

for a, b being Element of C,I st a = i & b = j holds

a - b = i - j

proof end;

theorem Th64: :: AOFA_A01:64

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for i, j being Integer

for a, b being Element of C,I st a = i & b = j & j <> 0 holds

a mod b = i mod j

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for I being integer SortSymbol of S

for i, j being Integer

for a, b being Element of C,I st a = i & b = j & j <> 0 holds

a mod b = i mod j

proof end;

theorem Th65: :: AOFA_A01:65

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds

for a being SortSymbol of S

for x being pure Element of the generators of G . a

for t being Element of T,a holds

( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds

((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds

for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds

for a being SortSymbol of S

for x being pure Element of the generators of G . a

for t being Element of T,a holds

( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds

((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds

for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )

proof end;

theorem Th66: :: AOFA_A01:66

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for b being pure Element of the generators of G . the bool-sort of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds

( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds

( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds

( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for b being pure Element of the generators of G . the bool-sort of S

for t1, t2 being Element of T,I

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds

( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds

( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds

( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )

proof end;

registration

let i, j be Real;

let a, b be boolean object ;

coherence

IFGT (i,j,a,b) is boolean by XXREAL_0:def 11;

end;
let a, b be boolean object ;

coherence

IFGT (i,j,a,b) is boolean by XXREAL_0:def 11;

theorem Th67: :: AOFA_A01:67

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for b being pure Element of the generators of G . the bool-sort of S

for t being Element of T,I

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds

( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds

( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for b being pure Element of the generators of G . the bool-sort of S

for t being Element of T,I

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds

( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds

( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )

proof end;

definition

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be IfWhileAlgebra of the generators of G;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be IfWhileAlgebra of the generators of G;

:: deftheorem defines elementary AOFA_A01:def 13 :

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G holds

( A is elementary iff rng the assignments of A c= ElementaryInstructions A );

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G holds

( A is elementary iff rng the assignments of A c= ElementaryInstructions A );

theorem Th68: :: AOFA_A01:68

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G st A is elementary holds

for a being SortSymbol of S

for x being Element of the generators of G . a

for t being Element of T,a holds x := (t,A) in ElementaryInstructions A

for X being V3() ManySortedSet of the carrier of S

for T being b

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G st A is elementary holds

for a being SortSymbol of S

for x being Element of the generators of G . a

for t being Element of T,a holds x := (t,A) in ElementaryInstructions A

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

ex b_{1} being strict IfWhileAlgebra of the generators of G st b_{1} is elementary

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

cluster non empty partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction non degenerated well_founded ECIW-strict strict elementary for ProgramAlgStr over S,T, the generators of G;

existence ex b

proof end;

registration

let S be non empty non void bool-correct 4,1 integer BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be elementary IfWhileAlgebra of the generators of G;

let a be SortSymbol of S;

let x be Element of the generators of G . a;

let t be Element of T,a;

coherence

x := (t,A) is absolutely-terminating

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be elementary IfWhileAlgebra of the generators of G;

let a be SortSymbol of S;

let x be Element of the generators of G . a;

let t be Element of T,a;

coherence

x := (t,A) is absolutely-terminating

proof end;

theorem :: AOFA_A01:69

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for x, y, m being pure Element of the generators of G . I

for b being pure Element of the generators of G . the bool-sort of S

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st

( d . x = 1 & d . y = 2 & d . m = 3 ) holds

(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for x, y, m being pure Element of the generators of G . I

for b being pure Element of the generators of G . the bool-sort of S

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st

( d . x = 1 & d . y = 2 & d . m = 3 ) holds

(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }

proof end;

theorem :: AOFA_A01:70

for S being non empty non void bool-correct 4,1 integer BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for x, y, m being pure Element of the generators of G . I

for b being pure Element of the generators of G . the bool-sort of S

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st

( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds

for s being Element of C -States the generators of G

for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds

((f . (s,((y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))))))) . I) . y = ((s . I) . x) |^ n

for X being V3() ManySortedSet of the carrier of S

for T being b

for C being bool-correct 4,1 integer image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for x, y, m being pure Element of the generators of G . I

for b being pure Element of the generators of G . the bool-sort of S

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st

( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds

for s being Element of C -States the generators of G

for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds

((f . (s,((y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))))))) . I) . y = ((s . I) . x) |^ n

proof end;

registration

let X be non empty set ;

let f be FinSequence of X ^omega ;

let x be Nat;

coherence

( f . x is Sequence-like & f . x is finite & f . x is Function-like & f . x is Relation-like )

end;
let f be FinSequence of X ^omega ;

let x be Nat;

coherence

( f . x is Sequence-like & f . x is finite & f . x is Function-like & f . x is Relation-like )

proof end;

registration

let X be non empty set ;

coherence

for b_{1} being FinSequence of X ^omega holds b_{1} is Function-yielding
;

end;
coherence

for b

registration

let i be Nat;

let f be finite i -based array;

let a, x be set ;

coherence

( f +* (a,x) is i -based & f +* (a,x) is finite & f +* (a,x) is segmental )

end;
let f be finite i -based array;

let a, x be set ;

coherence

( f +* (a,x) is i -based & f +* (a,x) is finite & f +* (a,x) is segmental )

proof end;

registration

let X be non empty set ;

let f be X -valued Function;

let a be set ;

let x be Element of X;

coherence

f +* (a,x) is X -valued

end;
let f be X -valued Function;

let a be set ;

let x be Element of X;

coherence

f +* (a,x) is X -valued

proof end;

scheme :: AOFA_A01:sch 1

Sch1{ F_{1}() -> non empty set , F_{2}() -> Nat, F_{3}() -> set , F_{4}( set , set , set ) -> set , F_{5}( set ) -> set } :

Sch1{ F

ex f being FinSequence of F_{1}() ^omega st

( len f = F_{2}() & ( f . 1 = F_{3}() or F_{2}() = 0 ) & ( for i being Nat st 1 <= i & i < F_{2}() holds

f . (i + 1) = F_{4}((f . i),i,F_{5}(i)) ) )

provided( len f = F

f . (i + 1) = F

A1:
for a being finite 0 -based array of F_{1}()

for i being Nat st 1 <= i & i < F_{2}() holds

for x being Element of F_{1}() holds F_{4}(a,i,x) is finite 0 -based array of F_{1}()
and

A2: F_{3}() is finite 0 -based array of F_{1}()
and

A3: for i being Nat st i < F_{2}() holds

F_{5}(i) in F_{1}()

for i being Nat st 1 <= i & i < F

for x being Element of F

A2: F

A3: for i being Nat st i < F

F

proof end;

theorem Th71: :: AOFA_A01:71

for S being non empty non void 11,1,1 -array BoolSignature

for J, L being set

for K being SortSymbol of S st the connectives of S . 11 is_of_type <*J,L*>,K holds

( J = the_array_sort_of S & ( for I being integer SortSymbol of S holds the_array_sort_of S <> I ) )

for J, L being set

for K being SortSymbol of S st the connectives of S . 11 is_of_type <*J,L*>,K holds

( J = the_array_sort_of S & ( for I being integer SortSymbol of S holds the_array_sort_of S <> I ) )

proof end;

theorem Th72: :: AOFA_A01:72

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S

for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S

for a, b being Element of A,I st a = 0 holds

init.array (a,b) = {}

for I being integer SortSymbol of S

for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S

for a, b being Element of A,I st a = 0 holds

init.array (a,b) = {}

proof end;

theorem Th73: :: AOFA_A01:73

for S being non empty non void bool-correct 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S holds

( the_array_sort_of S <> I & the connectives of S . 11 is_of_type <*(the_array_sort_of S),I*>,I & the connectives of S . (11 + 1) is_of_type <*(the_array_sort_of S),I,I*>, the_array_sort_of S & the connectives of S . (11 + 2) is_of_type <*(the_array_sort_of S)*>,I & the connectives of S . (11 + 3) is_of_type <*I,I*>, the_array_sort_of S )

for I being integer SortSymbol of S holds

( the_array_sort_of S <> I & the connectives of S . 11 is_of_type <*(the_array_sort_of S),I*>,I & the connectives of S . (11 + 1) is_of_type <*(the_array_sort_of S),I,I*>, the_array_sort_of S & the connectives of S . (11 + 2) is_of_type <*(the_array_sort_of S)*>,I & the connectives of S . (11 + 3) is_of_type <*I,I*>, the_array_sort_of S )

proof end;

theorem Th74: :: AOFA_A01:74

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S

for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S holds

( the Sorts of A . (the_array_sort_of S) = INT ^omega & ( for i, j being Element of A,I st i is non negative Integer holds

init.array (i,j) = (Segm i) --> j ) & ( for a being Element of the Sorts of A . (the_array_sort_of S) holds

( length (a,I) = card a & ( for i being Element of A,I

for f being Function st f = a & i in dom f holds

( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) ) ) )

for I being integer SortSymbol of S

for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S holds

( the Sorts of A . (the_array_sort_of S) = INT ^omega & ( for i, j being Element of A,I st i is non negative Integer holds

init.array (i,j) = (Segm i) --> j ) & ( for a being Element of the Sorts of A . (the_array_sort_of S) holds

( length (a,I) = card a & ( for i being Element of A,I

for f being Function st f = a & i in dom f holds

( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) ) ) )

proof end;

registration
end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let A be non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S;

coherence

for b_{1} being non-empty MSSubAlgebra of A holds b_{1} is 11,1,1 -array

end;
let A be non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S;

coherence

for b

proof end;

definition

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let A be non-empty MSAlgebra over S;

end;
let A be non-empty MSAlgebra over S;

attr A is integer-array means :Def14: :: AOFA_A01:def 14

ex C being image of A st C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S;

ex C being image of A st C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S;

:: deftheorem Def14 defines integer-array AOFA_A01:def 14 :

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for A being non-empty MSAlgebra over S holds

( A is integer-array iff ex C being image of A st C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S );

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for A being non-empty MSAlgebra over S holds

( A is integer-array iff ex C being image of A st C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S );

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

coherence

for b_{1} being non-empty MSAlgebra over S st b_{1} = Free (S,X) holds

b_{1} is integer-array

end;
let X be V3() ManySortedSet of the carrier of S;

coherence

for b

b

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

coherence

for b_{1} being non-empty MSAlgebra over S st b_{1} is integer-array holds

b_{1} is integer
;

let X be V3() ManySortedSet of the carrier of S;

ex b_{1} being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself strict VarMSAlgebra over S st

( b_{1} is vf-free & b_{1} is integer-array )

end;
coherence

for b

b

let X be V3() ManySortedSet of the carrier of S;

cluster non-empty X,S -terms all_vars_including inheriting_operations free_in_itself strict vf-free disjoint_valued integer-array for VarMSAlgebra over S;

existence ex b

( b

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

existence

ex b_{1} being non-empty MSAlgebra over S st b_{1} is integer-array

end;
existence

ex b

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let A be non-empty integer-array MSAlgebra over S;

ex b_{1} being bool-correct image of A st

( b_{1} is 4,1 integer & b_{1} is 11,1,1 -array )

end;
let A be non-empty integer-array MSAlgebra over S;

cluster non-empty A -Image Equations (S,A) -satisfying bool-correct 4,1 integer 11,1,1 -array for MSAlgebra over S;

existence ex b

( b

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let A be non-empty bool-correct 11,1,1 -array MSAlgebra over S;

coherence

for b_{1} being Element of the Sorts of A . (the_array_sort_of S) holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
let A be non-empty bool-correct 11,1,1 -array MSAlgebra over S;

coherence

for b

( b

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let A be non-empty bool-correct 11,1,1 -array MSAlgebra over S;

coherence

for b_{1} being Element of the Sorts of A . (the_array_sort_of S) holds

( b_{1} is finite & b_{1} is Sequence-like )

end;
let A be non-empty bool-correct 11,1,1 -array MSAlgebra over S;

coherence

for b

( b

proof end;

theorem Th75: :: AOFA_A01:75

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 11), the carrier' of S) holds

( the_arity_of o = <*(the_array_sort_of S),I*> & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 11), the carrier' of S) holds

( the_arity_of o = <*(the_array_sort_of S),I*> & the_result_sort_of o = I )

proof end;

theorem Th76: :: AOFA_A01:76

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 12), the carrier' of S) holds

( the_arity_of o = <*(the_array_sort_of S),I,I*> & the_result_sort_of o = the_array_sort_of S )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 12), the carrier' of S) holds

( the_arity_of o = <*(the_array_sort_of S),I,I*> & the_result_sort_of o = the_array_sort_of S )

proof end;

theorem Th77: :: AOFA_A01:77

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 13), the carrier' of S) holds

( the_arity_of o = <*(the_array_sort_of S)*> & the_result_sort_of o = I )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 13), the carrier' of S) holds

( the_arity_of o = <*(the_array_sort_of S)*> & the_result_sort_of o = I )

proof end;

theorem Th78: :: AOFA_A01:78

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 14), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = the_array_sort_of S )

for I being integer SortSymbol of S

for o being OperSymbol of S st o = In (( the connectives of S . 14), the carrier' of S) holds

( the_arity_of o = <*I,I*> & the_result_sort_of o = the_array_sort_of S )

proof end;

theorem Th79: :: AOFA_A01:79

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t being Element of T,(the_array_sort_of S)

for t1 being Element of T,I holds (t . t1) value_at (C,s) = (t value_at (C,s)) . (t1 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t being Element of T,(the_array_sort_of S)

for t1 being Element of T,I holds (t . t1) value_at (C,s) = (t value_at (C,s)) . (t1 value_at (C,s))

proof end;

theorem Th80: :: AOFA_A01:80

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t being Element of T,(the_array_sort_of S)

for t1, t2 being Element of T,I holds ((t,t1) <- t2) value_at (C,s) = ((t value_at (C,s)),(t1 value_at (C,s))) <- (t2 value_at (C,s))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t being Element of T,(the_array_sort_of S)

for t1, t2 being Element of T,I holds ((t,t1) <- t2) value_at (C,s) = ((t value_at (C,s)),(t1 value_at (C,s))) <- (t2 value_at (C,s))

proof end;

theorem Th81: :: AOFA_A01:81

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)

proof end;

theorem :: AOFA_A01:82

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))

proof end;

theorem :: AOFA_A01:83

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T,(the_array_sort_of S)

for t1 being Element of T,I holds (t . t1) value_at (C,u) = (t value_at (C,u)) . (t1 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T,(the_array_sort_of S)

for t1 being Element of T,I holds (t . t1) value_at (C,u) = (t value_at (C,u)) . (t1 value_at (C,u))

proof end;

theorem Th84: :: AOFA_A01:84

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T,(the_array_sort_of S)

for t1, t2 being Element of T,I holds ((t,t1) <- t2) value_at (C,u) = ((t value_at (C,u)),(t1 value_at (C,u))) <- (t2 value_at (C,u))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T,(the_array_sort_of S)

for t1, t2 being Element of T,I holds ((t,t1) <- t2) value_at (C,u) = ((t value_at (C,u)),(t1 value_at (C,u))) <- (t2 value_at (C,u))

proof end;

theorem :: AOFA_A01:85

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,u) = length ((t value_at (C,u)),I)

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,u) = length ((t value_at (C,u)),I)

proof end;

theorem :: AOFA_A01:86

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,u) = init.array ((t1 value_at (C,u)),(t2 value_at (C,u)))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for I being integer SortSymbol of S

for u being ManySortedFunction of FreeGen T, the Sorts of C

for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,u) = init.array ((t1 value_at (C,u)),(t2 value_at (C,u)))

proof end;

Lm1: now :: thesis: for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{1},S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let X be V3() ManySortedSet of the carrier of S; :: thesis: for T being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis: for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let I be integer SortSymbol of S; :: thesis: for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let i be Integer; :: thesis: for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let f1 be Function of INT,( the Sorts of T . I); :: thesis: ( f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) implies for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2 )

assume A1: ( f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) ; :: thesis: for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let f2 be Function of INT,( the Sorts of T . I); :: thesis: ( f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) implies f1 = f2 )

assume A2: ( f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) ; :: thesis: f1 = f2

defpred S_{1}[ Nat] means f1 . $1 = f2 . $1;

A3: S_{1}[ 0 ]
by A1, A2;

A4: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A3, A4);

end;
for T being non-empty b

for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let X be V3() ManySortedSet of the carrier of S; :: thesis: for T being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis: for I being integer SortSymbol of S

for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let I be integer SortSymbol of S; :: thesis: for i being Integer

for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let i be Integer; :: thesis: for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let f1 be Function of INT,( the Sorts of T . I); :: thesis: ( f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) implies for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2 )

assume A1: ( f1 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f1 . j = t holds

( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) ; :: thesis: for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds

f1 = f2

let f2 be Function of INT,( the Sorts of T . I); :: thesis: ( f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) implies f1 = f2 )

assume A2: ( f2 . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f2 . j = t holds

( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) ; :: thesis: f1 = f2

defpred S

A3: S

A4: for i being Nat st S

S

proof

A6:
for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A5: S_{1}[i]
; :: thesis: S_{1}[i + 1]

reconsider j = i as Element of INT by INT_1:def 2;

thus f1 . (i + 1) = (f1 . j) + (\1 (T,I)) by A1

.= f2 . (i + 1) by A2, A5 ; :: thesis: verum

end;
assume A5: S

reconsider j = i as Element of INT by INT_1:def 2;

thus f1 . (i + 1) = (f1 . j) + (\1 (T,I)) by A1

.= f2 . (i + 1) by A2, A5 ; :: thesis: verum

now :: thesis: for i being Element of INT holds f1 . i = f2 . i

hence
f1 = f2
; :: thesis: verum
let i be Element of INT ; :: thesis: f1 . b_{1} = f2 . b_{1}

consider n being Nat such that

A7: ( i = n or i = - n ) by INT_1:def 1;

end;
consider n being Nat such that

A7: ( i = n or i = - n ) by INT_1:def 1;

per cases
( i = n or ( i = - n & n = 0 ) or ( i = - n & n <> 0 ) )
by A7;

end;

suppose A8:
( i = - n & n <> 0 )
; :: thesis: f1 . b_{1} = f2 . b_{1}

then consider m being Nat such that

A9: n = m + 1 by NAT_1:6;

reconsider m0 = m, m1 = m + 1 as Element of INT by INT_1:def 2;

thus f1 . i = - ((f1 . m0) + (\1 (T,I))) by A1, A9, A8

.= - ((f2 . m0) + (\1 (T,I))) by A6

.= f2 . i by A2, A9, A8 ; :: thesis: verum

end;
A9: n = m + 1 by NAT_1:6;

reconsider m0 = m, m1 = m + 1 as Element of INT by INT_1:def 2;

thus f1 . i = - ((f1 . m0) + (\1 (T,I))) by A1, A9, A8

.= - ((f2 . m0) + (\1 (T,I))) by A6

.= f2 . i by A2, A9, A8 ; :: thesis: verum

definition

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let I be integer SortSymbol of S;

let i be Integer;

ex b_{1} being Element of T,I ex f being Function of INT,( the Sorts of T . I) st

( b_{1} = f . i & f . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) )

for b_{1}, b_{2} being Element of T,I st ex f being Function of INT,( the Sorts of T . I) st

( b_{1} = f . i & f . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) & ex f being Function of INT,( the Sorts of T . I) st

( b_{2} = f . i & f . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) holds

b_{1} = b_{2}
by Lm1;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let I be integer SortSymbol of S;

let i be Integer;

func ^ (i,T,I) -> Element of T,I means :Def15: :: AOFA_A01:def 15

ex f being Function of INT,( the Sorts of T . I) st

( it = f . i & f . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) );

existence ex f being Function of INT,( the Sorts of T . I) st

( it = f . i & f . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) );

ex b

( b

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) )

proof end;

uniqueness for b

( b

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) & ex f being Function of INT,( the Sorts of T . I) st

( b

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) holds

b

:: deftheorem Def15 defines ^ AOFA_A01:def 15 :

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S

for i being Integer

for b_{6} being Element of T,I holds

( b_{6} = ^ (i,T,I) iff ex f being Function of INT,( the Sorts of T . I) st

( b_{6} = f . i & f . 0 = \0 (T,I) & ( for j being Nat

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) );

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for I being integer SortSymbol of S

for i being Integer

for b

( b

( b

for t being Element of T,I st f . j = t holds

( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) );

theorem Th87: :: AOFA_A01:87

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S holds ^ (0,T,I) = \0 (T,I)

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for I being integer SortSymbol of S holds ^ (0,T,I) = \0 (T,I)

proof end;

theorem Th88: :: AOFA_A01:88

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S

for n being Nat holds

( ^ ((n + 1),T,I) = (^ (n,T,I)) + (\1 (T,I)) & ^ ((- (n + 1)),T,I) = - (^ ((n + 1),T,I)) )

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for I being integer SortSymbol of S

for n being Nat holds

( ^ ((n + 1),T,I) = (^ (n,T,I)) + (\1 (T,I)) & ^ ((- (n + 1)),T,I) = - (^ ((n + 1),T,I)) )

proof end;

theorem :: AOFA_A01:89

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for I being integer SortSymbol of S holds ^ (1,T,I) = (\0 (T,I)) + (\1 (T,I))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for I being integer SortSymbol of S holds ^ (1,T,I) = (\0 (T,I)) + (\1 (T,I))

proof end;

theorem Th90: :: AOFA_A01:90

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for i being Integer holds (^ (i,T,I)) value_at (C,s) = i

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for s being Element of C -States the generators of G

for i being Integer holds (^ (i,T,I)) value_at (C,s) = i

proof end;

definition

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let I be integer SortSymbol of S;

let M be pure Element of the generators of G . (the_array_sort_of S);

let i be Integer;

coherence

(@ M) . (^ (i,T,I)) is Element of T,I ;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let I be integer SortSymbol of S;

let M be pure Element of the generators of G . (the_array_sort_of S);

let i be Integer;

coherence

(@ M) . (^ (i,T,I)) is Element of T,I ;

:: deftheorem defines . AOFA_A01:def 16 :

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for M being pure Element of the generators of G . (the_array_sort_of S)

for i being Integer holds M . (i,I) = (@ M) . (^ (i,T,I));

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for M being pure Element of the generators of G . (the_array_sort_of S)

for i being Integer holds M . (i,I) = (@ M) . (^ (i,T,I));

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let M be pure Element of the generators of G . (the_array_sort_of S);

coherence

( (s . (the_array_sort_of S)) . M is Function-like & (s . (the_array_sort_of S)) . M is Relation-like )

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let M be pure Element of the generators of G . (the_array_sort_of S);

coherence

( (s . (the_array_sort_of S)) . M is Function-like & (s . (the_array_sort_of S)) . M is Relation-like )

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let M be pure Element of the generators of G . (the_array_sort_of S);

coherence

( (s . (the_array_sort_of S)) . M is finite & (s . (the_array_sort_of S)) . M is Sequence-like & (s . (the_array_sort_of S)) . M is INT -valued )

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let M be pure Element of the generators of G . (the_array_sort_of S);

coherence

( (s . (the_array_sort_of S)) . M is finite & (s . (the_array_sort_of S)) . M is Sequence-like & (s . (the_array_sort_of S)) . M is INT -valued )

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let M be pure Element of the generators of G . (the_array_sort_of S);

coherence

( rng ((s . (the_array_sort_of S)) . M) is finite & rng ((s . (the_array_sort_of S)) . M) is integer-membered ) ;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let M be pure Element of the generators of G . (the_array_sort_of S);

coherence

( rng ((s . (the_array_sort_of S)) . M) is finite & rng ((s . (the_array_sort_of S)) . M) is integer-membered ) ;

theorem :: AOFA_A01:91

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for M being pure Element of the generators of G . (the_array_sort_of S)

for s being Element of C -States the generators of G

for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & M . (j,I) in the generators of G . I holds

((s . (the_array_sort_of S)) . M) . j = (s . I) . (M . (j,I))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for M being pure Element of the generators of G . (the_array_sort_of S)

for s being Element of C -States the generators of G

for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & M . (j,I) in the generators of G . I holds

((s . (the_array_sort_of S)) . M) . j = (s . I) . (M . (j,I))

proof end;

theorem :: AOFA_A01:92

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for s being Element of C -States the generators of G

for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds

((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for s being Element of C -States the generators of G

for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds

((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))

proof end;

registration
end;

theorem :: AOFA_A01:93

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for m, i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m & (s . (the_array_sort_of S)) . M <> {} holds

for n being Nat st ((f . (s,((m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))))) . I) . m = n holds

for X being non empty finite integer-membered set st X = rng ((s . (the_array_sort_of S)) . M) holds

(M . (n,I)) value_at (C,s) = max X

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for A being IfWhileAlgebra of the generators of G

for I being integer SortSymbol of S

for m, i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m & (s . (the_array_sort_of S)) . M <> {} holds

for n being Nat st ((f . (s,((m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))))))) . I) . m = n holds

for X being non empty finite integer-membered set st X = rng ((s . (the_array_sort_of S)) . M) holds

(M . (n,I)) value_at (C,s) = max X

proof end;

theorem Th94: :: AOFA_A01:94

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for b being pure Element of the generators of G . the bool-sort of S

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported holds

for t0, t1 being Element of T,I

for J being Algorithm of A

for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds

( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds

for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for b being pure Element of the generators of G . the bool-sort of S

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported holds

for t0, t1 being Element of T,I

for J being Algorithm of A

for P being set st P is_invariant_wrt i := (t0,A),f & P is_invariant_wrt b gt (t1,(@ i),A),f & P is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f & P is_invariant_wrt J,f & J is_terminating_wrt f,P & ( for s being Element of C -States the generators of G holds

( ((f . (s,J)) . I) . i = (s . I) . i & ((f . (s,(b gt (t1,(@ i),A)))) . I) . i = (s . I) . i & t1 value_at (C,(f . (s,(b gt (t1,(@ i),A))))) = t1 value_at (C,s) & t1 value_at (C,(f . (s,(J \; (i := (((@ i) + (\1 (T,I))),A)))))) = t1 value_at (C,s) ) ) holds

for-do ((i := (t0,A)),(b gt (t1,(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),J) is_terminating_wrt f,P

proof end;

theorem :: AOFA_A01:95

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for m, i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds

(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for m, i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds

(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }

proof end;

definition

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

attr G is integer-array means :: AOFA_A01:def 17

for I being integer SortSymbol of S holds

( { ((@ M) . t) where M is pure Element of the generators of G . (the_array_sort_of S), t is Element of T,I : verum } c= the generators of G . I & ( for M being pure Element of the generators of G . (the_array_sort_of S)

for t being Element of T,I

for g being Element of G,I st g = (@ M) . t holds

ex x being pure Element of the generators of G . I st

( x nin (vf t) . I & supp-var g = x & ((supp-term g) . (the_array_sort_of S)) . M = ((@ M),t) <- (@ x) & ( for s being SortSymbol of S

for y being pure Element of the generators of G . I st y in (vf g) . s & ( s = the_array_sort_of S implies y <> M ) holds

((supp-term g) . s) . y = y ) ) ) );

for I being integer SortSymbol of S holds

( { ((@ M) . t) where M is pure Element of the generators of G . (the_array_sort_of S), t is Element of T,I : verum } c= the generators of G . I & ( for M being pure Element of the generators of G . (the_array_sort_of S)

for t being Element of T,I

for g being Element of G,I st g = (@ M) . t holds

ex x being pure Element of the generators of G . I st

( x nin (vf t) . I & supp-var g = x & ((supp-term g) . (the_array_sort_of S)) . M = ((@ M),t) <- (@ x) & ( for s being SortSymbol of S

for y being pure Element of the generators of G . I st y in (vf g) . s & ( s = the_array_sort_of S implies y <> M ) holds

((supp-term g) . s) . y = y ) ) ) );

:: deftheorem defines integer-array AOFA_A01:def 17 :

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T holds

( G is integer-array iff for I being integer SortSymbol of S holds

( { ((@ M) . t) where M is pure Element of the generators of G . (the_array_sort_of S), t is Element of T,I : verum } c= the generators of G . I & ( for M being pure Element of the generators of G . (the_array_sort_of S)

for t being Element of T,I

for g being Element of G,I st g = (@ M) . t holds

ex x being pure Element of the generators of G . I st

( x nin (vf t) . I & supp-var g = x & ((supp-term g) . (the_array_sort_of S)) . M = ((@ M),t) <- (@ x) & ( for s being SortSymbol of S

for y being pure Element of the generators of G . I st y in (vf g) . s & ( s = the_array_sort_of S implies y <> M ) holds

((supp-term g) . s) . y = y ) ) ) ) );

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for G being basic GeneratorSystem over S,X,T holds

( G is integer-array iff for I being integer SortSymbol of S holds

( { ((@ M) . t) where M is pure Element of the generators of G . (the_array_sort_of S), t is Element of T,I : verum } c= the generators of G . I & ( for M being pure Element of the generators of G . (the_array_sort_of S)

for t being Element of T,I

for g being Element of G,I st g = (@ M) . t holds

ex x being pure Element of the generators of G . I st

( x nin (vf t) . I & supp-var g = x & ((supp-term g) . (the_array_sort_of S)) . M = ((@ M),t) <- (@ x) & ( for s being SortSymbol of S

for y being pure Element of the generators of G . I st y in (vf g) . s & ( s = the_array_sort_of S implies y <> M ) holds

((supp-term g) . s) . y = y ) ) ) ) );

theorem Th96: :: AOFA_A01:96

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for M being pure Element of the generators of G . (the_array_sort_of S) st G is integer-array holds

for t being Element of T,I holds (@ M) . t in the generators of G . I

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for M being pure Element of the generators of G . (the_array_sort_of S) st G is integer-array holds

for t being Element of T,I holds (@ M) . t in the generators of G . I

proof end;

definition

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be elementary IfWhileAlgebra of the generators of G;

let a be SortSymbol of S;

let t1, t2 be Element of T,a;

assume A1: t1 in the generators of G . a ;

the assignments of A . [t1,t2] is absolutely-terminating Algorithm of A

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let A be elementary IfWhileAlgebra of the generators of G;

let a be SortSymbol of S;

let t1, t2 be Element of T,a;

assume A1: t1 in the generators of G . a ;

func t1 := (t2,A) -> absolutely-terminating Algorithm of A equals :Def19: :: AOFA_A01:def 19

the assignments of A . [t1,t2];

coherence the assignments of A . [t1,t2];

the assignments of A . [t1,t2] is absolutely-terminating Algorithm of A

proof end;

:: deftheorem Def19 defines := AOFA_A01:def 19 :

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for A being elementary IfWhileAlgebra of the generators of G

for a being SortSymbol of S

for t1, t2 being Element of T,a st t1 in the generators of G . a holds

t1 := (t2,A) = the assignments of A . [t1,t2];

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for G being basic GeneratorSystem over S,X,T

for A being elementary IfWhileAlgebra of the generators of G

for a being SortSymbol of S

for t1, t2 being Element of T,a st t1 in the generators of G . a holds

t1 := (t2,A) = the assignments of A . [t1,t2];

theorem Th97: :: AOFA_A01:97

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for I being integer SortSymbol of S

for X being V3() countable ManySortedSet of the carrier of S

for T being non-empty b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for M being pure Element of the generators of G . (the_array_sort_of S)

for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x

for I being integer SortSymbol of S

for X being V3() countable ManySortedSet of the carrier of S

for T being non-empty b

for G being basic GeneratorSystem over S,X,T

for M being pure Element of the generators of G . (the_array_sort_of S)

for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be disjoint_valued MSAlgebra over S;

coherence

the Sorts of A is disjoint_valued by MSAFREE1:def 2;

end;
let A be disjoint_valued MSAlgebra over S;

coherence

the Sorts of A is disjoint_valued by MSAFREE1:def 2;

definition

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

end;
let X be V3() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

attr T is array-degenerated means :: AOFA_A01:def 20

ex I being integer SortSymbol of S ex M being Element of (FreeGen T) . (the_array_sort_of S) ex t being Element of T,I st (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*>;

ex I being integer SortSymbol of S ex M being Element of (FreeGen T) . (the_array_sort_of S) ex t being Element of T,I st (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*>;

:: deftheorem defines array-degenerated AOFA_A01:def 20 :

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds

( T is array-degenerated iff ex I being integer SortSymbol of S ex M being Element of (FreeGen T) . (the_array_sort_of S) ex t being Element of T,I st (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*> );

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being b

( T is array-degenerated iff ex I being integer SortSymbol of S ex M being Element of (FreeGen T) . (the_array_sort_of S) ex t being Element of T,I st (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*> );

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

coherence

not Free (S,X) is array-degenerated

end;
let X be V3() ManySortedSet of the carrier of S;

coherence

not Free (S,X) is array-degenerated

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

not for b_{1} being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds b_{1} is array-degenerated

end;
let X be V3() ManySortedSet of the carrier of S;

cluster non-empty X,S -terms all_vars_including inheriting_operations free_in_itself disjoint_valued non array-degenerated for MSAlgebra over S;

existence not for b

proof end;

theorem Th98: :: AOFA_A01:98

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds

vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds

vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)

proof end;

theorem Th99: :: AOFA_A01:99

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds

for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for i being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds

for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))

proof end;

registration

let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ;

let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let b be pure Element of the generators of G . the bool-sort of S;

coherence

(s . the bool-sort of S) . b is boolean

end;
let X be V3() ManySortedSet of the carrier of S;

let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S;

let G be basic GeneratorSystem over S,X,T;

let C be bool-correct 4,1 integer 11,1,1 -array image of T;

let s be Element of C -States the generators of G;

let b be pure Element of the generators of G . the bool-sort of S;

coherence

(s . the bool-sort of S) . b is boolean

proof end;

theorem :: AOFA_A01:100

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for y being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for i1, i2 being pure Element of the generators of G . I

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & not T is array-degenerated & X is countable holds

for J being Algorithm of A st ( for s being Element of C -States the generators of G holds

( ((f . (s,J)) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ( for D being array of (#INT,<=#) st D = (s . (the_array_sort_of S)) . M holds

( ( D <> {} implies ( ((f . (s,J)) . I) . i1 in dom D & ((f . (s,J)) . I) . i2 in dom D ) ) & ( inversions D <> {} implies [(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)] in inversions D ) & ( ((f . (s,J)) . the bool-sort of S) . b = TRUE implies inversions D <> {} ) & ( inversions D <> {} implies ((f . (s,J)) . the bool-sort of S) . b = TRUE ) ) ) ) ) holds

for D being finite 0 -based array of (#INT,<=#) st D = (s . (the_array_sort_of S)) . M & y <> i1 & y <> i2 holds

( ((f . (s,(while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))))) . (the_array_sort_of S)) . M is ascending permutation of D & ( J is absolutely-terminating implies while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))) is_terminating_wrt f, { s1 where s1 is Element of C -States the generators of G : (s1 . (the_array_sort_of S)) . M <> {} } ) )

for X being V3() ManySortedSet of the carrier of S

for T being non-empty b

for C being bool-correct 4,1 integer 11,1,1 -array image of T

for G being basic GeneratorSystem over S,X,T

for I being integer SortSymbol of S

for y being pure Element of the generators of G . I

for M being pure Element of the generators of G . (the_array_sort_of S)

for b being pure Element of the generators of G . the bool-sort of S

for s being Element of C -States the generators of G

for i1, i2 being pure Element of the generators of G . I

for A being elementary IfWhileAlgebra of the generators of G

for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & not T is array-degenerated & X is countable holds

for J being Algorithm of A st ( for s being Element of C -States the generators of G holds

( ((f . (s,J)) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M & ( for D being array of (#INT,<=#) st D = (s . (the_array_sort_of S)) . M holds

( ( D <> {} implies ( ((f . (s,J)) . I) . i1 in dom D & ((f . (s,J)) . I) . i2 in dom D ) ) & ( inversions D <> {} implies [(((f . (s,J)) . I) . i1),(((f . (s,J)) . I) . i2)] in inversions D ) & ( ((f . (s,J)) . the bool-sort of S) . b = TRUE implies inversions D <> {} ) & ( inversions D <> {} implies ((f . (s,J)) . the bool-sort of S) . b = TRUE ) ) ) ) ) holds

for D being finite 0 -based array of (#INT,<=#) st D = (s . (the_array_sort_of S)) . M & y <> i1 & y <> i2 holds

( ((f . (s,(while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A))))))) . (the_array_sort_of S)) . M is ascending permutation of D & ( J is absolutely-terminating implies while (J,(((y := (((@ M) . (@ i1)),A)) \; (((@ M) . (@ i1)) := (((@ M) . (@ i2)),A))) \; (((@ M) . (@ i2)) := ((@ y),A)))) is_terminating_wrt f, { s1 where s1 is Element of C -States the generators of G : (s1 . (the_array_sort_of S)) . M <> {} } ) )

proof end;