:: Analysis of Algorithms: An Example of a Sort Algorithm
:: by Grzegorz Bancerek
::
:: Received November 9, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


theorem Th1: :: AOFA_A01:1
( 1 mod 2 = 1 & 2 mod 2 = 0 ) by NAT_D:24, NAT_D:25;

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
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 ) )
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 ) ) )
proof end;

definition
let S be non empty non void bool-correct 4,1 integer BoolSignature ;
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;
end;

:: 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 );

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 #)
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
proof end;

registration
let S be non empty non void bool-correct 4,1 integer BoolSignature ;
cluster non-empty integer for MSAlgebra over S;
existence
ex b1 being non-empty MSAlgebra over S st b1 is integer
proof end;
end;

registration
let S be non empty non void bool-correct 4,1 integer BoolSignature ;
let A be non-empty integer MSAlgebra over S;
cluster non-empty A -Image Equations (S,A) -satisfying bool-correct for MSAlgebra over S;
existence
ex b1 being image of A st b1 is bool-correct
proof end;
end;

registration
let S be non empty non void bool-correct 4,1 integer BoolSignature ;
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 b1 being bool-correct image of A st b1 is 4,1 integer
proof end;
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 )
proof end;

registration
let S be non empty non void bool-correct BoolSignature ;
let A be non-empty bool-correct MSAlgebra over S;
cluster non-empty -> non-empty bool-correct for MSSubAlgebra of A;
coherence
for b1 being non-empty MSSubAlgebra of A holds b1 is bool-correct
proof end;
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;
cluster non-empty -> non-empty 4,1 integer for MSSubAlgebra of A;
coherence
for b1 being non-empty MSSubAlgebra of A holds b1 is 4,1 integer
proof end;
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;
cluster Free (S,X) -> non-empty integer for non-empty MSAlgebra over S;
coherence
for b1 being non-empty MSAlgebra over S st b1 = Free (S,X) holds
b1 is integer
proof end;
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;

registration
let S be non empty non void bool-correct 4,1 integer BoolSignature ;
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 b1 being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st
( b1 is vf-free & b1 is integer )
proof end;
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;
func FreeGen T -> V3() GeneratorSet of T equals :: AOFA_A01:def 2
 FreeGen X;
coherence
FreeGen X is V3() GeneratorSet of T by MSAFREE4:45;
end;

:: 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 b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen T = FreeGen X;

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;
cluster FreeGen T -> V3() Equations (S,T) -free ;
coherence
( FreeGen T is Equations (S,T) -free & FreeGen T is non-empty ) by MSAFREE4:75;
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;
let G be GeneratorSet of T;
attr G is basic means :Def3: :: AOFA_A01:def 3
 FreeGen T c= G;
let s be SortSymbol of S;
let x be Element of G . s;
attr x is pure means :Def4: :: AOFA_A01:def 4
x in (FreeGen T) . s;
end;

:: 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 b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S
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 b2,b1 -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 );

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;
cluster FreeGen T -> V3() basic ;
coherence
FreeGen T is basic ;
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;
cluster non empty Relation-like V3() non empty-yielding the carrier of S -defined Function-like total basic for GeneratorSet of T;
existence
ex b1 being V3() GeneratorSet of T st b1 is basic
proof end;
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;
cluster pure for Element of G . s;
existence
ex b1 being Element of G . s st b1 is pure
proof end;
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 b2,b1 -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 )
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;
attr G is basic means :Def5: :: AOFA_A01:def 5
 the generators of G is basic ;
end;

:: 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 b2,b1 -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 );

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;
cluster basic for GeneratorSystem over S,X,T;
existence
ex b1 being GeneratorSystem over S,X,T st b1 is basic
proof end;
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;
cluster the generators of G -> basic ;
coherence
the generators of G is basic by Def5;
end;

definition
let S be non empty non void bool-correct BoolSignature ;
let A be non-empty MSAlgebra over S;
func \false A -> Element of A, the bool-sort of S equals :: AOFA_A01:def 6
 \not (\true A);
coherence
\not (\true A) is Element of A, the bool-sort of S ;
end;

:: 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);

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 b2,b1 -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
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
proof end;
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;
func @ x -> Element of T,s equals :: AOFA_A01:def 7
x;
coherence
x is Element of T,s
proof end;
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;

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;
func b leq (t1,t2,A) -> Algorithm of A equals :: AOFA_A01:def 8
b := ((leq (t1,t2)),A);
coherence
b := ((leq (t1,t2)),A) is Algorithm of A ;
func b gt (t1,t2,A) -> Algorithm of A equals :: AOFA_A01:def 9
b := ((\not (leq (t1,t2))),A);
coherence
b := ((\not (leq (t1,t2))),A) is Algorithm of A ;
end;

:: 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 b2,b1 -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);

:: 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 b2,b1 -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);

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;
func \2 (T,I) -> Element of T,I equals :: AOFA_A01:def 10
(\1 (T,I)) + (\1 (T,I));
coherence
(\1 (T,I)) + (\1 (T,I)) is Element of T,I ;
end;

:: 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 b2,b1 -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));

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;
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) 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) is Algorithm of A ;
end;

:: 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 b2,b1 -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);

:: 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 b2,b1 -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);

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;
cluster (s . I) . x -> integer ;
coherence
(s . I) . x is integer
proof end;
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;
cluster t value_at (C,s) -> integer ;
coherence
t value_at (C,s) is integer
proof end;
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;
cluster t value_at (C,u) -> integer ;
coherence
t value_at (C,u) is integer
proof end;
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;
cluster t value_at (C,s) -> boolean ;
coherence
t value_at (C,s) is boolean
proof end;
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;
cluster t value_at (C,u) -> boolean ;
coherence
t value_at (C,u) is boolean
proof end;
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 )
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 )
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 )
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 )
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 )
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 )
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 )
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 )
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 )
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 )
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) = {{}}
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)*>
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)*>
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)*>
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)*>
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)*>
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)*>
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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 )
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 b2,b1 -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 )
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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)))
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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 )
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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)))
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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 ) )
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 b2,b1 -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 ) ) )
proof end;

registration
let i, j be Real;
let a, b be boolean object ;
cluster IFGT (i,j,a,b) -> boolean ;
coherence
IFGT (i,j,a,b) is boolean by XXREAL_0:def 11;
end;

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 b2,b1 -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 ) ) )
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;
attr A is elementary means :: AOFA_A01:def 13
 rng the assignments of A c= ElementaryInstructions A;
end;

:: 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 b2,b1 -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 );

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 b2,b1 -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
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;
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 b1 being strict IfWhileAlgebra of the generators of G st b1 is elementary
proof end;
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;
cluster x := (t,A) -> absolutely-terminating ;
coherence
x := (t,A) is absolutely-terminating
proof end;
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 b2,b1 -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 }
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 b2,b1 -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
proof end;

registration
let X be non empty set ;
let f be FinSequence of X ^omega ;
let x be Nat;
cluster f . x -> Relation-like Sequence-like Function-like finite ;
coherence
( f . x is Sequence-like & f . x is finite & f . x is Function-like & f . x is Relation-like )
proof end;
end;

registration
let X be non empty set ;
cluster -> Function-yielding for FinSequence of X ^omega ;
coherence
for b1 being FinSequence of X ^omega holds b1 is Function-yielding ;
end;

registration
let i be Nat;
let f be finite i -based array;
let a, x be set ;
cluster f +* (a,x) -> finite segmental i -based ;
coherence
( f +* (a,x) is i -based & f +* (a,x) is finite & f +* (a,x) is segmental )
proof end;
end;

registration
let X be non empty set ;
let f be X -valued Function;
let a be set ;
let x be Element of X;
cluster f +* (a,x) -> X -valued ;
coherence
f +* (a,x) is X -valued
proof end;
end;

scheme :: AOFA_A01:sch 1
Sch1{ F1() -> non empty set , F2() -> Nat, F3() -> set , F4( set , set , set ) -> set , F5( set ) -> set } :
ex f being FinSequence of F1() ^omega st
( len f = F2() & ( f . 1 = F3() or F2() = 0 ) & ( for i being Nat st 1 <= i & i < F2() holds
f . (i + 1) = F4((f . i),i,F5(i)) ) )
provided
A1: for a being finite 0 -based array of F1()
for i being Nat st 1 <= i & i < F2() holds
for x being Element of F1() holds F4(a,i,x) is finite 0 -based array of F1() and
A2: F3() is finite 0 -based array of F1() and
A3: for i being Nat st i < F2() holds
F5(i) in F1()
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 ) )
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) = {}
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 )
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) ) ) ) ) ) )
proof end;

registration
let a be finite 0 -based array;
cluster len- a -> finite ;
coherence
len- a is finite
proof end;
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;
cluster non-empty -> non-empty 11,1,1 -array for MSSubAlgebra of A;
coherence
for b1 being non-empty MSSubAlgebra of A holds b1 is 11,1,1 -array
proof end;
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;
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;
end;

:: 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 );

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;
cluster Free (S,X) -> non-empty integer-array for non-empty MSAlgebra over S;
coherence
for b1 being non-empty MSAlgebra over S st b1 = Free (S,X) holds
b1 is integer-array
proof end;
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 ;
cluster non-empty integer-array -> non-empty integer for MSAlgebra over S;
coherence
for b1 being non-empty MSAlgebra over S st b1 is integer-array holds
b1 is integer ;
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 b1 being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself strict VarMSAlgebra over S st
( b1 is vf-free & b1 is integer-array )
proof end;
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 ;
cluster non-empty integer-array for MSAlgebra over S;
existence
ex b1 being non-empty MSAlgebra over S st b1 is integer-array
proof end;
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;
cluster non-empty A -Image Equations (S,A) -satisfying bool-correct 4,1 integer 11,1,1 -array for MSAlgebra over S;
existence
ex b1 being bool-correct image of A st
( b1 is 4,1 integer & b1 is 11,1,1 -array )
proof end;
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;
cluster -> Relation-like Function-like for Element of the Sorts of A . (the_array_sort_of S);
coherence
for b1 being Element of the Sorts of A . (the_array_sort_of S) holds
( b1 is Relation-like & b1 is Function-like )
proof end;
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;
cluster -> Sequence-like finite for Element of the Sorts of A . (the_array_sort_of S);
coherence
for b1 being Element of the Sorts of A . (the_array_sort_of S) holds
( b1 is finite & b1 is Sequence-like )
proof end;
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 )
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 )
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 )
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 )
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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)
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 b2,b1 -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)))
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 b2,b1 -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))
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 b2,b1 -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))
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 b2,b1 -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)
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 b2,b1 -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)))
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 b2,b1 -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 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 b1,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 S1[ Nat] means f1 . $1 = f2 . $1;
A3: S1[ 0 ] by A1, A2;
A4: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: S1[i] ; :: thesis: S1[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;
A6: for i being Nat holds S1[i] from NAT_1:sch 2(A3, A4);
now :: thesis: for i being Element of INT holds f1 . i = f2 . i
let i be Element of INT ; :: thesis: f1 . b1 = f2 . b1
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;
suppose ( i = n or ( i = - n & n = 0 ) ) ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = f2 . i by A6; :: thesis: verum
end;
suppose A8: ( i = - n & n <> 0 ) ; :: thesis: f1 . b1 = f2 . b1
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;
end;
end;
hence f1 = f2 ; :: thesis: verum
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 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 b1 being Element of T,I ex f being Function of INT,( the Sorts of T . I) st
( b1 = 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))) ) ) )
proof end;
uniqueness
for b1, b2 being Element of T,I st ex f being Function of INT,( the Sorts of T . I) st
( b1 = 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
( b2 = 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
b1 = b2 by Lm1;
end;

:: 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 b2,b1 -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 b6 being Element of T,I holds
( b6 = ^ (i,T,I) iff ex f being Function of INT,( the Sorts of T . I) st
( b6 = 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))) ) ) ) );

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 b2,b1 -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)
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 b2,b1 -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)) )
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 b2,b1 -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))
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 b2,b1 -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
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;
func M . (i,I) -> Element of T,I equals :: AOFA_A01:def 16
(@ M) . (^ (i,T,I));
coherence
(@ M) . (^ (i,T,I)) is Element of T,I ;
end;

:: 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 b2,b1 -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));

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);
cluster (s . (the_array_sort_of S)) . M -> Relation-like Function-like ;
coherence
( (s . (the_array_sort_of S)) . M is Function-like & (s . (the_array_sort_of S)) . M is Relation-like )
proof end;
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);
cluster (s . (the_array_sort_of S)) . M -> INT -valued Sequence-like finite ;
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;
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);
cluster rng ((s . (the_array_sort_of S)) . M) -> finite integer-membered ;
coherence
( rng ((s . (the_array_sort_of S)) . M) is finite & rng ((s . (the_array_sort_of S)) . M) is integer-membered ) ;
end;

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 b2,b1 -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))
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 b2,b1 -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))
proof end;

registration
let X be non empty set ;
cluster X ^omega -> infinite ;
coherence
not X ^omega is finite
proof end;
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 b2,b1 -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
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 b2,b1 -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
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 b2,b1 -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 <> {} }
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;
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 ) ) ) );
end;

:: 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 b2,b1 -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 ) ) ) ) );

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 b2,b1 -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
proof end;

definition
func (#INT,<=#) -> non empty strict real Poset equals :: AOFA_A01:def 18
 RealPoset INT;
coherence
RealPoset INT is non empty strict real Poset ;
end;

:: deftheorem defines (#INT,<=#) AOFA_A01:def 18 :
(#INT,<=#) = RealPoset INT;

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 ;
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] is absolutely-terminating Algorithm of A
proof end;
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 b2,b1 -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];

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 b3,b1 -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
proof end;

registration
let S be non empty non void ManySortedSign ;
let A be disjoint_valued MSAlgebra over S;
cluster the Sorts of A -> disjoint_valued ;
coherence
the Sorts of A is disjoint_valued by MSAFREE1:def 2;
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 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*>;
end;

:: 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 b2,b1 -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*> );

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;
cluster Free (S,X) -> non array-degenerated ;
coherence
not Free (S,X) is array-degenerated
proof end;
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;
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 b1 being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds b1 is array-degenerated
proof end;
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 b2,b1 -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)
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 b2,b1 -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)))
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;
cluster (s . the bool-sort of S) . b -> boolean ;
coherence
(s . the bool-sort of S) . b is boolean
proof end;
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 b2,b1 -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 <> {} } ) )
proof end;