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

theorem Th1: :: AOFA_A00:1

for A, B being set
for R being b₁ -valued Relation holds R .: B c= A

proof end;

definition

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

end;

registration

let I be set ;
let f be V2() ManySortedSet of I;
let i be object ;
let x be non empty set ;

cluster f +* (i,x) -> V2() ;

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

proof end;

end;

theorem Th2: :: AOFA_A00:2

for I being set
for f, g being ManySortedSet of I st f c= g holds
f # c= g #

proof end;

theorem :: AOFA_A00:3

for I being non empty set
for J being set
for A, B being ManySortedSet of I st A c= B holds
for f being Function of J,I holds A * f c= B * f

proof end;

registration

let f be Function-yielding Function;

cluster Frege f -> Function-yielding ;

coherence
Frege f is Function-yielding

proof end;

end;

theorem :: AOFA_A00:4

for f, g being Function-yielding Function holds doms (f * g) = (doms f) * g

proof end;

theorem Th5: :: AOFA_A00:5

for x, y being set
for f, g being Function st g = f . x holds
g . y = f .. (x,y)

proof end;

definition

let I be set ;
let i be Element of I;
let x be set ;

func i -singleton x -> ManySortedSet of I equals :: AOFA_A00:def 1
(EmptyMS I) +* (i,{x});

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

end;

:: deftheorem defines -singleton AOFA_A00:def 1 :
for I being set
for i being Element of I
for x being set holds i -singleton x = (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 = {} ) )

proof end;

theorem :: AOFA_A00:7

for I being non empty set
for i being Element of I
for A being ManySortedSet of I
for x being set st x in A . i holds
i -singleton x is ManySortedSubset of A

proof end;

definition

let I be set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
let i be set ;
assume A1: i in I ;
let j be set ;
assume A2: j in A . i ;
let v be set ;
assume A3: v in B . i ;

func F +* (i,j,v) -> ManySortedFunction of A,B means :: AOFA_A00:def 2
( it . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
it . s = F . s ) );

existence
ex b₁ being ManySortedFunction of A,B st
( b₁ . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b₁ . s = F . s ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of A,B st b₁ . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b₁ . s = F . s ) & b₂ . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b₂ . s = F . s ) holds
b₁ = b₂

proof end;

end;

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

canceled;

theorem :: AOFA_A00:8

canceled;

theorem :: AOFA_A00:9

canceled;

theorem :: AOFA_A00:10

canceled;

theorem :: AOFA_A00:11

canceled;

theorem :: AOFA_A00:12

canceled;

::$CD
::$CT 5

theorem :: AOFA_A00:13

for X being set
for a1, a2, a3, a4, a5, a6 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X holds
{a1,a2,a3,a4,a5,a6} c= X by ENUMSET1:def 4;

theorem :: AOFA_A00:14

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

theorem Th10: :: AOFA_A00:15

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

theorem :: AOFA_A00:16

for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} = {a1,a2,a3,a4,a5,a6,a7,a8,a9}

proof end;

theorem Th12: :: AOFA_A00:17

for a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 being object holds {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} = {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10}

proof end;

theorem Th13: :: AOFA_A00:18

for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds {a1,a2,a3} \/ {a4,a5,a6,a7,a8,a9} = {a1,a2,a3,a4,a5,a6,a7,a8,a9}

proof end;

theorem Th14: :: AOFA_A00:19

for a1, a2, a3, a4 being object st a1 <> a2 & a1 <> a3 & a1 <> a4 & a2 <> a3 & a2 <> a4 & a3 <> a4 holds
<*a1,a2,a3,a4*> is one-to-one

proof end;

definition

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

func <*a1,a2,a3,a4,a5,a6*> -> FinSequence equals :: AOFA_A00:def 3
<*a1,a2,a3,a4,a5*> ^ <*a6*>;

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

end;

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

definition

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

proof end;

end;

registration

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

cluster <*a1,a2,a3,a4,a5,a6*> -> 6 -element ;

coherence
<*a1,a2,a3,a4,a5,a6*> is 6 -element ;

end;

theorem :: AOFA_A00:20

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

proof end;

theorem :: AOFA_A00:21

for a1, a2, a3, a4, a5, a6 being object holds rng <*a1,a2,a3,a4,a5,a6*> = {a1,a2,a3,a4,a5,a6}

proof end;

definition

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

func <*a1,a2,a3,a4,a5,a6,a7*> -> FinSequence equals :: AOFA_A00:def 4
<*a1,a2,a3,a4,a5*> ^ <*a6,a7*>;

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

end;

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

definition

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

proof end;

end;

registration

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

cluster <*a1,a2,a3,a4,a5,a6,a7*> -> 7 -element ;

coherence
<*a1,a2,a3,a4,a5,a6,a7*> is 7 -element ;

end;

theorem :: AOFA_A00:22

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

proof end;

theorem :: AOFA_A00:23

for a1, a2, a3, a4, a5, a6, a7 being object holds rng <*a1,a2,a3,a4,a5,a6,a7*> = {a1,a2,a3,a4,a5,a6,a7}

proof end;

definition

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

func <*a1,a2,a3,a4,a5,a6,a7,a8*> -> FinSequence equals :: AOFA_A00:def 5
<*a1,a2,a3,a4,a5*> ^ <*a6,a7,a8*>;

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

end;

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

definition

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

proof end;

end;

registration

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

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

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

end;

theorem Th19: :: AOFA_A00:24

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

proof end;

theorem Th20: :: AOFA_A00:25

for a1, a2, a3, a4, a5, a6, a7, a8 being object holds rng <*a1,a2,a3,a4,a5,a6,a7,a8*> = {a1,a2,a3,a4,a5,a6,a7,a8}

proof end;

theorem Th21: :: AOFA_A00:26

for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds rng (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) = {a1,a2,a3,a4,a5,a6,a7,a8,a9}

proof end;

theorem Th22: :: AOFA_A00:27

Seg 9 = {1,2,3,4,5,6,7,8,9}

proof end;

theorem Th23: :: AOFA_A00:28

Seg 10 = {1,2,3,4,5,6,7,8,9,10}

proof end;

theorem Th24: :: AOFA_A00:29

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

proof end;

theorem Th25: :: AOFA_A00:30

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

proof end;

definition

let I, J be set ;
let S be ManySortedSet of I;

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

existence
ex b₁ being ManySortedFunction of I st
for i, j being set st i in I holds
( dom (b₁ . i) = S . i & ( j in S . i implies (b₁ . i) . j is ManySortedSet of J ) )

proof end;

end;

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

definition

let I, J be set ;
let S1 be ManySortedSet of I;
let S2 be ManySortedSet of J;

mode ManySortedMSSet of S1,S2 -> ManySortedMSSet of S1,J means :Def7: :: AOFA_A00:def 7
for i, a being set st i in I & a in S1 . i holds
(it . i) . a is ManySortedSubset of S2;

existence
ex b₁ being ManySortedMSSet of S1,J st
for i, a being set st i in I & a in S1 . i holds
(b₁ . i) . a is ManySortedSubset of S2

proof end;

end;

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

registration

let I be set ;
let X, Y be ManySortedSet of I;
let f be ManySortedMSSet of X,Y;
let x, y be set ;

cluster (f . x) . y -> Relation-like Function-like ;

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

proof end;

end;

definition

let S be ManySortedSign ;
let o, a be set ;
let r be Element of S;

pred o is_of_type a,r means :: AOFA_A00:def 8
( the Arity of S . o = a & the ResultSort of S . o = r );

end;

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

theorem Th26: :: AOFA_A00:31

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

proof end;

theorem Th27: :: AOFA_A00:32

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

proof end;

theorem Th28: :: AOFA_A00:33

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

proof end;

theorem Th29: :: AOFA_A00:34

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

proof end;

theorem :: AOFA_A00:35

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

definition

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

end;

registration

let S be non empty non void ManySortedSign ;
let U be V2() ManySortedSet of the carrier of S;
let C be ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S;
let v be ManySortedMSSet of U,U;

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

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

end;

registration

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;

cluster X,S -terms strict for VarMSAlgebra over S;

existence
ex b₁ being strict VarMSAlgebra over S st b₁ is X,S -terms

proof end;

end;

registration

let S be non empty non void ManySortedSign ;

cluster non-empty disjoint_valued for VarMSAlgebra over S;

existence
ex b₁ being VarMSAlgebra over S st
( b₁ is non-empty & b₁ is disjoint_valued )

proof end;

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

cluster X,S -terms all_vars_including -> non-empty X,S -terms for VarMSAlgebra over S;

coherence
for b₁ being X,S -terms VarMSAlgebra over S st b₁ is all_vars_including holds
b₁ is non-empty ;

end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty VarMSAlgebra over S;
let a be SortSymbol of S;
let t be Element of A,a;

func vf t -> ManySortedSubset of the Sorts of A equals :: AOFA_A00:def 9
( the free-vars of A . a) . t;

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

end;

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

definition

let S be non empty non void ManySortedSign ;
let A be non-empty VarMSAlgebra over S;

attr A is vf-correct means :: AOFA_A00:def 10
for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) holds
for b being Element of A,(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 ) } ;

end;

:: deftheorem defines vf-correct AOFA_A00:def 10 :
for S being non empty non void ManySortedSign
for A being non-empty VarMSAlgebra over S holds
( A is vf-correct iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) holds
for b being Element of A,(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

proof end;

theorem Th32: :: AOFA_A00:37

for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for G being GeneratorSet of A holds G is GeneratorSet of B

proof end;

theorem Th33: :: AOFA_A00:38

for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for G being GeneratorSet of A
for H being GeneratorSet of B st G = H & G is free holds
H is free

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;

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

existence
ex b₁ being X,S -terms strict VarMSAlgebra over S st
( b₁ is all_vars_including & b₁ is inheriting_operations & b₁ is free_in_itself )

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
let A be non-empty X,S -terms VarMSAlgebra over S;

attr A is vf-free means :Def11: :: AOFA_A00:def 11
for s, r being SortSymbol of S
for t being Element of A,s holds (vf t) . r = { (t | p) where p is Element of dom t : ((t | p) . {}) `2 = r } ;

end;

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

scheme :: AOFA_A00:sch 1
Scheme{ F₁() -> non empty set , F₂() -> V2() ManySortedSet of F₁(), F₃() -> V2() ManySortedSet of F₁(), F₄( object , object , object ) -> set } :

ex f being ManySortedMSSet of F₂(),F₃() st
for s, r being Element of F₁()
for t being Element of F₂() . s holds ((f . s) . t) . r = F₄(s,r,t)

provided

A1: for s, r being Element of F₁()
for t being Element of F₂() . s holds F₄(s,r,t) is Subset of (F₃() . r)

proof end;

theorem Th34: :: AOFA_A00:39

for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b₂,b₁ -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₂,b₁ -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st
( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;

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₁ being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st
( b₁ is strict & b₁ is vf-free )

proof end;

end;

theorem Th35: :: AOFA_A00:40

for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S
for s being SortSymbol of S
for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X

proof end;

theorem :: AOFA_A00:41

for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b₂,b₁ -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

proof end;

definition

let I be set ;
let S be ManySortedSet of I;

mode ManySortedElement of S -> ManySortedSet of I means :: AOFA_A00:def 12
for i being set st i in I holds
it . i is Element of S . i;

existence
ex b₁ being ManySortedSet of I st
for i being set st i in I holds
b₁ . i is Element of S . i

proof end;

end;

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

definition

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

end;

definition

let S be non empty non void ManySortedSign ;
let A be UndefMSAlgebra over S;
let s be SortSymbol of S;
let a be Element of A,s;

attr a is undefined means :: AOFA_A00:def 13
a = the undefined-map of A . s;

end;

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

definition

let S be non empty non void ManySortedSign ;
let A be UndefMSAlgebra over S;

attr A is undef-consequent means :: AOFA_A00:def 14
for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) & ex i being Nat ex s being SortSymbol of S ex a being Element of A,s st
( i in dom (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 ;

end;

:: deftheorem defines undef-consequent AOFA_A00:def 14 :
for S being non empty non void ManySortedSign
for A being UndefMSAlgebra over S holds
( A is undef-consequent iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) & ex i being Nat ex s being SortSymbol of S ex a being Element of A,s st
( i in dom (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;

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

end;

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

registration

let S be non empty ManySortedSign ;
let A be MSAlgebra over S;

cluster the Charact of A -> Function-yielding ;

coherence
the Charact of A is Function-yielding ;

end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;

cluster A -undef -> undef-consequent for UndefMSAlgebra over S;

coherence
for b₁ being UndefMSAlgebra over S st b₁ is A -undef holds
b₁ is undef-consequent ;

cluster non-empty strict A -undef for UndefMSAlgebra over S;

existence
ex b₁ being strict UndefMSAlgebra over S st
( b₁ is A -undef & b₁ is non-empty )

proof end;

end;

definition

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

end;

definition

let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
let A be ProgramAlgStr over J,T,X;

attr A is disjoint_valued means :: AOFA_A00:def 16
( the Sorts of T is disjoint_valued & the assignments of A is one-to-one );

end;

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

registration

let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;

cluster partial quasi_total non-empty strict for ProgramAlgStr over J,T,X;

existence
ex b₁ being strict ProgramAlgStr over J,T,X st
( b₁ is partial & b₁ is quasi_total & b₁ is non-empty )

proof end;

end;

registration

let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;

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₁ being non empty partial quasi_total non-empty strict ProgramAlgStr over J,T,X st
( b₁ is with_empty-instruction & b₁ is with_catenation & b₁ is with_if-instruction & b₁ is with_while-instruction )

proof end;

end;

theorem :: AOFA_A00:42

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

theorem Th38: :: AOFA_A00:43

for U1, U2 being preIfWhileAlgebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
ElementaryInstructions U1 = ElementaryInstructions U2

proof end;

theorem Th39: :: AOFA_A00:44

for U1, U2 being Universal_Algebra
for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2

proof end;

theorem Th40: :: AOFA_A00:45

for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 & S1 is opers_closed holds
S2 is opers_closed

proof end;

theorem Th41: :: AOFA_A00:46

for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for G being GeneratorSet of U1 holds G is GeneratorSet of U2

proof end;

theorem Th42: :: AOFA_A00:47

for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
signature U1 = signature U2

proof end;

registration

let J be non empty non void ManySortedSign ;
let T be MSAlgebra over J;
let X be GeneratorSet of T;

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₁ 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₁ is degenerated & b₁ is well_founded & b₁ is ECIW-strict & b₁ is infinite )

proof end;

end;

definition

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

end;

definition

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

end;

definition

let J be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over J;
let X be V2() GeneratorSet of T;
let A be non empty ProgramAlgStr over J,T,X;
let a be SortSymbol of J;
let x be Element of X . a;
let t be Element of T,a;

func x := (t,A) -> Algorithm of A equals :: AOFA_A00:def 17
the assignments of A . [x,t];

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

proof end;

end;

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

registration

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

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

existence
not for b₁ being ManySortedSubset of T holds b₁ is V2()

proof end;

end;

definition

let J be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over J;
let X be V2() GeneratorSet of T;

func C -States X -> Subset of (MSFuncs (X, the Sorts of C)) means :Def18: :: AOFA_A00:def 18
for s being ManySortedFunction of X, the Sorts of C holds
( s in it iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) );

existence
ex b₁ being Subset of (MSFuncs (X, the Sorts of C)) st
for s being ManySortedFunction of X, the Sorts of C holds
( s in b₁ iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (MSFuncs (X, the Sorts of C)) st ( for s being ManySortedFunction of X, the Sorts of C holds
( s in b₁ 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₂ iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) ) holds
b₁ = b₂

proof end;

end;

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

registration

let J be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over J;
let C be image of T;
let X be V2() GeneratorSet of T;

cluster C -States X -> non empty ;

coherence
not C -States X is empty

proof end;

end;

theorem Th43: :: AOFA_A00:48

for B being non empty non void ManySortedSign
for T, C being non-empty MSAlgebra over B
for X being V2() GeneratorSet of T
for g being set st g in C -States X holds
g is ManySortedFunction of X, the Sorts of C

proof end;

registration

let B be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;

cluster -> Relation-like Function-like for Element of C -States X;

coherence
for b₁ being Element of C -States X holds
( b₁ is Relation-like & b₁ is Function-like )

proof end;

end;

registration

let B be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;

cluster -> the carrier of B -defined Function-yielding for Element of C -States X;

coherence
for b₁ being Element of C -States X holds
( b₁ is Function-yielding & b₁ is the carrier of B -defined )

proof end;

end;

registration

let B be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over B;
let C be image of T;
let X be V2() GeneratorSet of T;

cluster -> total for Element of C -States X;

coherence
for b₁ being Element of C -States X holds b₁ is total by Th43;

end;

definition

let B be non empty non void ManySortedSign ;
let T, C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;
let a be SortSymbol of B;
let x be Element of X . a;
let f be Element of C,a;

func f -States (X,x) -> Subset of (C -States X) means :: AOFA_A00:def 19
for s being ManySortedFunction of X, the Sorts of C holds
( s in it iff ( s in C -States X & (s . a) . x <> f ) );

existence
ex b₁ being Subset of (C -States X) st
for s being ManySortedFunction of X, the Sorts of C holds
( s in b₁ iff ( s in C -States X & (s . a) . x <> f ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (C -States X) st ( for s being ManySortedFunction of X, the Sorts of C holds
( s in b₁ iff ( s in C -States X & (s . a) . x <> f ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds
( s in b₂ iff ( s in C -States X & (s . a) . x <> f ) ) ) holds
b₁ = b₂

proof end;

end;

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

registration

let B be non empty non void ManySortedSign ;
let T be non-empty free MSAlgebra over B;
let C be non-empty MSAlgebra over B;
let X be V2() GeneratorSet of T;

cluster C -States X -> non empty ;

coherence
not C -States X is empty

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let o be OperSymbol of S;

cluster -> Relation-like Function-like for Element of Args (o,A);

coherence
for b₁ being Element of Args (o,A) holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

end;

registration

let B be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of B;
let T be non-empty X,B -terms MSAlgebra over B;
let C be image of T;
let G be V2() GeneratorSet of T;

cluster C -States G -> non empty ;

coherence
not C -States G is empty ;

end;

definition

let B be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of B;
let T be non-empty X,B -terms MSAlgebra over B;
let C be image of T;
let a be SortSymbol of B;
let t be Element of T,a;
let s be Function-yielding Function;
given h being ManySortedFunction of T,C, Q being GeneratorSet of T such that A1: ( h is_homomorphism T,C & Q = doms s & s = h || Q ) ;

func t value_at (C,s) -> Element of C,a means :: AOFA_A00:def 20
ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & it = (f . a) . t );

existence
ex b₁ 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₁ = (f . a) . t )

proof end;

uniqueness
for b₁, b₂ 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₁ = (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₂ = (f . a) . t ) holds
b₁ = b₂ by EXTENS_1:19;

end;

:: deftheorem defines value_at AOFA_A00:def 20 :
for B being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of B
for T being non-empty b₂,b₁ -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₈ being Element of C,a holds
( b₈ = 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₈ = (f . a) . t ) );

definition

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

end;

definition

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;
let G be GeneratorSystem over S,X,T;
let s be SortSymbol of S;

mode Element of G,s -> Element of T,s means :Def21: :: AOFA_A00:def 21
it in the generators of G . s;

existence
ex b₁ being Element of T,s st b₁ in the generators of G . s

proof end;

end;

:: deftheorem Def21 defines Element AOFA_A00:def 21 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for T being b₂,b₁ -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₆ being Element of T,s holds
( b₆ is Element of G,s iff b₆ in the generators of G . s );

definition

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;
let G be GeneratorSystem over S,X,T;
let s be SortSymbol of S;

func G . s -> Component of the generators of G equals :: AOFA_A00:def 22
the generators of G . s;

coherence
the generators of G . s is Component of the generators of G ;
let g be Element of G,s;

func supp-var g -> Element of (FreeGen X) . s equals :: AOFA_A00:def 23
( the supported-var of G . s) . g;

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

end;

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

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

definition

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S;
let G be GeneratorSystem over S,X,T;
let s be SortSymbol of S;
let g be Element of G,s;
assume A1: ( the supported-term of G . s) . g is ManySortedFunction of vf g, the Sorts of T ;

func supp-term g -> ManySortedFunction of vf g, the Sorts of T equals :: AOFA_A00:def 24
( the supported-term of G . s) . g;

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

end;

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

definition

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S;
let C be image of T;
let G be GeneratorSystem over S,X,T;

attr G is C -supported means :: AOFA_A00:def 25
( FreeGen X is ManySortedSubset of the generators of G & ( for s being SortSymbol of S holds
( dom ( the supported-term of G . s) = G . s & ( for t being Element of G,s holds
( ( the supported-term of G . s) . t is ManySortedFunction of vf t, the Sorts of T & ( t in (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 ) ) ) ) ) );

end;

:: deftheorem defines -supported AOFA_A00:def 25 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for T being b₂,b₁ -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 ) ) ) ) ) ) );

definition

let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of S;
let A be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S;
let C be image of A;
let G be GeneratorSystem over S,X,A;
assume A1: G is C -supported ;
let s be Element of C -States the generators of G;
let r be SortSymbol of S;
let v be Element of C,r;
let t be Element of G,r;

func succ (s,t,v) -> Element of C -States the generators of G means :: AOFA_A00:def 26
( (it . r) . t = v & ( for p being SortSymbol of S
for x being Element of (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
ex b₁ being Element of C -States the generators of G st
( (b₁ . 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₁ . 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₁ . p) . x = q value_at (C,u) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of C -States the generators of G st (b₁ . 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₁ . 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₁ . p) . x = q value_at (C,u) ) ) ) & (b₂ . 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₂ . 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₂ . p) . x = q value_at (C,u) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines succ AOFA_A00:def 26 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of S
for A being b₂,b₁ -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₁₀ being Element of C -States the generators of G holds
( b₁₀ = succ (s,t,v) iff ( (b₁₀ . 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₁₀ . 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₁₀ . p) . x = q value_at (C,u) ) ) ) ) );

definition

let B be non empty non void ManySortedSign ;
let Y be V2() ManySortedSet of the carrier of B;
let T be Y,B -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over B;
let C be image of T;
let X be GeneratorSystem over B,Y,T;
let A be preIfWhileAlgebra of the generators of X;
let a be SortSymbol of B;
let x be Element of the generators of X . a;
let z be Element of C,a;

func C -Execution (A,x,z) -> Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) means :: AOFA_A00:def 27
for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in it iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) );

existence
ex b₁ 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₁ iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) )

proof end;

uniqueness
for b₁, b₂ 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₁ 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₂ 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₁ = b₂

proof end;

end;

:: deftheorem defines -Execution AOFA_A00:def 27 :
for B being non empty non void ManySortedSign
for Y being V2() ManySortedSet of the carrier of B
for T being b₂,b₁ -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₁₀ being Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) holds
( b₁₀ = 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₁₀ iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) ) );

definition

attr c₁ is strict ;
struct ConnectivesSignature -> ManySortedSign ;
aggr ConnectivesSignature(# carrier, carrier', Arity, ResultSort, connectives #) -> ConnectivesSignature ;
sel connectives c₁ -> FinSequence of the carrier' of c₁;

end;

definition

let S be ConnectivesSignature ;

attr S is 1-1-connectives means :Def28: :: AOFA_A00:def 28
the connectives of S is one-to-one ;

end;

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

definition

let n be Nat;
let S be ConnectivesSignature ;

attr S is n -connectives means :Def29: :: AOFA_A00:def 29
len the connectives of S = n;

end;

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

registration

let n be Nat;

cluster non empty non void strict n -connectives for ConnectivesSignature ;

existence
ex b₁ being strict ConnectivesSignature st
( b₁ is n -connectives & not b₁ is empty & not b₁ is void )

proof end;

end;

definition

attr c₁ is strict ;
struct BoolSignature -> ConnectivesSignature ;
aggr BoolSignature(# carrier, carrier', Arity, ResultSort, bool-sort, connectives #) -> BoolSignature ;
sel bool-sort c₁ -> Element of the carrier of c₁;

end;

registration

let n be Nat;

cluster non empty non void n -connectives strict for BoolSignature ;

existence
ex b₁ being strict BoolSignature st
( b₁ is n -connectives & not b₁ is empty & not b₁ is void )

proof end;

end;

definition

let B be BoolSignature ;

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

end;

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

registration

cluster non empty non void 1-1-connectives 3 -connectives strict bool-correct for BoolSignature ;

existence
ex b₁ being strict BoolSignature st
( b₁ is 3 -connectives & b₁ is 1-1-connectives & b₁ is bool-correct & not b₁ is empty & not b₁ is void )

proof end;

end;

registration

cluster non empty non void 1-1-connectives for ConnectivesSignature ;

existence
ex b₁ being ConnectivesSignature st
( b₁ is 1-1-connectives & not b₁ is empty & not b₁ is void )

proof end;

end;

registration

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

cluster the connectives of S -> one-to-one ;

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

end;

definition

let S be non empty non void BoolSignature ;
let B be MSAlgebra over S;

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

end;

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

theorem Th44: :: AOFA_A00:49

for A being non empty set
for n being Nat
for f being Function of (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;

cluster Relation-like A * -defined A -valued Function-like non empty homogeneous quasi_total n -ary for Element of bool [:(A *),A:];

existence
ex b₁ being non empty homogeneous quasi_total PartFunc of (A *),A st b₁ is n -ary

proof end;

end;

scheme :: AOFA_A00:sch 2
Sch1{ F₁() -> non empty set , F₂( set ) -> Element of F₁() } :

ex f being non empty homogeneous quasi_total 1 -ary PartFunc of (F₁() *),F₁() st
for a being Element of F₁() holds f . <*a*> = F₂(a)

proof end;

scheme :: AOFA_A00:sch 3
Sch2{ F₁() -> non empty set , F₂( set , set ) -> Element of F₁() } :

ex f being non empty homogeneous quasi_total 2 -ary PartFunc of (F₁() *),F₁() st
for a, b being Element of F₁() holds f . <*a,b*> = F₂(a,b)

proof end;

theorem Th45: :: AOFA_A00:50

for S being non empty non void ManySortedSign
for A being V2() ManySortedSet of the carrier of S
for f being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
for o being OperSymbol of S
for d being Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) holds f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S

proof end;

theorem Th46: :: AOFA_A00:51

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

proof end;

registration

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

cluster strict non-empty bool-correct for MSAlgebra over S;

existence
ex b₁ being strict MSAlgebra over S st
( b₁ is bool-correct & b₁ is non-empty )

proof end;

end;

definition

let S be non empty non void bool-correct BoolSignature ;
let B be non-empty MSAlgebra over S;
set f = the bool-sort of S;
set L = B;
A1: the connectives of S . 1 is_of_type {} , the bool-sort of S by Def30;
A2: the connectives of S . 2 is_of_type <* the bool-sort of S*>, the bool-sort of S by Def30;
A3: the connectives of S . 3 is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S by Def30;
A4: len the connectives of S >= 3 by Def30;
then ( 1 <= len the connectives of S & 2 <= len the connectives of S ) by XXREAL_0:2;
then A5: ( 2 in dom the connectives of S & 1 in dom the connectives of S & 3 in dom the connectives of S ) by 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)) . {} is Element of B, the bool-sort of S by A1, Th26, A6;
let p be Element of B, the bool-sort of S;

func \not p -> Element of B, the bool-sort of S equals :: AOFA_A00:def 33
(Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*p*>;

coherence
(Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*p*> is Element of B, the bool-sort of S by 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*> is Element of B, the bool-sort of S by A3, Th28;

end;

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

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

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

definition

let S be non empty non void bool-correct BoolSignature ;
let B be non-empty MSAlgebra over S;
let p, q be Element of B, the bool-sort of S;

func p \or q -> Element of B, the bool-sort of S equals :: AOFA_A00:def 35
\not ((\not p) \and (\not q));

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

func p \imp q -> Element of B, the bool-sort of S equals :: AOFA_A00:def 36
\not (p \and (\not q));

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

end;

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

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

definition

let S be non empty non void bool-correct BoolSignature ;
let B be non-empty MSAlgebra over S;
let p, q be Element of B, the bool-sort of S;

func p \iff q -> Element of B, the bool-sort of S equals :: AOFA_A00:def 37
(p \and q) \or ((\not p) \and (\not q));

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

end;

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

definition

let i be Nat;
let s be set ;
let S be BoolSignature ;

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

end;

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

theorem Th47: :: AOFA_A00:52

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

proof end;

registration

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

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

end;

definition

let S be non empty non void BoolSignature ;
let I be SortSymbol of S;

attr I is integer means :Def39: :: AOFA_A00:def 39
I = 1;

end;

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

registration

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

cluster integer for Element of the carrier of S;

existence
ex b₁ being SortSymbol of S st b₁ is integer

proof end;

end;

theorem Th48: :: AOFA_A00:53

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

proof end;

definition

let S be non empty non void 4,1 integer BoolSignature ;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
set f = the bool-sort of S;
set L = A;
A1: ( I = 1 & I <> the bool-sort of S & the connectives of S . 4 is_of_type {} ,I & the connectives of S . (4 + 1) is_of_type {} ,I & the connectives of S . 4 <> the connectives of S . (4 + 1) & the connectives of S . (4 + 2) is_of_type <*I*>,I & the connectives of S . (4 + 3) is_of_type <*I,I*>,I & the connectives of S . (4 + 4) is_of_type <*I,I*>,I & the connectives of S . (4 + 5) is_of_type <*I,I*>,I & the connectives of S . (4 + 3) <> the connectives of S . (4 + 4) & the connectives of S . (4 + 3) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 4) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 6) is_of_type <*I,I*>, the bool-sort of S ) by 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)) . {} 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)) . {} 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*> 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*> 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*> 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*> 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*> is Element of the Sorts of A . the bool-sort of S by A1, Th28;

end;

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

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

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

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

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

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

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

definition

let S be non empty non void 4,1 integer BoolSignature ;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
let a, b be Element of A,I;

func a - b -> Element of A,I equals :: AOFA_A00:def 47
a + (- b);

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

func a mod b -> Element of A,I equals :: AOFA_A00:def 48
a + (- ((a div b) * b));

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

end;

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

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

registration

let S be non empty non void 4,1 integer BoolSignature ;
let X be V2() ManySortedSet of the carrier of S;

cluster X . 1 -> non empty ;

coherence
not X . 1 is empty

proof end;

end;

definition

let n be Nat;
let s be set ;
let S be non empty non void bool-correct BoolSignature ;
let A be bool-correct MSAlgebra over S;

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

end;

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

theorem Th49: :: AOFA_A00:54

for n being Nat
for I being set st n >= 1 holds
for S being non empty non void bool-correct BoolSignature st S is n,I integer holds
ex A being strict non-empty bool-correct MSAlgebra over S st A is n,I integer

proof end;

registration

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

cluster strict non-empty V166(S) bool-correct 4,1 integer for MSAlgebra over S;

existence
ex b₁ being strict non-empty bool-correct MSAlgebra over S st b₁ is 4,1 integer by Th49;

end;

theorem :: AOFA_A00:55

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

proof end;

registration

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

cluster -> integer for Element of the Sorts of A . 1;

coherence
for b₁ being Element of the Sorts of A . 1 holds b₁ is integer

proof end;

end;

definition

let I, N be set ;
let n be Nat;
let S be ConnectivesSignature ;

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

end;

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

definition

let S be non empty non void ConnectivesSignature ;
let I, N be set ;
let n be Nat;
let A be MSAlgebra over S;

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

end;

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

definition

let B be non empty BoolSignature ;
let C be non empty ConnectivesSignature ;

func B +* C -> strict BoolSignature means :Def52: :: AOFA_A00:def 52
( ManySortedSign(# the carrier of it, the carrier' of it, the Arity of it, the ResultSort of it #) = B +* C & the bool-sort of it = the bool-sort of B & the connectives of it = the connectives of B ^ the connectives of C );

uniqueness
for b₁, b₂ being strict BoolSignature st ManySortedSign(# the carrier of b₁, the carrier' of b₁, the Arity of b₁, the ResultSort of b₁ #) = B +* C & the bool-sort of b₁ = the bool-sort of B & the connectives of b₁ = the connectives of B ^ the connectives of C & ManySortedSign(# the carrier of b₂, the carrier' of b₂, the Arity of b₂, the ResultSort of b₂ #) = B +* C & the bool-sort of b₂ = the bool-sort of B & the connectives of b₂ = the connectives of B ^ the connectives of C holds
b₁ = b₂ ;
existence
ex b₁ being strict BoolSignature st
( ManySortedSign(# the carrier of b₁, the carrier' of b₁, the Arity of b₁, the ResultSort of b₁ #) = B +* C & the bool-sort of b₁ = the bool-sort of B & the connectives of b₁ = the connectives of B ^ the connectives of C )

proof end;

end;

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

theorem Th51: :: AOFA_A00:56

for B being non empty BoolSignature
for C being non empty ConnectivesSignature holds
( the carrier of (B +* C) = the carrier of B \/ the carrier of C & the carrier' of (B +* C) = the carrier' of B \/ the carrier' of C & the Arity of (B +* C) = the Arity of B +* the Arity of C & the ResultSort of (B +* C) = the ResultSort of B +* the ResultSort of C )

proof end;

registration

let B be non empty BoolSignature ;
let C be non empty ConnectivesSignature ;

cluster B +* C -> non empty strict ;

coherence
not B +* C is empty

proof end;

end;

registration

let B be non empty non void BoolSignature ;
let C be non empty ConnectivesSignature ;

cluster B +* C -> non void strict ;

coherence
not B +* C is void

proof end;

end;

registration

let n1, n2 be Nat;
let B be non empty non void n1 -connectives BoolSignature ;
let C be non empty non void n2 -connectives ConnectivesSignature ;

cluster B +* C -> n1 + n2 -connectives strict ;

coherence
B +* C is n1 + n2 -connectives

proof end;

end;

theorem Th52: :: AOFA_A00:57

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

proof end;

registration

let I, N be set ;

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

existence
ex b₁ being non empty non void strict ConnectivesSignature st
( b₁ is 1,I,N -array & b₁ is 4 -connectives )

proof end;

end;

theorem Th53: :: AOFA_A00:58

for n, m being Nat st m > 0 holds
for B being non empty non void b₁ -connectives BoolSignature
for I, N being set
for C being non empty non void ConnectivesSignature st C is m,I,N -array holds
B +* C is n + m,I,N -array

proof end;

theorem Th54: :: AOFA_A00:59

for m being Nat st m > 0 holds
for s being set
for B being non empty non void BoolSignature
for C being non empty non void ConnectivesSignature st B is m,s integer & the carrier' of B misses the carrier' of C holds
B +* C is m,s integer

proof end;

theorem Th55: :: AOFA_A00:60

for B being non empty non void bool-correct BoolSignature
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
B +* C is bool-correct

proof end;

definition

let n be Nat;
let B be BoolSignature ;

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

end;

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

registration

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₁ being strict BoolSignature st
( b₁ is 1-1-connectives & b₁ is 14 -connectives & b₁ is 11,1,1 -array & b₁ is 11 array-correct & b₁ is 4,1 integer & b₁ is bool-correct & not b₁ is empty & not b₁ is void )

proof end;

end;

registration

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

cluster integer for Element of the carrier of S;

existence
ex b₁ being SortSymbol of S st b₁ is integer

proof end;

end;

definition

let S be non empty non void 11,1,1 -array BoolSignature ;
consider J, K, L being Element of S such that
A1: ( L = 1 & K = 1 & J <> L & J <> K & the connectives of S . 11 is_of_type <*J,K*>,L & the connectives of S . (11 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (11 + 2) is_of_type <*J*>,K & the connectives of S . (11 + 3) is_of_type <*K,L*>,J ) by Def50;

func the_array_sort_of S -> SortSymbol of S equals :: AOFA_A00:def 54
the ResultSort of S . ( the connectives of S . 12);

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

end;

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

definition

let S be non empty non void 4,1 integer 11,1,1 -array BoolSignature ;
let A be non-empty MSAlgebra over S;
let a be Element of the Sorts of A . (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*> is Element of the Sorts of A . I by A1, A2, Th27;
let i be Element of the Sorts of A . I;

func a . i -> Element of the Sorts of A . I equals :: AOFA_A00:def 56
(Den ((In (( the connectives of S . 11), the carrier' of S)),A)) . <*a,i*>;

coherence
(Den ((In (( the connectives of S . 11), the carrier' of S)),A)) . <*a,i*> is Element of the Sorts of A . I by A1, A2, Th28;
let x be Element of the Sorts of A . I;

func (a,i) <- x -> Element of the Sorts of A . (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*> is Element of the Sorts of A . (the_array_sort_of S) by A1, A2, Th29;

end;

:: deftheorem defines length AOFA_A00:def 55 :
for S being non empty non void 4,1 integer 11,1,1 -array BoolSignature
for A being non-empty MSAlgebra over S
for a being Element of the Sorts of A . (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*>;

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

definition

let S be non empty non void 4,1 integer 11,1,1 -array BoolSignature ;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
consider J, K, L being Element of S such that
A1: ( L = 1 & K = 1 & J <> L & J <> K & the connectives of S . 11 is_of_type <*J,K*>,L & the connectives of S . (11 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (11 + 2) is_of_type <*J*>,K & the connectives of S . (11 + 3) is_of_type <*K,L*>,J ) by Def50;
A2: I = 1 by Def39;
let i, x be Element of the Sorts of A . I;

func init.array (i,x) -> Element of the Sorts of A . (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*> is Element of the Sorts of A . (the_array_sort_of S) by A1, A2, Th28;

end;

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

registration

let X be non empty set ;

cluster <*X*> -> non-empty ;

coherence
<*X*> is non-empty

proof end;

let Y, Z be non empty set ;

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

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

end;

registration

let X be functional non empty set ;
let Y, Z be non empty set ;
let f be Element of product <*X,Y,Z*>;

cluster f . 1 -> Relation-like Function-like ;

coherence
( f . 1 is Relation-like & f . 1 is Function-like )

proof end;

end;

registration

let X be non empty integer-membered set ;
let Y be non empty set ;
let f be Element of product <*X,Y*>;

cluster f . 1 -> integer ;

coherence
f . 1 is integer

proof end;

end;

theorem Th56: :: AOFA_A00:61

for I, N being set
for S being non empty non void 1,b₁,b₂ -array ConnectivesSignature
for Y being non empty set
for X being V2() ManySortedSet of Y st ( the ResultSort of S . ( the connectives of S . 2) nin Y or X . ( the ResultSort of S . ( the connectives of S . 2)) = (X . I) ^omega ) & X . N = INT & I in Y holds
ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates X )

proof end;

registration

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

cluster strict non-empty V166(S) 1,I,N -array for MSAlgebra over S;

existence
ex b₁ being strict non-empty MSAlgebra over S st b₁ is 1,I,N -array

proof end;

end;

definition

let S1 be non empty BoolSignature ;
let S2 be non empty ConnectivesSignature ;
let A1 be non-empty MSAlgebra over S1;
let A2 be non-empty MSAlgebra over S2;

func (S1,A1) +* A2 -> strict non-empty MSAlgebra over S1 +* S2 equals :: AOFA_A00:def 59
A1 +* A2;

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

proof end;

end;

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

theorem Th57: :: AOFA_A00:62

for B being non empty non void bool-correct BoolSignature
for A1 being non-empty bool-correct MSAlgebra over B
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
(B,A1) +* A2 is bool-correct

proof end;

theorem Th58: :: AOFA_A00:63

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

proof end;

theorem Th59: :: AOFA_A00:64

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

proof end;

theorem Th60: :: AOFA_A00:65

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

proof end;

theorem Th61: :: AOFA_A00:66

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

proof end;

theorem Th62: :: AOFA_A00:67

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

proof end;

theorem Th63: :: AOFA_A00:68

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

proof end;

theorem Th64: :: AOFA_A00:69

for s, I being set
for S being non empty non void bool-correct BoolSignature st S is 4,I integer holds
for X being non empty set st s in the carrier of S & s <> I & s <> the bool-sort of S holds
ex A being non-empty bool-correct MSAlgebra over S st
( A is 4,I integer & the Sorts of A . s = X )

proof end;

registration

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

cluster strict non-empty V166(S) bool-correct 4,1 integer 11,1,1 -array for MSAlgebra over S;

existence
ex b₁ being strict non-empty bool-correct MSAlgebra over S st
( b₁ is 11,1,1 -array & b₁ is 4,1 integer )

proof end;

end;