:: by Grzegorz Bancerek

::

:: Received August 27, 2012

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

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

registration

let I be set ;

let f be V2() ManySortedSet of I;

let i be object ;

let x be non empty set ;

coherence

f +* (i,x) is non-empty

end;
let f be V2() ManySortedSet of I;

let i be object ;

let x be non empty set ;

coherence

f +* (i,x) is non-empty

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

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

definition

let I be set ;

let i be Element of I;

let x be set ;

coherence

(EmptyMS I) +* (i,{x}) is ManySortedSet of I ;

end;
let i be Element of I;

let x be set ;

coherence

(EmptyMS I) +* (i,{x}) is ManySortedSet of I ;

:: 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 = (EmptyMS I) +* (i,{x});

for I being set

for i being Element of I

for x being set holds i -singleton x = (EmptyMS I) +* (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 -singleton x) . i = {x} & ( i <> j implies (i -singleton x) . j = {} ) )

for i, j being Element of I

for x being set holds

( (i -singleton x) . i = {x} & ( i <> j implies (i -singleton x) . 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

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 ;

ex b_{1} being ManySortedFunction of A,B st

( b_{1} . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds

b_{1} . s = F . s ) )

for b_{1}, b_{2} being ManySortedFunction of A,B st b_{1} . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds

b_{1} . s = F . s ) & b_{2} . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds

b_{2} . s = F . s ) holds

b_{1} = b_{2}

end;
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 ( it . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds

it . s = F . s ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{8} being ManySortedFunction of A,B holds

( b_{8} = F +* (i,j,v) iff ( b_{8} . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds

b_{8} . s = F . s ) ) );

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 b

( b

b

canceled;

theorem :: AOFA_A00:13

theorem :: AOFA_A00:14

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

<*a1,a2,a3,a4*> is one-to-one

proof end;

definition
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*>;

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

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

registration
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 ) )

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;

definition

let a1, a2, a3, a4, a5, a6, a7 be object ;

<*a1,a2,a3,a4,a5*> ^ <*a6,a7*> is FinSequence ;

end;
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*>;

<*a1,a2,a3,a4,a5*> ^ <*a6,a7*> is FinSequence ;

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

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

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

registration
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 ) )

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 ;

<*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*> is FinSequence ;

end;
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*>;

<*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*> is FinSequence ;

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

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

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

registration

let a1, a2, a3, a4, a5, a6, a7, a8 be object ;

coherence

<*a1,a2,a3,a4,a5,a6,a7,a8*> is 8 -element ;

end;
coherence

<*a1,a2,a3,a4,a5,a6,a7,a8*> is 8 -element ;

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

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

( 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 )

( 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;

ex b_{1} being ManySortedFunction of I st

for i, j being set st i in I holds

( dom (b_{1} . i) = S . i & ( j in S . i implies (b_{1} . i) . j is ManySortedSet of J ) )

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

ex b

for i, j being set st i in I holds

( dom (b

proof end;

:: deftheorem Def6 defines ManySortedMSSet AOFA_A00:def 6 :

for I, J being set

for S being ManySortedSet of I

for b_{4} being ManySortedFunction of I holds

( b_{4} is ManySortedMSSet of S,J iff for i, j being set st i in I holds

( dom (b_{4} . i) = S . i & ( j in S . i implies (b_{4} . i) . j is ManySortedSet of J ) ) );

for I, J being set

for S being ManySortedSet of I

for b

( b

( dom (b

definition

let I, J be set ;

let S1 be ManySortedSet of I;

let S2 be ManySortedSet of J;

ex b_{1} being ManySortedMSSet of S1,J st

for i, a being set st i in I & a in S1 . i holds

(b_{1} . i) . a is ManySortedSubset of S2

end;
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 for i, a being set st i in I & a in S1 . i holds

(it . i) . a is ManySortedSubset of S2;

ex b

for i, a being set st i in I & a in S1 . i holds

(b

proof 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 b_{5} being ManySortedMSSet of S1,J holds

( b_{5} is ManySortedMSSet of S1,S2 iff for i, a being set st i in I & a in S1 . i holds

(b_{5} . i) . a is ManySortedSubset of S2 );

for I, J being set

for S1 being ManySortedSet of I

for S2 being ManySortedSet of J

for b

( b

(b

registration

let I be set ;

let X, Y be ManySortedSet of I;

let f be ManySortedMSSet of X,Y;

let x, y be set ;

coherence

( (f . x) . y is Function-like & (f . x) . y is Relation-like )

end;
let X, Y be ManySortedSet of I;

let f be ManySortedMSSet of X,Y;

let x, y be set ;

coherence

( (f . x) . y is Function-like & (f . x) . y is Relation-like )

proof end;

definition

let S be ManySortedSign ;

let o, a be set ;

let r be Element of S;

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

( the Arity of S . o = a & the ResultSort of S . o = r );

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

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

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

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

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

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 ;

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 c_{2} is strict ;

struct VarMSAlgebra over S -> MSAlgebra over S;

aggr VarMSAlgebra(# Sorts, Charact, free-vars #) -> VarMSAlgebra over S;

sel free-vars c_{2} -> ManySortedMSSet of the Sorts of c_{2}, the Sorts of c_{2};

end;
attr c

struct VarMSAlgebra over S -> MSAlgebra over S;

aggr VarMSAlgebra(# Sorts, Charact, free-vars #) -> VarMSAlgebra over S;

sel free-vars c

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;

coherence

VarMSAlgebra(# U,C,v #) is non-empty ;

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

coherence

VarMSAlgebra(# U,C,v #) is non-empty ;

registration

let S be non empty non void ManySortedSign ;

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

existence

ex b_{1} being strict VarMSAlgebra over S st b_{1} is X,S -terms

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

existence

ex b

proof end;

registration

let S be non empty non void ManySortedSign ;

existence

ex b_{1} being VarMSAlgebra over S st

( b_{1} is non-empty & b_{1} is disjoint_valued )

coherence

for b_{1} being X,S -terms VarMSAlgebra over S st b_{1} is all_vars_including holds

b_{1} is non-empty
;

end;
existence

ex b

( b

proof end;

let X be V2() ManySortedSet of the carrier of S;coherence

for b

b

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;

( the free-vars of A . a) . t is ManySortedSubset of the Sorts of A by Def7;

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

( the free-vars of A . a) . t is ManySortedSubset of the Sorts of A by Def7;

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

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;

end;
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,(the_result_sort_of o) 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 (the_arity_of o) & s0 = (the_arity_of o) . i & a = p . i ) } ;

for o being OperSymbol of S

for p being FinSequence st p in Args (o,A) holds

for b being Element of A,(the_result_sort_of o) 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 (the_arity_of o) & s0 = (the_arity_of o) . i & a = p . i ) } ;

:: 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,(the_result_sort_of o) 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 (the_arity_of o) & s0 = (the_arity_of o) . i & a = p . i ) } );

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,(the_result_sort_of o) 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 (the_arity_of o) & s0 = (the_arity_of o) . 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

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

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

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;

ex b_{1} being X,S -terms strict VarMSAlgebra over S st

( b_{1} is all_vars_including & b_{1} is inheriting_operations & b_{1} is free_in_itself )

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

cluster disjoint_valued X,S -terms all_vars_including inheriting_operations free_in_itself strict for VarMSAlgebra over S;

existence ex b

( b

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

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

let A be non-empty X,S -terms VarMSAlgebra over S;

:: 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 b_{2},b_{1} -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 } );

for S being non empty non void ManySortedSign

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

for A being non-empty b

( 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{ F_{1}() -> non empty set , F_{2}() -> V2() ManySortedSet of F_{1}(), F_{3}() -> V2() ManySortedSet of F_{1}(), F_{4}( object , object , object ) -> set } :

Scheme{ F

ex f being ManySortedMSSet of F_{2}(),F_{3}() st

for s, r being Element of F_{1}()

for t being Element of F_{2}() . s holds ((f . s) . t) . r = F_{4}(s,r,t)

providedfor s, r being Element of F

for t being Element of F

A1:
for s, r being Element of F_{1}()

for t being Element of F_{2}() . s holds F_{4}(s,r,t) is Subset of (F_{3}() . r)

for t being Element of F

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 b_{2},b_{1} -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 b_{2},b_{1} -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 )

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

for A being b

( 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;

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

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

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

cluster non-empty V166(S) disjoint_valued X,S -terms all_vars_including inheriting_operations free_in_itself strict vf-free for VarMSAlgebra over S;

existence ex b

( b

proof 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 b_{2},b_{1} -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

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

for A being b

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 b_{2},b_{1} -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 (FreeGen X) . s holds

vf x = s -singleton x

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

for A being b

for s being SortSymbol of S

for x being Element of A,s st x in (FreeGen X) . s holds

vf x = s -singleton x

proof end;

definition

let I be set ;

let S be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

b_{1} . i is Element of S . i

end;
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 for i being set st i in I holds

it . i is Element of S . i;

ex b

for i being set st i in I holds

b

proof end;

:: deftheorem defines ManySortedElement AOFA_A00:def 12 :

for I being set

for S, b_{3} being ManySortedSet of I holds

( b_{3} is ManySortedElement of S iff for i being set st i in I holds

b_{3} . i is Element of S . i );

for I being set

for S, b

( b

b

definition

let S be non empty non void ManySortedSign ;

attr c_{2} is strict ;

struct UndefMSAlgebra over S -> MSAlgebra over S;

aggr UndefMSAlgebra(# Sorts, Charact, undefined-map #) -> UndefMSAlgebra over S;

sel undefined-map c_{2} -> ManySortedElement of the Sorts of c_{2};

end;
attr c

struct UndefMSAlgebra over S -> MSAlgebra over S;

aggr UndefMSAlgebra(# Sorts, Charact, undefined-map #) -> UndefMSAlgebra over S;

sel undefined-map c

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;

end;
let A be UndefMSAlgebra over S;

let s be SortSymbol of S;

let a be Element of A,s;

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

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;

end;
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 (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) holds

for b being Element of A,(the_result_sort_of o) st b = (Den (o,A)) . p holds

b is undefined ;

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 (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) holds

for b being Element of A,(the_result_sort_of o) st b = (Den (o,A)) . p holds

b is undefined ;

:: 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 (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) holds

for b being Element of A,(the_result_sort_of o) st b = (Den (o,A)) . p holds

b is undefined );

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 (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) holds

for b being Element of A,(the_result_sort_of o) 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;

end;
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 . (the_result_sort_of o) ) );

( 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 . (the_result_sort_of o) ) );

:: 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 . (the_result_sort_of o) ) ) );

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 . (the_result_sort_of o) ) ) );

registration

let S be non empty ManySortedSign ;

let A be MSAlgebra over S;

coherence

the Charact of A is Function-yielding ;

end;
let A be MSAlgebra over S;

coherence

the Charact of A is Function-yielding ;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

coherence

for b_{1} being UndefMSAlgebra over S st b_{1} is A -undef holds

b_{1} is undef-consequent
;

existence

ex b_{1} being strict UndefMSAlgebra over S st

( b_{1} is A -undef & b_{1} is non-empty )

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

coherence

for b

b

existence

ex b

( b

proof end;

definition

let J be non empty non void ManySortedSign ;

let T be MSAlgebra over J;

let X be GeneratorSet of T;

attr c_{4} is strict ;

struct ProgramAlgStr over J,T,X -> UAStr ;

aggr ProgramAlgStr(# carrier, charact, assignments #) -> ProgramAlgStr over J,T,X;

sel assignments c_{4} -> Function of (Union [|X, the Sorts of T|]), the carrier of c_{4};

end;
let T be MSAlgebra over J;

let X be GeneratorSet of T;

attr c

struct ProgramAlgStr over J,T,X -> UAStr ;

aggr ProgramAlgStr(# carrier, charact, assignments #) -> ProgramAlgStr over J,T,X;

sel assignments c

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;

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

( the Sorts of T is disjoint_valued & the assignments of A is one-to-one );

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

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 b_{1} being strict ProgramAlgStr over J,T,X st

( b_{1} is partial & b_{1} is quasi_total & b_{1} is non-empty )

end;
let T be MSAlgebra over J;

let X be GeneratorSet of T;

existence

ex b

( b

proof end;

registration

let J be non empty non void ManySortedSign ;

let T be MSAlgebra over J;

let X be GeneratorSet of T;

ex b_{1} being non empty partial quasi_total non-empty strict ProgramAlgStr over J,T,X st

( b_{1} is with_empty-instruction & b_{1} is with_catenation & b_{1} is with_if-instruction & b_{1} is with_while-instruction )

end;
let T be MSAlgebra over J;

let X be GeneratorSet of T;

cluster non empty partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction strict for ProgramAlgStr over J,T,X;

existence ex b

( b

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

( 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

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

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

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

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

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;

ex b_{1} 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 b_{1} is degenerated & b_{1} is well_founded & b_{1} is ECIW-strict & b_{1} is infinite )

end;
let T be MSAlgebra over J;

let X be GeneratorSet of T;

cluster non empty partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction infinite non degenerated well_founded ECIW-strict strict for ProgramAlgStr over J,T,X;

existence ex b

( not b

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

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

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;

coherence

the assignments of A . [x,t] is Algorithm of A

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

coherence

the assignments of A . [x,t] is Algorithm of A

proof 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];

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;

not for b_{1} being ManySortedSubset of T holds b_{1} is V2()

end;
let T be V2() disjoint_valued ManySortedSet of S;

cluster Relation-like V2() S -defined Function-like total disjoint_valued for ManySortedSubset of T;

existence not for b

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

ex b_{1} being Subset of (MSFuncs (X, the Sorts of C)) st

for s being ManySortedFunction of X, the Sorts of C holds

( s in b_{1} iff ex f being ManySortedFunction of T,C st

( f is_homomorphism T,C & s = f || X ) )

for b_{1}, b_{2} being Subset of (MSFuncs (X, the Sorts of C)) st ( for s being ManySortedFunction of X, the Sorts of C holds

( s in b_{1} 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 b_{2} iff ex f being ManySortedFunction of T,C st

( f is_homomorphism T,C & s = f || X ) ) ) holds

b_{1} = b_{2}

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

ex b

for s being ManySortedFunction of X, the Sorts of C holds

( s in b

( f is_homomorphism T,C & s = f || X ) )

proof end;

uniqueness for b

( s in b

( f is_homomorphism T,C & s = f || X ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds

( s in b

( f is_homomorphism T,C & s = f || X ) ) ) holds

b

proof 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 b_{5} being Subset of (MSFuncs (X, the Sorts of C)) holds

( b_{5} = C -States X iff for s being ManySortedFunction of X, the Sorts of C holds

( s in b_{5} iff ex f being ManySortedFunction of T,C st

( f is_homomorphism T,C & s = f || X ) ) );

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 b

( b

( s in b

( 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;

coherence

not C -States X is empty

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

let C be image of T;

let X be V2() GeneratorSet of T;

coherence

not C -States X is empty

proof 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

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 b_{1} being Element of C -States X holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
let T, C be non-empty MSAlgebra over B;

let X be V2() GeneratorSet of T;

coherence

for b

( b

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 b_{1} being Element of C -States X holds

( b_{1} is Function-yielding & b_{1} is the carrier of B -defined )

end;
let T, C be non-empty MSAlgebra over B;

let X be V2() GeneratorSet of T;

coherence

for b

( b

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

coherence

for b_{1} being Element of C -States X holds b_{1} is total
by Th43;

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

let C be image of T;

let X be V2() GeneratorSet of T;

coherence

for b

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;

ex b_{1} being Subset of (C -States X) st

for s being ManySortedFunction of X, the Sorts of C holds

( s in b_{1} iff ( s in C -States X & (s . a) . x <> f ) )

for b_{1}, b_{2} being Subset of (C -States X) st ( for s being ManySortedFunction of X, the Sorts of C holds

( s in b_{1} iff ( s in C -States X & (s . a) . x <> f ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds

( s in b_{2} iff ( s in C -States X & (s . a) . x <> f ) ) ) holds

b_{1} = b_{2}

end;
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 for s being ManySortedFunction of X, the Sorts of C holds

( s in it iff ( s in C -States X & (s . a) . x <> f ) );

ex b

for s being ManySortedFunction of X, the Sorts of C holds

( s in b

proof end;

uniqueness for b

( s in b

( s in b

b

proof 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 b_{8} being Subset of (C -States X) holds

( b_{8} = f -States (X,x) iff for s being ManySortedFunction of X, the Sorts of C holds

( s in b_{8} iff ( s in C -States X & (s . a) . x <> f ) ) );

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 b

( b

( s in b

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;

coherence

not C -States X is empty

end;
let T be non-empty free MSAlgebra over B;

let C be non-empty MSAlgebra over B;

let X be V2() GeneratorSet of T;

coherence

not C -States X is empty

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let o be OperSymbol of S;

coherence

for b_{1} being Element of Args (o,A) holds

( b_{1} is Function-like & b_{1} is Relation-like )

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

let o be OperSymbol of S;

coherence

for b

( b

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

coherence

not C -States G is empty ;

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

coherence

not C -States G is empty ;

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

ex b_{1} 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 & b_{1} = (f . a) . t )

for b_{1}, b_{2} 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 & b_{1} = (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 & b_{2} = (f . a) . t ) holds

b_{1} = b_{2}
by EXTENS_1:19;

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

ex b

( f is_homomorphism T,C & Q = doms s & s = f || Q & b

proof end;

uniqueness for b

( f is_homomorphism T,C & Q = doms s & s = f || Q & b

( f is_homomorphism T,C & Q = doms s & s = f || Q & b

b

:: 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 b_{2},b_{1} -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 b_{8} being Element of C,a holds

( b_{8} = 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 & b_{8} = (f . a) . t ) );

for B being non empty non void ManySortedSign

for X being V2() ManySortedSet of the carrier of B

for T being non-empty 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 b

( b

( f is_homomorphism T,C & Q = doms s & s = f || Q & b

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 c_{4} is strict ;

struct GeneratorSystem over S,X,T -> ;

aggr GeneratorSystem(# generators, supported-var, supported-term #) -> GeneratorSystem over S,X,T;

sel generators c_{4} -> V2() GeneratorSet of T;

sel supported-var c_{4} -> ManySortedFunction of the generators of c_{4}, FreeGen X;

sel supported-term c_{4} -> ManySortedMSSet of the generators of c_{4}, the carrier of S;

end;
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 c

struct GeneratorSystem over S,X,T -> ;

aggr GeneratorSystem(# generators, supported-var, supported-term #) -> GeneratorSystem over S,X,T;

sel generators c

sel supported-var c

sel supported-term c

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;

ex b_{1} being Element of T,s st b_{1} in the generators of G . s

end;
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 it in the generators of G . s;

ex b

proof 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 b_{2},b_{1} -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 b_{6} being Element of T,s holds

( b_{6} is Element of G,s iff b_{6} in the generators of G . s );

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of S

for T being b

for G being GeneratorSystem over S,X,T

for s being SortSymbol of S

for b

( b

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;

coherence

the generators of G . s is Component of the generators of G ;

let g be Element of G,s;

( the supported-var of G . s) . g is Element of (FreeGen X) . s by Def21, FUNCT_2:5;

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

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 (FreeGen X) . s equals :: AOFA_A00:def 23

( the supported-var of G . s) . g;

coherence ( the supported-var of G . s) . g;

( the supported-var of G . s) . g is Element of (FreeGen X) . s by Def21, FUNCT_2:5;

:: deftheorem defines . AOFA_A00:def 22 :

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of S

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

for G being GeneratorSystem over S,X,T

for s being SortSymbol of S holds G . s = the generators of G . s;

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of S

for T being b

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 b_{2},b_{1} -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;

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of S

for T being b

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 ;

( the supported-term of G . s) . g is ManySortedFunction of vf g, the Sorts of T by A1;

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

( the supported-term of G . s) . g is ManySortedFunction of vf g, the Sorts of T by A1;

:: 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 b_{2},b_{1} -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;

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of S

for T being b

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;

end;
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 (FreeGen X) . s implies ( supp-term t = id (s -singleton t) & supp-var t = t ) ) & ( for v being Element of C -States the generators of G st (v . s) . (supp-var t) = (v . s) . t holds

for r being SortSymbol of S

for x being Element of (FreeGen X) . r

for q being Element of the Sorts of T . r st x in (vf t) . r & q = ((supp-term t) . r) . x holds

(v . r) . x = q value_at (C,v) ) & ( t nin (FreeGen X) . 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 (FreeGen X) . a st z in (vf t) . a holds

for q being Element of T,a st q = ((supp-term t) . a) . z holds

(u . a) . z = q value_at (C,((f || H) +* (s,(supp-var t),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 ) ) ) ) ) );

( 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 (FreeGen X) . s implies ( supp-term t = id (s -singleton t) & supp-var t = t ) ) & ( for v being Element of C -States the generators of G st (v . s) . (supp-var t) = (v . s) . t holds

for r being SortSymbol of S

for x being Element of (FreeGen X) . r

for q being Element of the Sorts of T . r st x in (vf t) . r & q = ((supp-term t) . r) . x holds

(v . r) . x = q value_at (C,v) ) & ( t nin (FreeGen X) . 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 (FreeGen X) . a st z in (vf t) . a holds

for q being Element of T,a st q = ((supp-term t) . a) . z holds

(u . a) . z = q value_at (C,((f || H) +* (s,(supp-var t),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 ) ) ) ) ) );

:: 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 b_{2},b_{1} -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 (FreeGen X) . s implies ( supp-term t = id (s -singleton t) & supp-var t = t ) ) & ( for v being Element of C -States the generators of G st (v . s) . (supp-var t) = (v . s) . t holds

for r being SortSymbol of S

for x being Element of (FreeGen X) . r

for q being Element of the Sorts of T . r st x in (vf t) . r & q = ((supp-term t) . r) . x holds

(v . r) . x = q value_at (C,v) ) & ( t nin (FreeGen X) . 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 (FreeGen X) . a st z in (vf t) . a holds

for q being Element of T,a st q = ((supp-term t) . a) . z holds

(u . a) . z = q value_at (C,((f || H) +* (s,(supp-var t),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 ) ) ) ) ) ) );

for S being non empty non void ManySortedSign

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

for T being b

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 (FreeGen X) . s implies ( supp-term t = id (s -singleton t) & supp-var t = t ) ) & ( for v being Element of C -States the generators of G st (v . s) . (supp-var t) = (v . s) . t holds

for r being SortSymbol of S

for x being Element of (FreeGen X) . r

for q being Element of the Sorts of T . r st x in (vf t) . r & q = ((supp-term t) . r) . x holds

(v . r) . x = q value_at (C,v) ) & ( t nin (FreeGen X) . 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 (FreeGen X) . a st z in (vf t) . a holds

for q being Element of T,a st q = ((supp-term t) . a) . z holds

(u . a) . z = q value_at (C,((f || H) +* (s,(supp-var t),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;

ex b_{1} being Element of C -States the generators of G st

( (b_{1} . r) . t = v & ( for p being SortSymbol of S

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b_{1} . 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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b_{1} . p) . x = q value_at (C,u) ) ) ) )

for b_{1}, b_{2} being Element of C -States the generators of G st (b_{1} . r) . t = v & ( for p being SortSymbol of S

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b_{1} . 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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b_{1} . p) . x = q value_at (C,u) ) ) ) & (b_{2} . r) . t = v & ( for p being SortSymbol of S

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b_{2} . 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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b_{2} . p) . x = q value_at (C,u) ) ) ) holds

b_{1} = b_{2}

end;
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 (FreeGen X) . 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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(it . p) . x = q value_at (C,u) ) ) ) );

existence ( (it . r) . t = v & ( for p being SortSymbol of S

for x being Element of (FreeGen X) . 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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(it . p) . x = q value_at (C,u) ) ) ) );

ex b

( (b

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b

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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b

proof end;

uniqueness for b

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b

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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b

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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b

b

proof 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 b_{2},b_{1} -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 b_{10} being Element of C -States the generators of G holds

( b_{10} = succ (s,t,v) iff ( (b_{10} . r) . t = v & ( for p being SortSymbol of S

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b_{10} . 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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b_{10} . p) . x = q value_at (C,u) ) ) ) ) );

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of S

for A being b

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 b

( b

for x being Element of (FreeGen X) . p st ( p = r implies x <> t ) holds

( ( x nin (vf t) . p implies (b

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,(supp-var t),v) & x in (vf t) . p holds

for q being Element of A,p st q = ((supp-term t) . p) . x holds

(b

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;

ex b_{1} 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 b_{1} 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 b_{1}, b_{2} 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 b_{1} 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 b_{2} 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

b_{1} = b_{2}

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

ex b

for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds

( f in b

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 b

( f in b

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 b

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

b

proof 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 b_{2},b_{1} -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 b_{10} being Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) holds

( b_{10} = 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 b_{10} 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 B being non empty non void ManySortedSign

for Y being V2() ManySortedSet of the carrier of B

for T being 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 b

( b

( f in b

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

attr c_{1} is strict ;

struct ConnectivesSignature -> ManySortedSign ;

aggr ConnectivesSignature(# carrier, carrier', Arity, ResultSort, connectives #) -> ConnectivesSignature ;

sel connectives c_{1} -> FinSequence of the carrier' of c_{1};

end;
struct ConnectivesSignature -> ManySortedSign ;

aggr ConnectivesSignature(# carrier, carrier', Arity, ResultSort, connectives #) -> ConnectivesSignature ;

sel connectives c

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

for S being ConnectivesSignature holds

( S is 1-1-connectives iff the connectives of S is one-to-one );

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

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 b_{1} being strict ConnectivesSignature st

( b_{1} is n -connectives & not b_{1} is empty & not b_{1} is void )

end;
existence

ex b

( b

proof end;

definition

attr c_{1} is strict ;

struct BoolSignature -> ConnectivesSignature ;

aggr BoolSignature(# carrier, carrier', Arity, ResultSort, bool-sort, connectives #) -> BoolSignature ;

sel bool-sort c_{1} -> Element of the carrier of c_{1};

end;
struct BoolSignature -> ConnectivesSignature ;

aggr BoolSignature(# carrier, carrier', Arity, ResultSort, bool-sort, connectives #) -> BoolSignature ;

sel bool-sort c

registration

let n be Nat;

existence

ex b_{1} being strict BoolSignature st

( b_{1} is n -connectives & not b_{1} is empty & not b_{1} is void )

end;
existence

ex b

( b

proof end;

definition

let B be BoolSignature ;

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

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

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

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 b_{1} being strict BoolSignature st

( b_{1} is 3 -connectives & b_{1} is 1-1-connectives & b_{1} is bool-correct & not b_{1} is empty & not b_{1} is void )

end;
ex b

( b

proof end;

registration

existence

ex b_{1} being ConnectivesSignature st

( b_{1} is 1-1-connectives & not b_{1} is empty & not b_{1} is void )

end;
ex b

( b

proof end;

registration

let S be non empty non void 1-1-connectives ConnectivesSignature ;

coherence

the connectives of S is one-to-one by Def28;

end;
coherence

the connectives of S is one-to-one by Def28;

definition

let S be non empty non void BoolSignature ;

let B be MSAlgebra over S;

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

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

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

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 (n -tuples_on A),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 ) )

for n being Nat

for f being Function of (n -tuples_on A),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;

ex b_{1} being non empty homogeneous quasi_total PartFunc of (A *),A st b_{1} is n -ary

end;
let n be Nat;

cluster Relation-like A * -defined A -valued Function-like non empty homogeneous quasi_total n -ary for PartFunc of ,;

existence ex 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

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 )

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 b_{1} being strict MSAlgebra over S st

( b_{1} is bool-correct & b_{1} is non-empty )

end;
existence

ex b

( b

proof 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 A4, FINSEQ_3:25;

A6: ( the connectives of S . 1 in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by A5, RELAT_1:def 19, FUNCT_1:def 3;

(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;

(Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*p*> is Element of B, the bool-sort of S by A2, Th27;

let q be Element of B, the bool-sort of S;

(Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*p,q*> is Element of B, the bool-sort of S by A3, Th28;

end;
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 A4, FINSEQ_3:25;

A6: ( the connectives of S . 1 in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by A5, RELAT_1:def 19, FUNCT_1:def 3;

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)) . {};

(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*>;

(Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*p*> is Element of B, the bool-sort of S by A2, Th27;

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*>;

(Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*p,q*> is Element of B, the bool-sort of S by A3, Th28;

:: 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)) . {};

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*>;

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*>;

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;

\not ((\not p) \and (\not q)) is Element of B, the bool-sort of S ;

coherence

\not (p \and (\not q)) is Element of B, the bool-sort of S ;

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

\not ((\not p) \and (\not q)) is Element of B, the bool-sort of S ;

coherence

\not (p \and (\not q)) is Element of B, the bool-sort of S ;

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

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

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;

(p \and q) \or ((\not p) \and (\not q)) is Element of B, the bool-sort of S ;

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

(p \and q) \or ((\not p) \and (\not q)) is Element of B, the bool-sort of S ;

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

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 ;

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

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

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

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

( 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

ex b_{1} being strict BoolSignature st

( b_{1} is 10 -connectives & b_{1} is 1-1-connectives & b_{1} is 4,1 integer & b_{1} is bool-correct & not b_{1} is empty & not b_{1} is void )
by Th47;

end;

cluster non empty non void 1-1-connectives 10 -connectives strict bool-correct 4,1 integer for BoolSignature ;

existence ex b

( b

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

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 ;

existence

ex b_{1} being SortSymbol of S st b_{1} is integer

end;
existence

ex b

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

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 Def39, Th48;

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 A2, RELAT_1:def 19, FUNCT_1:def 3;

(Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {} is Element of the Sorts of A . I by Th48, Th26, A3;

A4: ( the connectives of S . 5 in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by A2, RELAT_1:def 19, FUNCT_1:def 3;

(Den ((In (( the connectives of S . 5), the carrier' of S)),A)) . {} is Element of the Sorts of A . I by Th48, Th26, A4;

let a be Element of the Sorts of A . I;

(Den ((In (( the connectives of S . 6), the carrier' of S)),A)) . <*a*> is Element of the Sorts of A . I by A1, Th27;

let b be Element of the Sorts of A . I;

(Den ((In (( the connectives of S . 7), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I by A1, Th28;

(Den ((In (( the connectives of S . 8), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I by A1, Th28;

(Den ((In (( the connectives of S . 9), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I by A1, Th28;

(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 A1, Th28;

end;
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 Def39, Th48;

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 A2, RELAT_1:def 19, FUNCT_1:def 3;

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)) . {};

(Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {} is Element of the Sorts of A . I by Th48, Th26, A3;

A4: ( the connectives of S . 5 in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by A2, RELAT_1:def 19, FUNCT_1:def 3;

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)) . {};

(Den ((In (( the connectives of S . 5), the carrier' of S)),A)) . {} is Element of the Sorts of A . I by Th48, Th26, A4;

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*>;

(Den ((In (( the connectives of S . 6), the carrier' of S)),A)) . <*a*> is Element of the Sorts of A . I by A1, Th27;

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*>;

(Den ((In (( the connectives of S . 7), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I by A1, Th28;

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*>;

(Den ((In (( the connectives of S . 8), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I by A1, Th28;

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*>;

(Den ((In (( the connectives of S . 9), the carrier' of S)),A)) . <*a,b*> is Element of the Sorts of A . I by A1, Th28;

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*>;

(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 A1, Th28;

:: 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)) . {};

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)) . {};

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*>;

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*>;

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*>;

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*>;

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*>;

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;

coherence

a + (- b) is Element of A,I ;

coherence

a + (- ((a div b) * b)) is Element of A,I ;

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

let I be integer SortSymbol of S;

let a, b be Element of A,I;

coherence

a + (- b) is Element of A,I ;

coherence

a + (- ((a div b) * b)) is Element of A,I ;

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

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

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;

coherence

not X . 1 is empty

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

coherence

not X . 1 is empty

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

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

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

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

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

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 ;

existence

ex b_{1} being strict non-empty bool-correct MSAlgebra over S st b_{1} is 4,1 integer
by Th49;

end;
existence

ex b

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

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;

coherence

for b_{1} being Element of the Sorts of A . 1 holds b_{1} is integer

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

coherence

for b

proof end;

definition

let I, N be set ;

let n be Nat;

let S be ConnectivesSignature ;

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

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

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

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;

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

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

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

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 ;

for b_{1}, b_{2} being strict BoolSignature st ManySortedSign(# the carrier of b_{1}, the carrier' of b_{1}, the Arity of b_{1}, the ResultSort of b_{1} #) = B +* C & the bool-sort of b_{1} = the bool-sort of B & the connectives of b_{1} = the connectives of B ^ the connectives of C & ManySortedSign(# the carrier of b_{2}, the carrier' of b_{2}, the Arity of b_{2}, the ResultSort of b_{2} #) = B +* C & the bool-sort of b_{2} = the bool-sort of B & the connectives of b_{2} = the connectives of B ^ the connectives of C holds

b_{1} = b_{2}
;

existence

ex b_{1} being strict BoolSignature st

( ManySortedSign(# the carrier of b_{1}, the carrier' of b_{1}, the Arity of b_{1}, the ResultSort of b_{1} #) = B +* C & the bool-sort of b_{1} = the bool-sort of B & the connectives of b_{1} = the connectives of B ^ the connectives of C )

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

for b

b

existence

ex b

( ManySortedSign(# the carrier of b

proof end;

:: deftheorem Def52 defines +* AOFA_A00:def 52 :

for B being non empty BoolSignature

for C being non empty ConnectivesSignature

for b_{3} being strict BoolSignature holds

( b_{3} = B +* C iff ( ManySortedSign(# the carrier of b_{3}, the carrier' of b_{3}, the Arity of b_{3}, the ResultSort of b_{3} #) = B +* C & the bool-sort of b_{3} = the bool-sort of B & the connectives of b_{3} = the connectives of B ^ the connectives of C ) );

for B being non empty BoolSignature

for C being non empty ConnectivesSignature

for b

( b

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 )

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 ;

coherence

not B +* C is empty

end;
let C be non empty ConnectivesSignature ;

coherence

not B +* C is empty

proof end;

registration

let B be non empty non void BoolSignature ;

let C be non empty ConnectivesSignature ;

coherence

not B +* C is void

end;
let C be non empty ConnectivesSignature ;

coherence

not B +* C is void

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

coherence

B +* C is n1 + n2 -connectives

end;
let B be non empty non void n1 -connectives BoolSignature ;

let C be non empty non void n2 -connectives ConnectivesSignature ;

coherence

B +* C is n1 + n2 -connectives

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

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 ;

ex b_{1} being non empty non void strict ConnectivesSignature st

( b_{1} is 1,I,N -array & b_{1} is 4 -connectives )

end;
cluster non empty non void V57() V165() strict 4 -connectives 1,I,N -array for ConnectivesSignature ;

existence ex b

( b

proof end;

theorem Th53: :: AOFA_A00:58

for n, m being Nat st m > 0 holds

for B being non empty non void b_{1} -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

for B being non empty non void b

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

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

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 ;

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

the ResultSort of B . ( the connectives of B . (n + 1)) <> the bool-sort of B;

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

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

ex b_{1} being strict BoolSignature st

( b_{1} is 1-1-connectives & b_{1} is 14 -connectives & b_{1} is 11,1,1 -array & b_{1} is 11 array-correct & b_{1} is 4,1 integer & b_{1} is bool-correct & not b_{1} is empty & not b_{1} is void )
end;

cluster non empty non void 1-1-connectives 14 -connectives strict bool-correct 4,1 integer 11,1,1 -array 11 array-correct for BoolSignature ;

existence ex b

( b

proof end;

registration

let S be non empty non void 11,1,1 -array BoolSignature ;

existence

ex b_{1} being SortSymbol of S st b_{1} is integer

end;
existence

ex b

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

the ResultSort of S . ( the connectives of S . 12) is SortSymbol of S by A1;

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

the ResultSort of S . ( the connectives of S . 12) is SortSymbol of S by A1;

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

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 . (the_array_sort_of 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;

(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;

(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;

(Den ((In (( the connectives of S . 12), the carrier' of S)),A)) . <*a,i,x*> is Element of the Sorts of A . (the_array_sort_of S) by A1, A2, Th29;

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

let a be Element of the Sorts of A . (the_array_sort_of 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;

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*>;

(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*>;

(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 . (the_array_sort_of S) 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*>;

(Den ((In (( the connectives of S . 12), the carrier' of S)),A)) . <*a,i,x*> is Element of the Sorts of A . (the_array_sort_of S) by A1, A2, Th29;

:: 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 . (the_array_sort_of S)

for I being integer SortSymbol of S holds length (a,I) = (Den ((In (( the connectives of S . 13), the carrier' of S)),A)) . <*a*>;

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 . (the_array_sort_of S)

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 . (the_array_sort_of S)

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*>;

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 . (the_array_sort_of S)

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 . (the_array_sort_of S)

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*>;

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 . (the_array_sort_of S)

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;

(Den ((In (( the connectives of S . 14), the carrier' of S)),A)) . <*i,x*> is Element of the Sorts of A . (the_array_sort_of S) by A1, A2, Th28;

end;
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 . (the_array_sort_of S) 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*>;

(Den ((In (( the connectives of S . 14), the carrier' of S)),A)) . <*i,x*> is Element of the Sorts of A . (the_array_sort_of S) by A1, A2, Th28;

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

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

<*X*> is non-empty

coherence

<*X,Y,Z*> is non-empty ;

end;
coherence

<*X*> is non-empty

proof end;

let Y, Z be non empty set ;coherence

<*X,Y,Z*> is non-empty ;

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 )

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

registration

let X be non empty integer-membered set ;

let Y be non empty set ;

let f be Element of product <*X,Y*>;

coherence

f . 1 is integer

end;
let Y be non empty set ;

let f be Element of product <*X,Y*>;

coherence

f . 1 is integer

proof end;

theorem Th56: :: AOFA_A00:61

for I, N being set

for S being non empty non void 1,b_{1},b_{2} -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 )

for S being non empty non void 1,b

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 ;

existence

ex b_{1} being strict non-empty MSAlgebra over S st b_{1} is 1,I,N -array

end;
let S be non empty non void 1,I,N -array ConnectivesSignature ;

existence

ex b

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

coherence

A1 +* A2 is strict non-empty MSAlgebra over S1 +* S2

end;
let S2 be non empty ConnectivesSignature ;

let A1 be non-empty MSAlgebra over S1;

let A2 be non-empty MSAlgebra over S2;

coherence

A1 +* A2 is strict non-empty MSAlgebra over S1 +* S2

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

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

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

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 b_{2} -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

for s, r being set st n >= 1 & m >= 1 holds

for B being non empty non void b

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

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

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

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 )

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 )

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 ;

existence

ex b_{1} being strict non-empty bool-correct MSAlgebra over S st

( b_{1} is 11,1,1 -array & b_{1} is 4,1 integer )

end;
existence

ex b

( b

proof end;

::$CT 5