:: 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 b₁ being non-empty MSAlgebra over S st b₁ 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 b₁ being image of A st b₁ 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 b₁ being bool-correct image of A st b₁ 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 b₁ being non-empty MSSubAlgebra of A holds b₁ 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 b₁ being non-empty MSSubAlgebra of A holds b₁ 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 b₁ being non-empty MSAlgebra over S st b₁ = Free (S,X) holds
b₁ 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 b₁ being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st
( b₁ is vf-free & b₁ 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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₁ being V3() GeneratorSet of T st b₁ 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 b₁ being Element of G . s st b₁ 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 b₂,b₁ -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 b₂,b₁ -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 b₁ being GeneratorSystem over S,X,T st b₁ 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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₁ being strict IfWhileAlgebra of the generators of G st b₁ 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 b₂,b₁ -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 b₂,b₁ -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 b₁ being FinSequence of X ^omega holds b₁ 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{ F₁() -> non empty set , F₂() -> Nat, F₃() -> set , F₄( set , set , set ) -> set , F₅( set ) -> set } :

ex f being FinSequence of F₁() ^omega st
( len f = F₂() & ( f . 1 = F₃() or F₂() = 0 ) & ( for i being Nat st 1 <= i & i < F₂() holds
f . (i + 1) = F₄((f . i),i,F₅(i)) ) )

provided

A1: for a being finite 0 -based array of F₁()
for i being Nat st 1 <= i & i < F₂() holds
for x being Element of F₁() holds F₄(a,i,x) is finite 0 -based array of F₁() and
A2: F₃() is finite 0 -based array of F₁() and
A3: for i being Nat st i < F₂() holds
F₅(i) in F₁()

proof end;

theorem Th71: :: AOFA_A01:71

for S being non empty non void 11,1,1 -array BoolSignature
for J, L being set
for K being SortSymbol of S st the connectives of S . 11 is_of_type <*J,L*>,K holds
( J = the_array_sort_of S & ( for I being integer SortSymbol of S holds the_array_sort_of S <> I ) )

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 b₁ being non-empty MSSubAlgebra of A holds b₁ 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 b₁ being non-empty MSAlgebra over S st b₁ = Free (S,X) holds
b₁ 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 b₁ being non-empty MSAlgebra over S st b₁ is integer-array holds
b₁ 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 b₁ being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself strict VarMSAlgebra over S st
( b₁ is vf-free & b₁ 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 b₁ being non-empty MSAlgebra over S st b₁ 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 b₁ being bool-correct image of A st
( b₁ is 4,1 integer & b₁ 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 b₁ being Element of the Sorts of A . (the_array_sort_of S) holds
( b₁ is Relation-like & b₁ 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 b₁ being Element of the Sorts of A . (the_array_sort_of S) holds
( b₁ is finite & b₁ 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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for I being integer SortSymbol of S
for i being Integer
for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f1 . j = t holds
( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
f1 = f2
let X be V3() ManySortedSet of the carrier of S; :: thesis: for T being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for I being integer SortSymbol of S
for i being Integer
for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f1 . j = t holds
( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
f1 = f2
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis: for I being integer SortSymbol of S
for i being Integer
for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f1 . j = t holds
( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
f1 = f2
let I be integer SortSymbol of S; :: thesis: for i being Integer
for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f1 . j = t holds
( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
f1 = f2
let i be Integer; :: thesis: for f1 being Function of INT,( the Sorts of T . I) st f1 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f1 . j = t holds
( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
f1 = f2
let f1 be Function of INT,( the Sorts of T . I); :: thesis: ( f1 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f1 . j = t holds
( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) implies for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
f1 = f2 )
assume A1: ( f1 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f1 . j = t holds
( f1 . (j + 1) = t + (\1 (T,I)) & f1 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) ; :: thesis: for f2 being Function of INT,( the Sorts of T . I) st f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) holds
f1 = f2
let f2 be Function of INT,( the Sorts of T . I); :: thesis: ( f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) implies f1 = f2 )
assume A2: ( f2 . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f2 . j = t holds
( f2 . (j + 1) = t + (\1 (T,I)) & f2 . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) ; :: thesis: f1 = f2
defpred S₁[ Nat] means f1 . $1 = f2 . $1;
A3: S₁[ 0 ] by A1, A2;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[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 S₁[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 . b₁ = f2 . b₁
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 . b₁ = f2 . b₁

hence f1 . i = f2 . i by A6; :: thesis: verum

end;

suppose A8: ( i = - n & n <> 0 ) ; :: thesis: f1 . b₁ = f2 . b₁

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 b₁ being Element of T,I ex f being Function of INT,( the Sorts of T . I) st
( b₁ = 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 b₁, b₂ being Element of T,I st ex f being Function of INT,( the Sorts of T . I) st
( b₁ = f . i & f . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f . j = t holds
( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) & ex f being Function of INT,( the Sorts of T . I) st
( b₂ = f . i & f . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f . j = t holds
( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) ) holds
b₁ = b₂ 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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for I being integer SortSymbol of S
for i being Integer
for b₆ being Element of T,I holds
( b₆ = ^ (i,T,I) iff ex f being Function of INT,( the Sorts of T . I) st
( b₆ = 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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₃,b₁ -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 b₂,b₁ -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 b₁ being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds b₁ 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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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;