:: Program Algebra over an Algebra
:: by Grzegorz Bancerek
::
:: Copyright (c) 2012-2021 Association of Mizar Users

theorem Th1: :: AOFA_A00:1
for A, B being set
for R being b1 -valued Relation holds R .: B c= A
proof end;

definition
let I be set ;
let f be ManySortedSet of I;
let i be object ;
let x be set ;
:: original: +*
redefine func f +* (i,x) -> ManySortedSet of I;
coherence
f +* (i,x) is ManySortedSet of I
;
end;

registration
let I be set ;
let f be V2() ManySortedSet of I;
let i be object ;
let x be non empty set ;
cluster f +* (i,x) -> V2() ;
coherence
f +* (i,x) is non-empty
proof end;
end;

theorem Th2: :: AOFA_A00:2
for I being set
for f, g being ManySortedSet of I st f c= g holds
f # c= g #
proof end;

theorem :: AOFA_A00:3
for I being non empty set
for J being set
for A, B being ManySortedSet of I st A c= B holds
for f being Function of J,I holds A * f c= B * f
proof end;

registration
let f be Function-yielding Function;
coherence
proof end;
end;

theorem :: AOFA_A00:4
for f, g being Function-yielding Function holds doms (f * g) = (doms f) * g
proof end;

theorem Th5: :: AOFA_A00:5
for x, y being set
for f, g being Function st g = f . x holds
g . y = f .. (x,y)
proof end;

definition
let I be set ;
let i be Element of I;
let x be set ;
func i -singleton x -> ManySortedSet of I equals :: AOFA_A00:def 1
() +* (i,{x});
coherence
() +* (i,{x}) is ManySortedSet of I
;
end;

:: deftheorem defines -singleton AOFA_A00:def 1 :
for I being set
for i being Element of I
for x being set holds i -singleton x = () +* (i,{x});

theorem Th6: :: AOFA_A00:6
for I being non empty set
for i, j being Element of I
for x being set holds
( () . i = {x} & ( i <> j implies () . j = {} ) )
proof end;

theorem :: AOFA_A00:7
for I being non empty set
for i being Element of I
for A being ManySortedSet of I
for x being set st x in A . i holds
i -singleton x is ManySortedSubset of A
proof end;

definition
let I be set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
let i be set ;
assume A1: i in I ;
let j be set ;
assume A2: j in A . i ;
let v be set ;
assume A3: v in B . i ;
func F +* (i,j,v) -> ManySortedFunction of A,B means :: AOFA_A00:def 2
( it . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
it . s = F . s ) );
existence
ex b1 being ManySortedFunction of A,B st
( b1 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b1 . s = F . s ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of A,B st b1 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b1 . s = F . s ) & b2 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b2 . s = F . s ) holds
b1 = b2
proof end;
end;

:: deftheorem defines +* AOFA_A00:def 2 :
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for i being set st i in I holds
for j being set st j in A . i holds
for v being set st v in B . i holds
for b8 being ManySortedFunction of A,B holds
( b8 = F +* (i,j,v) iff ( b8 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b8 . s = F . s ) ) );

canceled;

theorem :: AOFA_A00:8
canceled;

theorem :: AOFA_A00:9
canceled;

theorem :: AOFA_A00:10
canceled;

theorem :: AOFA_A00:11
canceled;

theorem :: AOFA_A00:12
canceled;

::$CD ::$CT 5
theorem :: AOFA_A00:13
for X being set
for a1, a2, a3, a4, a5, a6 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X holds
{a1,a2,a3,a4,a5,a6} c= X by ENUMSET1:def 4;

theorem :: AOFA_A00:14
for X being set
for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X & a7 in X & a8 in X & a9 in X holds
{a1,a2,a3,a4,a5,a6,a7,a8,a9} c= X by ENUMSET1:def 7;

theorem Th10: :: AOFA_A00:15
for X being set
for a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X & a7 in X & a8 in X & a9 in X & a10 in X holds
{a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} c= X by ENUMSET1:def 8;

theorem :: AOFA_A00:16
for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} = {a1,a2,a3,a4,a5,a6,a7,a8,a9}
proof end;

theorem Th12: :: AOFA_A00:17
for a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 being object holds {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} = {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10}
proof end;

theorem Th13: :: AOFA_A00:18
for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds {a1,a2,a3} \/ {a4,a5,a6,a7,a8,a9} = {a1,a2,a3,a4,a5,a6,a7,a8,a9}
proof end;

theorem Th14: :: AOFA_A00:19
for a1, a2, a3, a4 being object st a1 <> a2 & a1 <> a3 & a1 <> a4 & a2 <> a3 & a2 <> a4 & a3 <> a4 holds
<*a1,a2,a3,a4*> is one-to-one
proof end;

definition
let a1, a2, a3, a4, a5, a6 be object ;
func <*a1,a2,a3,a4,a5,a6*> -> FinSequence equals :: AOFA_A00:def 3
<*a1,a2,a3,a4,a5*> ^ <*a6*>;
coherence
<*a1,a2,a3,a4,a5*> ^ <*a6*> is FinSequence
;
end;

:: deftheorem defines <* AOFA_A00:def 3 :
for a1, a2, a3, a4, a5, a6 being object holds <*a1,a2,a3,a4,a5,a6*> = <*a1,a2,a3,a4,a5*> ^ <*a6*>;

definition
let X be non empty set ;
let a1, a2, a3, a4, a5, a6 be Element of X;
:: original: <*
redefine func <*a1,a2,a3,a4,a5,a6*> -> FinSequence of X;
coherence
<*a1,a2,a3,a4,a5,a6*> is FinSequence of X
proof end;
end;

registration
let a1, a2, a3, a4, a5, a6 be object ;
cluster <*a1,a2,a3,a4,a5,a6*> -> 6 -element ;
coherence
<*a1,a2,a3,a4,a5,a6*> is 6 -element
;
end;

theorem :: AOFA_A00:20
for a1, a2, a3, a4, a5, a6 being object
for f being FinSequence holds
( f = <*a1,a2,a3,a4,a5,a6*> iff ( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 ) )
proof end;

theorem :: AOFA_A00:21
for a1, a2, a3, a4, a5, a6 being object holds rng <*a1,a2,a3,a4,a5,a6*> = {a1,a2,a3,a4,a5,a6}
proof end;

definition
let a1, a2, a3, a4, a5, a6, a7 be object ;
func <*a1,a2,a3,a4,a5,a6,a7*> -> FinSequence equals :: AOFA_A00:def 4
<*a1,a2,a3,a4,a5*> ^ <*a6,a7*>;
coherence
<*a1,a2,a3,a4,a5*> ^ <*a6,a7*> is FinSequence
;
end;

:: deftheorem defines <* AOFA_A00:def 4 :
for a1, a2, a3, a4, a5, a6, a7 being object holds <*a1,a2,a3,a4,a5,a6,a7*> = <*a1,a2,a3,a4,a5*> ^ <*a6,a7*>;

definition
let X be non empty set ;
let a1, a2, a3, a4, a5, a6, a7 be Element of X;
:: original: <*
redefine func <*a1,a2,a3,a4,a5,a6,a7*> -> FinSequence of X;
coherence
<*a1,a2,a3,a4,a5,a6,a7*> is FinSequence of X
proof end;
end;

registration
let a1, a2, a3, a4, a5, a6, a7 be object ;
cluster <*a1,a2,a3,a4,a5,a6,a7*> -> 7 -element ;
coherence
<*a1,a2,a3,a4,a5,a6,a7*> is 7 -element
;
end;

theorem :: AOFA_A00:22
for a1, a2, a3, a4, a5, a6, a7 being object
for f being FinSequence holds
( f = <*a1,a2,a3,a4,a5,a6,a7*> iff ( len f = 7 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 ) )
proof end;

theorem :: AOFA_A00:23
for a1, a2, a3, a4, a5, a6, a7 being object holds rng <*a1,a2,a3,a4,a5,a6,a7*> = {a1,a2,a3,a4,a5,a6,a7}
proof end;

definition
let a1, a2, a3, a4, a5, a6, a7, a8 be object ;
func <*a1,a2,a3,a4,a5,a6,a7,a8*> -> FinSequence equals :: AOFA_A00:def 5
<*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*>;
coherence
<*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*> is FinSequence
;
end;

:: deftheorem defines <* AOFA_A00:def 5 :
for a1, a2, a3, a4, a5, a6, a7, a8 being object holds <*a1,a2,a3,a4,a5,a6,a7,a8*> = <*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*>;

definition
let X be non empty set ;
let a1, a2, a3, a4, a5, a6, a7, a8 be Element of X;
:: original: <*
redefine func <*a1,a2,a3,a4,a5,a6,a7,a8*> -> FinSequence of X;
coherence
<*a1,a2,a3,a4,a5,a6,a7,a8*> is FinSequence of X
proof end;
end;

registration
let a1, a2, a3, a4, a5, a6, a7, a8 be object ;
cluster <*a1,a2,a3,a4,a5,a6,a7,a8*> -> 8 -element ;
coherence
<*a1,a2,a3,a4,a5,a6,a7,a8*> is 8 -element
;
end;

theorem Th19: :: AOFA_A00:24
for a1, a2, a3, a4, a5, a6, a7, a8 being object
for f being FinSequence holds
( f = <*a1,a2,a3,a4,a5,a6,a7,a8*> iff ( len f = 8 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 & f . 8 = a8 ) )
proof end;

theorem Th20: :: AOFA_A00:25
for a1, a2, a3, a4, a5, a6, a7, a8 being object holds rng <*a1,a2,a3,a4,a5,a6,a7,a8*> = {a1,a2,a3,a4,a5,a6,a7,a8}
proof end;

theorem Th21: :: AOFA_A00:26
for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds rng (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) = {a1,a2,a3,a4,a5,a6,a7,a8,a9}
proof end;

theorem Th22: :: AOFA_A00:27
Seg 9 = {1,2,3,4,5,6,7,8,9}
proof end;

theorem Th23: :: AOFA_A00:28
Seg 10 = {1,2,3,4,5,6,7,8,9,10}
proof end;

theorem Th24: :: AOFA_A00:29
for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds
( dom (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) = Seg 9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 1 = a1 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 2 = a2 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) . 9 = a9 )
proof end;

theorem Th25: :: AOFA_A00:30
for a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 being object holds
( dom (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) = Seg 10 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 1 = a1 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 2 = a2 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
proof end;

definition
let I, J be set ;
let S be ManySortedSet of I;
mode ManySortedMSSet of S,J -> ManySortedFunction of I means :Def6: :: AOFA_A00:def 6
for i, j being set st i in I holds
( dom (it . i) = S . i & ( j in S . i implies (it . i) . j is ManySortedSet of J ) );
existence
ex b1 being ManySortedFunction of I st
for i, j being set st i in I holds
( dom (b1 . i) = S . i & ( j in S . i implies (b1 . i) . j is ManySortedSet of J ) )
proof end;
end;

:: deftheorem Def6 defines ManySortedMSSet AOFA_A00:def 6 :
for I, J being set
for S being ManySortedSet of I
for b4 being ManySortedFunction of I holds
( b4 is ManySortedMSSet of S,J iff for i, j being set st i in I holds
( dom (b4 . i) = S . i & ( j in S . i implies (b4 . i) . j is ManySortedSet of J ) ) );

definition
let I, J be set ;
let S1 be ManySortedSet of I;
let S2 be ManySortedSet of J;
mode ManySortedMSSet of S1,S2 -> ManySortedMSSet of S1,J means :Def7: :: AOFA_A00:def 7
for i, a being set st i in I & a in S1 . i holds
(it . i) . a is ManySortedSubset of S2;
existence
ex b1 being ManySortedMSSet of S1,J st
for i, a being set st i in I & a in S1 . i holds
(b1 . i) . a is ManySortedSubset of S2
proof end;
end;

:: deftheorem Def7 defines ManySortedMSSet AOFA_A00:def 7 :
for I, J being set
for S1 being ManySortedSet of I
for S2 being ManySortedSet of J
for b5 being ManySortedMSSet of S1,J holds
( b5 is ManySortedMSSet of S1,S2 iff for i, a being set st i in I & a in S1 . i holds
(b5 . i) . a is ManySortedSubset of S2 );

registration
let I be set ;
let X, Y be ManySortedSet of I;
let f be ManySortedMSSet of X,Y;
let x, y be set ;
cluster (f . x) . y -> Relation-like Function-like ;
coherence
( (f . x) . y is Function-like & (f . x) . y is Relation-like )
proof end;
end;

definition
let S be ManySortedSign ;
let o, a be set ;
let r be Element of S;
pred o is_of_type a,r means :: AOFA_A00:def 8
( the Arity of S . o = a & the ResultSort of S . o = r );
end;

:: deftheorem defines is_of_type AOFA_A00:def 8 :
for S being ManySortedSign
for o, a being set
for r being Element of S holds
( o is_of_type a,r iff ( the Arity of S . o = a & the ResultSort of S . o = r ) );

theorem Th26: :: AOFA_A00:31
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for r being SortSymbol of S st o is_of_type {} ,r holds
for A being MSAlgebra over S st the Sorts of A . r <> {} holds
(Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r
proof end;

theorem Th27: :: AOFA_A00:32
for S being non empty non void ManySortedSign
for o, a being set
for r being SortSymbol of S st o is_of_type <*a*>,r holds
for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r
proof end;

theorem Th28: :: AOFA_A00:33
for S being non empty non void ManySortedSign
for o, a, b being set
for r being SortSymbol of S st o is_of_type <*a,b*>,r holds
for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . b <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r
proof end;

theorem Th29: :: AOFA_A00:34
for S being non empty non void ManySortedSign
for o, a, b, c being set
for r being SortSymbol of S st o is_of_type <*a,b,c*>,r holds
for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . b <> {} & the Sorts of A . c <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b
for z being Element of the Sorts of A . c holds (Den ((In (o, the carrier' of S)),A)) . <*x,y,z*> is Element of the Sorts of A . r
proof end;

theorem :: AOFA_A00:35
for S1, S2 being ManySortedSign st ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) holds
for o, a being set
for r1 being Element of S1
for r2 being Element of S2 st r1 = r2 & o is_of_type a,r1 holds
o is_of_type a,r2 ;

definition
let S be non empty non void ManySortedSign ;
attr c2 is strict ;
struct VarMSAlgebra over S -> MSAlgebra over S;
aggr VarMSAlgebra(# Sorts, Charact, free-vars #) -> VarMSAlgebra over S;
sel free-vars c2 -> ManySortedMSSet of the Sorts of c2, the Sorts of c2;
end;

registration
let S be non empty non void ManySortedSign ;
let U be V2() ManySortedSet of the carrier of S;
let C be ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S;
let v be ManySortedMSSet of U,U;
cluster VarMSAlgebra(# U,C,v #) -> non-empty ;
coherence
VarMSAlgebra(# U,C,v #) is non-empty
;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster X,S -terms strict for VarMSAlgebra over S;
existence
ex b1 being strict VarMSAlgebra over S st b1 is X,S -terms
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
existence
ex b1 being VarMSAlgebra over S st
( b1 is non-empty & b1 is disjoint_valued )
proof end;
let X be V2() ManySortedSet of the carrier of S;
cluster X,S -terms all_vars_including -> non-empty X,S -terms for VarMSAlgebra over S;
coherence
for b1 being X,S -terms VarMSAlgebra over S st b1 is all_vars_including holds
b1 is non-empty
;
end;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty VarMSAlgebra over S;
let a be SortSymbol of S;
let t be Element of A,a;
func vf t -> ManySortedSubset of the Sorts of A equals :: AOFA_A00:def 9
( the free-vars of A . a) . t;
coherence
( the free-vars of A . a) . t is ManySortedSubset of the Sorts of A
by Def7;
end;

:: deftheorem defines vf AOFA_A00:def 9 :
for S being non empty non void ManySortedSign
for A being non-empty VarMSAlgebra over S
for a being SortSymbol of S
for t being Element of A,a holds vf t = ( the free-vars of A . a) . t;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty VarMSAlgebra over S;
attr A is vf-correct means :: AOFA_A00:def 10
for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) holds
for b being Element of A, st b = (Den (o,A)) . p holds
for s being SortSymbol of S holds (vf b) . s c= union { ((vf a) . s) where s0 is SortSymbol of S, a is Element of A,s0 : ex i being Nat st
( i in dom () & s0 = () . i & a = p . i )
}
;
end;

:: deftheorem defines vf-correct AOFA_A00:def 10 :
for S being non empty non void ManySortedSign
for A being non-empty VarMSAlgebra over S holds
( A is vf-correct iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) holds
for b being Element of A, st b = (Den (o,A)) . p holds
for s being SortSymbol of S holds (vf b) . s c= union { ((vf a) . s) where s0 is SortSymbol of S, a is Element of A,s0 : ex i being Nat st
( i in dom () & s0 = () . i & a = p . i )
}
);

theorem Th31: :: AOFA_A00:36
for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for G being MSSubset of A
for H being MSSubset of B st G = H holds
GenMSAlg G = GenMSAlg H
proof end;

theorem Th32: :: AOFA_A00:37
for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for G being GeneratorSet of A holds G is GeneratorSet of B
proof end;

theorem Th33: :: AOFA_A00:38
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for G being GeneratorSet of A
for H being GeneratorSet of B st G = H & G is free holds
H is free
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
existence
ex b1 being X,S -terms strict VarMSAlgebra over S st
( b1 is all_vars_including & b1 is inheriting_operations & b1 is free_in_itself )
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
let A be non-empty X,S -terms VarMSAlgebra over S;
attr A is vf-free means :Def11: :: AOFA_A00:def 11
for s, r being SortSymbol of S
for t being Element of A,s holds (vf t) . r = { (t | p) where p is Element of dom t : ((t | p) . {}) 2 = r } ;
end;

:: deftheorem Def11 defines vf-free AOFA_A00:def 11 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being non-empty b2,b1 -terms VarMSAlgebra over S holds
( A is vf-free iff for s, r being SortSymbol of S
for t being Element of A,s holds (vf t) . r = { (t | p) where p is Element of dom t : ((t | p) . {}) 2 = r } );

scheme :: AOFA_A00:sch 1
Scheme{ F1() -> non empty set , F2() -> V2() ManySortedSet of F1(), F3() -> V2() ManySortedSet of F1(), F4( object , object , object ) -> set } :
ex f being ManySortedMSSet of F2(),F3() st
for s, r being Element of F1()
for t being Element of F2() . s holds ((f . s) . t) . r = F4(s,r,t)
provided
A1: for s, r being Element of F1()
for t being Element of F2() . s holds F4(s,r,t) is Subset of (F3() . r)
proof end;

theorem Th34: :: AOFA_A00:39
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being b2,b1 -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st
( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
existence
ex b1 being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st
( b1 is strict & b1 is vf-free )
proof end;
end;

theorem Th35: :: AOFA_A00:40
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S
for s being SortSymbol of S
for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X
proof end;

theorem :: AOFA_A00:41
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b2,b1 -terms all_vars_including vf-free VarMSAlgebra over S
for s being SortSymbol of S
for x being Element of A,s st x in () . s holds
vf x = s -singleton x
proof end;

definition
let I be set ;
let S be ManySortedSet of I;
mode ManySortedElement of S -> ManySortedSet of I means :: AOFA_A00:def 12
for i being set st i in I holds
it . i is Element of S . i;
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is Element of S . i
proof end;
end;

:: deftheorem defines ManySortedElement AOFA_A00:def 12 :
for I being set
for S, b3 being ManySortedSet of I holds
( b3 is ManySortedElement of S iff for i being set st i in I holds
b3 . i is Element of S . i );

definition
let S be non empty non void ManySortedSign ;
attr c2 is strict ;
struct UndefMSAlgebra over S -> MSAlgebra over S;
aggr UndefMSAlgebra(# Sorts, Charact, undefined-map #) -> UndefMSAlgebra over S;
sel undefined-map c2 -> ManySortedElement of the Sorts of c2;
end;

definition
let S be non empty non void ManySortedSign ;
let A be UndefMSAlgebra over S;
let s be SortSymbol of S;
let a be Element of A,s;
attr a is undefined means :: AOFA_A00:def 13
a = the undefined-map of A . s;
end;

:: deftheorem defines undefined AOFA_A00:def 13 :
for S being non empty non void ManySortedSign
for A being UndefMSAlgebra over S
for s being SortSymbol of S
for a being Element of A,s holds
( a is undefined iff a = the undefined-map of A . s );

definition
let S be non empty non void ManySortedSign ;
let A be UndefMSAlgebra over S;
attr A is undef-consequent means :: AOFA_A00:def 14
for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) & ex i being Nat ex s being SortSymbol of S ex a being Element of A,s st
( i in dom () & s = () . i & a = p . i & a is undefined ) holds
for b being Element of A, st b = (Den (o,A)) . p holds
b is undefined ;
end;

:: deftheorem defines undef-consequent AOFA_A00:def 14 :
for S being non empty non void ManySortedSign
for A being UndefMSAlgebra over S holds
( A is undef-consequent iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) & ex i being Nat ex s being SortSymbol of S ex a being Element of A,s st
( i in dom () & s = () . i & a = p . i & a is undefined ) holds
for b being Element of A, st b = (Den (o,A)) . p holds
b is undefined );

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let B be UndefMSAlgebra over S;
attr B is A -undef means :: AOFA_A00:def 15
( B is undef-consequent & the undefined-map of B = the Sorts of A & ( for s being SortSymbol of S holds the Sorts of B . s = succ ( the Sorts of A . s) ) & ( for o being OperSymbol of S
for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds
(Den (o,B)) . a = the undefined-map of B . ) );
end;

:: deftheorem defines -undef AOFA_A00:def 15 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for B being UndefMSAlgebra over S holds
( B is A -undef iff ( B is undef-consequent & the undefined-map of B = the Sorts of A & ( for s being SortSymbol of S holds the Sorts of B . s = succ ( the Sorts of A . s) ) & ( for o being OperSymbol of S
for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds
(Den (o,B)) . a = the undefined-map of B . ) ) );

registration
let S be non empty ManySortedSign ;
let A be MSAlgebra over S;
cluster the Charact of A -> Function-yielding ;
coherence
the Charact of A is Function-yielding
;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster A -undef -> undef-consequent for UndefMSAlgebra over S;
coherence
for b1 being UndefMSAlgebra over S st b1 is A -undef holds
b1 is undef-consequent
;
existence
ex b1 being strict UndefMSAlgebra over S st
( b1 is A -undef & b1 is non-empty )
proof end;
end;

definition
let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
attr c4 is strict ;
struct ProgramAlgStr over J,T,X -> UAStr ;
aggr ProgramAlgStr(# carrier, charact, assignments #) -> ProgramAlgStr over J,T,X;
sel assignments c4 -> Function of (Union [|X, the Sorts of T|]), the carrier of c4;
end;

definition
let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
let A be ProgramAlgStr over J,T,X;
attr A is disjoint_valued means :: AOFA_A00:def 16
( the Sorts of T is disjoint_valued & the assignments of A is one-to-one );
end;

:: deftheorem defines disjoint_valued AOFA_A00:def 16 :
for J being non empty non void ManySortedSign
for T being MSAlgebra over J
for X being GeneratorSet of T
for A being ProgramAlgStr over J,T,X holds
( A is disjoint_valued iff ( the Sorts of T is disjoint_valued & the assignments of A is one-to-one ) );

registration
let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
existence
ex b1 being strict ProgramAlgStr over J,T,X st
( b1 is partial & b1 is quasi_total & b1 is non-empty )
proof end;
end;

registration
let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
existence
ex b1 being non empty partial quasi_total non-empty strict ProgramAlgStr over J,T,X st
( b1 is with_empty-instruction & b1 is with_catenation & b1 is with_if-instruction & b1 is with_while-instruction )
proof end;
end;

theorem :: AOFA_A00:42
for U1, U2 being preIfWhileAlgebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
( EmptyIns U1 = EmptyIns U2 & ( for I1, J1 being Element of U1
for I2, J2 being Element of U2 st I1 = I2 & J1 = J2 holds
( I1 \; J1 = I2 \; J2 & while (I1,J1) = while (I2,J2) & ( for C1 being Element of U1
for C2 being Element of U2 st C1 = C2 holds
if-then-else (C1,I1,J1) = if-then-else (C2,I2,J2) ) ) ) ) ;

theorem Th38: :: AOFA_A00:43
for U1, U2 being preIfWhileAlgebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
ElementaryInstructions U1 = ElementaryInstructions U2
proof end;

theorem Th39: :: AOFA_A00:44
for U1, U2 being Universal_Algebra
for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2
proof end;

theorem Th40: :: AOFA_A00:45
for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 & S1 is opers_closed holds
S2 is opers_closed
proof end;

theorem Th41: :: AOFA_A00:46
for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for G being GeneratorSet of U1 holds G is GeneratorSet of U2
proof end;

theorem Th42: :: AOFA_A00:47
for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
signature U1 = signature U2
proof end;

registration
let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
existence
ex b1 being non empty partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction strict ProgramAlgStr over J,T,X st
( not b1 is degenerated & b1 is well_founded & b1 is ECIW-strict & b1 is infinite )
proof end;
end;

definition
let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
mode preIfWhileAlgebra of X is non empty partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction ProgramAlgStr over J,T,X;
end;

definition
let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
mode IfWhileAlgebra of X is non degenerated well_founded ECIW-strict preIfWhileAlgebra of X;
end;

definition
let J be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over J;
let X be V2() GeneratorSet of T;
let A be non empty ProgramAlgStr over J,T,X;
let a be SortSymbol of J;
let x be Element of X . a;
let t be Element of T,a;
func x := (t,A) -> Algorithm of A equals :: AOFA_A00:def 17
the assignments of A . [x,t];
coherence
the assignments of A . [x,t] is Algorithm of A
proof end;
end;

:: deftheorem defines := AOFA_A00:def 17 :
for J being non empty non void ManySortedSign
for T being non-empty MSAlgebra over J
for X being V2() GeneratorSet of T
for A being non empty ProgramAlgStr over J,T,X
for a being SortSymbol of J
for x being Element of X . a
for t being Element of T,a holds x := (t,A) = the assignments of A . [x,t];

registration
let S be set ;
let T be V2() disjoint_valued ManySortedSet of S;
existence
not for b1 being ManySortedSubset of T holds b1 is V2()
proof end;
end;

definition
let J be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over J;
let X be V2() GeneratorSet of T;
func C -States X -> Subset of (MSFuncs (X, the Sorts of C)) means :Def18: :: AOFA_A00:def 18
for s being ManySortedFunction of X, the Sorts of C holds
( s in it iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) );
existence
ex b1 being Subset of (MSFuncs (X, the Sorts of C)) st
for s being ManySortedFunction of X, the Sorts of C holds
( s in b1 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) )
proof end;
uniqueness
for b1, b2 being Subset of (MSFuncs (X, the Sorts of C)) st ( for s being ManySortedFunction of X, the Sorts of C holds
( s in b1 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds
( s in b2 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines -States AOFA_A00:def 18 :
for J being non empty non void ManySortedSign
for T, C being non-empty MSAlgebra over J
for X being V2() GeneratorSet of T
for b5 being Subset of (MSFuncs (X, the Sorts of C)) holds
( b5 = C -States X iff for s being ManySortedFunction of X, the Sorts of C holds
( s in b5 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) );

registration
let J be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over J;
let C be image of T;
let X be V2() GeneratorSet of T;
cluster C -States X -> non empty ;
coherence
not C -States X is empty
proof end;
end;

theorem Th43: :: AOFA_A00:48
for B being non empty non void ManySortedSign
for T, C being non-empty MSAlgebra over B
for X being V2() GeneratorSet of T
for g being set st g in C -States X holds
g is ManySortedFunction of X, the Sorts of C
proof end;

registration
let B be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;
coherence
for b1 being Element of C -States X holds
( b1 is Relation-like & b1 is Function-like )
proof end;
end;

registration
let B be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;
cluster -> the carrier of B -defined Function-yielding for Element of C -States X;
coherence
for b1 being Element of C -States X holds
( b1 is Function-yielding & b1 is the carrier of B -defined )
proof end;
end;

registration
let B be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over B;
let C be image of T;
let X be V2() GeneratorSet of T;
cluster -> total for Element of C -States X;
coherence
for b1 being Element of C -States X holds b1 is total
by Th43;
end;

definition
let B be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;
let a be SortSymbol of B;
let x be Element of X . a;
let f be Element of C,a;
func f -States (X,x) -> Subset of (C -States X) means :: AOFA_A00:def 19
for s being ManySortedFunction of X, the Sorts of C holds
( s in it iff ( s in C -States X & (s . a) . x <> f ) );
existence
ex b1 being Subset of (C -States X) st
for s being ManySortedFunction of X, the Sorts of C holds
( s in b1 iff ( s in C -States X & (s . a) . x <> f ) )
proof end;
uniqueness
for b1, b2 being Subset of (C -States X) st ( for s being ManySortedFunction of X, the Sorts of C holds
( s in b1 iff ( s in C -States X & (s . a) . x <> f ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds
( s in b2 iff ( s in C -States X & (s . a) . x <> f ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines -States AOFA_A00:def 19 :
for B being non empty non void ManySortedSign
for T, C being non-empty MSAlgebra over B
for X being V2() GeneratorSet of T
for a being SortSymbol of B
for x being Element of X . a
for f being Element of C,a
for b8 being Subset of (C -States X) holds
( b8 = f -States (X,x) iff for s being ManySortedFunction of X, the Sorts of C holds
( s in b8 iff ( s in C -States X & (s . a) . x <> f ) ) );

registration
let B be non empty non void ManySortedSign ;
let T be non-empty free MSAlgebra over B;
let C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;
cluster C -States X -> non empty ;
coherence
not C -States X is empty
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let o be OperSymbol of S;
cluster -> Relation-like Function-like for Element of Args (o,A);
coherence
for b1 being Element of Args (o,A) holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let B be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of B;
let T be non-empty X,B -terms MSAlgebra over B;
let C be image of T;
let G be V2() GeneratorSet of T;
cluster C -States G -> non empty ;
coherence
not C -States G is empty
;
end;

definition
let B be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of B;
let T be non-empty X,B -terms MSAlgebra over B;
let C be image of T;
let a be SortSymbol of B;
let t be Element of T,a;
let s be Function-yielding Function;
given h being ManySortedFunction of T,C, Q being GeneratorSet of T such that A1: ( h is_homomorphism T,C & Q = doms s & s = h || Q ) ;
func t value_at (C,s) -> Element of C,a means :: AOFA_A00:def 20
ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & it = (f . a) . t );
existence
ex b1 being Element of C,a ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & b1 = (f . a) . t )
proof end;
uniqueness
for b1, b2 being Element of C,a st ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & b1 = (f . a) . t ) & ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & b2 = (f . a) . t ) holds
b1 = b2
by EXTENS_1:19;
end;

:: deftheorem defines value_at AOFA_A00:def 20 :
for B being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of B
for T being non-empty b2,b1 -terms MSAlgebra over B
for C being image of T
for a being SortSymbol of B
for t being Element of T,a
for s being Function-yielding Function st ex h being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( h is_homomorphism T,C & Q = doms s & s = h || Q ) holds
for b8 being Element of C,a holds
( b8 = t value_at (C,s) iff ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & b8 = (f . a) . t ) );

definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;
attr c4 is strict ;
struct GeneratorSystem over S,X,T -> ;
aggr GeneratorSystem(# generators, supported-var, supported-term #) -> GeneratorSystem over S,X,T;
sel generators c4 -> V2() GeneratorSet of T;
sel supported-var c4 -> ManySortedFunction of the generators of c4, FreeGen X;
sel supported-term c4 -> ManySortedMSSet of the generators of c4, the carrier of S;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet 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 s be SortSymbol of S;
mode Element of G,s -> Element of T,s means :Def21: :: AOFA_A00:def 21
it in the generators of G . s;
existence
ex b1 being Element of T,s st b1 in the generators of G . s
proof end;
end;

:: deftheorem Def21 defines Element AOFA_A00:def 21 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for T being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSystem over S,X,T
for s being SortSymbol of S
for b6 being Element of T,s holds
( b6 is Element of G,s iff b6 in the generators of G . s );

definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet 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 s be SortSymbol of S;
func G . s -> Component of the generators of G equals :: AOFA_A00:def 22
the generators of G . s;
coherence
the generators of G . s is Component of the generators of G
;
let g be Element of G,s;
func supp-var g -> Element of () . s equals :: AOFA_A00:def 23
( the supported-var of G . s) . g;
coherence
( the supported-var of G . s) . g is Element of () . s
by ;
end;

:: deftheorem defines . AOFA_A00:def 22 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for T being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSystem over S,X,T
for s being SortSymbol of S holds G . s = the generators of G . s;

:: deftheorem defines supp-var AOFA_A00:def 23 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for T being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSystem over S,X,T
for s being SortSymbol of S
for g being Element of G,s holds supp-var g = ( the supported-var of G . s) . g;

definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S;
let G be GeneratorSystem over S,X,T;
let s be SortSymbol of S;
let g be Element of G,s;
assume A1: ( the supported-term of G . s) . g is ManySortedFunction of vf g, the Sorts of T ;
func supp-term g -> ManySortedFunction of vf g, the Sorts of T equals :: AOFA_A00:def 24
( the supported-term of G . s) . g;
coherence
( the supported-term of G . s) . g is ManySortedFunction of vf g, the Sorts of T
by A1;
end;

:: deftheorem defines supp-term AOFA_A00:def 24 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for T being b2,b1 -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S
for G being GeneratorSystem over S,X,T
for s being SortSymbol of S
for g being Element of G,s st ( the supported-term of G . s) . g is ManySortedFunction of vf g, the Sorts of T holds
supp-term g = ( the supported-term of G . s) . g;

definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S;
let C be image of T;
let G be GeneratorSystem over S,X,T;
attr G is C -supported means :: AOFA_A00:def 25
( FreeGen X is ManySortedSubset of the generators of G & ( for s being SortSymbol of S holds
( dom ( the supported-term of G . s) = G . s & ( for t being Element of G,s holds
( ( the supported-term of G . s) . t is ManySortedFunction of vf t, the Sorts of T & ( t in () . s implies ( supp-term t = id () & supp-var t = t ) ) & ( for v being Element of C -States the generators of G st (v . s) . () = (v . s) . t holds
for r being SortSymbol of S
for x being Element of () . r
for q being Element of the Sorts of T . r st x in (vf t) . r & q = (() . r) . x holds
(v . r) . x = q value_at (C,v) ) & ( t nin () . s implies for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for v being Element of C,s
for f being ManySortedFunction of the generators of G, the Sorts of C st f in C -States the generators of G holds
for u being ManySortedFunction of FreeGen X, the Sorts of C st ( for a being SortSymbol of S
for z being Element of () . a st z in (vf t) . a holds
for q being Element of T,a st q = (() . a) . z holds
(u . a) . z = q value_at (C,((f || H) +* (s,(),v))) ) holds
for H being ManySortedSubset of the Sorts of T st H = FreeGen X holds
for h being ManySortedFunction of T,C st h is_homomorphism T,C & h || H = u holds
v = (h . s) . t ) ) ) ) ) );
end;

:: deftheorem defines -supported AOFA_A00:def 25 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for T being b2,b1 -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S
for C being image of T
for G being GeneratorSystem over S,X,T holds
( G is C -supported iff ( FreeGen X is ManySortedSubset of the generators of G & ( for s being SortSymbol of S holds
( dom ( the supported-term of G . s) = G . s & ( for t being Element of G,s holds
( ( the supported-term of G . s) . t is ManySortedFunction of vf t, the Sorts of T & ( t in () . s implies ( supp-term t = id () & supp-var t = t ) ) & ( for v being Element of C -States the generators of G st (v . s) . () = (v . s) . t holds
for r being SortSymbol of S
for x being Element of () . r
for q being Element of the Sorts of T . r st x in (vf t) . r & q = (() . r) . x holds
(v . r) . x = q value_at (C,v) ) & ( t nin () . s implies for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for v being Element of C,s
for f being ManySortedFunction of the generators of G, the Sorts of C st f in C -States the generators of G holds
for u being ManySortedFunction of FreeGen X, the Sorts of C st ( for a being SortSymbol of S
for z being Element of () . a st z in (vf t) . a holds
for q being Element of T,a st q = (() . a) . z holds
(u . a) . z = q value_at (C,((f || H) +* (s,(),v))) ) holds
for H being ManySortedSubset of the Sorts of T st H = FreeGen X holds
for h being ManySortedFunction of T,C st h is_homomorphism T,C & h || H = u holds
v = (h . s) . t ) ) ) ) ) ) );

definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of S;
let A be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S;
let C be image of A;
let G be GeneratorSystem over S,X,A;
assume A1: G is C -supported ;
let s be Element of C -States the generators of G;
let r be SortSymbol of S;
let v be Element of C,r;
let t be Element of G,r;
func succ (s,t,v) -> Element of C -States the generators of G means :: AOFA_A00:def 26
( (it . r) . t = v & ( for p being SortSymbol of S
for x being Element of () . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (it . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(),v) & x in (vf t) . p holds
for q being Element of A,p st q = (() . p) . x holds
(it . p) . x = q value_at (C,u) ) ) ) );
existence
ex b1 being Element of C -States the generators of G st
( (b1 . r) . t = v & ( for p being SortSymbol of S
for x being Element of () . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (b1 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(),v) & x in (vf t) . p holds
for q being Element of A,p st q = (() . p) . x holds
(b1 . p) . x = q value_at (C,u) ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of C -States the generators of G st (b1 . r) . t = v & ( for p being SortSymbol of S
for x being Element of () . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (b1 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(),v) & x in (vf t) . p holds
for q being Element of A,p st q = (() . p) . x holds
(b1 . p) . x = q value_at (C,u) ) ) ) & (b2 . r) . t = v & ( for p being SortSymbol of S
for x being Element of () . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (b2 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(),v) & x in (vf t) . p holds
for q being Element of A,p st q = (() . p) . x holds
(b2 . p) . x = q value_at (C,u) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines succ AOFA_A00:def 26 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for A being b2,b1 -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S
for C being image of A
for G being GeneratorSystem over S,X,A st G is C -supported holds
for s being Element of C -States the generators of G
for r being SortSymbol of S
for v being Element of C,r
for t being Element of G,r
for b10 being Element of C -States the generators of G holds
( b10 = succ (s,t,v) iff ( (b10 . r) . t = v & ( for p being SortSymbol of S
for x being Element of () . p st ( p = r implies x <> t ) holds
( ( x nin (vf t) . p implies (b10 . p) . x = (s . p) . x ) & ( for u being ManySortedFunction of FreeGen X, the Sorts of C
for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for f being ManySortedFunction of the generators of G, the Sorts of C st f = s & u = (f || H) +* (r,(),v) & x in (vf t) . p holds
for q being Element of A,p st q = (() . p) . x holds
(b10 . p) . x = q value_at (C,u) ) ) ) ) );

definition
let B be non empty non void ManySortedSign ;
let Y be V2() ManySortedSet of the carrier of B;
let T be Y,B -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over B;
let C be image of T;
let X be GeneratorSystem over B,Y,T;
let A be preIfWhileAlgebra of the generators of X;
let a be SortSymbol of B;
let x be Element of the generators of X . a;
let z be Element of C,a;
func C -Execution (A,x,z) -> Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) means :: AOFA_A00:def 27
for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in it iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) );
existence
ex b1 being Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) st
for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in b1 iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) st ( for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in b1 iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) ) ) & ( for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in b2 iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines -Execution AOFA_A00:def 27 :
for B being non empty non void ManySortedSign
for Y being V2() ManySortedSet of the carrier of B
for T being b2,b1 -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over B
for C being image of T
for X being GeneratorSystem over B,Y,T
for A being preIfWhileAlgebra of the generators of X
for a being SortSymbol of B
for x being Element of the generators of X . a
for z being Element of C,a
for b10 being Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) holds
( b10 = C -Execution (A,x,z) iff for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in b10 iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) ) );

definition end;

definition
let S be ConnectivesSignature ;
attr S is 1-1-connectives means :Def28: :: AOFA_A00:def 28
the connectives of S is one-to-one ;
end;

:: deftheorem Def28 defines 1-1-connectives AOFA_A00:def 28 :
for S being ConnectivesSignature holds
( S is 1-1-connectives iff the connectives of S is one-to-one );

definition
let n be Nat;
let S be ConnectivesSignature ;
attr S is n -connectives means :Def29: :: AOFA_A00:def 29
len the connectives of S = n;
end;

:: deftheorem Def29 defines -connectives AOFA_A00:def 29 :
for n being Nat
for S being ConnectivesSignature holds
( S is n -connectives iff len the connectives of S = n );

registration
let n be Nat;
existence
ex b1 being strict ConnectivesSignature st
( b1 is n -connectives & not b1 is empty & not b1 is void )
proof end;
end;

definition end;

registration
let n be Nat;
existence
ex b1 being strict BoolSignature st
( b1 is n -connectives & not b1 is empty & not b1 is void )
proof end;
end;

definition
let B be BoolSignature ;
attr B is bool-correct means :Def30: :: AOFA_A00:def 30
( len the connectives of B >= 3 & the connectives of B . 1 is_of_type {} , the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B );
end;

:: deftheorem Def30 defines bool-correct AOFA_A00:def 30 :
for B being BoolSignature holds
( B is bool-correct iff ( len the connectives of B >= 3 & the connectives of B . 1 is_of_type {} , the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B ) );

registration
existence
ex b1 being strict BoolSignature st
( b1 is 3 -connectives & b1 is 1-1-connectives & b1 is bool-correct & not b1 is empty & not b1 is void )
proof end;
end;

registration
existence
ex b1 being ConnectivesSignature st
( b1 is 1-1-connectives & not b1 is empty & not b1 is void )
proof end;
end;

registration
let S be non empty non void 1-1-connectives ConnectivesSignature ;
cluster the connectives of S -> one-to-one ;
coherence
the connectives of S is one-to-one
by Def28;
end;

definition
let S be non empty non void BoolSignature ;
let B be MSAlgebra over S;
attr B is bool-correct means :Def31: :: AOFA_A00:def 31
( the Sorts of B . the bool-sort of S = BOOLEAN & (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> = x '&' y ) ) );
end;

:: deftheorem Def31 defines bool-correct AOFA_A00:def 31 :
for S being non empty non void BoolSignature
for B being MSAlgebra over S holds
( B is bool-correct iff ( the Sorts of B . the bool-sort of S = BOOLEAN & (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> = x '&' y ) ) ) );

theorem Th44: :: AOFA_A00:49
for A being non empty set
for n being Nat
for f being Function of (),A holds
( f is non empty homogeneous quasi_total PartFunc of (A *),A & ( for g being homogeneous Function st f = g holds
g is n -ary ) )
proof end;

registration
let A be non empty set ;
let n be Nat;
existence
ex b1 being non empty homogeneous quasi_total PartFunc of (A *),A st b1 is n -ary
proof end;
end;

scheme :: AOFA_A00:sch 2
Sch1{ F1() -> non empty set , F2( set ) -> Element of F1() } :
ex f being non empty homogeneous quasi_total 1 -ary PartFunc of (F1() *),F1() st
for a being Element of F1() holds f . <*a*> = F2(a)
proof end;

scheme :: AOFA_A00:sch 3
Sch2{ F1() -> non empty set , F2( set , set ) -> Element of F1() } :
ex f being non empty homogeneous quasi_total 2 -ary PartFunc of (F1() *),F1() st
for a, b being Element of F1() holds f . <*a,b*> = F2(a,b)
proof end;

theorem Th45: :: AOFA_A00:50
for S being non empty non void ManySortedSign
for A being V2() ManySortedSet of the carrier of S
for f being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
for o being OperSymbol of S
for d being Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) holds f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
proof end;

theorem Th46: :: AOFA_A00:51
for S being non empty non void bool-correct BoolSignature
for A being V2() ManySortedSet of the carrier of S ex B being strict non-empty MSAlgebra over S st
( the Sorts of B = A +* ( the bool-sort of S,BOOLEAN) & B is bool-correct )
proof end;

registration
let S be non empty non void bool-correct BoolSignature ;
existence
ex b1 being strict MSAlgebra over S st
( b1 is bool-correct & b1 is non-empty )
proof end;
end;

definition
let S be non empty non void bool-correct BoolSignature ;
let B be non-empty MSAlgebra over S;
set f = the bool-sort of S;
set L = B;
A1: the connectives of S . 1 is_of_type {} , the bool-sort of S by Def30;
A2: the connectives of S . 2 is_of_type <* the bool-sort of S*>, the bool-sort of S by Def30;
A3: the connectives of S . 3 is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S by Def30;
A4: len the connectives of S >= 3 by Def30;
then ( 1 <= len the connectives of S & 2 <= len the connectives of S ) by XXREAL_0:2;
then A5: ( 2 in dom the connectives of S & 1 in dom the connectives of S & 3 in dom the connectives of S ) by ;
A6: ( the connectives of S . 1 in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by ;
func \true B -> Element of B, the bool-sort of S equals :: AOFA_A00:def 32
(Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {};
coherence
(Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} is Element of B, the bool-sort of S
by A1, Th26, A6;
let p be Element of B, the bool-sort of S;
func \not p -> Element of B, the bool-sort of S equals :: AOFA_A00:def 33
(Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*p*>;
coherence
(Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*p*> is Element of B, the bool-sort of S
by ;
let q be Element of B, the bool-sort of S;
func p \and q -> Element of B, the bool-sort of S equals :: AOFA_A00:def 34
(Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*p,q*>;
coherence
(Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*p,q*> is Element of B, the bool-sort of S
by ;
end;

:: deftheorem defines \true AOFA_A00:def 32 :
for S being non empty non void bool-correct BoolSignature
for B being non-empty MSAlgebra over S holds \true B = (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {};

:: deftheorem defines \not AOFA_A00:def 33 :
for S being non empty non void bool-correct BoolSignature
for B being non-empty MSAlgebra over S
for p being Element of B, the bool-sort of S holds \not p = (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*p*>;

:: deftheorem defines \and AOFA_A00:def 34 :
for S being non empty non void bool-correct BoolSignature
for B being non-empty MSAlgebra over S
for p, q being Element of B, the bool-sort of S holds p \and q = (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*p,q*>;

definition
let S be non empty non void bool-correct BoolSignature ;
let B be non-empty MSAlgebra over S;
let p, q be Element of B, the bool-sort of S;
func p \or q -> Element of B, the bool-sort of S equals :: AOFA_A00:def 35
\not ((\not p) \and (\not q));
coherence
\not ((\not p) \and (\not q)) is Element of B, the bool-sort of S
;
func p \imp q -> Element of B, the bool-sort of S equals :: AOFA_A00:def 36
\not (p \and (\not q));
coherence
\not (p \and (\not q)) is Element of B, the bool-sort of S
;
end;

:: deftheorem defines \or AOFA_A00:def 35 :
for S being non empty non void bool-correct BoolSignature
for B being non-empty MSAlgebra over S
for p, q being Element of B, the bool-sort of S holds p \or q = \not ((\not p) \and (\not q));

:: deftheorem defines \imp AOFA_A00:def 36 :
for S being non empty non void bool-correct BoolSignature
for B being non-empty MSAlgebra over S
for p, q being Element of B, the bool-sort of S holds p \imp q = \not (p \and (\not q));

definition
let S be non empty non void bool-correct BoolSignature ;
let B be non-empty MSAlgebra over S;
let p, q be Element of B, the bool-sort of S;
func p \iff q -> Element of B, the bool-sort of S equals :: AOFA_A00:def 37
(p \and q) \or ((\not p) \and (\not q));
coherence
(p \and q) \or ((\not p) \and (\not q)) is Element of B, the bool-sort of S
;
end;

:: deftheorem defines \iff AOFA_A00:def 37 :
for S being non empty non void bool-correct BoolSignature
for B being non-empty MSAlgebra over S
for p, q being Element of B, the bool-sort of S holds p \iff q = (p \and q) \or ((\not p) \and (\not q));

definition
let i be Nat;
let s be set ;
let S be BoolSignature ;
attr S is i,s integer means :Def38: :: AOFA_A00:def 38
( len the connectives of S >= i + 6 & ex I being Element of S st
( I = s & I <> the bool-sort of S & the connectives of S . i is_of_type {} ,I & the connectives of S . (i + 1) is_of_type {} ,I & the connectives of S . i <> the connectives of S . (i + 1) & the connectives of S . (i + 2) is_of_type <*I*>,I & the connectives of S . (i + 3) is_of_type <*I,I*>,I & the connectives of S . (i + 4) is_of_type <*I,I*>,I & the connectives of S . (i + 5) is_of_type <*I,I*>,I & the connectives of S . (i + 3) <> the connectives of S . (i + 4) & the connectives of S . (i + 3) <> the connectives of S . (i + 5) & the connectives of S . (i + 4) <> the connectives of S . (i + 5) & the connectives of S . (i + 6) is_of_type <*I,I*>, the bool-sort of S ) );
end;

:: deftheorem Def38 defines integer AOFA_A00:def 38 :
for i being Nat
for s being set
for S being BoolSignature holds
( S is i,s integer iff ( len the connectives of S >= i + 6 & ex I being Element of S st
( I = s & I <> the bool-sort of S & the connectives of S . i is_of_type {} ,I & the connectives of S . (i + 1) is_of_type {} ,I & the connectives of S . i <> the connectives of S . (i + 1) & the connectives of S . (i + 2) is_of_type <*I*>,I & the connectives of S . (i + 3) is_of_type <*I,I*>,I & the connectives of S . (i + 4) is_of_type <*I,I*>,I & the connectives of S . (i + 5) is_of_type <*I,I*>,I & the connectives of S . (i + 3) <> the connectives of S . (i + 4) & the connectives of S . (i + 3) <> the connectives of S . (i + 5) & the connectives of S . (i + 4) <> the connectives of S . (i + 5) & the connectives of S . (i + 6) is_of_type <*I,I*>, the bool-sort of S ) ) );

theorem Th47: :: AOFA_A00:52
ex S being non empty non void 10 -connectives strict BoolSignature st
( S is 1-1-connectives & S is 4,1 integer & S is bool-correct & the carrier of S = {0,1} & ex I being SortSymbol of S st
( I = 1 & the connectives of S . 4 is_of_type {} ,I ) )
proof end;

registration
existence
ex b1 being strict BoolSignature st
( b1 is 10 -connectives & b1 is 1-1-connectives & b1 is 4,1 integer & b1 is bool-correct & not b1 is empty & not b1 is void )
by Th47;
end;

definition
let S be non empty non void BoolSignature ;
let I be SortSymbol of S;
attr I is integer means :Def39: :: AOFA_A00:def 39
I = 1;
end;

:: deftheorem Def39 defines integer AOFA_A00:def 39 :
for S being non empty non void BoolSignature
for I being SortSymbol of S holds
( I is integer iff I = 1 );

registration
let S be non empty non void 4,1 integer BoolSignature ;
cluster integer for Element of the carrier of S;
existence
ex b1 being SortSymbol of S st b1 is integer
proof end;
end;

theorem Th48: :: AOFA_A00:53
for S being non empty non void 4,1 integer BoolSignature
for I being integer SortSymbol of S holds
( I <> the bool-sort of S & the connectives of S . 4 is_of_type {} ,I & the connectives of S . (4 + 1) is_of_type {} ,I & the connectives of S . 4 <> the connectives of S . (4 + 1) & the connectives of S . (4 + 2) is_of_type <*I*>,I & the connectives of S . (4 + 3) is_of_type <*I,I*>,I & the connectives of S . (4 + 4) is_of_type <*I,I*>,I & the connectives of S . (4 + 5) is_of_type <*I,I*>,I & the connectives of S . (4 + 3) <> the connectives of S . (4 + 4) & the connectives of S . (4 + 3) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 4) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 6) is_of_type <*I,I*>, the bool-sort of S )
proof end;

definition
let S be non empty non void 4,1 integer BoolSignature ;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
set f = the bool-sort of S;
set L = A;
A1: ( I = 1 & I <> the bool-sort of S & the connectives of S . 4 is_of_type {} ,I & the connectives of S . (4 + 1) is_of_type {} ,I & the connectives of S . 4 <> the connectives of S . (4 + 1) & the connectives of S . (4 + 2) is_of_type <*I*>,I & the connectives of S . (4 + 3) is_of_type <*I,I*>,I & the connectives of S . (4 + 4) is_of_type <*I,I*>,I & the connectives of S . (4 + 5) is_of_type <*I,I*>,I & the connectives of S . (4 + 3) <> the connectives of S . (4 + 4) & the connectives of S . (4 + 3) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 4) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 6) is_of_type <*I,I*>, the bool-sort of S ) by ;
len the connectives of S >= 4 + 6 by Def38;
then ( 4 <= len the connectives of S & 5 <= len the connectives of S & 6 <= len the connectives of S & 7 <= len the connectives of S & 8 <= len the connectives of S & 9 <= len the connectives of S & 10 <= len the connectives of S ) by XXREAL_0:2;
then A2: ( 4 in dom the connectives of S & 5 in dom the connectives of S & 6 in dom the connectives of S & 7 in dom the connectives of S & 8 in dom the connectives of S & 9 in dom the connectives of S & 10 in dom the connectives of S ) by FINSEQ_3:25;
A3: ( the connectives of S . 4 in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by ;
func \0 (A,I) -> Element of the Sorts of A . I equals :: AOFA_A00:def 40
(Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {};
coherence
(Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {} is Element of the Sorts of A . I
by ;
A4: ( the connectives of S . 5 in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by ;
func \1 (A,I) -> Element of the Sorts of A . I equals :: AOFA_A00:def 41
(Den ((In (( the connectives of S . 5), the carrier' of S)),A)) . {};
coherence
(Den ((In (( the connectives of S . 5), the carrier' of S)),A)) . {} is Element of the Sorts of A . I
by ;
let a be Element of the Sorts of A . I;
func - a -> Element of the Sorts of A . I equals :: AOFA_A00:def 42
(Den ((In (( the connectives of S . 6), the carrier' of S)),A)) . <*a*>;
coherence
(Den ((In (( the connectives of S . 6), the carrier' of S)),A)) . <*a*> is Element of the Sorts of A . I
by ;
let b be Element of the Sorts of A . I;
func a + b -> Element of the Sorts of A . I equals :: AOFA_A00:def 43
(Den ((In (( the connectives of S . 7), the carrier' of S)),A)) . <*a,b*>;
coherence
(Den ((In (( the connectives of S . 7), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I
by ;
func a * b -> Element of the Sorts of A . I equals :: AOFA_A00:def 44
(Den ((In (( the connectives of S . 8), the carrier' of S)),A)) . <*a,b*>;
coherence
(Den ((In (( the connectives of S . 8), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I
by ;
func a div b -> Element of the Sorts of A . I equals :: AOFA_A00:def 45
(Den ((In (( the connectives of S . 9), the carrier' of S)),A)) . <*a,b*>;
coherence
(Den ((In (( the connectives of S . 9), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I
by ;
func leq (a,b) -> Element of the Sorts of A . the bool-sort of S equals :: AOFA_A00:def 46
(Den ((In (( the connectives of S . 10), the carrier' of S)),A)) . <*a,b*>;
coherence
(Den ((In (( the connectives of S . 10), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . the bool-sort of S
by ;
end;

:: deftheorem defines \0 AOFA_A00:def 40 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S holds \0 (A,I) = (Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {};

:: deftheorem defines \1 AOFA_A00:def 41 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S holds \1 (A,I) = (Den ((In (( the connectives of S . 5), the carrier' of S)),A)) . {};

:: deftheorem defines - AOFA_A00:def 42 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a being Element of the Sorts of A . I holds - a = (Den ((In (( the connectives of S . 6), the carrier' of S)),A)) . <*a*>;

:: deftheorem defines + AOFA_A00:def 43 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of the Sorts of A . I holds a + b = (Den ((In (( the connectives of S . 7), the carrier' of S)),A)) . <*a,b*>;

:: deftheorem defines * AOFA_A00:def 44 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of the Sorts of A . I holds a * b = (Den ((In (( the connectives of S . 8), the carrier' of S)),A)) . <*a,b*>;

:: deftheorem defines div AOFA_A00:def 45 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of the Sorts of A . I holds a div b = (Den ((In (( the connectives of S . 9), the carrier' of S)),A)) . <*a,b*>;

:: deftheorem defines leq AOFA_A00:def 46 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of the Sorts of A . I holds leq (a,b) = (Den ((In (( the connectives of S . 10), the carrier' of S)),A)) . <*a,b*>;

definition
let S be non empty non void 4,1 integer BoolSignature ;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
let a, b be Element of A,I;
func a - b -> Element of A,I equals :: AOFA_A00:def 47
a + (- b);
coherence
a + (- b) is Element of A,I
;
func a mod b -> Element of A,I equals :: AOFA_A00:def 48
a + (- ((a div b) * b));
coherence
a + (- ((a div b) * b)) is Element of A,I
;
end;

:: deftheorem defines - AOFA_A00:def 47 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of A,I holds a - b = a + (- b);

:: deftheorem defines mod AOFA_A00:def 48 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of A,I holds a mod b = a + (- ((a div b) * b));

registration
let S be non empty non void 4,1 integer BoolSignature ;
let X be V2() ManySortedSet of the carrier of S;
cluster X . 1 -> non empty ;
coherence
not X . 1 is empty
proof end;
end;

definition
let n be Nat;
let s be set ;
let S be non empty non void bool-correct BoolSignature ;
let A be bool-correct MSAlgebra over S;
attr A is n,s integer means :Def49: :: AOFA_A00:def 49
ex I being SortSymbol of S st
( I = s & the connectives of S . n is_of_type {} ,I & the Sorts of A . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) );
end;

:: deftheorem Def49 defines integer AOFA_A00:def 49 :
for n being Nat
for s being set
for S being non empty non void bool-correct BoolSignature
for A being bool-correct MSAlgebra over S holds
( A is n,s integer iff ex I being SortSymbol of S st
( I = s & the connectives of S . n is_of_type {} ,I & the Sorts of A . I = INT & (Den ((In (( the connectives of S . n), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) ) );

theorem Th49: :: AOFA_A00:54
for n being Nat
for I being set st n >= 1 holds
for S being non empty non void bool-correct BoolSignature st S is n,I integer holds
ex A being strict non-empty bool-correct MSAlgebra over S st A is n,I integer
proof end;

registration
let S be non empty non void bool-correct 4,1 integer BoolSignature ;
cluster strict non-empty V166(S) bool-correct 4,1 integer for MSAlgebra over S;
existence
ex b1 being strict non-empty bool-correct MSAlgebra over S st b1 is 4,1 integer
by Th49;
end;

theorem :: AOFA_A00:55
for S being non empty non void bool-correct 4,1 integer BoolSignature
for A being non-empty bool-correct 4,1 integer MSAlgebra over S
for I being integer SortSymbol of S holds
( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer
for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )
proof end;

registration
let S be non empty non void bool-correct 4,1 integer BoolSignature ;
let A be non-empty bool-correct 4,1 integer MSAlgebra over S;
cluster -> integer for Element of the Sorts of A . 1;
coherence
for b1 being Element of the Sorts of A . 1 holds b1 is integer
proof end;
end;

definition
let I, N be set ;
let n be Nat;
let S be ConnectivesSignature ;
attr S is n,I,N -array means :Def50: :: AOFA_A00:def 50
( len the connectives of S >= n + 3 & ex J, K, L being Element of S st
( L = I & K = N & J <> L & J <> K & the connectives of S . n is_of_type <*J,K*>,L & the connectives of S . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S . (n + 2) is_of_type <*J*>,K & the connectives of S . (n + 3) is_of_type <*K,L*>,J ) );
end;

:: deftheorem Def50 defines -array AOFA_A00:def 50 :
for I, N being set
for n being Nat
for S being ConnectivesSignature holds
( S is n,I,N -array iff ( len the connectives of S >= n + 3 & ex J, K, L being Element of S st
( L = I & K = N & J <> L & J <> K & the connectives of S . n is_of_type <*J,K*>,L & the connectives of S . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S . (n + 2) is_of_type <*J*>,K & the connectives of S . (n + 3) is_of_type <*K,L*>,J ) ) );

definition
let S be non empty non void ConnectivesSignature ;
let I, N be set ;
let n be Nat;
let A be MSAlgebra over S;
attr A is n,I,N -array means :: AOFA_A00:def 51
ex J, K being Element of S st
( K = I & the connectives of S . n is_of_type <*J,N*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . N = INT & ( for a being finite 0 -based array of the Sorts of A . K holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. n),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. (n + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (n + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,K st i >= 0 holds
(Den (( the connectives of S /. (n + 3)),A)) . <*i,x*> = (Segm i) --> x ) );
end;

:: deftheorem defines -array AOFA_A00:def 51 :
for S being non empty non void ConnectivesSignature
for I, N being set
for n being Nat
for A being MSAlgebra over S holds
( A is n,I,N -array iff ex J, K being Element of S st
( K = I & the connectives of S . n is_of_type <*J,N*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . N = INT & ( for a being finite 0 -based array of the Sorts of A . K holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. n),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. (n + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (n + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,K st i >= 0 holds
(Den (( the connectives of S /. (n + 3)),A)) . <*i,x*> = (Segm i) --> x ) ) );

definition
let B be non empty BoolSignature ;
let C be non empty ConnectivesSignature ;
func B +* C -> strict BoolSignature means :Def52: :: AOFA_A00:def 52
( ManySortedSign(# the carrier of it, the carrier' of it, the Arity of it, the ResultSort of it #) = B +* C & the bool-sort of it = the bool-sort of B & the connectives of it = the connectives of B ^ the connectives of C );
uniqueness
for b1, b2 being strict BoolSignature st ManySortedSign(# the carrier of b1, the carrier' of b1, the Arity of b1, the ResultSort of b1 #) = B +* C & the bool-sort of b1 = the bool-sort of B & the connectives of b1 = the connectives of B ^ the connectives of C & ManySortedSign(# the carrier of b2, the carrier' of b2, the Arity of b2, the ResultSort of b2 #) = B +* C & the bool-sort of b2 = the bool-sort of B & the connectives of b2 = the connectives of B ^ the connectives of C holds
b1 = b2
;
existence
ex b1 being strict BoolSignature st
( ManySortedSign(# the carrier of b1, the carrier' of b1, the Arity of b1, the ResultSort of b1 #) = B +* C & the bool-sort of b1 = the bool-sort of B & the connectives of b1 = the connectives of B ^ the connectives of C )
proof end;
end;

:: deftheorem Def52 defines +* AOFA_A00:def 52 :
for B being non empty BoolSignature
for C being non empty ConnectivesSignature
for b3 being strict BoolSignature holds
( b3 = B +* C iff ( ManySortedSign(# the carrier of b3, the carrier' of b3, the Arity of b3, the ResultSort of b3 #) = B +* C & the bool-sort of b3 = the bool-sort of B & the connectives of b3 = the connectives of B ^ the connectives of C ) );

theorem Th51: :: AOFA_A00:56
for B being non empty BoolSignature
for C being non empty ConnectivesSignature holds
( the carrier of (B +* C) = the carrier of B \/ the carrier of C & the carrier' of (B +* C) = the carrier' of B \/ the carrier' of C & the Arity of (B +* C) = the Arity of B +* the Arity of C & the ResultSort of (B +* C) = the ResultSort of B +* the ResultSort of C )
proof end;

registration
let B be non empty BoolSignature ;
let C be non empty ConnectivesSignature ;
cluster B +* C -> non empty strict ;
coherence
not B +* C is empty
proof end;
end;

registration
let B be non empty non void BoolSignature ;
let C be non empty ConnectivesSignature ;
cluster B +* C -> non void strict ;
coherence
not B +* C is void
proof end;
end;

registration
let n1, n2 be Nat;
let B be non empty non void n1 -connectives BoolSignature ;
let C be non empty non void n2 -connectives ConnectivesSignature ;
cluster B +* C -> n1 + n2 -connectives strict ;
coherence
B +* C is n1 + n2 -connectives
proof end;
end;

theorem Th52: :: AOFA_A00:57
for M, O, N, I being set st I in M & N in M holds
ex C being non empty non void strict 4 -connectives ConnectivesSignature st
( C is 1,I,N -array & C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )
proof end;

registration
let I, N be set ;
cluster non empty non void V57() V165() strict 4 -connectives 1,I,N -array for ConnectivesSignature ;
existence
ex b1 being non empty non void strict ConnectivesSignature st
( b1 is 1,I,N -array & b1 is 4 -connectives )
proof end;
end;

theorem Th53: :: AOFA_A00:58
for n, m being Nat st m > 0 holds
for B being non empty non void b1 -connectives BoolSignature
for I, N being set
for C being non empty non void ConnectivesSignature st C is m,I,N -array holds
B +* C is n + m,I,N -array
proof end;

theorem Th54: :: AOFA_A00:59
for m being Nat st m > 0 holds
for s being set
for B being non empty non void BoolSignature
for C being non empty non void ConnectivesSignature st B is m,s integer & the carrier' of B misses the carrier' of C holds
B +* C is m,s integer
proof end;

theorem Th55: :: AOFA_A00:60
for B being non empty non void bool-correct BoolSignature
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
B +* C is bool-correct
proof end;

definition
let n be Nat;
let B be BoolSignature ;
attr B is n array-correct means :Def53: :: AOFA_A00:def 53
the ResultSort of B . ( the connectives of B . (n + 1)) <> the bool-sort of B;
end;

:: deftheorem Def53 defines array-correct AOFA_A00:def 53 :
for n being Nat
for B being BoolSignature holds
( B is n array-correct iff the ResultSort of B . ( the connectives of B . (n + 1)) <> the bool-sort of B );

registration
existence
ex b1 being strict BoolSignature st
( b1 is 1-1-connectives & b1 is 14 -connectives & b1 is 11,1,1 -array & b1 is 11 array-correct & b1 is 4,1 integer & b1 is bool-correct & not b1 is empty & not b1 is void )
proof end;
end;

registration
let S be non empty non void 11,1,1 -array BoolSignature ;
cluster integer for Element of the carrier of S;
existence
ex b1 being SortSymbol of S st b1 is integer
proof end;
end;

definition
let S be non empty non void 11,1,1 -array BoolSignature ;
consider J, K, L being Element of S such that
A1: ( L = 1 & K = 1 & J <> L & J <> K & the connectives of S . 11 is_of_type <*J,K*>,L & the connectives of S . (11 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (11 + 2) is_of_type <*J*>,K & the connectives of S . (11 + 3) is_of_type <*K,L*>,J ) by Def50;
func the_array_sort_of S -> SortSymbol of S equals :: AOFA_A00:def 54
the ResultSort of S . ( the connectives of S . 12);
coherence
the ResultSort of S . ( the connectives of S . 12) is SortSymbol of S
by A1;
end;

:: deftheorem defines the_array_sort_of AOFA_A00:def 54 :
for S being non empty non void 11,1,1 -array BoolSignature holds the_array_sort_of S = the ResultSort of S . ( the connectives of S . 12);

definition
let S be non empty non void 4,1 integer 11,1,1 -array BoolSignature ;
let A be non-empty MSAlgebra over S;
let a be Element of the Sorts of A . ;
let I be integer SortSymbol of S;
consider J, K, L being Element of S such that
A1: ( L = 1 & K = 1 & J <> L & J <> K & the connectives of S . 11 is_of_type <*J,K*>,L & the connectives of S . (11 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (11 + 2) is_of_type <*J*>,K & the connectives of S . (11 + 3) is_of_type <*K,L*>,J ) by Def50;
A2: I = 1 by Def39;
func length (a,I) -> Element of the Sorts of A . I equals :: AOFA_A00:def 55
(Den ((In (( the connectives of S . 13), the carrier' of S)),A)) . <*a*>;
coherence
(Den ((In (( the connectives of S . 13), the carrier' of S)),A)) . <*a*> is Element of the Sorts of A . I
by A1, A2, Th27;
let i be Element of the Sorts of A . I;
func a . i -> Element of the Sorts of A . I equals :: AOFA_A00:def 56
(Den ((In (( the connectives of S . 11), the carrier' of S)),A)) . <*a,i*>;
coherence
(Den ((In (( the connectives of S . 11), the carrier' of S)),A)) . <*a,i*> is Element of the Sorts of A . I
by A1, A2, Th28;
let x be Element of the Sorts of A . I;
func (a,i) <- x -> Element of the Sorts of A . equals :: AOFA_A00:def 57
(Den ((In (( the connectives of S . 12), the carrier' of S)),A)) . <*a,i,x*>;
coherence
(Den ((In (( the connectives of S . 12), the carrier' of S)),A)) . <*a,i,x*> is Element of the Sorts of A .
by A1, A2, Th29;
end;

:: deftheorem defines length AOFA_A00:def 55 :
for S being non empty non void 4,1 integer 11,1,1 -array BoolSignature
for A being non-empty MSAlgebra over S
for a being Element of the Sorts of A .
for I being integer SortSymbol of S holds length (a,I) = (Den ((In (( the connectives of S . 13), the carrier' of S)),A)) . <*a*>;

:: deftheorem defines . AOFA_A00:def 56 :
for S being non empty non void 4,1 integer 11,1,1 -array BoolSignature
for A being non-empty MSAlgebra over S
for a being Element of the Sorts of A .
for I being integer SortSymbol of S
for i being Element of the Sorts of A . I holds a . i = (Den ((In (( the connectives of S . 11), the carrier' of S)),A)) . <*a,i*>;

:: deftheorem defines <- AOFA_A00:def 57 :
for S being non empty non void 4,1 integer 11,1,1 -array BoolSignature
for A being non-empty MSAlgebra over S
for a being Element of the Sorts of A .
for I being integer SortSymbol of S
for i, x being Element of the Sorts of A . I holds (a,i) <- x = (Den ((In (( the connectives of S . 12), the carrier' of S)),A)) . <*a,i,x*>;

definition
let S be non empty non void 4,1 integer 11,1,1 -array BoolSignature ;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
consider J, K, L being Element of S such that
A1: ( L = 1 & K = 1 & J <> L & J <> K & the connectives of S . 11 is_of_type <*J,K*>,L & the connectives of S . (11 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (11 + 2) is_of_type <*J*>,K & the connectives of S . (11 + 3) is_of_type <*K,L*>,J ) by Def50;
A2: I = 1 by Def39;
let i, x be Element of the Sorts of A . I;
func init.array (i,x) -> Element of the Sorts of A . equals :: AOFA_A00:def 58
(Den ((In (( the connectives of S . 14), the carrier' of S)),A)) . <*i,x*>;
coherence
(Den ((In (( the connectives of S . 14), the carrier' of S)),A)) . <*i,x*> is Element of the Sorts of A .
by A1, A2, Th28;
end;

:: deftheorem defines init.array AOFA_A00:def 58 :
for S being non empty non void 4,1 integer 11,1,1 -array BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for i, x being Element of the Sorts of A . I holds init.array (i,x) = (Den ((In (( the connectives of S . 14), the carrier' of S)),A)) . <*i,x*>;

registration
let X be non empty set ;
coherence
proof end;
let Y, Z be non empty set ;
cluster <*X,Y,Z*> -> non-empty ;
coherence
<*X,Y,Z*> is non-empty
;
end;

registration
let X be functional non empty set ;
let Y, Z be non empty set ;
let f be Element of product <*X,Y,Z*>;
coherence
( f . 1 is Relation-like & f . 1 is Function-like )
proof end;
end;

registration
let X be non empty integer-membered set ;
let Y be non empty set ;
let f be Element of product <*X,Y*>;
cluster f . 1 -> integer ;
coherence
f . 1 is integer
proof end;
end;

theorem Th56: :: AOFA_A00:61
for I, N being set
for S being non empty non void 1,b1,b2 -array ConnectivesSignature
for Y being non empty set
for X being V2() ManySortedSet of Y st ( the ResultSort of S . ( the connectives of S . 2) nin Y or X . ( the ResultSort of S . ( the connectives of S . 2)) = (X . I) ^omega ) & X . N = INT & I in Y holds
ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates X )
proof end;

registration
let I, N be set ;
let S be non empty non void 1,I,N -array ConnectivesSignature ;
cluster strict non-empty V166(S) 1,I,N -array for MSAlgebra over S;
existence
ex b1 being strict non-empty MSAlgebra over S st b1 is 1,I,N -array
proof end;
end;

definition
let S1 be non empty BoolSignature ;
let S2 be non empty ConnectivesSignature ;
let A1 be non-empty MSAlgebra over S1;
let A2 be non-empty MSAlgebra over S2;
func (S1,A1) +* A2 -> strict non-empty MSAlgebra over S1 +* S2 equals :: AOFA_A00:def 59
A1 +* A2;
coherence
A1 +* A2 is strict non-empty MSAlgebra over S1 +* S2
proof end;
end;

:: deftheorem defines +* AOFA_A00:def 59 :
for S1 being non empty BoolSignature
for S2 being non empty ConnectivesSignature
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2 holds (S1,A1) +* A2 = A1 +* A2;

theorem Th57: :: AOFA_A00:62
for B being non empty non void bool-correct BoolSignature
for A1 being non-empty bool-correct MSAlgebra over B
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
(B,A1) +* A2 is bool-correct
proof end;

theorem Th58: :: AOFA_A00:63
for n being Nat
for I being set st n >= 4 holds
for B being non empty non void bool-correct BoolSignature st B is n,I integer holds
for A1 being non-empty bool-correct MSAlgebra over B st A1 is n,I integer holds
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,I integer
proof end;

theorem Th59: :: AOFA_A00:64
for n, m being Nat
for s, r being set st n >= 1 & m >= 1 holds
for B being non empty non void b2 -connectives BoolSignature
for A1 being non-empty MSAlgebra over B
for C being non empty non void ConnectivesSignature st C is n,s,r -array holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 & A2 is n,s,r -array holds
for S being non empty non void BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty MSAlgebra over S st A = (B,A1) +* A2 holds
A is m + n,s,r -array
proof end;

theorem Th60: :: AOFA_A00:65
for n being Nat
for s being set
for S1, S2 being BoolSignature st the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & ( for i being Nat st i >= 1 & i <= 3 holds
( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is bool-correct holds
S2 is bool-correct
proof end;

theorem Th61: :: AOFA_A00:66
for n being Nat
for s being set
for S1, S2 being non empty BoolSignature st n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n + 6 & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & ( for i being Nat st i >= n & i <= n + 6 holds
( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is n,s integer holds
S2 is n,s integer
proof end;

theorem Th62: :: AOFA_A00:67
for n, m being Nat
for s, r being set
for S1, S2 being non empty ConnectivesSignature st 1 <= n & len the connectives of S1 >= n + 3 & ( for i being Nat st i >= n & i <= n + 3 holds
( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . (i + m)) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . (i + m)) ) ) & S2 is n + m,s,r -array holds
S1 is n,s,r -array
proof end;

theorem Th63: :: AOFA_A00:68
for j, k being set
for i, m, n being Nat st m >= 4 & m + 6 <= n & i >= 1 holds
for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds
ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st
( BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C & B is n -connectives & B is m,k integer & C is i,j,k -array & the carrier of B = the carrier of C & the carrier' of B = the carrier' of S \ (rng the connectives of C) & the carrier' of C = rng the connectives of C & the connectives of B = the connectives of S | n & the connectives of C = the connectives of S /^ n )
proof end;

theorem Th64: :: AOFA_A00:69
for s, I being set
for S being non empty non void bool-correct BoolSignature st S is 4,I integer holds
for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )
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 ;
cluster strict non-empty V166(S) bool-correct 4,1 integer 11,1,1 -array for MSAlgebra over S;
existence
ex b1 being strict non-empty bool-correct MSAlgebra over S st
( b1 is 11,1,1 -array & b1 is 4,1 integer )
proof end;
end;