:: Algebraic Approach to Algorithmic Logic
:: by Grzegorz Bancerek
::
:: Received September 15, 2014
:: Copyright (c) 2014-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 FUNCT_1, PBOOLE, UNIALG_1, MSUALG_1, FINSEQ_1, MSUALG_6,
FINSET_1, FUNCT_7, ORDINAL2, ARYTM_3, RELAT_1, CATALG_1, XBOOLE_0,
FOMODEL2, ZFMISC_1, ORDINAL1, STRUCT_0, SUBSET_1, TARSKI, CARD_3,
MARGREL1, CARD_1, FUNCOP_1, FUNCT_3, NUMBERS, ARYTM_1, NAT_1, FACIRC_1,
XXREAL_0, ORDINAL4, FUNCT_2, INCPROJ, FUNCT_4, COMPUT_1, PARTFUN1,
WELLORD1, MSAFREE, UNIALG_2, AOFA_000, AOFA_L00, MCART_1, AOFA_A00,
GRAPHSP, QC_LANG1, ZF_LANG, FOMODEL1, SETLIM_2, REAL_1, INSTALG1,
PUA2MSS1, MATROID0, ALGSPEC1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ENUMSET1, MCART_1,
MATROID0, XTUPLE_0, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, FINSET_1,
FINSEQ_1, FINSEQ_2, FUNCOP_1, NUMBERS, XREAL_0, NAT_1, NAT_D, FUNCT_3,
FUNCT_4, MARGREL1, FUNCT_7, ORDINAL1, ORDINAL2, PBOOLE, CARD_1, CARD_3,
FINSEQ_4, XXREAL_0, XCMPLX_0, STRUCT_0, FACIRC_1, COMPUT_1, INSTALG1,
CATALG_1, UNIALG_1, MSUALG_1, MSAFREE, PUA2MSS1, UNIALG_2, FREEALG,
CIRCCOMB, CLOSURE2, MSUALG_6, ALGSPEC1, MSAFREE3, MSAFREE4, PARTFUN1,
AOFA_000, AOFA_A00, MSAFREE5;
constructors RELAT_1, FUNCT_1, XXREAL_0, FINSEQ_1, FINSEQ_3, ENUMSET1,
FUNCOP_1, NAT_1, FUNCT_4, BINOP_1, FUNCT_7, ORDINAL1, XCMPLX_0, CARD_1,
CARD_3, FINSEQ_4, FACIRC_1, STRUCT_0, UNIALG_1, MSUALG_1, INSTALG1,
MSUALG_6, PBOOLE, MARGREL1, FUNCT_2, REALSET2, RELSET_1, COMPUT_1,
AOFA_000, PUA2MSS1, FREEALG, UNIALG_2, ZFMISC_1, SUBSET_1, NUMBERS,
FINSEQ_2, MSAFREE, MSAFREE3, CATALG_1, CLOSURE2, MSAFREE4, AOFA_A00,
XTUPLE_0, ARYTM_1, NAT_D, ORDINAL2, CIRCCOMB, ALGSPEC1, MSAFREE5,
RELSET_2;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1,
FACIRC_1, NAT_1, FINSEQ_2, PBOOLE, STRUCT_0, TEX_2, FINSEQ_1, FINSEQ_4,
XCMPLX_0, XXREAL_0, UNIALG_1, MSAFREE, INSTALG1, CATALG_1, CARD_1,
MSUALG_1, MSAFREE3, XREAL_0, RELAT_1, FUNCT_2, ZFMISC_1, MARGREL1,
FUNCT_4, COMPUT_1, AOFA_000, XTUPLE_0, INDEX_1, CARD_3, CLOSURE2,
MSAFREE4, AOFA_A00, MSUALG_9, CIRCCOMB, FOMODEL0, PARTFUN1, RAMSEY_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Algorithmic language signature
reserve X,Y for set, x,y,z for object, i,j,n for natural number;
registration
let f be non empty-yielding Function;
cluster Union f -> non empty;
end;
definition
let I be set;
let f be ManySortedSet of I;
let i be set;
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 set;
let x be non empty set;
cluster f+*(i,x) -> non-empty;
end;
registration
let S be non empty non void ManySortedSign;
cluster non-empty for strict VarMSAlgebra over S;
end;
definition
let f,g be Function;
attr g is f-tolerating means
:: AOFA_L00:def 1
f tolerates g;
end;
theorem :: AOFA_L00:1
for f,g being Function holds g is f-tolerating iff
for x st x in dom f & x in dom g holds f.x = g.x;
theorem :: AOFA_L00:2
for I,J being set for f being ManySortedSet of I
for g being ManySortedSet of J holds g is f-tolerating iff
for x st x in I & x in J holds f.x = g.x;
theorem :: AOFA_L00:3
for f,g being Function holds f tolerates g+*f;
registration
let X,Y be Function;
cluster Y+*X -> X-tolerating;
end;
registration
let X be Function;
let J be set;
let Y be ManySortedSet of J;
cluster Y+*(X|J) -> X-tolerating;
end;
registration
let J be set;
let X be Function;
cluster X-tolerating for ManySortedSet of J;
end;
registration
let J be set;
let X be non-empty Function;
cluster X-tolerating for non-empty ManySortedSet of J;
end;
registration
let I be non empty set;
let X be non empty-yielding ManySortedSet of I;
cluster Union X -> non empty;
end;
theorem :: AOFA_L00:4
for S being non empty non void ManySortedSign
for o being OperSymbol of S, r being SortSymbol of S,
T being MSAlgebra over S holds
o is_of_type {},r implies {} in Args(o,T);
theorem :: AOFA_L00:5
for S being non empty non void ManySortedSign
for o being OperSymbol of S, s,r being SortSymbol of S,
T being MSAlgebra over S holds
o is_of_type <*s*>,r & x in (the Sorts of T).s implies <*x*> in Args(o,T);
theorem :: AOFA_L00:6
for S being non empty non void ManySortedSign
for o being OperSymbol of S, s1,s2,r being SortSymbol of S,
T being MSAlgebra over S holds
o is_of_type <*s1,s2*>,r &
x in (the Sorts of T).s1 & y in (the Sorts of T).s2
implies <*x,y*> in Args(o,T);
theorem :: AOFA_L00:7
for S being non empty non void ManySortedSign
for o being OperSymbol of S, s1,s2,s3,r being SortSymbol of S,
T being MSAlgebra over S holds
o is_of_type <*s1,s2,s3*>,r & x in (the Sorts of T).s1 &
y in (the Sorts of T).s2 & z in (the Sorts of T).s3
implies <*x,y,z*> in Args(o,T);
definition
let S,E be Signature;
attr E is S-extension means
:: AOFA_L00:def 2
S is Subsignature of E;
end;
registration
let S be Signature;
cluster -> S-extension for Extension of S;
end;
theorem :: AOFA_L00:8
for S,E being non empty Signature st E is S-extension
for a being SortSymbol of S holds a is SortSymbol of E;
theorem :: AOFA_L00:9
for S,E being non void Signature st E is S-extension
for o being OperSymbol of S
for a being set for r being Element of S for r1 being Element of E
st r = r1 & o is_of_type a,r holds o is_of_type a,r1;
definition
let X be Function;
let J,Y be set;
func X extended_by(Y,J) -> ManySortedSet of J equals
:: AOFA_L00:def 3
(J-->Y)+*(X|J);
end;
registration
let X be Function;
let J,Y be set;
cluster X extended_by(Y,J) -> X-tolerating;
end;
definition
struct(ConnectivesSignature) PCLangSignature(#
carrier -> set,
carrier' -> set,
Arity -> Function of the carrier', the carrier*,
ResultSort -> Function of the carrier', the carrier,
formula-sort -> (Element of the carrier),
connectives -> (FinSequence of the carrier')
:: <* not-op, and-op, or-op, imp-op, iff-op, true *>
#);
end;
definition
let X be set; :: set of variable symbols
struct(PCLangSignature) QCLangSignature over X(#
carrier -> set,
carrier' -> set,
Arity -> Function of the carrier', the carrier*,
ResultSort -> Function of the carrier', the carrier,
formula-sort -> (Element of the carrier),
connectives -> (FinSequence of the carrier'),
:: <* not-op, and-op, or-op, imp-op, iff-op, true *>
quant-sort -> set,
quantifiers -> Function of [:the quant-sort, X:], the carrier'
#);
end;
definition
let X be set;
struct(QCLangSignature over X) AlgLangSignature over X(#
carrier -> set,
carrier' -> set,
Arity -> Function of the carrier', the carrier*,
ResultSort -> Function of the carrier', the carrier,
formula-sort, program-sort -> (Element of the carrier),
connectives -> (FinSequence of the carrier'),
:: <* not-op, and-op, or-op, imp-op, iff-op, true, alg-imp *>
quant-sort -> set,
quantifiers -> Function of [:the quant-sort, X:], the carrier'
#);
end;
definition
let n be Nat;
let L be PCLangSignature;
attr L is n PC-correct means
:: AOFA_L00:def 4
len the connectives of L >= n+5 &
(the connectives of L)|{n,n+1,n+2,n+3,n+4,n+5} is one-to-one &
(the connectives of L).n is_of_type
<*the formula-sort of L*>, the formula-sort of L &
(the connectives of L).(n+5) is_of_type {}, the formula-sort of L &
((the connectives of L).(n+1) is_of_type
<*the formula-sort of L, the formula-sort of L*>, the formula-sort of L
& ... &
(the connectives of L).(n+4) is_of_type
<*the formula-sort of L, the formula-sort of L*>, the formula-sort of L);
end;
definition
let X;
let L be QCLangSignature over X;
attr L is QC-correct means
:: AOFA_L00:def 5
:: (ex q1,q2 being set st q1 <> q2 & the quant-sort of L = {q1,q2}) &
the quant-sort of L = {1,2} & :: { \for, \ex }
the quantifiers of L is one-to-one &
rng the quantifiers of L misses rng the connectives of L &
for q,x being object st q in the quant-sort of L & x in X holds
(the quantifiers of L).(q,x) is_of_type
<*the formula-sort of L*>, the formula-sort of L;
end;
definition
let n be Nat;
let X be set;
let L be AlgLangSignature over X;
attr L is n AL-correct means
:: AOFA_L00:def 6
the program-sort of L <> the formula-sort of L &
len the connectives of L >= n+8 &
((the connectives of L).(n+6) is_of_type
<*the program-sort of L,the formula-sort of L*>, the formula-sort of L
& ... &
(the connectives of L).(n+8) is_of_type
<*the program-sort of L,the formula-sort of L*>, the formula-sort of L);
end;
registration
let n;
cluster n PC-correct -> non void for PCLangSignature;
end;
definition
let X,Y be set such that
Y c= X;
func incl(Y,X) -> Function of Y,X equals
:: AOFA_L00:def 7
id Y;
end;
registration
let n be non empty natural number;
let X be set;
cluster non void non empty n PC-correct QC-correct
for QCLangSignature over X;
end;
registration
let n be non empty natural number;
cluster non void non empty n PC-correct for PCLangSignature;
end;
registration
let X be set;
cluster non void non empty for strict AlgLangSignature over X;
end;
registration
cluster ordinal -> non pair for set;
end;
theorem :: AOFA_L00:10
for a being ordinal number
for n1,n2 being natural number st n1 <> n2 holds a+^n1 <> a+^n2;
registration
let R be non empty Relation;
cluster -> pair for Element of R;
end;
theorem :: AOFA_L00:11
for n being non empty natural number
for X being non empty set
for J being Signature
ex S being strict non void non empty AlgLangSignature over X st
S is n PC-correct QC-correct n AL-correct J-extension &
(for i st i = 0 or ... or i = 8 holds
(the connectives of S).(n+i) = (sup the carrier' of J)+^i) &
(for x being Element of X holds
(the quantifiers of S).(1,x) = [the carrier' of J,1,x] &
(the quantifiers of S).(2,x) = [the carrier' of J,2,x]) &
the formula-sort of S = sup the carrier of J &
the program-sort of S = (sup the carrier of J)+^1 &
the carrier of S = (the carrier of J) \/
{the formula-sort of S, the program-sort of S} &
for w being Ordinal st w = sup the carrier' of J holds
the carrier' of S = (the carrier' of J) \/
{w+^0,w+^1,w+^2,w+^3,w+^4,w+^5,w+^6,w+^7,w+^8}\/
[:{the carrier' of J},{1,2},X:];
registration
let n be non empty natural number;
let X be non empty set;
let J be Signature;
cluster J-extension n PC-correct QC-correct n AL-correct
for non void non empty strict AlgLangSignature over X;
end;
registration
let X be non empty set;
let n be non empty natural number;
cluster n PC-correct QC-correct n AL-correct
for non void non empty strict AlgLangSignature over X;
end;
begin :: Language
definition
let J be non empty non void Signature;
let T be MSAlgebra over J;
mode VariableSet of T -> set means
:: AOFA_L00:def 8
ex G being GeneratorSet of T st it = Union G;
end;
definition
let J be non empty non void Signature;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
redefine func Union X -> VariableSet of T;
end;
theorem :: AOFA_L00:12
for J being non empty non void Signature
for T being MSAlgebra over J
for X being VariableSet of T holds X c= Union the Sorts of T;
definition
let S be non empty non void Signature;
let X be ManySortedSet of the carrier of S;
let T be VarMSAlgebra over S;
attr T is X-vf-yielding means
:: AOFA_L00:def 9
the free-vars of T is ManySortedMSSet of the Sorts of T, X;
end;
definition
let J be non empty set;
let Q be ManySortedSet of J;
let Y be set;
let f be Function of [:Union Q, Y:], Union Q;
attr f is sort-preserving means
:: AOFA_L00:def 10
for j being Element of J holds f.:[:Q.j, Y:] c= Q.j;
end;
registration
let J be non empty set;
let Q be ManySortedSet of J;
let Y be set;
cluster sort-preserving for Function of [:Union Q, Y:], Union Q;
end;
definition
let J be non empty non void Signature;
let X be ManySortedSet of the carrier of J;
struct (MSAlgebra over J) SubstMSAlgebra over J,X (#
Sorts -> (ManySortedSet of the carrier of J),
Charact -> (ManySortedFunction of (the Sorts)# * the Arity of J,
the Sorts * the ResultSort of J),
subst-op -> sort-preserving Function of
[:Union the Sorts, Union [|X, the Sorts|]:], Union the Sorts
#);
end;
theorem :: AOFA_L00:13
for I being set
for X being ManySortedSet of I
for S being ManySortedSubset of X
for x holds S.x is Subset of X.x;
definition
let J be non empty non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of J;
let Q be SubstMSAlgebra over J,X such that
X is ManySortedSubset of the Sorts of Q;
let x be Element of Union X;
func @(x,Q) -> Element of Union the Sorts of Q equals
:: AOFA_L00:def 11
x;
end;
definition
let J be non empty non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of J;
let Q be SubstMSAlgebra over J,X such that
X is ManySortedSubset of the Sorts of Q;
let j be SortSymbol of J such that
(the Sorts of Q).j <> {};
let A be Element of Q,j;
let x be Element of Union X;
let y be Element of Union X;
given a being SortSymbol of J such that
x in X.a & y in X.a;
func A/(x,y) -> Element of Q,j equals
:: AOFA_L00:def 12
(the subst-op of Q).[A,[x,y]];
end;
definition
let J be non empty non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of J;
let Q be SubstMSAlgebra over J,X;
let j be SortSymbol of J;
let A be Element of Q,j such that
(the Sorts of Q).j <> {};
let x be Element of Union X;
let t be Element of Union the Sorts of Q;
given a be SortSymbol of J such that
x in X.a & t in (the Sorts of Q).a;
func A/(x,t) -> Element of Q,j equals
:: AOFA_L00:def 13
(the subst-op of Q).[A,[x,t]];
end;
registration
let J be non empty non void ManySortedSign;
let X be ManySortedSet of the carrier of J;
cluster non-empty for SubstMSAlgebra over J,X;
end;
definition
let J be non empty non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of J;
let Q be non-empty SubstMSAlgebra over J,X;
let o be OperSymbol of J;
let p be Element of Args(o,Q);
let x be Element of Union X;
let y be Element of Union the Sorts of Q;
func p/(x,y) -> Element of Args(o,Q) means
:: AOFA_L00:def 14
for i being Nat st i in dom the_arity_of o
ex j being SortSymbol of J st j = (the_arity_of o).i &
ex A being Element of Q,j st A = p.i & it.i = A/(x,y);
end;
definition
let I be non empty set;
let X be non-empty ManySortedSet of I;
let S be non-empty ManySortedSubset of X;
let x be Element of I;
let z be Element of S.x;
func @z -> Element of X.x equals
:: AOFA_L00:def 15
z;
end;
definition
let J be non empty non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of J;
let Q be non-empty SubstMSAlgebra over J,X;
attr Q is subst-correct means
:: AOFA_L00:def 16
for x being Element of Union X
for a being SortSymbol of J st x in X.a holds
(for j being SortSymbol of J for A being Element of Q,j holds A/(x,x) = A) &
for y being Element of Union the Sorts of Q st y in (the Sorts of Q).a
for o being OperSymbol of J
for p being Element of Args(o,Q)
for A being Element of Q, the_result_sort_of o
st A = Den(o,Q).p holds
not (ex S being QCLangSignature over Union X st J = S &
ex z being (Element of Union X), q being Element of {1,2} st
o = (the quantifiers of S).(q,z))
implies A/(x,y) = Den(o,Q).(p/(x,y));
attr Q is subst-correct2 means
:: AOFA_L00:def 17
for j being SortSymbol of J for q being Element of Q,j,
t being Element of Q,j for x being Element of Union X st t = x in X.j
holds t/(x,q) = q;
end;
theorem :: AOFA_L00:14
for J being non empty non void Signature
for X being non empty-yielding ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X
st X is ManySortedSubset of the Sorts of Q
for a being SortSymbol of J st (the Sorts of Q).a <> {}
for A being Element of Q,a
for x,y being Element of Union X
for t being Element of Union the Sorts of Q st y = t
for j being SortSymbol of J st x in X.j & y in X.j
holds A/(x,y) = A/(x,t);
registration
let J be non void Signature;
cluster J-extension -> non void non empty for Signature;
end;
registration
let J be Signature;
cluster J-extension for non empty non void Signature;
let X be non empty set;
cluster J-extension for non empty non void QCLangSignature over X;
let n be non empty natural number;
cluster J-extension for non empty non void n PC-correct QC-correct
QCLangSignature over X;
end;
definition
let J be Signature;
let X be non empty set;
let n be non empty Nat;
let S be J-extension n PC-correct feasible AlgLangSignature over X;
attr S is essential means
:: AOFA_L00:def 18
(the connectives of S).:(n+9 \ n) misses the carrier' of J &
rng the quantifiers of S misses the carrier' of J &
{the formula-sort of S, the program-sort of S} misses the carrier of J;
end;
registration
let n be non empty natural number;
let X be non empty set;
let J be Signature;
cluster essential for J-extension n PC-correct QC-correct n AL-correct
non void non empty strict AlgLangSignature over X;
end;
registration
let J be non empty Signature;
let S be J-extension non empty Signature;
let X be non empty-yielding ManySortedSet of the carrier of J;
cluster X-tolerating for non empty-yielding
ManySortedSet of the carrier of S;
end;
definition
let J be non empty Signature;
let S be non empty Signature;
let T be MSAlgebra over J;
let Q be MSAlgebra over S;
attr Q is T-extension means
:: AOFA_L00:def 19
Q|J = the MSAlgebra of T;
end;
theorem :: AOFA_L00:15
for J being non empty non void Signature
for S being J-extension Signature
for T being MSAlgebra over J
for Q1,Q2 being MSAlgebra over S
st the MSAlgebra of Q1 = the MSAlgebra of Q2
holds Q1 is T-extension implies Q2 is T-extension;
theorem :: AOFA_L00:16
for J being non empty non void Signature
for S being J-extension Signature
for T being MSAlgebra over J
for Q being MSAlgebra over S st Q is T-extension
for x st x in the carrier of J holds (the Sorts of T).x = (the Sorts of Q).x;
theorem :: AOFA_L00:17
for J being non empty non void Signature
for S being J-extension Signature
for T being MSAlgebra over J
for I being set st I c= (the carrier of S)\the carrier of J
for X being ManySortedSet of I
ex Q being MSAlgebra over S st Q is T-extension & (the Sorts of Q)|I = X;
theorem :: AOFA_L00:18
for J being non empty non void Signature
for S being J-extension Signature
for T being non-empty MSAlgebra over J
for I being set st I c= (the carrier of S)\the carrier of J
for X being non-empty ManySortedSet of I
ex Q being non-empty MSAlgebra over S st
Q is T-extension & (the Sorts of Q)|I = X;
registration
let J be non empty non void Signature;
let S be J-extension Signature;
let T be MSAlgebra over J;
cluster T-extension for MSAlgebra over S;
end;
registration
let J be non empty non void Signature;
let S be J-extension Signature;
let T be non-empty MSAlgebra over J;
cluster T-extension for non-empty MSAlgebra over S;
end;
theorem :: AOFA_L00:19
for I being set, a being object holds pr1(I,{a}) is one-to-one;
theorem :: AOFA_L00:20
for S1,S2,E1,E2 being Signature
st the ManySortedSign of S1 = the ManySortedSign of S2 &
the ManySortedSign of E1 = the ManySortedSign of E2 &
E1 is Extension of S1
holds E2 is Extension of S2;
registration
let I be set;
let a be object;
cluster pr1(I,{a}) -> one-to-one;
end;
definition
let a,b,c be non empty set;
let g be Function of a,b;
let f be Function of b,c;
redefine func f*g -> Function of a,c;
end;
theorem :: AOFA_L00:21
for f being one-to-one Function st X misses Y
holds f.:X misses f.:Y;
theorem :: AOFA_L00:22
for n being non empty natural number, X being set
for J being non empty Signature
ex Q being non empty non void n PC-correct QC-correct
QCLangSignature over X st
the carrier of Q misses the carrier of J &
the carrier' of Q misses the carrier' of J;
registration
let J be non empty Signature;
cluster J-extension for non empty non void Signature;
let X be set;
cluster J-extension for non empty non void QCLangSignature over X;
let n be non empty natural number;
cluster J-extension for non empty non void n PC-correct QC-correct
QCLangSignature over X;
end;
definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void QCLangSignature over Union X;
let Y be X-tolerating ManySortedSet of the carrier of S;
struct (VarMSAlgebra over S,SubstMSAlgebra over S,Y) LanguageStr over T,Y,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,
:: Function of (the Sorts).the formula-sort of S, Bool X,
subst-op -> sort-preserving Function of
[:Union the Sorts, Union [|Y, the Sorts|]:], Union the Sorts,
equality -> Function of Union [|the Sorts of T, the Sorts of T|],
(the Sorts).the formula-sort of S
#);
end;
definition
let S be non empty PCLangSignature;
let L be MSAlgebra over S;
attr L is language means
:: AOFA_L00:def 20
(the Sorts of L).the formula-sort of S is not empty;
end;
registration
let S be non empty PCLangSignature;
cluster non-empty -> language for MSAlgebra over S;
cluster language for MSAlgebra over S;
end;
theorem :: AOFA_L00:23
for J being non void Signature
for S being J-extension non void Signature
for A1,A2 being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of A2
holds A1|J = A2|J;
registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void QCLangSignature over Union X;
cluster X-tolerating for
non empty-yielding ManySortedSet of the carrier of S;
end;
registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
cluster non-empty language T-extension
for LanguageStr over T,Y,S;
end;
definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be non-empty LanguageStr over T,Y,S;
attr L is subst-correct3 means
:: AOFA_L00:def 21
for s,s1 being SortSymbol of S
for t being Element of L,s
for t1 being Element of L,s1
for y being Element of Union Y st y in Y.s holds y nin (vf t1).s &
(y nin (vf t1).s implies t1/(y,t) = t1) &
(t1 = y in Y.s1 implies t1/(y,t) = t) &
for x being Element of Union Y st x in Y.s holds t1/(x,y)/(y,x) = t1;
end;
registration
let J be non empty Signature;
let S be J-extension non empty Signature;
let X be non empty-yielding ManySortedSet of the carrier of J;
let Y be set;
cluster X extended_by(Y,the carrier of S) -> non empty-yielding;
end;
registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void QCLangSignature over Union X;
cluster X extended_by({},the carrier of S)-vf-yielding non-empty language
T-extension for LanguageStr over T,X extended_by({},the carrier of S),S;
end;
registration
let X be set;
let S be non empty QCLangSignature over X;
let L be language MSAlgebra over S;
cluster (the Sorts of L).the formula-sort of S -> non empty;
end;
definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
mode Language of Y,S is language T-extension LanguageStr over T,Y,S;
end;
definition
let S be non empty PCLangSignature;
let L be language MSAlgebra over S;
mode Formula of L is Element of (the Sorts of L).the formula-sort of S;
end;
definition
let n be non empty natural number;
let S be non void non empty n PC-correct PCLangSignature;
let L be language MSAlgebra over S;
func \true_L -> Formula of L equals
:: AOFA_L00:def 22
Den(In((the connectives of S).(n+5), the carrier' of S), L).{};
let A be Formula of L;
func \notA -> Formula of L equals
:: AOFA_L00:def 23
Den(In((the connectives of S).n, the carrier' of S), L).<*A*>;
let B be Formula of L;
func A\andB -> Formula of L equals
:: AOFA_L00:def 24
Den(In((the connectives of S).(n+1), the carrier' of S), L).<*A,B*>;
func A\orB -> Formula of L equals
:: AOFA_L00:def 25
Den(In((the connectives of S).(n+2), the carrier' of S), L).<*A,B*>;
func A\impB -> Formula of L equals
:: AOFA_L00:def 26
Den(In((the connectives of S).(n+3), the carrier' of S), L).<*A,B*>;
func A\iffB -> Formula of L equals
:: AOFA_L00:def 27
Den(In((the connectives of S).(n+4), the carrier' of S), L).<*A,B*>;
end;
registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
cluster non empty for VariableSet of T;
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be Language of Y,S;
let A be Formula of L;
let x be Element of Union X;
func \for(x,A) -> Formula of L equals
:: AOFA_L00:def 28
Den(In((the quantifiers of S).(1,x), the carrier' of S), L).<*A*>;
func \ex(x,A) -> Formula of L equals
:: AOFA_L00:def 29
Den(In((the quantifiers of S).(2,x), the carrier' of S), L).<*A*>;
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be Language of Y,S;
let A be Formula of L;
let x,y be Element of Union X;
func \for(x,y,A) -> Formula of L equals
:: AOFA_L00:def 30
\for(x,\for(y,A));
func \ex(x,y,A) -> Formula of L equals
:: AOFA_L00:def 31
\ex(x,\ex(y,A));
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be Language of Y,S;
let A be Formula of L;
let x,y,z be Element of Union X;
func \for(x,y,z,A) -> Formula of L equals
:: AOFA_L00:def 32
\for(x,y,\for(z,A));
func \ex(x,y,z,A) -> Formula of L equals
:: AOFA_L00:def 33
\ex(x,y,\ex(z,A));
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be Language of Y,S;
let t1,t2 be object;
given a being SortSymbol of J such that
t1 in (the Sorts of T).a & t2 in (the Sorts of T).a;
func t1 '=' (t2,L) -> Formula of L equals
:: AOFA_L00:def 34
(the equality of L).(t1,t2);
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be non-empty Language of Y,S;
attr L is vf-qc-correct means
:: AOFA_L00:def 35
for A,B being Formula of L holds
vf \notA = vf A & vf(A\andB) = (vf A) (\/) (vf B) &
vf(A\orB) = (vf A) (\/) (vf B) &
vf(A\impB) = (vf A) (\/) (vf B) & vf(A\iffB) = (vf A) (\/) (vf B) &
vf \true_L = EmptyMS the carrier of S &
for x being Element of Union X
for a being SortSymbol of S st x in X.a holds
vf \for(x,A) = (vf A) (\) a-singleton(x) &
vf \ex(x,A) = (vf A) (\) a-singleton(x);
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be non-empty T-extension Language of Y,S;
attr L is vf-finite means
:: AOFA_L00:def 36
for s being SortSymbol of S, t being Element of L,s
holds vf t is finite-yielding;
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X;
let Y be X-tolerating non empty-yielding ManySortedSet of the carrier of S;
let L be non-empty T-extension Language of Y,S;
attr L is subst-forex means
:: AOFA_L00:def 37
for A being Formula of L
for x being Element of Union X
for s,s1 being SortSymbol of S
for t being Element of L,s st x in X.s1
for y being Element of Union Y st y in Y.s holds
(x = y implies \for(x,A)/(y,t) = \for(x,A) & \ex(x,A)/(y,t) = \ex(x,A)) &
(x <> y & x in (vf t).s1 implies
ex z being (Element of Union X), x0,z0 being Element of Union Y
st x = x0 & z0 = z = the Element of X.s1\(vf t).s1\(vf A).s1 &
\for(x,A)/(y,t) = \for(z,A/(x0,z0)/(y,t)) &
\ex(x,A)/(y,t) = \ex(z,A/(x0,z0)/(y,t))) &
(x <> y & x nin (vf t).s implies \for(x,A)/(y,t) = \for(x,A/(y,t)) &
\ex(x,A)/(y,t) = \ex(x,A/(y,t)));
end;
theorem :: AOFA_L00:24
for J being non void Signature
for T being MSAlgebra over J
for X being ManySortedSubset of the Sorts of T
for S being J-extension non void Signature
for Q being T-extension MSAlgebra over S holds
X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q;
theorem :: AOFA_L00:25
for J being non void Signature
for T being MSAlgebra over J
for X being ManySortedSubset of the Sorts of T
for S being J-extension non void Signature holds
Union (X extended_by ({},the carrier of S)) = Union X;
theorem :: AOFA_L00:26
for n being non empty natural number
for X being non empty set
for S being non empty non void n PC-correct QC-correct
QCLangSignature over X
for Q being language MSAlgebra over S holds
{} in Args(In((the connectives of S).(n+5), the carrier' of S),Q) &
for A being Formula of Q holds
<*A*> in Args(In((the connectives of S).n, the carrier' of S),Q) &
for B being Formula of Q holds
(<*A,B*> in Args(In((the connectives of S).(n+1), the carrier' of S),Q)
& ... &
<*A,B*> in Args(In((the connectives of S).(n+4), the carrier' of S),Q)) &
for x being Element of X holds
<*A*> in Args(In((the quantifiers of S).(1,x), the carrier' of S),Q) &
<*A*> in Args(In((the quantifiers of S).(2,x), the carrier' of S),Q);
theorem :: AOFA_L00:27
for n being non empty natural number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being non empty-yielding GeneratorSet of T
for S being J-extension non void non empty n PC-correct QC-correct
QCLangSignature over Union X
for Y being X-tolerating non empty-yielding ManySortedSet of the carrier of S
for L being non-empty Language of Y,S
for x being Element of Union Y
for t being Element of Union the Sorts of L
for s being SortSymbol of S
st x in Y.s & t in (the Sorts of L).s
holds
(for a being Element of
Args(In((the connectives of S).(n+5), the carrier' of S),L) st a = {}
holds a/(x,t) = {}) &
for A being Formula of L holds
(for a being Element of Args(In((the connectives of S).n,
the carrier' of S),L) st <*A*> = a holds a/(x,t) = <*A/(x,t)*>) &
for B being Formula of L holds
((for a being Element of Args(In((the connectives of S).(n+1),
the carrier' of S),L) st <*A,B*> = a holds a/(x,t) = <*A/(x,t),B/(x,t)*>)
& ... &
(for a being Element of Args(In((the connectives of S).(n+4),
the carrier' of S),L) st <*A,B*> = a holds a/(x,t) = <*A/(x,t),B/(x,t)*>)) &
for z being Element of Union X holds
(for a being Element of Args(In((the quantifiers of S).(1,z),
the carrier' of S),L) st <*A*> = a holds a/(x,t) = <*A/(x,t)*>) &
(for a being Element of Args(In((the quantifiers of S).(2,z),
the carrier' of S),L) st <*A*> = a holds a/(x,t) = <*A/(x,t)*>);
theorem :: AOFA_L00:28
for n being non empty natural number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being non empty-yielding GeneratorSet of T
for S being J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X
for Y being X-tolerating non empty-yielding ManySortedSet of the carrier of S
for L being non-empty Language of Y,S st L is subst-correct &
Y is ManySortedSubset of the Sorts of L
for x,y being Element of Union Y
for a being SortSymbol of S st x in Y.a & y in Y.a
for A being Formula of L
holds (\notA)/(x,y) = \not(A/(x,y)) &
for B being Formula of L
holds (A\andB)/(x,y) = (A/(x,y))\and(B/(x,y)) &
(A\orB)/(x,y) = (A/(x,y))\or(B/(x,y)) &
(A\impB)/(x,y) = (A/(x,y))\imp(B/(x,y)) &
(A\iffB)/(x,y) = (A/(x,y))\iff(B/(x,y)) & \true_L/(x,y) = \true_L;
begin :: Algorithmic Theory
definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty QCLangSignature over Union X;
let Y be X-tolerating ManySortedSet of the carrier of S;
struct (LanguageStr over T,Y,S,ProgramAlgStr over J,T,X)
BialgebraStr over S,Y (#
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,
subst-op -> sort-preserving Function of [:Union the Sorts,
Union [|Y, the Sorts|]:], Union the Sorts,
equality -> Function of Union [|the Sorts of T, the Sorts of T|],
(the Sorts).the formula-sort of S,
carrier -> set,
charact -> PFuncFinSequence of the carrier,
assignments -> (Function of Union [|X, the Sorts of T|], the carrier)
#);
end;
registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
cluster J-extension for non void non empty AlgLangSignature over Union X;
end;
definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty AlgLangSignature over Union X;
let Y be X-tolerating ManySortedSet of the carrier of S;
let L be BialgebraStr over S,Y;
attr L is AL-correct means
:: AOFA_L00:def 38
the carrier of L = (the Sorts of L).the program-sort of S;
end;
notation
let S be 1-sorted;
synonym S is 1s-empty for S is empty;
end;
notation
let S be UAStr;
synonym S is ua-non-empty for S is non-empty;
end;
registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non void non empty AlgLangSignature over Union X;
let Y be X-tolerating ManySortedSet of the carrier of S;
cluster non 1s-empty for strict BialgebraStr over S,Y;
end;
registration
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be essential J-extension n PC-correct non void non empty feasible
AlgLangSignature over Union X;
let Y be X-tolerating ManySortedSet of the carrier of S;
cluster non-empty language AL-correct quasi_total partial ua-non-empty
with_empty-instruction with_catenation with_if-instruction
with_while-instruction T-extension
for non 1s-empty strict BialgebraStr over S,Y;
end;
theorem :: AOFA_L00:29
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_L00:30
for U1,U2 be preIfWhileAlgebra st the UAStr of U1 = the UAStr of U2
holds ElementaryInstructions U1 = ElementaryInstructions U2;
theorem :: AOFA_L00:31
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
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_L00:32
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_L00:33
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_L00:34
for U1,U2 be Universal_Algebra st the UAStr of U1 = the UAStr of U2
holds signature U1 = signature U2;
registration
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be essential J-extension non void non empty n PC-correct QC-correct
AlgLangSignature over Union X;
cluster AL-correct vf-qc-correct vf-correct vf-finite subst-correct
subst-forex non degenerated well_founded ECIW-strict
for non-empty quasi_total partial ua-non-empty
with_empty-instruction with_catenation with_if-instruction
with_while-instruction language non 1s-empty T-extension BialgebraStr over
S, X extended_by ({}, the carrier of S);
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be essential J-extension non empty non void n PC-correct QC-correct
n AL-correct AlgLangSignature over Union X;
mode IfWhileAlgebra of X,S is AL-correct vf-qc-correct vf-correct
subst-correct subst-forex non degenerated well_founded ECIW-strict
non-empty quasi_total partial ua-non-empty
with_empty-instruction with_catenation with_if-instruction
with_while-instruction language non 1s-empty T-extension BialgebraStr over
S, X extended_by ({}, the carrier of S);
end;
definition
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be essential J-extension non empty non void n PC-correct QC-correct
n AL-correct AlgLangSignature over Union X;
let L be IfWhileAlgebra of X,S;
let K be Formula of L;
let P be Algorithm of L;
func P*K -> Formula of L equals
:: AOFA_L00:def 39
Den(In((the connectives of S).(n+6), the carrier' of S), L).<*P,K*>;
func \Cup(P,K) -> Formula of L equals
:: AOFA_L00:def 40
Den(In((the connectives of S).(n+7), the carrier' of S), L).<*P,K*>;
func \Cap(P,K) -> Formula of L equals
:: AOFA_L00:def 41
Den(In((the connectives of S).(n+8), the carrier' of S), L).<*P,K*>;
end;
definition
let n be non empty Nat;
let S be non empty non void n PC-correct PCLangSignature;
let L be language MSAlgebra over S;
let F be Subset of (the Sorts of L).the formula-sort of S;
attr F is PC-closed means
:: AOFA_L00:def 42
for A,B,C being Formula of L holds
A\imp(B\impA) in F &
(A\imp(B\impC))\imp((A\impB)\imp(A\impC)) in F &
(\notA\imp\notB)\imp(B\impA) in F &
A\imp(A\orB) in F & A\imp(B\orA) in F &
(A\impC)\imp((B\impC)\imp((A\orB)\impC)) in F &
A\andB\impA in F & A\andB\impB in F & A\imp(B\impA\andB) in F &
A\and\notA\impB in F &
(A\impB)\imp((A\imp\notB)\imp\notA) in F &
A\or\notA in F &
(A\iffB)\imp(A\impB) in F & (A\iffB)\imp(B\impA) in F &
(A\impB)\and(B\impA)\imp(A\iffB) in F &
\true_L in F & (\true_L)\andA\iffA in F & (\true_L)\orA\iff\true_L in F &
(A in F & A\impB in F implies B in F);
end;
definition
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X;
let L be non-empty Language of X extended_by ({},the carrier of S), S;
let F be Subset of (the Sorts of L).the formula-sort of S;
attr F is QC-closed means
:: AOFA_L00:def 43
for A,B being Element of (the Sorts of L).the formula-sort of S
for x being Element of Union X holds
(for a being SortSymbol of J holds
(for t being Element of Union the Sorts of L
st x in (X extended_by ({}, the carrier of S)).a &
t in (the Sorts of L).a holds
for y being Element of Union (X extended_by ({}, the carrier of S)) st x = y
holds
\for(x,A)\imp(A/(y,t)) in F) &
(x in X.a & x nin (vf A).a implies
\for(x,A\impB)\imp(A\imp\for(x,B)) in F)) &
\not\ex(x,A)\iff\for(x,\notA) in F &
\ex(x,\notA)\iff\not\for(x,A) in F &
(A in F implies \for(x,A) in F);
end;
definition
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X;
let L be non-empty T-extension Language of
X extended_by ({},the carrier of S), S;
attr L is subst-eq-correct means
:: AOFA_L00:def 44
for x0 being Element of Union (X extended_by({},the carrier of S))
for s,s1 being SortSymbol of S st x0 in X.s
for t being Element of L,s, t1,t2 being Element of L,s1
holds (t1 '=' (t2,L))/(x0,t) = (t1/(x0,t)) '=' (t2/(x0,t),L);
attr L is vf-eq-correct means
:: AOFA_L00:def 45
for s being SortSymbol of S holds
(for t1,t2 being Element of L,s
holds vf(t1 '=' (t2,L)) = (vf t1) (\/) (vf t2)) &
for s being SortSymbol of S
for t being Element of L,s st t in X.s
holds vf t = s-singleton t;
let F be Subset of (the Sorts of L).the formula-sort of S;
attr F is with_equality means
:: AOFA_L00:def 46
(for t being Element of T holds t '=' (t,L) in F) &
for b being SortSymbol of S
for t1,t2 being Element of L,b
for x being Element of Union (X extended_by ({},the carrier of S))
st x in X.b
holds (for c being SortSymbol of S st c in the carrier of J
for t being Element of L,c holds
(t1 '=' (t2,L))\imp(t/(x,t1) '=' (t/(x,t2),L)) in F) &
for A being Formula of L holds
(t1 '=' (t2,L))\imp(A/(x,t1)\imp(A/(x,t2))) in F;
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty VarMSAlgebra over J;
let X be non-empty GeneratorSet of T;
let S be essential J-extension non empty non void n PC-correct QC-correct
n AL-correct AlgLangSignature over Union X;
let L be non 1s-empty IfWhileAlgebra of X,S;
let V be Formula of L; :: true state test
let F be Subset of (the Sorts of L).the formula-sort of S;
attr F is V AL-closed means
:: AOFA_L00:def 47
for A,B being Formula of L holds
(for M being Algorithm of L holds
(M*(A\andB)) \iff (M*A)\and(M*B) in F &
(M*(A\orB)) \iff (M*A)\or(M*B) in F &
\Cup(M,A) \iff A\or\Cup(M, M*A) in F &
\Cap(M,A) \iff A\and\Cap(M, M*A) in F &
(A\impB in F implies
\Cup(M,A)\imp\Cup(M,B) in F & \Cap(M,A)\imp\Cap(M,B) in F)) &
(for a being SortSymbol of J
for x being Element of X.a
for x0 being Element of Union (X extended_by ({},the carrier of S))
st x = x0 holds
for t being Element of (the Sorts of T).a
for t1 being Element of Union the Sorts of L st t1 = t holds
((x:=(t,L))*A) \iff (A/(x0,t1)) in F &
(for y being Element of X.a st y nin (vf t).a holds
for y0 being Element of Union (X extended_by ({},the carrier of S)) st y = y0
holds ((x:=(t,L))*\ex(x,A)) \iff
\ex(y, (x:=(t,L))*((y:=(@x,L))*(A/(x0,y0)))) in F) &
((x:=(t,L))*A) \imp \ex(x,A) in F) &
for M,M1,M2 being Algorithm of L holds
((M\;M1)*A) \iff (M*(M1*A)) in F &
(if-then-else(M,M1,M2)*A) \iff
((M*V)\and(M*(M1*A)))\or((M*\notV)\and(M*(M2*A))) in F &
(while(M,M1)*A) \iff
((M*\notV)\andA)\or((M*V)\and(M*(M1*(while(M,M1)*A)))) in F;
end;
registration
let n be non empty Nat;
let S be non empty non void n PC-correct PCLangSignature;
let L be language MSAlgebra over S;
cluster [#]((the Sorts of L).the formula-sort of S) -> PC-closed;
cluster PC-closed -> non empty for
Subset of (the Sorts of L).the formula-sort of S;
cluster PC-closed for Subset of (the Sorts of L).the formula-sort of S;
end;
registration
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X;
let L be non-empty Language of X extended_by ({}, the carrier of S),S;
cluster [#]((the Sorts of L).the formula-sort of S) -> QC-closed;
cluster QC-closed PC-closed for
Subset of (the Sorts of L).the formula-sort of S;
end;
registration
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S be J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X;
let L be non-empty T-extension Language of
X extended_by ({}, the carrier of S),S;
cluster [#]((the Sorts of L).the formula-sort of S) -> with_equality;
cluster QC-closed PC-closed with_equality for
Subset of (the Sorts of L).the formula-sort of S;
end;
definition
let n be non empty Nat;
let S being non empty non void n PC-correct PCLangSignature;
let L be language MSAlgebra over S;
mode PC-theory of L is
PC-closed Subset of (the Sorts of L).the formula-sort of S;
end;
definition
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S being J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X;
let L be non-empty Language of X extended_by ({}, the carrier of S), S;
mode QC-theory of L is
QC-closed PC-closed Subset of (the Sorts of L).the formula-sort of S;
end;
definition
let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be non empty-yielding GeneratorSet of T;
let S being J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X;
let L be non-empty T-extension Language of
X extended_by ({}, the carrier of S), S;
mode QC-theory_with_equality of L is
QC-closed PC-closed with_equality
Subset of (the Sorts of L).the formula-sort of S;
end;
registration
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty VarMSAlgebra over J;
let X be non-empty GeneratorSet of T;
let S be essential J-extension non empty non void n PC-correct QC-correct
n AL-correct AlgLangSignature over Union X;
let L be non 1s-empty IfWhileAlgebra of X,S;
let V be Formula of L;
cluster V AL-closed for PC-closed QC-closed with_equality
Subset of (the Sorts of L).the formula-sort of S;
end;
definition
let n be non empty natural number;
let J be non empty non void Signature;
let T be non-empty VarMSAlgebra over J;
let X be non-empty GeneratorSet of T;
let S be essential J-extension non empty non void n PC-correct QC-correct
n AL-correct AlgLangSignature over Union X;
let L be non empty IfWhileAlgebra of X,S;
let V be Formula of L;
mode AL-theory of V,L is PC-closed QC-closed with_equality V AL-closed
Subset of (the Sorts of L).the formula-sort of S;
end;
begin :: Propositional Calculus
reserve
n for non empty Nat,
S for non empty non void n PC-correct PCLangSignature,
L for language MSAlgebra over S,
F for PC-theory of L,
A,B,C,D for Formula of L;
theorem :: AOFA_L00:35
A\impA in F;
theorem :: AOFA_L00:36
A\andB in F iff A in F & B in F;
theorem :: AOFA_L00:37
A\orB\impB\orA in F;
theorem :: AOFA_L00:38
(B\impC)\imp((A\impB)\imp(A\impC)) in F;
theorem :: AOFA_L00:39
A\imp(B\impC) in F implies B\imp(A\impC) in F;
theorem :: AOFA_L00:40 :: Hypothetical syllogism
(A\impB)\imp((B\impC)\imp(A\impC)) in F;
theorem :: AOFA_L00:41
A\imp(B\imp(A\impB)) in F;
theorem :: AOFA_L00:42 :: Contraposition
(A\imp(B\impC))\imp(B\imp(A\impC)) in F;
theorem :: AOFA_L00:43 :: Modus ponendo ponens
B\imp((B\impA)\impA) in F;
theorem :: AOFA_L00:44
A\iffB in F iff A\impB in F & B\impA in F;
theorem :: AOFA_L00:45
B in F implies A\impB in F;
theorem :: AOFA_L00:46
A\impB in F & B\impC in F implies A\impC in F;
theorem :: AOFA_L00:47
C\imp(B\impA) in F & B in F implies C\impA in F;
theorem :: AOFA_L00:48
(( A\andB )\impC )\imp( A\imp( B\impC )) in F;
theorem :: AOFA_L00:49
( A\imp( B\impC ))\imp(( A\andB )\impC ) in F;
theorem :: AOFA_L00:50
( C\impA )\imp(( C\impB )\imp( C\imp( A\andB ))) in F;
theorem :: AOFA_L00:51
A\andB\impB\andA in F;
theorem :: AOFA_L00:52
(A\iffB)\imp(B\iffA) in F;
theorem :: AOFA_L00:53
A\orA\impA in F;
theorem :: AOFA_L00:54
A\impA\andA in F;
theorem :: AOFA_L00:55
A\impB in F & A\impC in F implies A\imp(B\andC) in F;
theorem :: AOFA_L00:56
(A\andB)\or(A\andC) \imp A\and(B\orC) in F;
theorem :: AOFA_L00:57
A\or(B\andC) \imp (A\orB)\and(A\orC) in F;
theorem :: AOFA_L00:58
A\imp(\notA\impB) in F;
theorem :: AOFA_L00:59
A\impB\imp(\notB\imp\notA) in F;
theorem :: AOFA_L00:60
A\impB in F iff \notB\imp\notA in F;
theorem :: AOFA_L00:61
A\impB in F & C\impD in F implies A\orC\impB\orD in F;
theorem :: AOFA_L00:62
A\impB\imp(C\orA\impC\orB) in F;
theorem :: AOFA_L00:63
A\impB in F & C\impD in F & \notB\or\notD in F implies \notA\or\notC in F;
theorem :: AOFA_L00:64
A\orB\imp(\notA\impB) in F;
theorem :: AOFA_L00:65
A\orB\imp(\notB\impA) in F;
theorem :: AOFA_L00:66
A\imp\not\notA in F;
theorem :: AOFA_L00:67
\not\notA\impA in F;
theorem :: AOFA_L00:68
A\iff\not\notA in F;
theorem :: AOFA_L00:69
A\imp\notB in F iff B\imp\notA in F;
theorem :: AOFA_L00:70
\notA\impB in F iff \notB\impA in F;
theorem :: AOFA_L00:71
A\imp(B\impC) in F & C\impD in F implies A\imp(B\impD) in F;
theorem :: AOFA_L00:72
\not(A\andB)\imp\notA\or\notB in F;
theorem :: AOFA_L00:73
\not(A\orB)\imp\notA\and\notB in F;
theorem :: AOFA_L00:74
A\impB in F & C\impD in F implies A\andC\impB\andD in F;
theorem :: AOFA_L00:75
\notA\or\notB\imp\not(A\andB) in F;
theorem :: AOFA_L00:76
\notA\and\notB\imp\not(A\orB) in F;
theorem :: AOFA_L00:77
A\or(B\orC)\imp(A\orB)\orC in F;
theorem :: AOFA_L00:78
(A\orB)\orC\iffA\or(B\orC) in F;
theorem :: AOFA_L00:79
A\and(B\andC)\imp(A\andB)\andC in F;
theorem :: AOFA_L00:80
(A\andB)\andC\iffA\and(B\andC) in F;
theorem :: AOFA_L00:81
C\or(A\impB)\imp(C\orA\impC\orB) in F;
theorem :: AOFA_L00:82
(A\orB)\and(A\orC) \imp A\or(B\andC) in F;
theorem :: AOFA_L00:83
A\and(B\orC) \imp (A\andB)\or(A\andC) in F;
theorem :: AOFA_L00:84
A\impB\imp\notA\orB in F;
theorem :: AOFA_L00:85
A\impB\imp\not(A\and\notB) in F;
theorem :: AOFA_L00:86
B\or\notC\andC\impB in F;
theorem :: AOFA_L00:87
B\orC\and\notC\impB in F;
theorem :: AOFA_L00:88
A\iffB\impA\andB\or\notA\and\notB in F;
theorem :: AOFA_L00:89
A\iffB\imp(A\or\notB)\and(\notA\orB) in F;
theorem :: AOFA_L00:90
\not(A\and\notA) in F;
theorem :: AOFA_L00:91
A\iffA in F;
theorem :: AOFA_L00:92
A\iffB in F implies B\iffA in F;
theorem :: AOFA_L00:93
A\iffB in F & B\iffC in F implies A\iffC in F;
theorem :: AOFA_L00:94
A\iffB in F & B\impC in F implies A\impC in F;
theorem :: AOFA_L00:95
A\impB in F & B\iffC in F implies A\impC in F;
theorem :: AOFA_L00:96
A\iffB in F iff \notA\iff\notB in F;
theorem :: AOFA_L00:97
A\iffB in F iff \not\notA\iffB in F;
theorem :: AOFA_L00:98
A\imp(B\impC) in F & D\impB in F implies A\imp(D\impC) in F;
theorem :: AOFA_L00:99
A\iffB\andC in F & C\iffD in F implies A\iffB\andD in F;
theorem :: AOFA_L00:100
A\iffB\andC in F & B\iffD in F implies A\iffD\andC in F;
theorem :: AOFA_L00:101
A\iffB\orC in F & C\iffD in F implies A\iffB\orD in F;
theorem :: AOFA_L00:102
A\iffB\orC in F & B\iffD in F implies A\iffD\orC in F;
theorem :: AOFA_L00:103
A\impB in F implies B\impC\imp(A\impC) in F;
theorem :: AOFA_L00:104
A\impB in F implies C\impA\imp(C\impB) in F;
theorem :: AOFA_L00:105
A\impB in F & C\impD in F implies B\impC\imp(A\impD) in F;
begin :: Quantifier calculus
reserve
J for non empty non void Signature,
T for non-empty MSAlgebra over J,
X for non empty-yielding GeneratorSet of T,
S1 for J-extension non empty non void n PC-correct QC-correct
QCLangSignature over Union X,
L for non-empty Language of X extended_by ({},the carrier of S1), S1,
G for QC-theory of L,
A,B,C,D for Formula of L;
reserve x,y,z for Element of Union X;
reserve x0,y0,z0 for Element of Union (X extended_by ({},the carrier of S1));
theorem :: AOFA_L00:106
L is subst-correct implies \for(x,A)\impA in G;
theorem :: AOFA_L00:107
\ex(x,A)\iff\not\for(x,\notA) in G;
theorem :: AOFA_L00:108
\for(x,A)\iff\not\ex(x,\notA) in G;
theorem :: AOFA_L00:109
L is subst-correct implies
\for(x,A\impB)\imp(\for(x,A)\impB) in G;
theorem :: AOFA_L00:110
for a being SortSymbol of J
st x in X.a & x nin (vf A).a & \for(x,A\impB) in G
holds A\imp\for(x,B) in G;
:: x nin (vf A).a implies \for(x,A\impB)\imp(A\imp\for(x,B)) in G by AX2;
theorem :: AOFA_L00:111
L is subst-correct vf-qc-correct implies
\for(x,A\impB)\imp(\for(x,A)\imp\for(x,B)) in G;
theorem :: AOFA_L00:112
L is subst-correct implies
for a being SortSymbol of J st x in X.a & y in X.a & x0 = x & y0 = y
holds A/(x0,y0)\imp\ex(x,A) in G;
theorem :: AOFA_L00:113
L is subst-correct vf-qc-correct implies
\ex(x,y,A)\iff\not\for(x,y,\notA) in G;
theorem :: AOFA_L00:114
L is subst-correct implies A\imp\ex(x,A) in G;
theorem :: AOFA_L00:115
L is vf-qc-correct implies
for a being SortSymbol of S1 st x in X.a
holds x nin (vf \for(x,A)).a;
theorem :: AOFA_L00:116
L is vf-qc-correct implies
for a being SortSymbol of S1 st x in X.a holds x nin (vf \ex(x,A)).a;
theorem :: AOFA_L00:117
L is subst-correct vf-qc-correct &
A\impB in G implies (\for(x,A)\imp\for(x,B)) in G;
theorem :: AOFA_L00:118
L is subst-correct vf-qc-correct implies
\for(x,\notA\imp\notB)\imp(\for(x,B)\imp\for(x,A)) in G;
theorem :: AOFA_L00:119
L is subst-correct vf-qc-correct implies
\for(x,A\impB)\imp(\for(x,\notB)\imp\for(x,\notA)) in G;
theorem :: AOFA_L00:120
L is subst-correct vf-qc-correct &
A\iffB in G implies \for(x,A)\iff\for(x,B) in G;
theorem :: AOFA_L00:121
\ex(x,\notA)\iff\not\for(x,A) in G;
theorem :: AOFA_L00:122
L is subst-correct vf-qc-correct implies
for a being SortSymbol of J
st x in X.a & x nin (vf B).a holds \for(x,A\impB)\imp(\ex(x,A)\impB) in G;
theorem :: AOFA_L00:123
L is subst-correct vf-qc-correct implies
\for(x,A\impB)\imp(\ex(x,A)\imp\ex(x,B)) in G;
theorem :: AOFA_L00:124
L is subst-correct vf-qc-correct implies
\for(x,\notA)\iff\not\ex(x,A) in G;
theorem :: AOFA_L00:125
L is subst-correct vf-qc-correct implies
\for(x,y,A)\iff\not\ex(x,y,\notA) in G;
theorem :: AOFA_L00:126
L is subst-correct vf-qc-correct implies
\for(x,A)\iff\for(x,\not\notA) in G;
theorem :: AOFA_L00:127
L is subst-correct vf-qc-correct implies
\for(x,A\andB)\imp(\for(x,A)\and\for(x,B)) in G;
theorem :: AOFA_L00:128
L is vf-qc-correct subst-correct implies
(\for(x,A)\and\for(x,B))\imp\for(x,A\andB) in G;
theorem :: AOFA_L00:129
L is subst-correct vf-qc-correct implies
(\for(x,A)\or\for(x,B))\imp\for(x,A\orB) in G;
theorem :: AOFA_L00:130
L is subst-correct vf-qc-correct &
A\impB in G implies \ex(x,A)\imp\ex(x,B) in G;
theorem :: AOFA_L00:131
L is subst-correct vf-qc-correct &
A\iffB in G implies \ex(x,A)\iff\ex(x,B) in G;
theorem :: AOFA_L00:132
L is subst-correct vf-qc-correct implies
\ex(x,A)\iff\ex(x,\not\notA) in G;
theorem :: AOFA_L00:133
L is subst-correct vf-qc-correct implies
\ex(x,A)\or\ex(x,B)\iff\ex(x,A\orB) in G;
theorem :: AOFA_L00:134
L is subst-correct implies
for a being SortSymbol of J st x in X.a & x nin (vf A).a
holds A\iff\for(x,A) in G;
reserve a for SortSymbol of J;
theorem :: AOFA_L00:135
L is subst-correct vf-qc-correct &
x in X.a & x nin (vf A).a implies \for(x,A\orB)\imp(A\or\for(x,B)) in G;
theorem :: AOFA_L00:136
L is subst-correct vf-qc-correct &
x in X.a & x nin (vf A).a implies \ex(x,A\andB)\impA\and\ex(x,B) in G;
theorem :: AOFA_L00:137
L is subst-correct vf-qc-correct &
x in X.a & x nin (vf A).a implies \ex(x,A\andB)\iffA\and\ex(x,B) in G;
theorem :: AOFA_L00:138
L is subst-correct vf-qc-correct &
x in X.a & x nin (vf A).a implies \ex(x,A\impB)\imp(A\imp\ex(x,B)) in G;
theorem :: AOFA_L00:139
L is vf-qc-correct implies
\for(x,A)\imp\for(x,x,A) in G;
theorem :: AOFA_L00:140
L is vf-qc-correct subst-correct implies
\for(x,y,A)\imp\for(y,x,A) in G;
theorem :: AOFA_L00:141
L is vf-qc-correct subst-correct implies
\ex(x,y,A)\imp\ex(y,x,A) in G;
theorem :: AOFA_L00:142
L is vf-qc-correct subst-correct implies
\ex(x,\for(y,A))\imp\for(y,\ex(x,A)) in G;
theorem :: AOFA_L00:143
L is subst-correct vf-qc-correct implies
\for(x,A\andA)\iff\for(x,A) in G;
theorem :: AOFA_L00:144
L is subst-correct vf-qc-correct implies
\for(x,A\orA)\iff\for(x,A) in G;
theorem :: AOFA_L00:145
L is subst-correct vf-qc-correct implies
\ex(x,A\orA)\iff\ex(x,A) in G;
reserve
L for non-empty T-extension Language of
X extended_by ({},the carrier of S1), S1,
G1 for QC-theory_with_equality of L,
A,B,C,D for Formula of L,
s,s1 for SortSymbol of S1,
t,t9 for Element of L,s,
t1,t2,t3 for Element of L,s1;
theorem :: AOFA_L00:146
L is subst-eq-correct & x0 in X.s & t1 '=' (t2,L) in G1
implies (t1/(x0,t) '=' (t2/(x0,t),L)) in G1;
theorem :: AOFA_L00:147
L is subst-eq-correct vf-finite subst-correct2 subst-correct3 &
s1 in the carrier of J & X.s1 is infinite implies
t1 '=' (t2,L)\imp(t2 '=' (t1,L)) in G1;
theorem :: AOFA_L00:148
L is subst-eq-correct vf-finite subst-correct2 subst-correct3 &
s1 in the carrier of J & X.s1 is infinite implies
t1 '=' (t2,L)\and(t2 '=' (t3,L))\imp(t1 '=' (t3,L)) in G1;
theorem :: AOFA_L00:149
L is subst-correct3 vf-finite subst-correct2 subst-correct subst-eq-correct
vf-qc-correct vf-eq-correct &
x = x0 in X.s & y = y0 in X.s & x <> y nin (vf A).s & X.s is infinite implies
\for(x,A\iff\ex(y, x '=' (y,L)\and(A/(x0,y0)))) in G1;
theorem :: AOFA_L00:150
L is subst-correct3 vf-finite subst-correct2 subst-correct subst-eq-correct
vf-qc-correct vf-eq-correct &
x = x0 in X.s & y = y0 in X.s & x <> y nin (vf A).s & X.s is infinite implies
\for(x,A\iff\for(y, x '=' (y,L)\imp(A/(x0,y0)))) in G1;
theorem :: AOFA_L00:151
L is subst-correct subst-eq-correct subst-correct3 vf-eq-correct &
x in X.s & y in X.s & x <> y implies \for(x,\ex(y,x '=' (y,L))) in G1;
theorem :: AOFA_L00:152
L is subst-correct & x = x0 in X.s & y = y0 in X.s implies
A\and (x '=' (y,L))\imp(A/(x0,y0)) in G1;
theorem :: AOFA_L00:153
L is subst-correct & x = x0 in X.s & y = y0 in X.s implies
A\and\not(A/(x0,y0))\imp\not(x '=' (y,L)) in G1;
begin :: Algorithmic logic
reserve
n for non empty natural number,
J for non empty non void Signature,
T for non-empty VarMSAlgebra over J,
X for non-empty GeneratorSet of T,
S for essential J-extension non empty non void n PC-correct QC-correct
n AL-correct AlgLangSignature over Union X,
L for non empty IfWhileAlgebra of X,S,
M,M1,M2 for Algorithm of L,
A,B,C,V for Formula of L,
H for AL-theory of V,L,
a for SortSymbol of J,
x,y for (Element of X.a),
t for Element of T,a;
theorem :: AOFA_L00:154
(M*(A\andB\andC))\iff(M*A)\and(M*B)\and(M*C) in H;
theorem :: AOFA_L00:155
(M*(A\orB\orC))\iff(M*A)\or(M*B)\or(M*C) in H;
theorem :: AOFA_L00:156
A\iffB in H implies \Cup(M,A)\iff\Cup(M,B) in H;
theorem :: AOFA_L00:157
A\iffB in H implies \Cap(M,A)\iff\Cap(M,B) in H;
theorem :: AOFA_L00:158
\Cup(M,A) \iff A\or(M*A)\or\Cup(M, (M\;M)*A) in H;
theorem :: AOFA_L00:159
\Cap(M,A) \iff A\and(M*A)\and\Cap(M, (M\;M)*A) in H;
theorem :: AOFA_L00:160
for x0,y0 being Element of Union (X extended_by ({},the carrier of S))
st x = x0 & y = y0 holds
((x:=(@y,L))*A) \iff (A/(x0,y0)) in H;
theorem :: AOFA_L00:161
M*V in H & M*(M1*A) in H or M*\notV in H & M*(M2*A) in H implies
if-then-else(M,M1,M2)*A in H;
theorem :: AOFA_L00:162
M*\notV in H & A in H or M*V in H & M*(M1*(while(M,M1)*A)) in H implies
while(M,M1)*A in H;