:: Program Algebra over an Algebra
:: by Grzegorz Bancerek
::
:: Received August 27, 2012
:: Copyright (c) 2012-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies AOFA_A00, AOFA_000, PROB_2, UNIALG_1, FUNCT_1, RELAT_1, NAT_1,
FUNCT_2, XBOOLE_0, MSUALG_1, FUNCOP_1, TREES_4, FINSET_1, MCART_1,
SUBSET_1, ZF_MODEL, PBOOLE, INCPROJ, MSUALG_3, AOFA_I00, CARD_3,
ZFMISC_1, MSAFREE, MEMBERED, MSATERM, STRUCT_0, PZFMISC1, GRAPHSP,
TARSKI, MARGREL1, REALSET1, PRELAMB, COMPUT_1, CARD_1, PARTFUN1, FUNCT_7,
FINSEQ_1, UNIALG_2, WELLORD1, XXREAL_0, XBOOLEAN, INT_1, NUMBERS,
ARYTM_1, ARYTM_3, ORDINAL4, FUNCT_4, FINSEQ_2, ORDINAL1, MSUALG_2,
FUNCT_6, FUNCT_5, FINSEQ_4, MSAFREE4, EXCHSORT, AFINSQ_1, RFINSEQ,
MATRIX_7, ALGSTR_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
PARTFUN1, ORDINAL1, TREES_1, ENUMSET1, FUNCT_2, FUNCOP_1, FINSET_1,
FINSEQ_2, FINSEQ_1, FINSEQ_4, RFINSEQ, FUNCT_4, BINOP_1, CARD_1, CARD_3,
PROB_2, NUMBERS, MEMBERED, FUNCT_7, COMPUT_1, PBOOLE, PZFMISC1, MARGREL1,
AFINSQ_1, XXREAL_0, XCMPLX_0, INT_1, FUNCT_5, FUNCT_6, TREES_2, TREES_4,
STRUCT_0, MATRIX_7, BORSUK_7, UNIALG_1, UNIALG_2, FREEALG, MSUALG_1,
MSUALG_2, MSUALG_3, MSUALG_6, CIRCCOMB, AUTALG_1, MSAFREE, MSAFREE1,
MSATERM, MSAFREE3, AOFA_000, MSAFREE4, EXCHSORT;
constructors PZFMISC1, AOFA_000, CATALG_1, PUA2MSS1, MSAFREE1, MSUALG_3,
COMPUT_1, FINSEQ_4, MSAFREE4, AUTALG_1, EXCHSORT, AFINSQ_1, CIRCCOMB,
RFINSEQ, MATRIX_7, BORSUK_7, BINOP_1;
registrations RELAT_1, RELSET_1, FUNCT_1, FUNCOP_1, FINSEQ_1, UNIALG_1,
STRUCT_0, PUA2MSS1, PBOOLE, MSUALG_1, INSTALG1, MSAFREE1, CARD_3,
XBOOLE_0, AOFA_000, MSAFREE, ORDINAL1, INT_1, XREAL_0, FUNCT_4, FINSEQ_4,
CARD_1, MARGREL1, SUBSET_1, FINSEQ_2, NUMBERS, CATALG_1, TREES_2,
MSUALG_2, TREES_3, MSAFREE4, EXCHSORT, NAT_1, XTUPLE_0, FUNCT_7,
AFINSQ_1, XBOOLEAN, MEMBERED, FOMODEL0, PRE_CIRC, BORSUK_7, PRE_POLY;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminary
reserve i for Nat, x,y for set;
reserve S for non empty non void ManySortedSign;
reserve X for non-empty ManySortedSet of S;
theorem :: AOFA_A00:1
for A,B being set
for R being A-valued Relation
holds R.:B c= A;
definition
let I be set;
let f be ManySortedSet of I;
let i be object;
let x;
redefine func f+*(i,x) -> ManySortedSet of I;
end;
registration
let I be set;
let f be non-empty ManySortedSet of I;
let i be object;
let x be non empty set;
cluster f+*(i,x) -> non-empty;
end;
theorem :: AOFA_A00:2
for I being set
for f,g being ManySortedSet of I st f c= g holds f# c= g#;
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
for f being Function of J,I holds A*f c= B*f;
registration
let f be Function-yielding Function;
cluster Frege f -> Function-yielding;
end;
theorem :: AOFA_A00:4
for f,g being Function-yielding Function holds doms (f*g) = (doms f)*g;
theorem :: AOFA_A00:5
for f,g being Function st g = f.x holds g.y = f..(x,y);
definition
let I be set;
let i be Element of I;
let x;
func i-singleton(x) -> ManySortedSet of I equals
:: AOFA_A00:def 1
(EmptyMS I)+*(i,{x});
end;
theorem :: AOFA_A00:6
for I being non empty set
for i,j being Element of I
for x holds (i-singleton x).i = {x} & (i <> j implies (i-singleton x).j = {})
;
theorem :: AOFA_A00:7
for I being non empty set
for i being Element of I
for A being ManySortedSet of I
for x st x in A.i holds i-singleton x is ManySortedSubset of A;
definition
let I be set;
let A,B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
let i be set such that i in I;
let j be set such that j in A.i;
let v be set such that 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;
end;
::$CD
::$CT 5
theorem :: AOFA_A00:13
for X being set, 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;
theorem :: AOFA_A00:14
for X being set, 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;
theorem :: AOFA_A00:15
for X being set, 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;
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};
theorem :: 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};
theorem :: 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};
theorem :: 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;
definition
let a1,a2,a3,a4,a5,a6 be object;
func <*a1,a2,a3,a4,a5,a6*> -> FinSequence equals
:: AOFA_A00:def 4
<*a1,a2,a3,a4,a5*>^<*a6*>;
end;
definition
let X be non empty set;
let a1,a2,a3,a4,a5,a6 be Element of X;
redefine func <*a1,a2,a3,a4,a5,a6*> -> FinSequence of X;
end;
registration
let a1,a2,a3,a4,a5,a6 be object;
cluster <*a1,a2,a3,a4,a5,a6*> -> 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;
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};
definition
let a1,a2,a3,a4,a5,a6,a7 be object;
func <*a1,a2,a3,a4,a5,a6,a7*> -> FinSequence equals
:: AOFA_A00:def 5
<*a1,a2,a3,a4,a5*>^<*a6,a7*>;
end;
definition
let X be non empty set;
let a1,a2,a3,a4,a5,a6,a7 be Element of X;
redefine func <*a1,a2,a3,a4,a5,a6,a7*> -> FinSequence of X;
end;
registration
let a1,a2,a3,a4,a5,a6,a7 be object;
cluster <*a1,a2,a3,a4,a5,a6,a7*> -> 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;
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};
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 6
<*a1,a2,a3,a4,a5*>^<*a6,a7,a8*>;
end;
definition
let X be non empty set;
let a1,a2,a3,a4,a5,a6,a7,a8 be Element of X;
redefine func <*a1,a2,a3,a4,a5,a6,a7,a8*> -> FinSequence of X;
end;
registration
let a1,a2,a3,a4,a5,a6,a7,a8 be object;
cluster <*a1,a2,a3,a4,a5,a6,a7,a8*> -> 8-element;
end;
theorem :: 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;
theorem :: 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};
theorem :: 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};
theorem :: AOFA_A00:27
Seg 9 = {1,2,3,4,5,6,7,8,9};
theorem :: AOFA_A00:28
Seg 10 = {1,2,3,4,5,6,7,8,9,10};
theorem :: 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;
theorem :: 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;
definition
let I,J be set;
let S be ManySortedSet of I;
mode ManySortedMSSet of S,J -> ManySortedFunction of I means
:: AOFA_A00:def 7
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);
end;
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
:: AOFA_A00:def 8
for i,a being set st i in I & a in S1.i
holds it.i.a is ManySortedSubset of S2;
end;
registration
let I be set;
let X,Y be ManySortedSet of I;
let f be ManySortedMSSet of X,Y;
let x,y;
cluster f.x.y -> Function-like Relation-like;
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 9
(the Arity of S).o = a & (the ResultSort of S).o = r;
end;
theorem :: AOFA_A00:31
for S being non void non empty ManySortedSign
for o being OperSymbol of S
for r being SortSymbol of S st o is_of_type {}, r
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;
theorem :: AOFA_A00:32
for S being non void non empty ManySortedSign
for o,a being set
for r being SortSymbol of S st o is_of_type <*a*>, r
for A being MSAlgebra over S
st (the Sorts of A).a <> {} & (the Sorts of A).r <> {}
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;
theorem :: AOFA_A00:33
for S being non void non empty ManySortedSign
for o,a,b being set
for r being SortSymbol of S st o is_of_type <*a,b*>, r
for A being MSAlgebra over S
st (the Sorts of A).a <> {} & (the Sorts of A).b <> {} &
(the Sorts of A).r <> {}
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;
theorem :: AOFA_A00:34
for S being non void non empty ManySortedSign
for o,a,b,c being set
for r being SortSymbol of S st o is_of_type <*a,b,c*>, r
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 <> {}
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;
theorem :: AOFA_A00:35
for S1,S2 being ManySortedSign
st the ManySortedSign of S1 = the ManySortedSign of S2
for o,a be set, r1 be Element of S1 for r2 being Element of S2 st r1 = r2
holds o is_of_type a,r1 implies o is_of_type a,r2;
begin :: Free Variables
definition
let S be non empty non void ManySortedSign;
struct (MSAlgebra over S) VarMSAlgebra over S (#
Sorts -> ManySortedSet of the carrier of S,
Charact -> ManySortedFunction of (the Sorts)# * the Arity of S,
the Sorts * the ResultSort of S,
free-vars -> ManySortedMSSet of the Sorts, the Sorts
#);
end;
registration
let S be non empty non void ManySortedSign;
let U be non-empty 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;
end;
registration
let S be non empty non void ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
cluster (X,S)-terms for strict VarMSAlgebra over S;
end;
registration
let S be non empty non void ManySortedSign;
cluster non-empty disjoint_valued for VarMSAlgebra over S;
let X be non-empty ManySortedSet of the carrier of S;
cluster all_vars_including -> non-empty for (X,S)-terms VarMSAlgebra over S;
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 10
(the free-vars of A).a.t;
end;
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 11
for o being OperSymbol of S
for p being FinSequence st p in Args(o,A)
for b being Element of A, the_result_sort_of o st b = Den(o,A).p
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;
theorem :: AOFA_A00:36
for S being non empty non void ManySortedSign
for A,B being MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B
for G being MSSubset of A
for H being MSSubset of B st G = H
holds GenMSAlg G = GenMSAlg H;
theorem :: AOFA_A00:37
for S being non empty non void ManySortedSign
for A,B being MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B
for G being GeneratorSet of A holds G is GeneratorSet of B;
theorem :: AOFA_A00:38
for S being non empty non void ManySortedSign
for A,B being non-empty MSAlgebra over S
st the MSAlgebra of A = the MSAlgebra of B
for G being GeneratorSet of A
for H being GeneratorSet of B st G = H
holds G is free implies H is free;
registration
let S be non empty non void ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
cluster all_vars_including inheriting_operations free_in_itself
for (X,S)-terms strict VarMSAlgebra over S;
end;
definition
let S be non empty non void ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
let A be non-empty (X,S)-terms VarMSAlgebra over S;
attr A is vf-free means
:: AOFA_A00:def 12
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;
scheme :: AOFA_A00:sch 1
Scheme{I() -> non empty set,
X,Y() -> non-empty ManySortedSet of I(),
F(object,object,object) -> set}:
ex f being ManySortedMSSet of X(),Y() st
for s,r being Element of I() for t being Element of X().s
holds f.s.t.r = F(s,r,t)
provided
for s,r being Element of I() for t being Element of X().s holds
F(s,r,t) is Subset of Y().r;
theorem :: AOFA_A00:39
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for A being all_vars_including inheriting_operations free_in_itself
(X,S)-terms MSAlgebra over S
ex VF being ManySortedMSSet of the Sorts of A,the Sorts of A,
B being all_vars_including inheriting_operations free_in_itself (X,S)-terms
VarMSAlgebra over S
st B = VarMSAlgebra(#the Sorts of A, the Charact of A, VF#) &
B is vf-free;
registration
let S be non empty non void ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
cluster strict vf-free for all_vars_including inheriting_operations
free_in_itself (X,S)-terms VarMSAlgebra over S;
end;
theorem :: AOFA_A00:40
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for A being vf-free all_vars_including inheriting_operations free_in_itself
(X,S)-terms VarMSAlgebra over S
for s being SortSymbol of S
for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X;
theorem :: AOFA_A00:41
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for A being vf-free all_vars_including (X,S)-terms 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);
begin :: Algebra with undefined values
definition
let I be set;
let S be ManySortedSet of I;
mode ManySortedElement of S -> ManySortedSet of I means
:: AOFA_A00:def 13
for i being set st i in I holds it.i is Element of S.i;
end;
definition
let S be non empty non void ManySortedSign;
struct (MSAlgebra over S) UndefMSAlgebra over S (#
Sorts -> ManySortedSet of the carrier of S,
Charact -> ManySortedFunction of (the Sorts)# * the Arity of S,
the Sorts * the ResultSort of S,
undefined-map -> ManySortedElement of the Sorts
#);
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 14
a = (the undefined-map of A).s;
end;
definition
let S be non empty non void ManySortedSign;
let A be UndefMSAlgebra over S;
attr A is undef-consequent means
:: AOFA_A00:def 15
for o being OperSymbol of S
for p being FinSequence st p in Args(o, A) &
ex i being Nat, s being SortSymbol of S,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
for b being Element of A, the_result_sort_of o
st b = Den(o,A).p holds b is undefined;
end;
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 16
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, a being Element of Args(o,A)
st Args(o,A) <> {} holds Den(o,B).a <> Den(o,A).a implies
Den(o,B).a = (the undefined-map of B).the_result_sort_of o;
end;
registration
let S be non empty ManySortedSign;
let A be MSAlgebra over S;
cluster the Charact of A -> 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;
cluster A-undef non-empty for strict UndefMSAlgebra over S;
end;
begin :: Program algebra
definition
let J be non empty non void ManySortedSign;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
struct (UAStr) ProgramAlgStr over J,T,X(#
carrier -> set,
charact -> PFuncFinSequence of the carrier,
assignments -> Function of Union [|X, the Sorts of T|], the carrier
#);
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 17
the Sorts of T is disjoint_valued &
the assignments of A is one-to-one;
end;
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 for strict ProgramAlgStr over J,T,X;
end;
registration
let J be non empty non void ManySortedSign;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
cluster with_empty-instruction with_catenation with_if-instruction
with_while-instruction
for partial quasi_total non-empty non empty strict ProgramAlgStr over J,T,X;
end;
theorem :: AOFA_A00:42
for U1,U2 be preIfWhileAlgebra st the UAStr of U1 = the UAStr 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 :: AOFA_A00:43
for U1,U2 be preIfWhileAlgebra st the UAStr of U1 = the UAStr of U2
holds ElementaryInstructions U1 = ElementaryInstructions U2;
theorem :: AOFA_A00:44
for U1,U2 being Universal_Algebra
for S1 being Subset of U1, S2 being Subset of U2 st S1 = S2
for o1 being operation of U1, o2 being operation of U2 st o1 = o2
holds S1 is_closed_on o1 implies S2 is_closed_on o2;
theorem :: AOFA_A00:45
for U1,U2 being Universal_Algebra st the UAStr of U1 = the UAStr of U2
for S1 being Subset of U1, S2 being Subset of U2 st S1 = S2
holds S1 is opers_closed implies S2 is opers_closed;
theorem :: AOFA_A00:46
for U1,U2 being Universal_Algebra st the UAStr of U1 = the UAStr of U2
for G being GeneratorSet of U1 holds G is GeneratorSet of U2;
theorem :: AOFA_A00:47
for U1,U2 be Universal_Algebra st the UAStr of U1 = the UAStr of U2
holds signature U1 = signature U2;
registration
let J be non empty non void ManySortedSign;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
cluster non degenerated well_founded ECIW-strict infinite
for with_empty-instruction with_catenation with_if-instruction
with_while-instruction
partial quasi_total non-empty non empty strict 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 preIfWhileAlgebra of X is
with_empty-instruction with_catenation with_if-instruction
with_while-instruction
partial quasi_total non-empty non empty 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 non-empty 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 18
(the assignments of A).[x,t];
end;
registration
let S be set;
let T be disjoint_valued non-empty ManySortedSet of S;
cluster non-empty for ManySortedSubset of T;
end;
definition
let J be non void non empty ManySortedSign;
let T,C be non-empty MSAlgebra over J;
let X be non-empty GeneratorSet of T;
func C-States(X) -> Subset of MSFuncs(X, the Sorts of C) means
:: AOFA_A00:def 19
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;
end;
registration
let J be non void non empty ManySortedSign;
let T be non-empty MSAlgebra over J;
let C be non-empty image of T;
let X be non-empty GeneratorSet of T;
cluster C-States(X) -> non empty;
end;
theorem :: AOFA_A00:48
for B being non void non empty ManySortedSign
for T,C being non-empty MSAlgebra over B
for X being non-empty GeneratorSet of T
for g being set st g in C-States(X)
holds g is ManySortedFunction of X, the Sorts of C;
registration
let B be non void non empty ManySortedSign;
let T,C be non-empty MSAlgebra over B;
let X be non-empty GeneratorSet of T;
cluster -> Relation-like Function-like for Element of C-States(X);
end;
registration
let B be non void non empty ManySortedSign;
let T,C be non-empty MSAlgebra over B;
let X be non-empty GeneratorSet of T;
cluster -> Function-yielding the carrier of B-defined
for Element of (C)-States(X);
end;
registration
let B be non void non empty ManySortedSign;
let T be non-empty MSAlgebra over B;
let C be non-empty image of T;
let X be non-empty GeneratorSet of T;
cluster -> total for Element of (C)-States(X);
end;
definition
let B be non void non empty ManySortedSign;
let T be non-empty MSAlgebra over B;
let C be non-empty MSAlgebra over B;
let X be non-empty 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 20
for s being ManySortedFunction of X, the Sorts of C holds
s in it iff s in (C)-States(X) & s.a.x <> f;
end;
registration
let B be non void non empty ManySortedSign;
let T be free non-empty MSAlgebra over B;
let C be non-empty MSAlgebra over B;
let X be non-empty GeneratorSet of T;
cluster C-States(X) -> non empty;
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 -> Function-like Relation-like for Element of Args(o,A);
end;
registration
let B be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of B;
let T be (X,B)-terms non-empty MSAlgebra over B;
let C be non-empty image of T;
let G be non-empty GeneratorSet of T;
cluster C-States(G) -> non empty;
end;
definition
let B be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of B;
let T be (X,B)-terms non-empty MSAlgebra over B;
let C be non-empty 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
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 21
ex f being ManySortedFunction of T,C,
Q being GeneratorSet of T st
f is_homomorphism T,C & Q = doms s & s = f||Q & it = f.a.t;
end;
begin :: Generator system
definition
let S,X;
let T be all_vars_including inheriting_operations free_in_itself
(X,S)-terms MSAlgebra over S;
struct GeneratorSystem over S,X,T(#
generators -> non-empty GeneratorSet of T,
supported-var -> (ManySortedFunction of the generators, FreeGen X),
supported-term -> ManySortedMSSet of the generators, the carrier of S
#);
end;
definition
let S,X;
let T be all_vars_including inheriting_operations free_in_itself
(X,S)-terms 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
:: AOFA_A00:def 22
it in (the generators of G).s;
end;
definition
let S,X;
let T be all_vars_including inheriting_operations free_in_itself
(X,S)-terms 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 23
(the generators of G).s;
let g be Element of G,s;
func supp-var g -> Element of (FreeGen X).s equals
:: AOFA_A00:def 24
(the supported-var of G).s.g;
end;
definition
let S,X;
let T be all_vars_including inheriting_operations free_in_itself
(X,S)-terms 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
(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 25
(the supported-term of G).s.g;
end;
definition
let S be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
let T be all_vars_including inheriting_operations free_in_itself
(X,S)-terms VarMSAlgebra over S;
let C be non-empty image of T;
let G be GeneratorSystem over S,X,T;
attr G is C-supported means
:: AOFA_A00:def 26
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
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
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
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))
for H being ManySortedSubset of the Sorts of T st H = FreeGen X
for h being ManySortedFunction of T,C st h is_homomorphism T,C & h||H = u
holds v = h.s.t);
end;
definition
let S;
let X;
let A be vf-free all_vars_including inheriting_operations free_in_itself
(X,S)-terms VarMSAlgebra over S;
let C be non-empty image of A;
let G be GeneratorSystem over S,X,A such that
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 27
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
for f being ManySortedFunction of the generators of G, the Sorts of C st
f = s & u = (f||H)+*(r,supp-var t,v) holds
(x in (vf t).p implies for q being Element of A,p st q = (supp-term t).p.x
holds it.p.x = q value_at(C, u));
end;
definition
let B be non void non empty ManySortedSign;
let Y be non-empty ManySortedSet of the carrier of B;
let T be vf-free all_vars_including inheriting_operations free_in_itself
(Y,B)-terms VarMSAlgebra over B;
let C be non-empty 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 28
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
for t being Element of T, b
holds f.(s, v:=(t,A)) = succ(s,v0,t value_at(C,s));
end;
begin :: Boolean signature
definition
struct (ManySortedSign) ConnectivesSignature (#
carrier,carrier' -> set,
Arity -> Function of the carrier',(the carrier)*,
ResultSort -> Function of the carrier', the carrier,
connectives -> FinSequence of the carrier'
#);
end;
definition
let S be ConnectivesSignature;
attr S is 1-1-connectives means
:: AOFA_A00:def 29
the connectives of S is one-to-one;
end;
definition
let n be Nat;
let S be ConnectivesSignature;
attr S is n-connectives means
:: AOFA_A00:def 30
len the connectives of S = n;
end;
registration
let n be Nat;
cluster n-connectives non empty non void for strict ConnectivesSignature;
end;
definition
struct (ConnectivesSignature) BoolSignature (#
carrier,carrier' -> set,
Arity -> Function of the carrier',(the carrier)*,
ResultSort -> Function of the carrier', the carrier,
bool-sort -> (Element of the carrier),
connectives -> FinSequence of the carrier'
#);
end;
registration
let n be Nat;
cluster n-connectives non empty non void for strict BoolSignature;
end;
definition
let B be BoolSignature;
attr B is bool-correct means
:: AOFA_A00:def 31
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;
registration
cluster 3-connectives 1-1-connectives bool-correct non empty non void
for strict BoolSignature;
end;
registration
cluster 1-1-connectives non empty non void for ConnectivesSignature;
end;
registration
let S be 1-1-connectives non empty non void ConnectivesSignature;
cluster the connectives of S -> one-to-one;
end;
definition
let S be non empty non void BoolSignature;
let B be MSAlgebra over S;
attr B is bool-correct means
:: AOFA_A00:def 32
(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 be 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;
theorem :: AOFA_A00:49
for A being non empty set, n being Nat
for f being Function of n-tuples_on A,A holds
f is homogeneous quasi_total non empty PartFunc of A*,A &
for g being homogeneous Function st f = g holds g is n-ary;
registration
let A be non empty set;
let n be Nat;
cluster n-ary for homogeneous quasi_total non empty PartFunc of A*,A;
end;
scheme :: AOFA_A00:sch 2
Sch1 {A() -> non empty set, F(set) -> Element of A()}:
ex f being 1-ary homogeneous quasi_total non empty PartFunc of A()*,A() st
for a being Element of A() holds f.<*a*> = F(a);
scheme :: AOFA_A00:sch 3
Sch2 {A() -> non empty set, F(set,set) -> Element of A()}:
ex f being 2-ary homogeneous quasi_total non empty PartFunc of A()*,A() st
for a,b being Element of A() holds f.<*a,b*> = F(a,b);
theorem :: AOFA_A00:50
for S being non empty non void ManySortedSign
for A being non-empty 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;
theorem :: AOFA_A00:51
for S being bool-correct non empty non void BoolSignature
for A being non-empty ManySortedSet of the carrier of S
ex B being non-empty strict MSAlgebra over S st
the Sorts of B = A+*(the bool-sort of S, BOOLEAN) &
B is bool-correct;
registration
let S be bool-correct non empty non void BoolSignature;
cluster bool-correct non-empty for strict MSAlgebra over S;
end;
definition
let S be bool-correct non empty non void BoolSignature;
let B be non-empty MSAlgebra over S;
func \trueB -> Element of B, the bool-sort of S equals
:: AOFA_A00:def 33
Den(In((the connectives of S).1, the carrier' of S), B).{};
let p be Element of B, the bool-sort of S;
func \notp -> Element of B, the bool-sort of S equals
:: AOFA_A00:def 34
Den(In((the connectives of S).2, the carrier' of S), B).<*p*>;
let q be Element of B, the bool-sort of S;
func p\andq -> Element of B, the bool-sort of S equals
:: AOFA_A00:def 35
Den(In((the connectives of S).3, the carrier' of S), B).<*p,q*>;
end;
definition
let S be bool-correct non empty non void BoolSignature;
let B be non-empty MSAlgebra over S;
let p be Element of B, the bool-sort of S;
let q be Element of B, the bool-sort of S;
func p\orq -> Element of B, the bool-sort of S equals
:: AOFA_A00:def 36
\not(\notp\and\notq);
func p\impq -> Element of B, the bool-sort of S equals
:: AOFA_A00:def 37
\not(p\and\notq);
end;
definition
let S be bool-correct non empty non void BoolSignature;
let B be non-empty MSAlgebra over S;
let p be Element of B, the bool-sort of S;
let q be Element of B, the bool-sort of S;
func p\iffq -> Element of B, the bool-sort of S equals
:: AOFA_A00:def 38
p\andq\or(\notp\and\notq);
end;
begin :: Algebra with integers
definition
let i be Nat;
let s be set;
let S be BoolSignature;
attr S is (i,s) integer means
:: AOFA_A00:def 39
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 & :: 0
(the connectives of S).(i+1) is_of_type {},I & :: 1
(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 & :: div
(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;
theorem :: AOFA_A00:52
ex S being 10-connectives non empty non void strict BoolSignature st
S is 1-1-connectives (4,1) integer 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;
registration
cluster 10-connectives 1-1-connectives (4,1) integer
bool-correct non empty non void for strict BoolSignature;
end;
definition
let S be non empty non void BoolSignature;
let I be SortSymbol of S;
attr I is integer means
:: AOFA_A00:def 40
I = 1;
end;
registration
let S be (4,1) integer non empty non void BoolSignature;
cluster integer for SortSymbol of S;
end;
theorem :: AOFA_A00:53
for S being (4,1) integer non empty non void 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;
definition
let S be (4,1) integer non empty non void BoolSignature;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
func \0(A,I) -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 41
Den(In((the connectives of S).4, the carrier' of S), A).{};
func \1(A,I) -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 42
Den(In((the connectives of S).5, the carrier' of S), A).{};
let a be Element of (the Sorts of A).I;
func -a -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 43
Den(In((the connectives of S).6, the carrier' of S), A).<*a*>;
let b be Element of (the Sorts of A).I;
func a+b -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 44
Den(In((the connectives of S).7, the carrier' of S), A).<*a,b*>;
func a*b -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 45
Den(In((the connectives of S).8, the carrier' of S), A).<*a,b*>;
func a div b -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 46
Den(In((the connectives of S).9, the carrier' of S), A).<*a,b*>;
func leq(a,b) -> Element of (the Sorts of A).the bool-sort of S equals
:: AOFA_A00:def 47
Den(In((the connectives of S).10, the carrier' of S), A).<*a,b*>;
end;
definition
let S be (4,1) integer non empty non void 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 48
a+-b;
func a mod b -> Element of A,I equals
:: AOFA_A00:def 49
a+-(a div b)*b;
end;
registration
let S be (4,1) integer non empty non void BoolSignature;
let X be non-empty ManySortedSet of the carrier of S;
cluster X.1 -> non empty;
end;
definition
let n be Nat;
let s be set;
let S be bool-correct non empty non void BoolSignature;
let A be bool-correct MSAlgebra over S;
attr A is (n,s) integer means
:: AOFA_A00:def 50
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;
theorem :: AOFA_A00:54
for n being Nat, I being set st n >= 1
for S being bool-correct non empty non void BoolSignature
st S is (n,I) integer
ex A being bool-correct non-empty strict MSAlgebra over S st
A is (n,I) integer;
registration
let S be (4,1) integer bool-correct non empty non void BoolSignature;
cluster (4,1) integer for bool-correct non-empty strict MSAlgebra over S;
end;
theorem :: AOFA_A00:55
for S being (4,1) integer bool-correct non empty non void BoolSignature
for A being (4,1) integer bool-correct non-empty 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,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 iff i <= j) & (leq(a,b) = FALSE iff i > j);
registration
let S be (4,1) integer bool-correct non empty non void BoolSignature;
let A be (4,1) integer bool-correct non-empty MSAlgebra over S;
cluster -> integer for Element of (the Sorts of A).1;
end;
begin :: Algebras with arrays
definition
let I,N be set;
let n be Nat;
let S be ConnectivesSignature;
attr S is (n,I,N)-array means
:: AOFA_A00:def 51
len the connectives of S >= n+3 & :: I=L - type of elements of an array
:: N=K - intgers
:: J - array of I
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 & ::(a,i) -> a[i]
(the connectives of S).(n+1) is_of_type <*J,K,L*>, J & :: a[i]:=x
(the connectives of S).(n+2) is_of_type <*J*>, K & :: length
(the connectives of S).(n+3) is_of_type <*K,L*>, J; :: init
end;
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 52
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 0-based finite 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, x being Element of A,K st i >= 0 holds
Den((the connectives of S)/.(n+3),A).<*i,x*> = Segm(i)-->x;
end;
definition
let B be non empty BoolSignature;
let C be non empty ConnectivesSignature;
func B+*C -> strict BoolSignature means
:: AOFA_A00:def 53
the ManySortedSign 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;
end;
theorem :: 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;
registration
let B be non empty BoolSignature;
let C be non empty ConnectivesSignature;
cluster B+*C -> non empty;
end;
registration
let B be non void non empty BoolSignature;
let C be non empty ConnectivesSignature;
cluster B+*C -> non void;
end;
registration
let n1,n2 be Nat;
let B be n1-connectives non empty non void BoolSignature;
let C be n2-connectives non empty non void ConnectivesSignature;
cluster B+*C -> n1+n2-connectives;
end;
theorem :: AOFA_A00:57
for M,O,N,I being set st I in M & N in M
ex C being 4-connectives non empty non void strict ConnectivesSignature st
C is (1,I,N)-array 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;
registration
let I,N be set;
cluster (1,I,N)-array 4-connectives for non empty non void strict
ConnectivesSignature;
end;
theorem :: AOFA_A00:58
for n,m being Nat st m > 0
for B being n-connectives non empty non void 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;
theorem :: AOFA_A00:59
for m being Nat st m > 0
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;
theorem :: AOFA_A00:60
for B being bool-correct non empty non void 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;
definition
let n be Nat;
let B be BoolSignature;
attr B is n array-correct means
:: AOFA_A00:def 54
(the ResultSort of B).((the connectives of B).(n+1)) <> the bool-sort of B;
end;
registration
cluster 1-1-connectives 14-connectives (11,1,1)-array 11 array-correct
(4,1) integer bool-correct non empty non void for strict BoolSignature;
end;
registration
let S be (11,1,1)-array non empty non void BoolSignature;
cluster integer for SortSymbol of S;
end;
definition
let S be (11,1,1)-array non empty non void BoolSignature;
func the_array_sort_of S -> SortSymbol of S equals
:: AOFA_A00:def 55
(the ResultSort of S).((the connectives of S).12);
end;
definition
let S be (4,1) integer (11,1,1)-array non empty non void 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;
func length(a,I) -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 56
Den(In((the connectives of S).13, the carrier' of S), A).<*a*>;
let i be Element of (the Sorts of A).I;
func a.(i) -> Element of (the Sorts of A).I equals
:: AOFA_A00:def 57
Den(In((the connectives of S).11, the carrier' of S), A).<*a,i*>;
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 58
Den(In((the connectives of S).12, the carrier' of S), A).<*a,i,x*>;
end;
definition
let S be (4,1) integer (11,1,1)-array non empty non void BoolSignature;
let A be non-empty MSAlgebra over S;
let I be integer SortSymbol of S;
let i be Element of (the Sorts of A).I;
let 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 59
Den(In((the connectives of S).14, the carrier' of S), A).<*i,x*>;
end;
registration
let X be non empty set;
cluster <*X*> -> non-empty;
let Y,Z be non empty set;
cluster <*X,Y,Z*> -> 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;
end;
registration
let X be integer-membered non empty set;
let Y be non empty set;
let f be Element of product <*X,Y*>;
cluster f.1 -> integer;
end;
theorem :: AOFA_A00:61
for I,N being set
for S being (1,I,N)-array non empty non void ConnectivesSignature
for Y being non empty set
for X being non-empty 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
ex A being non-empty strict MSAlgebra over S st A is (1,I,N)-array &
the Sorts of A tolerates X;
registration
let I,N be set;
let S be (1,I,N)-array non empty non void ConnectivesSignature;
cluster (1,I,N)-array for non-empty strict MSAlgebra over S;
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 60
A1 +* A2;
end;
theorem :: AOFA_A00:62
for B being bool-correct non empty non void BoolSignature
for A1 being bool-correct non-empty MSAlgebra over B
for C being non empty non void ConnectivesSignature
st the carrier' of B misses the carrier' of C
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;
theorem :: AOFA_A00:63
for n being Nat, I being set st n >= 4
for B being bool-correct non empty non void BoolSignature
st B is (n,I) integer
for A1 being bool-correct non-empty MSAlgebra over B
st A1 is (n,I) integer
for C being non empty non void ConnectivesSignature
st the carrier' of B misses the carrier' of C
for A2 being non-empty MSAlgebra over C
st the Sorts of A1 tolerates the Sorts of A2
for S being bool-correct non empty non void BoolSignature
st the BoolSignature of S = B+*C
for A being bool-correct non-empty MSAlgebra over S
st A = (B,A1)+*A2 holds A is (n,I) integer;
theorem :: AOFA_A00:64
for n,m being Nat, s,r being set st n >= 1 & m >= 1
for B being m-connectives non empty non void BoolSignature
for A1 being non-empty MSAlgebra over B
for C being non empty non void ConnectivesSignature
st C is (n,s,r)-array
for A2 being non-empty MSAlgebra over C
st the Sorts of A1 tolerates the Sorts of A2 & A2 is (n,s,r)-array
for S being non empty non void BoolSignature
st the BoolSignature of S = B+*C
for A being non-empty MSAlgebra over S
st A = (B,A1)+*A2 holds A is (m+n,s,r)-array;
theorem :: AOFA_A00:65
for n being Nat, 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 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)
holds S1 is bool-correct implies S2 is bool-correct;
theorem :: AOFA_A00:66
for n being Nat, 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 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)
holds S1 is (n,s) integer implies S2 is (n,s) integer;
theorem :: AOFA_A00:67
for n,m being Nat, s,r being set
for S1,S2 being non empty ConnectivesSignature st
1 <= n & len the connectives of S1 >= n+3 &
for i 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))
holds S2 is (n+m,s,r)-array implies S1 is (n,s,r)-array;
theorem :: AOFA_A00:68
for j,k be set, i,m,n being Nat st m >= 4 & m+6 <= n & i >= 1
for S being 1-1-connectives bool-correct non empty non void BoolSignature
st S is (n+i,j,k)-array (m,k) integer
ex B being bool-correct non empty non void BoolSignature,
C being non empty non void ConnectivesSignature st
the BoolSignature of S = B+*C &
B is n-connectives (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;
theorem :: AOFA_A00:69
for s,I being set
for S being bool-correct non empty non void BoolSignature
st S is (4,I) integer
for X being non empty set
st s in the carrier of S & s <> I & s <> the bool-sort of S
ex A being bool-correct non-empty MSAlgebra over S st A is (4,I) integer &
(the Sorts of A).s = X;
registration
let S be 1-1-connectives (11,1,1)-array 11 array-correct (4,1) integer
bool-correct non empty non void BoolSignature;
cluster (11,1,1)-array (4,1) integer for bool-correct
non-empty strict MSAlgebra over S;
end;