:: Algebraic Approach to Algorithmic Logic :: by Grzegorz Bancerek :: :: Received September 15, 2014 :: Copyright (c) 2014-2017 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;