:: Algebraic Approach to Algorithmic Logic
:: by Grzegorz Bancerek
::
:: Received September 15, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


registration
let f be non empty-yielding Function;
cluster Union f -> non empty ;
coherence
not Union f is empty
proof end;
end;

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

registration
let I be set ;
let f be V2() ManySortedSet of I;
let i be set ;
let x be non empty set ;
cluster f +* (i,x) -> non-empty ;
coherence
f +* (i,x) is non-empty
;
end;

registration
let S be non empty non void ManySortedSign ;
cluster non-empty strict for VarMSAlgebra over S;
existence
ex b1 being strict VarMSAlgebra over S st b1 is non-empty
proof end;
end;

definition
let f, g be Function;
attr g is f -tolerating means :: AOFA_L00:def 1
f tolerates g;
end;

:: deftheorem defines -tolerating AOFA_L00:def 1 :
for f, g being Function holds
( g is f -tolerating iff f tolerates g );

theorem Th1: :: AOFA_L00:1
for f, g being Function holds
( g is f -tolerating iff for x being object st x in dom f & x in dom g holds
f . x = g . x )
proof end;

theorem Th2: :: 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 being object st x in I & x in J holds
f . x = g . x )
proof end;

theorem Th3: :: AOFA_L00:3
for f, g being Function holds f tolerates g +* f
proof end;

registration
let X, Y be Function;
cluster Y +* X -> X -tolerating ;
coherence
Y +* X is X -tolerating
by Th3;
end;

registration
let X be Function;
let J be set ;
let Y be ManySortedSet of J;
cluster Y +* (X | J) -> X -tolerating ;
coherence
Y +* (X | J) is X -tolerating
proof end;
end;

registration
let J be set ;
let X be Function;
cluster Relation-like J -defined Function-like total X -tolerating for set ;
existence
ex b1 being ManySortedSet of J st b1 is X -tolerating
proof end;
end;

registration
let J be set ;
let X be non-empty Function;
cluster Relation-like V2() J -defined Function-like total X -tolerating for set ;
existence
ex b1 being V2() ManySortedSet of J st b1 is X -tolerating
proof end;
end;

registration
let I be non empty set ;
let X be V3() ManySortedSet of I;
cluster Union X -> non empty ;
coherence
not Union X is empty
;
end;

theorem Th4: :: AOFA_L00:4
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type {} ,r holds
{} in Args (o,T)
proof end;

theorem Th5: :: AOFA_L00:5
for x being object
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s*>,r & x in the Sorts of T . s holds
<*x*> in Args (o,T)
proof end;

Lm1: now :: thesis: for I being set
for A being ManySortedSet of I holds A is Function of I,(bool (Union A))
let I be set ; :: thesis: for A being ManySortedSet of I holds A is Function of I,(bool (Union A))
let A be ManySortedSet of I; :: thesis: A is Function of I,(bool (Union A))
A1: dom A = I by PARTFUN1:def 2;
rng A c= bool (Union A)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng A or x in bool (Union A) )
reconsider X = x as set by TARSKI:1;
assume x in rng A ; :: thesis: x in bool (Union A)
then ( X c= union (rng A) & union (rng A) = Union A ) by ZFMISC_1:74;
hence x in bool (Union A) ; :: thesis: verum
end;
hence A is Function of I,(bool (Union A)) by A1, FUNCT_2:2; :: thesis: verum
end;

theorem Th6: :: AOFA_L00:6
for x, y being object
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s1, s2, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds
<*x,y*> in Args (o,T)
proof end;

theorem :: AOFA_L00:7
for x, y, z being object
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s1, s2, s3, r being SortSymbol of S
for T being MSAlgebra over S st 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 holds
<*x,y,z*> in Args (o,T)
proof end;

definition
let S, E be Signature;
attr E is S -extension means :Def2: :: AOFA_L00:def 2
S is Subsignature of E;
end;

:: deftheorem Def2 defines -extension AOFA_L00:def 2 :
for S, E being Signature holds
( E is S -extension iff S is Subsignature of E );

registration
let S be Signature;
cluster -> S -extension for Extension of S;
coherence
for b1 being Extension of S holds b1 is S -extension
by ALGSPEC1:def 5;
end;

theorem Th8: :: AOFA_L00:8
for S, E being non empty Signature st E is S -extension holds
for a being SortSymbol of S holds a is SortSymbol of E
proof end;

theorem Th9: :: AOFA_L00:9
for S, E being non void Signature st E is S -extension holds
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
proof end;

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);
coherence
(J --> Y) +* (X | J) is ManySortedSet of J
;
end;

:: deftheorem defines extended_by AOFA_L00:def 3 :
for X being Function
for J, Y being set holds X extended_by (Y,J) = (J --> Y) +* (X | J);

registration
let X be Function;
let J, Y be set ;
cluster X extended_by (Y,J) -> X -tolerating ;
coherence
X extended_by (Y,J) is X -tolerating
;
end;

definition
attr c1 is strict ;
struct PCLangSignature -> ConnectivesSignature ;
aggr PCLangSignature(# carrier, carrier', Arity, ResultSort, formula-sort, connectives #) -> PCLangSignature ;
sel formula-sort c1 -> Element of the carrier of c1;
end;

definition
let X be set ;
attr c2 is strict ;
struct QCLangSignature over X -> PCLangSignature ;
aggr QCLangSignature(# carrier, carrier', Arity, ResultSort, formula-sort, connectives, quant-sort, quantifiers #) -> QCLangSignature over X;
sel quant-sort c2 -> set ;
sel quantifiers c2 -> Function of [: the quant-sort of c2,X:], the carrier' of c2;
end;

definition
let X be set ;
attr c2 is strict ;
struct AlgLangSignature over X -> QCLangSignature over X;
aggr AlgLangSignature(# carrier, carrier', Arity, ResultSort, formula-sort, program-sort, connectives, quant-sort, quantifiers #) -> AlgLangSignature over X;
sel program-sort c2 -> Element of the carrier of c2;
end;

definition
let n be Nat;
let L be PCLangSignature ;
attr L is n PC-correct means :Def4: :: 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;

:: deftheorem Def4 defines PC-correct AOFA_L00:def 4 :
for n being Nat
for L being PCLangSignature holds
( L is n PC-correct iff ( 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 ) );

definition
let X be set ;
let L be QCLangSignature over X;
attr L is QC-correct means :Def5: :: AOFA_L00:def 5
( the quant-sort of L = {1,2} & 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;

:: deftheorem Def5 defines QC-correct AOFA_L00:def 5 :
for X being set
for L being QCLangSignature over X holds
( L is QC-correct iff ( the quant-sort of L = {1,2} & 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 ) ) );

definition
let n be Nat;
let X be set ;
let L be AlgLangSignature over X;
attr L is n AL-correct means :Def6: :: 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;

:: deftheorem Def6 defines AL-correct AOFA_L00:def 6 :
for n being Nat
for X being set
for L being AlgLangSignature over X holds
( L is n AL-correct iff ( 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 ) );

registration
let n be natural number ;
cluster n PC-correct -> non void for PCLangSignature ;
coherence
for b1 being PCLangSignature st b1 is n PC-correct holds
not b1 is void
;
end;

definition
let X, Y be set ;
assume A1: Y c= X ;
func incl (Y,X) -> Function of Y,X equals :Def7: :: AOFA_L00:def 7
id Y;
coherence
id Y is Function of Y,X
proof end;
end;

:: deftheorem Def7 defines incl AOFA_L00:def 7 :
for X, Y being set st Y c= X holds
incl (Y,X) = id Y;

registration
let n be natural non empty number ;
let X be set ;
cluster non empty non void n PC-correct QC-correct for QCLangSignature over X;
existence
ex b1 being QCLangSignature over X st
( not b1 is void & not b1 is empty & b1 is n PC-correct & b1 is QC-correct )
proof end;
end;

registration
let n be natural non empty number ;
cluster non empty non void n PC-correct for PCLangSignature ;
existence
ex b1 being PCLangSignature st
( not b1 is void & not b1 is empty & b1 is n PC-correct )
proof end;
end;

registration
let X be set ;
cluster non empty non void strict for AlgLangSignature over X;
existence
ex b1 being strict AlgLangSignature over X st
( not b1 is void & not b1 is empty )
proof end;
end;

registration
cluster ordinal -> non pair for set ;
coherence
for b1 being set st b1 is ordinal holds
not b1 is pair
proof end;
end;

theorem :: AOFA_L00:10
for a being ordinal number
for n1, n2 being natural number st n1 <> n2 holds
a +^ n1 <> a +^ n2 by ORDINAL3:21;

registration
let R be non empty Relation;
cluster -> pair for Element of R;
coherence
for b1 being Element of R holds b1 is pair
;
end;

theorem Th11: :: AOFA_L00:11
for n being natural non empty number
for X being non empty set
for J being Signature ex S being non empty non void strict AlgLangSignature over X st
( S is n PC-correct & S is QC-correct & S is n AL-correct & S is J -extension & ( for i being natural number st not not i = 0 & ... & not 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:] ) )
proof end;

registration
let n be natural non empty number ;
let X be non empty set ;
let J be Signature;
cluster non empty non void feasible feasible J -extension strict n PC-correct QC-correct n AL-correct for AlgLangSignature over X;
existence
ex b1 being non empty non void strict AlgLangSignature over X st
( b1 is J -extension & b1 is n PC-correct & b1 is QC-correct & b1 is n AL-correct )
proof end;
end;

registration
let X be non empty set ;
let n be natural non empty number ;
cluster non empty non void feasible feasible strict n PC-correct QC-correct n AL-correct for AlgLangSignature over X;
existence
ex b1 being non empty non void strict AlgLangSignature over X st
( b1 is n PC-correct & b1 is QC-correct & b1 is n AL-correct )
proof end;
end;

definition
let J be non empty non void Signature;
let T be MSAlgebra over J;
mode VariableSet of T -> set means :Def8: :: AOFA_L00:def 8
ex G being GeneratorSet of T st it = Union G;
existence
ex b1 being set ex G being GeneratorSet of T st b1 = Union G
proof end;
end;

:: deftheorem Def8 defines VariableSet AOFA_L00:def 8 :
for J being non empty non void Signature
for T being MSAlgebra over J
for b3 being set holds
( b3 is VariableSet of T iff ex G being GeneratorSet of T st b3 = Union G );

definition
let J be non empty non void Signature;
let T be MSAlgebra over J;
let X be GeneratorSet of T;
:: original: Union
redefine func Union X -> VariableSet of T;
coherence
Union X is VariableSet of T
by Def8;
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
proof end;

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;

:: deftheorem defines -vf-yielding AOFA_L00:def 9 :
for S being non empty non void Signature
for X being ManySortedSet of the carrier of S
for T being VarMSAlgebra over S holds
( T is X -vf-yielding iff the free-vars of T is ManySortedMSSet of the Sorts of T,X );

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 :Def10: :: AOFA_L00:def 10
for j being Element of J holds f .: [:(Q . j),Y:] c= Q . j;
end;

:: deftheorem Def10 defines sort-preserving AOFA_L00:def 10 :
for J being non empty set
for Q being ManySortedSet of J
for Y being set
for f being Function of [:(Union Q),Y:],(Union Q) holds
( f is sort-preserving iff for j being Element of J holds f .: [:(Q . j),Y:] c= Q . j );

registration
let J be non empty set ;
let Q be ManySortedSet of J;
let Y be set ;
cluster Relation-like [:(Union Q),Y:] -defined Union Q -valued Function-like quasi_total sort-preserving for Element of bool [:[:(Union Q),Y:],(Union Q):];
existence
ex b1 being Function of [:(Union Q),Y:],(Union Q) st b1 is sort-preserving
proof end;
end;

definition
let J be non empty non void Signature;
let X be ManySortedSet of the carrier of J;
attr c3 is strict ;
struct SubstMSAlgebra over J,X -> MSAlgebra over J;
aggr SubstMSAlgebra(# Sorts, Charact, subst-op #) -> SubstMSAlgebra over J,X;
sel subst-op c3 -> sort-preserving Function of [:(Union the Sorts of c3),(Union [|X, the Sorts of c3|]):],(Union the Sorts of c3);
end;

theorem Th13: :: AOFA_L00:13
for I being set
for X being ManySortedSet of I
for S being ManySortedSubset of X
for x being object holds S . x is Subset of (X . x)
proof end;

definition
let J be non empty non void Signature;
let X be V3() ManySortedSet of the carrier of J;
let Q be SubstMSAlgebra over J,X;
assume A1: X is ManySortedSubset of the Sorts of Q ;
let x be Element of Union X;
A2: ( x in Union X & Union X c= Union the Sorts of Q ) by A1, PBOOLE:def 18, MSAFREE4:1;
func @ (x,Q) -> Element of Union the Sorts of Q equals :: AOFA_L00:def 11
x;
coherence
x is Element of Union the Sorts of Q
by A2;
end;

:: deftheorem defines @ AOFA_L00:def 11 :
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for x being Element of Union X holds @ (x,Q) = x;

definition
let J be non empty non void Signature;
let X be V3() ManySortedSet of the carrier of J;
let Q be SubstMSAlgebra over J,X;
assume A1: X is ManySortedSubset of the Sorts of Q ;
let j be SortSymbol of J;
assume A2: the Sorts of Q . j <> {} ;
let A be Element of Q,j;
let x, y be Element of Union X;
given a being SortSymbol of J such that A3: ( x in X . a & y in X . a ) ;
func A / (x,y) -> Element of Q,j equals :Def12: :: AOFA_L00:def 12
the subst-op of Q . [A,[x,y]];
coherence
the subst-op of Q . [A,[x,y]] is Element of Q,j
proof end;
end;

:: deftheorem Def12 defines / AOFA_L00:def 12 :
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for j being SortSymbol of J st the Sorts of Q . j <> {} holds
for A being Element of Q,j
for x, y being Element of Union X st ex a being SortSymbol of J st
( x in X . a & y in X . a ) holds
A / (x,y) = the subst-op of Q . [A,[x,y]];

definition
let J be non empty non void Signature;
let X be V3() 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;
assume A1: the Sorts of Q . j <> {} ;
let x be Element of Union X;
let t be Element of Union the Sorts of Q;
given a being SortSymbol of J such that A2: ( x in X . a & t in the Sorts of Q . a ) ;
func A / (x,t) -> Element of Q,j equals :Def13: :: AOFA_L00:def 13
the subst-op of Q . [A,[x,t]];
coherence
the subst-op of Q . [A,[x,t]] is Element of Q,j
proof end;
end;

:: deftheorem Def13 defines / AOFA_L00:def 13 :
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X
for j being SortSymbol of J
for A being Element of Q,j st the Sorts of Q . j <> {} holds
for x being Element of Union X
for t being Element of Union the Sorts of Q st ex a being SortSymbol of J st
( x in X . a & t in the Sorts of Q . a ) holds
A / (x,t) = the subst-op of Q . [A,[x,t]];

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;
existence
ex b1 being SubstMSAlgebra over J,X st b1 is non-empty
proof end;
end;

definition
let J be non empty non void Signature;
let X be V3() 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 :Def14: :: AOFA_L00:def 14
for i being Nat st i in dom (the_arity_of o) holds
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) ) );
existence
ex b1 being Element of Args (o,Q) st
for i being Nat st i in dom (the_arity_of o) holds
ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & b1 . i = A / (x,y) ) )
proof end;
uniqueness
for b1, b2 being Element of Args (o,Q) st ( for i being Nat st i in dom (the_arity_of o) holds
ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & b1 . i = A / (x,y) ) ) ) & ( for i being Nat st i in dom (the_arity_of o) holds
ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & b2 . i = A / (x,y) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines / AOFA_L00:def 14 :
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being non-empty SubstMSAlgebra over J,X
for o being OperSymbol of J
for p being Element of Args (o,Q)
for x being Element of Union X
for y being Element of Union the Sorts of Q
for b8 being Element of Args (o,Q) holds
( b8 = p / (x,y) iff for i being Nat st i in dom (the_arity_of o) holds
ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & b8 . i = A / (x,y) ) ) );

definition
let I be non empty set ;
let X be V2() ManySortedSet of I;
let S be V2() 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;
coherence
z is Element of X . x
proof end;
end;

:: deftheorem defines @ AOFA_L00:def 15 :
for I being non empty set
for X being V2() ManySortedSet of I
for S being V2() ManySortedSubset of X
for x being Element of I
for z being Element of S . x holds @ z = z;

definition
let J be non empty non void Signature;
let X be V3() 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 holds
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 & ( for S being QCLangSignature over Union X holds
( not J = S or for z being Element of Union X
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
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, t being Element of Q,j
for x being Element of Union X st t = x & x in X . j holds
t / (x,q) = q;
end;

:: deftheorem defines subst-correct AOFA_L00:def 16 :
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being non-empty SubstMSAlgebra over J,X holds
( Q is subst-correct iff 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 holds
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 & ( for S being QCLangSignature over Union X holds
( not J = S or for z being Element of Union X
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,Q)) . (p / (x,y)) ) ) );

:: deftheorem defines subst-correct2 AOFA_L00:def 17 :
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being non-empty SubstMSAlgebra over J,X holds
( Q is subst-correct2 iff for j being SortSymbol of J
for q, t being Element of Q,j
for x being Element of Union X st t = x & x in X . j holds
t / (x,q) = q );

theorem Th14: :: AOFA_L00:14
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for a being SortSymbol of J st the Sorts of Q . a <> {} holds
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 holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
proof end;

registration
let J be non void Signature;
cluster feasible J -extension -> non empty non void for ManySortedSign ;
coherence
for b1 being Signature st b1 is J -extension holds
( not b1 is void & not b1 is empty )
proof end;
end;

registration
let J be Signature;
cluster non empty non void feasible feasible J -extension for ManySortedSign ;
existence
ex b1 being non empty non void Signature st b1 is J -extension
proof end;
let X be non empty set ;
cluster non empty non void feasible feasible J -extension for QCLangSignature over X;
existence
ex b1 being non empty non void QCLangSignature over X st b1 is J -extension
proof end;
let n be natural non empty number ;
cluster non empty non void feasible feasible J -extension n PC-correct QC-correct for QCLangSignature over X;
existence
ex b1 being non empty non void n PC-correct QC-correct QCLangSignature over X st b1 is J -extension
proof end;
end;

definition
let J be Signature;
let X be non empty set ;
let n be non empty Nat;
let S be feasible J -extension n PC-correct AlgLangSignature over X;
attr S is essential means :Def16: :: 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;

:: deftheorem Def16 defines essential AOFA_L00:def 18 :
for J being Signature
for X being non empty set
for n being non empty Nat
for S being feasible b1 -extension b3 PC-correct AlgLangSignature over X holds
( S is essential iff ( 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 ) );

registration
let n be natural non empty number ;
let X be non empty set ;
let J be Signature;
cluster non empty non void feasible feasible J -extension strict n PC-correct QC-correct n AL-correct essential for AlgLangSignature over X;
existence
ex b1 being non empty non void J -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X st b1 is essential
proof end;
end;

registration
let J be non empty Signature;
let S be non empty J -extension Signature;
let X be V3() ManySortedSet of the carrier of J;
cluster Relation-like V3() the carrier of S -defined Function-like non empty total X -tolerating for set ;
existence
ex b1 being V3() ManySortedSet of the carrier of S st b1 is X -tolerating
proof end;
end;

definition
let J, S be non empty Signature;
let T be MSAlgebra over J;
let Q be MSAlgebra over S;
attr Q is T -extension means :Def17: :: AOFA_L00:def 19
Q | J = MSAlgebra(# the Sorts of T, the Charact of T #);
end;

:: deftheorem Def17 defines -extension AOFA_L00:def 19 :
for J, S being non empty Signature
for T being MSAlgebra over J
for Q being MSAlgebra over S holds
( Q is T -extension iff Q | J = MSAlgebra(# the Sorts of T, the Charact of T #) );

theorem Th15: :: AOFA_L00:15
for J being non empty non void Signature
for S being b1 -extension Signature
for T being MSAlgebra over J
for Q1, Q2 being MSAlgebra over S st MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) & Q1 is T -extension holds
Q2 is T -extension
proof end;

theorem Th16: :: AOFA_L00:16
for J being non empty non void Signature
for S being b1 -extension Signature
for T being MSAlgebra over J
for Q being MSAlgebra over S st Q is T -extension holds
for x being object st x in the carrier of J holds
the Sorts of T . x = the Sorts of Q . x
proof end;

theorem Th17: :: AOFA_L00:17
for J being non empty non void Signature
for S being b1 -extension Signature
for T being MSAlgebra over J
for I being set st I c= the carrier of S \ the carrier of J holds
for X being ManySortedSet of I ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )
proof end;

theorem Th18: :: AOFA_L00:18
for J being non empty non void Signature
for S being b1 -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 holds
for X being V2() ManySortedSet of I ex Q being non-empty MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )
proof end;

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;
existence
ex b1 being MSAlgebra over S st b1 is T -extension
proof end;
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 non-empty non empty T -extension for MSAlgebra over S;
existence
ex b1 being non-empty MSAlgebra over S st b1 is T -extension
proof end;
end;

theorem Th19: :: AOFA_L00:19
for I being set
for a being object holds pr1 (I,{a}) is one-to-one
proof end;

theorem Th20: :: AOFA_L00:20
for S1, S2, E1, E2 being Signature st ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) & ManySortedSign(# the carrier of E1, the carrier' of E1, the Arity of E1, the ResultSort of E1 #) = ManySortedSign(# the carrier of E2, the carrier' of E2, the Arity of E2, the ResultSort of E2 #) & E1 is Extension of S1 holds
E2 is Extension of S2
proof end;

registration
let I be set ;
let a be object ;
cluster pr1 (I,{a}) -> one-to-one ;
coherence
pr1 (I,{a}) is one-to-one
by Th19;
end;

definition
let a, b, c be non empty set ;
let g be Function of a,b;
let f be Function of b,c;
:: original: *
redefine func f * g -> Function of a,c;
coherence
g * f is Function of a,c
proof end;
end;

theorem Lem6: :: AOFA_L00:21
for X, Y being set
for f being one-to-one Function st X misses Y holds
f .: X misses f .: Y
proof end;

theorem Th21: :: AOFA_L00:22
for n being natural non empty number
for X being set
for J being non empty Signature ex Q being non empty non void b1 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 )
proof end;

registration
let J be non empty Signature;
cluster non empty non void feasible feasible J -extension for ManySortedSign ;
existence
ex b1 being non empty non void Signature st b1 is J -extension
proof end;
let X be set ;
cluster non empty non void feasible feasible J -extension for QCLangSignature over X;
existence
ex b1 being non empty non void QCLangSignature over X st b1 is J -extension
proof end;
let n be natural non empty number ;
cluster non empty non void feasible feasible J -extension n PC-correct QC-correct for QCLangSignature over X;
existence
ex b1 being non empty non void n PC-correct QC-correct QCLangSignature over X st b1 is J -extension
proof end;
end;

definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
let Y be X -tolerating ManySortedSet of the carrier of S;
attr c6 is strict ;
struct LanguageStr over T,Y,S -> VarMSAlgebra over S, SubstMSAlgebra over S,Y;
aggr LanguageStr(# Sorts, Charact, free-vars, subst-op, equality #) -> LanguageStr over T,Y,S;
sel equality c6 -> Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of c6 . the formula-sort of S);
end;

definition
let S be non empty PCLangSignature ;
let L be MSAlgebra over S;
attr L is language means :Def18: :: AOFA_L00:def 20
not the Sorts of L . the formula-sort of S is empty ;
end;

:: deftheorem Def18 defines language AOFA_L00:def 20 :
for S being non empty PCLangSignature
for L being MSAlgebra over S holds
( L is language iff not the Sorts of L . the formula-sort of S is empty );

registration
let S be non empty PCLangSignature ;
cluster non-empty -> language for MSAlgebra over S;
coherence
for b1 being MSAlgebra over S st b1 is non-empty holds
b1 is language
;
cluster language for MSAlgebra over S;
existence
ex b1 being MSAlgebra over S st b1 is language
proof end;
end;

theorem Th22: :: AOFA_L00:23
for J being non void Signature
for S being non void b1 -extension Signature
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
A1 | J = A2 | J
proof end;

registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
cluster Relation-like V3() the carrier of S -defined Function-like non empty total X -tolerating for set ;
existence
ex b1 being V3() ManySortedSet of the carrier of S st b1 is X -tolerating
proof end;
end;

registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
let Y be V3() X -tolerating ManySortedSet of the carrier of S;
cluster non-empty T -extension language for LanguageStr over T,Y,S;
existence
ex b1 being LanguageStr over T,Y,S st
( b1 is non-empty & b1 is language & b1 is T -extension )
proof end;
end;

definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
let Y be V3() X -tolerating 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 & 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;

:: deftheorem defines subst-correct3 AOFA_L00:def 21 :
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b1 -extension QCLangSignature over Union X
for Y being V3() b3 -tolerating ManySortedSet of the carrier of S
for L being non-empty LanguageStr over T,Y,S holds
( L is subst-correct3 iff 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 & 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 ) ) );

registration
let J be non empty Signature;
let S be non empty J -extension Signature;
let X be V3() ManySortedSet of the carrier of J;
let Y be set ;
cluster X extended_by (Y, the carrier of S) -> V3() ;
coherence
not X extended_by (Y, the carrier of S) is empty-yielding
proof end;
end;

registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
cluster non-empty X extended_by ({}, the carrier of S) -vf-yielding T -extension language for LanguageStr over T,X extended_by ({}, the carrier of S),S;
existence
ex b1 being LanguageStr over T,X extended_by ({}, the carrier of S),S st
( b1 is X extended_by ({}, the carrier of S) -vf-yielding & b1 is non-empty & b1 is language & b1 is T -extension )
proof end;
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 ;
coherence
not the Sorts of L . the formula-sort of S is empty
by Def18;
end;

definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
let Y be V3() X -tolerating ManySortedSet of the carrier of S;
mode Language of Y,S is T -extension language 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 natural non empty number ;
let S be non empty non void n PC-correct PCLangSignature ;
let L be language MSAlgebra over S;
set f = the formula-sort of S;
A1: the Sorts of L . the formula-sort of S <> {} by Def18;
A2: the connectives of S . n is_of_type <* the formula-sort of S*>, the formula-sort of S by Def4;
A3: the connectives of S . (n + 5) is_of_type {} , the formula-sort of S by Def4;
A4: len the connectives of S >= n + 5 by Def4;
n + 1 <= n + 5 & ... & n + 5 <= n + 5 by XREAL_1:6;
then ( 1 <= n + 1 & n + 1 <= len the connectives of S ) & ... & ( 1 <= n + 5 & n + 5 <= len the connectives of S ) by A4, NAT_1:12, XXREAL_0:2;
then A5: n + 1 in dom the connectives of S & ... & n + 5 in dom the connectives of S by FINSEQ_3:25;
A6: the connectives of S . (n + 1) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & ... & the connectives of S . (n + 4) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S by Def4;
A7: ( the connectives of S . (n + 5) in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by A5, FUNCT_1:def 3;
func \true_ L -> Formula of L equals :: AOFA_L00:def 22
(Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),L)) . {};
coherence
(Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),L)) . {} is Formula of L
by A1, A3, A7, AOFA_A00:31;
let A be Formula of L;
func \not A -> Formula of L equals :: AOFA_L00:def 23
(Den ((In (( the connectives of S . n), the carrier' of S)),L)) . <*A*>;
coherence
(Den ((In (( the connectives of S . n), the carrier' of S)),L)) . <*A*> is Formula of L
by A1, A2, AOFA_A00:32;
let B be Formula of L;
func A \and B -> Formula of L equals :: AOFA_L00:def 24
(Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),L)) . <*A,B*>;
coherence
(Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),L)) . <*A,B*> is Formula of L
by A1, A6, AOFA_A00:33;
func A \or B -> Formula of L equals :: AOFA_L00:def 25
(Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),L)) . <*A,B*>;
coherence
(Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),L)) . <*A,B*> is Formula of L
by A1, A6, AOFA_A00:33;
func A \imp B -> Formula of L equals :: AOFA_L00:def 26
(Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),L)) . <*A,B*>;
coherence
(Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),L)) . <*A,B*> is Formula of L
by A1, A6, AOFA_A00:33;
func A \iff B -> Formula of L equals :: AOFA_L00:def 27
(Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),L)) . <*A,B*>;
coherence
(Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),L)) . <*A,B*> is Formula of L
by A1, A6, AOFA_A00:33;
end;

:: deftheorem defines \true_ AOFA_L00:def 22 :
for n being natural non empty number
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S holds \true_ L = (Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),L)) . {};

:: deftheorem defines \not AOFA_L00:def 23 :
for n being natural non empty number
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for A being Formula of L holds \not A = (Den ((In (( the connectives of S . n), the carrier' of S)),L)) . <*A*>;

:: deftheorem defines \and AOFA_L00:def 24 :
for n being natural non empty number
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for A, B being Formula of L holds A \and B = (Den ((In (( the connectives of S . (n + 1)), the carrier' of S)),L)) . <*A,B*>;

:: deftheorem defines \or AOFA_L00:def 25 :
for n being natural non empty number
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for A, B being Formula of L holds A \or B = (Den ((In (( the connectives of S . (n + 2)), the carrier' of S)),L)) . <*A,B*>;

:: deftheorem defines \imp AOFA_L00:def 26 :
for n being natural non empty number
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for A, B being Formula of L holds A \imp B = (Den ((In (( the connectives of S . (n + 3)), the carrier' of S)),L)) . <*A,B*>;

:: deftheorem defines \iff AOFA_L00:def 27 :
for n being natural non empty number
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for A, B being Formula of L holds A \iff B = (Den ((In (( the connectives of S . (n + 4)), the carrier' of S)),L)) . <*A,B*>;

registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
cluster non empty for VariableSet of T;
existence
not for b1 being VariableSet of T holds b1 is empty
proof end;
end;

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let Y be V3() X -tolerating 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;
set f = the formula-sort of S;
A1: the quant-sort of S = {1,2} by Def5;
reconsider j = 1 as Element of the quant-sort of S by A1, TARSKI:def 2;
[j,x] in [: the quant-sort of S,(Union X):] by A1, ZFMISC_1:87;
then A2: ( the quantifiers of S . (1,x) = In (( the quantifiers of S . (1,x)), the carrier' of S) & the quantifiers of S . (1,x) is_of_type <* the formula-sort of S*>, the formula-sort of S ) by A1, Def5, SUBSET_1:def 8, FUNCT_2:5;
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*>;
coherence
(Den ((In (( the quantifiers of S . (1,x)), the carrier' of S)),L)) . <*A*> is Formula of L
by A2, AOFA_A00:32;
A3: the quant-sort of S = {1,2} by Def5;
reconsider j = 2 as Element of the quant-sort of S by A3, TARSKI:def 2;
[j,x] in [: the quant-sort of S,(Union X):] by A3, ZFMISC_1:87;
then A4: ( the quantifiers of S . (2,x) = In (( the quantifiers of S . (2,x)), the carrier' of S) & the quantifiers of S . (2,x) is_of_type <* the formula-sort of S*>, the formula-sort of S ) by A3, Def5, SUBSET_1:def 8, FUNCT_2:5;
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*>;
coherence
(Den ((In (( the quantifiers of S . (2,x)), the carrier' of S)),L)) . <*A*> is Formula of L
by A4, AOFA_A00:32;
end;

:: deftheorem defines \for AOFA_L00:def 28 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x being Element of Union X holds \for (x,A) = (Den ((In (( the quantifiers of S . (1,x)), the carrier' of S)),L)) . <*A*>;

:: deftheorem defines \ex AOFA_L00:def 29 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x being Element of Union X holds \ex (x,A) = (Den ((In (( the quantifiers of S . (2,x)), the carrier' of S)),L)) . <*A*>;

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let Y be V3() X -tolerating 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)));
coherence
\for (x,(\for (y,A))) is Formula of L
;
func \ex (x,y,A) -> Formula of L equals :: AOFA_L00:def 31
\ex (x,(\ex (y,A)));
coherence
\ex (x,(\ex (y,A))) is Formula of L
;
end;

:: deftheorem defines \for AOFA_L00:def 30 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x, y being Element of Union X holds \for (x,y,A) = \for (x,(\for (y,A)));

:: deftheorem defines \ex AOFA_L00:def 31 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x, y being Element of Union X holds \ex (x,y,A) = \ex (x,(\ex (y,A)));

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let Y be V3() X -tolerating 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)));
coherence
\for (x,y,(\for (z,A))) is Formula of L
;
func \ex (x,y,z,A) -> Formula of L equals :: AOFA_L00:def 33
\ex (x,y,(\ex (z,A)));
coherence
\ex (x,y,(\ex (z,A))) is Formula of L
;
end;

:: deftheorem defines \for AOFA_L00:def 32 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x, y, z being Element of Union X holds \for (x,y,z,A) = \for (x,y,(\for (z,A)));

:: deftheorem defines \ex AOFA_L00:def 33 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x, y, z being Element of Union X holds \ex (x,y,z,A) = \ex (x,y,(\ex (z,A)));

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let Y be V3() X -tolerating 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 A1: ( 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);
coherence
the equality of L . (t1,t2) is Formula of L
proof end;
end;

:: deftheorem defines '=' AOFA_L00:def 34 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for t1, t2 being object st ex a being SortSymbol of J st
( t1 in the Sorts of T . a & t2 in the Sorts of T . a ) holds
t1 '=' (t2,L) = the equality of L . (t1,t2);

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let Y be V3() X -tolerating 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 (\not A) = vf A & vf (A \and B) = (vf A) (\/) (vf B) & vf (A \or B) = (vf A) (\/) (vf B) & vf (A \imp B) = (vf A) (\/) (vf B) & vf (A \iff B) = (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;

:: deftheorem defines vf-qc-correct AOFA_L00:def 35 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S holds
( L is vf-qc-correct iff for A, B being Formula of L holds
( vf (\not A) = vf A & vf (A \and B) = (vf A) (\/) (vf B) & vf (A \or B) = (vf A) (\/) (vf B) & vf (A \imp B) = (vf A) (\/) (vf B) & vf (A \iff B) = (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) ) ) ) );

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let Y be V3() X -tolerating ManySortedSet of the carrier of S;
let L be non-empty Language of Y,S;
attr L is vf-finite means :: AOFA_L00:def 36
for s being SortSymbol of S
for t being Element of L,s holds vf t is V31();
end;

:: deftheorem defines vf-finite AOFA_L00:def 36 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S holds
( L is vf-finite iff for s being SortSymbol of S
for t being Element of L,s holds vf t is V31() );

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let Y be V3() X -tolerating ManySortedSet of the carrier of S;
let L be non-empty 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 holds
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 ex x0, z0 being Element of Union Y st
( x = x0 & z0 = z & 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;

:: deftheorem defines subst-forex AOFA_L00:def 37 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S holds
( L is subst-forex iff 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 holds
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 ex x0, z0 being Element of Union Y st
( x = x0 & z0 = z & 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))) ) ) ) );

theorem Th23: :: 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 non void b1 -extension Signature
for Q being b2 -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q
proof end;

theorem Th24: :: 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 non void b1 -extension Signature holds Union (X extended_by ({}, the carrier of S)) = Union X
proof end;

theorem Th25: :: AOFA_L00:26
for n being natural non empty number
for X being non empty set
for S being non empty non void b1 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) ) ) ) ) ) ) )
proof end;

theorem Th26: :: AOFA_L00:27
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating 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))*> ) ) ) ) ) ) ) )
proof end;

theorem Th27: :: AOFA_L00:28
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b4 -tolerating 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 holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
proof end;

definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
let Y be X -tolerating ManySortedSet of the carrier of S;
attr c6 is strict ;
struct BialgebraStr over S,Y -> LanguageStr over T,Y,S, ProgramAlgStr over J,T,X;
aggr BialgebraStr(# Sorts, Charact, free-vars, subst-op, equality, carrier, charact, assignments #) -> BialgebraStr over S,Y;
end;

registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
cluster non empty non void feasible feasible J -extension for AlgLangSignature over Union X;
existence
ex b1 being non empty non void AlgLangSignature over Union X st b1 is J -extension
proof end;
end;

definition
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension 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 :Def34: :: AOFA_L00:def 38
the carrier of L = the Sorts of L . the program-sort of S;
end;

:: deftheorem Def34 defines AL-correct AOFA_L00:def 38 :
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b1 -extension AlgLangSignature over Union X
for Y being b3 -tolerating ManySortedSet of the carrier of S
for L being BialgebraStr over S,Y holds
( L is AL-correct iff the carrier of L = the Sorts of L . the program-sort of S );

notation
let S be 1-sorted ;
synonym 1s-empty S for empty ;
end;

notation
let S be UAStr ;
synonym ua-non-empty S for non-empty ;
end;

registration
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension AlgLangSignature over Union X;
let Y be X -tolerating ManySortedSet of the carrier of S;
cluster non 1s-empty strict for BialgebraStr over S,Y;
existence
not for b1 being strict BialgebraStr over S,Y holds b1 is 1s-empty
proof end;
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 V3() GeneratorSet of T;
let S be non empty non void feasible J -extension n PC-correct essential AlgLangSignature over Union X;
let Y be X -tolerating ManySortedSet of the carrier of S;
cluster non 1s-empty partial quasi_total ua-non-empty non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction T -extension language strict AL-correct for BialgebraStr over S,Y;
existence
ex b1 being non 1s-empty strict BialgebraStr over S,Y st
( b1 is non-empty & b1 is language & b1 is AL-correct & b1 is quasi_total & b1 is partial & b1 is ua-non-empty & b1 is with_empty-instruction & b1 is with_catenation & b1 is with_if-instruction & b1 is with_while-instruction & b1 is T -extension )
proof end;
end;

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

theorem Th29: :: AOFA_L00:30
for U1, U2 being preIfWhileAlgebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
ElementaryInstructions U1 = ElementaryInstructions U2
proof end;

theorem :: AOFA_L00:31
for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2 ;

theorem Th31: :: AOFA_L00:32
for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 & S1 is opers_closed holds
S2 is opers_closed
proof end;

theorem Th32: :: AOFA_L00:33
for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for G being GeneratorSet of U1 holds G is GeneratorSet of U2
proof end;

theorem Th33: :: AOFA_L00:34
for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
signature U1 = signature U2
proof end;

registration
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct essential AlgLangSignature over Union X;
cluster non 1s-empty partial quasi_total ua-non-empty non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction non degenerated well_founded ECIW-strict non empty vf-correct subst-correct T -extension language vf-qc-correct vf-finite subst-forex AL-correct for BialgebraStr over S,X extended_by ({}, the carrier of S);
existence
ex b1 being non 1s-empty partial quasi_total ua-non-empty non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction T -extension language BialgebraStr over S,X extended_by ({}, the carrier of S) st
( b1 is AL-correct & b1 is vf-qc-correct & b1 is vf-correct & b1 is vf-finite & b1 is subst-correct & b1 is subst-forex & not b1 is degenerated & b1 is well_founded & b1 is ECIW-strict )
proof end;
end;

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X;
mode IfWhileAlgebra of X,S is non 1s-empty partial quasi_total ua-non-empty non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction non degenerated well_founded ECIW-strict vf-correct subst-correct T -extension language vf-qc-correct subst-forex AL-correct 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 V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X;
let L be IfWhileAlgebra of X,S;
set f = the formula-sort of S;
set p = the program-sort of S;
A1: the connectives of S . (n + 6) is_of_type <* the program-sort of S, the formula-sort of S*>, the formula-sort of S & ... & the connectives of S . (n + 8) is_of_type <* the program-sort of S, the formula-sort of S*>, the formula-sort of S by Def6;
A2: the Sorts of L . the program-sort of S = the carrier of L by Def34;
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*>;
coherence
(Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),L)) . <*P,K*> is Formula of L
by A1, A2, AOFA_A00:33;
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*>;
coherence
(Den ((In (( the connectives of S . (n + 7)), the carrier' of S)),L)) . <*P,K*> is Formula of L
by A1, A2, AOFA_A00:33;
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*>;
coherence
(Den ((In (( the connectives of S . (n + 8)), the carrier' of S)),L)) . <*P,K*> is Formula of L
by A1, A2, AOFA_A00:33;
end;

:: deftheorem defines * AOFA_L00:def 39 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being IfWhileAlgebra of X,S
for K being Formula of L
for P being Algorithm of L holds P * K = (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),L)) . <*P,K*>;

:: deftheorem defines \Cup AOFA_L00:def 40 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being IfWhileAlgebra of X,S
for K being Formula of L
for P being Algorithm of L holds \Cup (P,K) = (Den ((In (( the connectives of S . (n + 7)), the carrier' of S)),L)) . <*P,K*>;

:: deftheorem defines \Cap AOFA_L00:def 41 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being IfWhileAlgebra of X,S
for K being Formula of L
for P being Algorithm of L holds \Cap (P,K) = (Den ((In (( the connectives of S . (n + 8)), the carrier' of S)),L)) . <*P,K*>;

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 :Def38: :: AOFA_L00:def 42
for A, B, C being Formula of L holds
( A \imp (B \imp A) in F & (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) in F & ((\not A) \imp (\not B)) \imp (B \imp A) in F & A \imp (A \or B) in F & A \imp (B \or A) in F & (A \imp C) \imp ((B \imp C) \imp ((A \or B) \imp C)) in F & (A \and B) \imp A in F & (A \and B) \imp B in F & A \imp (B \imp (A \and B)) in F & (A \and (\not A)) \imp B in F & (A \imp B) \imp ((A \imp (\not B)) \imp (\not A)) in F & A \or (\not A) in F & (A \iff B) \imp (A \imp B) in F & (A \iff B) \imp (B \imp A) in F & ((A \imp B) \and (B \imp A)) \imp (A \iff B) in F & \true_ L in F & ((\true_ L) \and A) \iff A in F & ((\true_ L) \or A) \iff (\true_ L) in F & ( A in F & A \imp B in F implies B in F ) );
end;

:: deftheorem Def38 defines PC-closed AOFA_L00:def 42 :
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being Subset of ( the Sorts of L . the formula-sort of S) holds
( F is PC-closed iff for A, B, C being Formula of L holds
( A \imp (B \imp A) in F & (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) in F & ((\not A) \imp (\not B)) \imp (B \imp A) in F & A \imp (A \or B) in F & A \imp (B \or A) in F & (A \imp C) \imp ((B \imp C) \imp ((A \or B) \imp C)) in F & (A \and B) \imp A in F & (A \and B) \imp B in F & A \imp (B \imp (A \and B)) in F & (A \and (\not A)) \imp B in F & (A \imp B) \imp ((A \imp (\not B)) \imp (\not A)) in F & A \or (\not A) in F & (A \iff B) \imp (A \imp B) in F & (A \iff B) \imp (B \imp A) in F & ((A \imp B) \and (B \imp A)) \imp (A \iff B) in F & \true_ L in F & ((\true_ L) \and A) \iff A in F & ((\true_ L) \or A) \iff (\true_ L) in F & ( A in F & A \imp B in F implies B in F ) ) );

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 V3() GeneratorSet of T;
let S be non empty non void J -extension 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 :Def39: :: 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 \imp B))) \imp (A \imp (\for (x,B))) in F ) ) ) & (\not (\ex (x,A))) \iff (\for (x,(\not A))) in F & (\ex (x,(\not A))) \iff (\not (\for (x,A))) in F & ( A in F implies \for (x,A) in F ) );
end;

:: deftheorem Def39 defines QC-closed AOFA_L00:def 43 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S),S
for F being Subset of ( the Sorts of L . the formula-sort of S) holds
( F is QC-closed iff 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 \imp B))) \imp (A \imp (\for (x,B))) in F ) ) ) & (\not (\ex (x,A))) \iff (\for (x,(\not A))) in F & (\ex (x,(\not A))) \iff (\not (\for (x,A))) in F & ( A in F implies \for (x,A) in F ) ) );

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 V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let L be non-empty 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 holds
for t being Element of L,s
for 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 :Def42: :: 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 holds
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;

:: deftheorem defines subst-eq-correct AOFA_L00:def 44 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S),S holds
( L is subst-eq-correct iff 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 holds
for t being Element of L,s
for t1, t2 being Element of L,s1 holds (t1 '=' (t2,L)) / (x0,t) = (t1 / (x0,t)) '=' ((t2 / (x0,t)),L) );

:: deftheorem defines vf-eq-correct AOFA_L00:def 45 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S),S holds
( L is vf-eq-correct iff 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 ) ) );

:: deftheorem Def42 defines with_equality AOFA_L00:def 46 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S),S
for F being Subset of ( the Sorts of L . the formula-sort of S) holds
( F is with_equality iff ( ( 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 holds
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 ) ) ) ) );

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty VarMSAlgebra over J;
let X be V2() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X;
let L be IfWhileAlgebra of X,S;
let V be Formula of L;
let F be Subset of ( the Sorts of L . the formula-sort of S);
attr F is V AL-closed means :Def43: :: AOFA_L00:def 47
for A, B being Formula of L holds
( ( for M being Algorithm of L holds
( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \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 \imp B 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 * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) );
end;

:: deftheorem Def43 defines AL-closed AOFA_L00:def 47 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being IfWhileAlgebra of X,S
for V being Formula of L
for F being Subset of ( the Sorts of L . the formula-sort of S) holds
( F is V AL-closed iff for A, B being Formula of L holds
( ( for M being Algorithm of L holds
( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \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 \imp B 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 * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) ) );

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 ;
coherence
[#] ( the Sorts of L . the formula-sort of S) is PC-closed
proof end;
cluster PC-closed -> non empty for Element of bool ( the Sorts of L . the formula-sort of S);
coherence
for b1 being Subset of ( the Sorts of L . the formula-sort of S) st b1 is PC-closed holds
not b1 is empty
;
cluster PC-closed for Element of bool ( the Sorts of L . the formula-sort of S);
existence
ex b1 being Subset of ( the Sorts of L . the formula-sort of S) st b1 is PC-closed
proof end;
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 V3() GeneratorSet of T;
let S be non empty non void J -extension 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 ;
coherence
[#] ( the Sorts of L . the formula-sort of S) is QC-closed
proof end;
cluster PC-closed QC-closed for Element of bool ( the Sorts of L . the formula-sort of S);
existence
ex b1 being Subset of ( the Sorts of L . the formula-sort of S) st
( b1 is QC-closed & b1 is PC-closed )
proof end;
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 V3() GeneratorSet of T;
let S be non empty non void J -extension 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) -> with_equality ;
coherence
[#] ( the Sorts of L . the formula-sort of S) is with_equality
proof end;
cluster PC-closed QC-closed with_equality for Element of bool ( the Sorts of L . the formula-sort of S);
existence
ex b1 being Subset of ( the Sorts of L . the formula-sort of S) st
( b1 is QC-closed & b1 is PC-closed & b1 is with_equality )
proof end;
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;
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 V3() GeneratorSet of T;
let S be non empty non void J -extension 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 PC-closed QC-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 V3() GeneratorSet of T;
let S be non empty non void J -extension 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_with_equality of L is PC-closed QC-closed with_equality Subset of ( the Sorts of L . the formula-sort of S);
end;

registration
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty VarMSAlgebra over J;
let X be V2() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X;
let L be IfWhileAlgebra of X,S;
let V be Formula of L;
cluster non empty PC-closed QC-closed with_equality V AL-closed for Element of bool ( the Sorts of L . the formula-sort of S);
existence
ex b1 being PC-closed QC-closed with_equality Subset of ( the Sorts of L . the formula-sort of S) st b1 is V AL-closed
proof end;
end;

definition
let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty VarMSAlgebra over J;
let X be V2() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential 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;

theorem Th34: :: AOFA_L00:35
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds A \imp A in F
proof end;

theorem Th35: :: AOFA_L00:36
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds
( A \and B in F iff ( A in F & B in F ) )
proof end;

theorem Th36: :: AOFA_L00:37
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \or B) \imp (B \or A) in F
proof end;

theorem Th37: :: AOFA_L00:38
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (B \imp C) \imp ((A \imp B) \imp (A \imp C)) in F
proof end;

theorem Th38: :: AOFA_L00:39
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \imp (B \imp C) in F holds
B \imp (A \imp C) in F
proof end;

theorem Th39: :: AOFA_L00:40
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \imp B) \imp ((B \imp C) \imp (A \imp C)) in F
proof end;

theorem :: AOFA_L00:41
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds A \imp (B \imp (A \imp B)) in F
proof end;

theorem Th41: :: AOFA_L00:42
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \imp (B \imp C)) \imp (B \imp (A \imp C)) in F
proof end;

theorem :: AOFA_L00:43
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds B \imp ((B \imp A) \imp A) in F
proof end;

theorem Th43: :: AOFA_L00:44
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds
( A \iff B in F iff ( A \imp B in F & B \imp A in F ) )
proof end;

theorem Th44: :: AOFA_L00:45
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L st B in F holds
A \imp B in F
proof end;

theorem Th45: :: AOFA_L00:46
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \imp B in F & B \imp C in F holds
A \imp C in F
proof end;

theorem Th46: :: AOFA_L00:47
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st C \imp (B \imp A) in F & B in F holds
C \imp A in F
proof end;

theorem Th47: :: AOFA_L00:48
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds ((A \and B) \imp C) \imp (A \imp (B \imp C)) in F
proof end;

theorem Th48: :: AOFA_L00:49
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \imp (B \imp C)) \imp ((A \and B) \imp C) in F
proof end;

theorem Th49: :: AOFA_L00:50
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (C \imp A) \imp ((C \imp B) \imp (C \imp (A \and B))) in F
proof end;

theorem Th50: :: AOFA_L00:51
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \and B) \imp (B \and A) in F
proof end;

theorem :: AOFA_L00:52
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \iff B) \imp (B \iff A) in F
proof end;

theorem Th52: :: AOFA_L00:53
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds (A \or A) \imp A in F
proof end;

theorem Th53: :: AOFA_L00:54
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds A \imp (A \and A) in F
proof end;

theorem Th201: :: AOFA_L00:55
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \imp B in F & A \imp C in F holds
A \imp (B \and C) in F
proof end;

theorem Th54: :: AOFA_L00:56
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds ((A \and B) \or (A \and C)) \imp (A \and (B \or C)) in F
proof end;

theorem :: AOFA_L00:57
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F
proof end;

theorem Th56: :: AOFA_L00:58
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds A \imp ((\not A) \imp B) in F
proof end;

theorem Th57: :: AOFA_L00:59
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \imp B) \imp ((\not B) \imp (\not A)) in F
proof end;

theorem Th58: :: AOFA_L00:60
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds
( A \imp B in F iff (\not B) \imp (\not A) in F )
proof end;

theorem Th59: :: AOFA_L00:61
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds
(A \or C) \imp (B \or D) in F
proof end;

theorem Th60: :: AOFA_L00:62
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \imp B) \imp ((C \or A) \imp (C \or B)) in F
proof end;

theorem :: AOFA_L00:63
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F & (\not B) \or (\not D) in F holds
(\not A) \or (\not C) in F
proof end;

theorem Th62: :: AOFA_L00:64
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \or B) \imp ((\not A) \imp B) in F
proof end;

theorem :: AOFA_L00:65
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \or B) \imp ((\not B) \imp A) in F
proof end;

theorem Th64: :: AOFA_L00:66
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds A \imp (\not (\not A)) in F
proof end;

theorem Th65: :: AOFA_L00:67
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds (\not (\not A)) \imp A in F
proof end;

theorem Th66: :: AOFA_L00:68
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds A \iff (\not (\not A)) in F
proof end;

theorem Th67: :: AOFA_L00:69
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds
( A \imp (\not B) in F iff B \imp (\not A) in F )
proof end;

theorem Th68: :: AOFA_L00:70
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds
( (\not A) \imp B in F iff (\not B) \imp A in F )
proof end;

theorem Th69: :: AOFA_L00:71
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \imp (B \imp C) in F & C \imp D in F holds
A \imp (B \imp D) in F
proof end;

theorem Th70: :: AOFA_L00:72
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (\not (A \and B)) \imp ((\not A) \or (\not B)) in F
proof end;

theorem Th71: :: AOFA_L00:73
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (\not (A \or B)) \imp ((\not A) \and (\not B)) in F
proof end;

theorem Th72: :: AOFA_L00:74
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds
(A \and C) \imp (B \and D) in F
proof end;

theorem Th73: :: AOFA_L00:75
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds ((\not A) \or (\not B)) \imp (\not (A \and B)) in F
proof end;

theorem Th74: :: AOFA_L00:76
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds ((\not A) \and (\not B)) \imp (\not (A \or B)) in F
proof end;

theorem :: AOFA_L00:77
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \or (B \or C)) \imp ((A \or B) \or C) in F
proof end;

theorem Th76: :: AOFA_L00:78
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds ((A \or B) \or C) \iff (A \or (B \or C)) in F
proof end;

theorem :: AOFA_L00:79
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \and (B \and C)) \imp ((A \and B) \and C) in F
proof end;

theorem Th78: :: AOFA_L00:80
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds ((A \and B) \and C) \iff (A \and (B \and C)) in F
proof end;

theorem Th79: :: AOFA_L00:81
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (C \or (A \imp B)) \imp ((C \or A) \imp (C \or B)) in F
proof end;

theorem Th80: :: AOFA_L00:82
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds ((A \or B) \and (A \or C)) \imp (A \or (B \and C)) in F
proof end;

theorem Th81: :: AOFA_L00:83
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L holds (A \and (B \or C)) \imp ((A \and B) \or (A \and C)) in F
proof end;

theorem Th82: :: AOFA_L00:84
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \imp B) \imp ((\not A) \or B) in F
proof end;

theorem :: AOFA_L00:85
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \imp B) \imp (\not (A \and (\not B))) in F
proof end;

theorem Th84: :: AOFA_L00:86
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for B, C being Formula of L holds (B \or ((\not C) \and C)) \imp B in F
proof end;

theorem Th85: :: AOFA_L00:87
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for B, C being Formula of L holds (B \or (C \and (\not C))) \imp B in F
proof end;

theorem Th86: :: AOFA_L00:88
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \iff B) \imp ((A \and B) \or ((\not A) \and (\not B))) in F
proof end;

theorem :: AOFA_L00:89
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \iff B) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F
proof end;

theorem :: AOFA_L00:90
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds \not (A \and (\not A)) in F
proof end;

theorem :: AOFA_L00:91
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A being Formula of L holds A \iff A in F
proof end;

theorem Th90: :: AOFA_L00:92
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L st A \iff B in F holds
B \iff A in F
proof end;

theorem Th91: :: AOFA_L00:93
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \iff B in F & B \iff C in F holds
A \iff C in F
proof end;

theorem Th92: :: AOFA_L00:94
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \iff B in F & B \imp C in F holds
A \imp C in F
proof end;

theorem Th93: :: AOFA_L00:95
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \imp B in F & B \iff C in F holds
A \imp C in F
proof end;

theorem Th94: :: AOFA_L00:96
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds
( A \iff B in F iff (\not A) \iff (\not B) in F )
proof end;

theorem Th95: :: AOFA_L00:97
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds
( A \iff B in F iff (\not (\not A)) \iff B in F )
proof end;

theorem Th96: :: AOFA_L00:98
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \imp (B \imp C) in F & D \imp B in F holds
A \imp (D \imp C) in F
proof end;

theorem Th97: :: AOFA_L00:99
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \iff (B \and C) in F & C \iff D in F holds
A \iff (B \and D) in F
proof end;

theorem Th98: :: AOFA_L00:100
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \iff (B \and C) in F & B \iff D in F holds
A \iff (D \and C) in F
proof end;

theorem Th99: :: AOFA_L00:101
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \iff (B \or C) in F & C \iff D in F holds
A \iff (B \or D) in F
proof end;

theorem Th100: :: AOFA_L00:102
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \iff (B \or C) in F & B \iff D in F holds
A \iff (D \or C) in F
proof end;

theorem Th101: :: AOFA_L00:103
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \imp B in F holds
(B \imp C) \imp (A \imp C) in F
proof end;

theorem Th102: :: AOFA_L00:104
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C being Formula of L st A \imp B in F holds
(C \imp A) \imp (C \imp B) in F
proof end;

theorem Th103: :: AOFA_L00:105
for n being non empty Nat
for S being non empty non void b1 PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds
(B \imp C) \imp (A \imp D) in F
proof end;

theorem Th104: :: AOFA_L00:106
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct holds
(\for (x,A)) \imp A in G
proof end;

theorem Th105: :: AOFA_L00:107
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X holds (\ex (x,A)) \iff (\not (\for (x,(\not A)))) in G
proof end;

theorem Th106: :: AOFA_L00:108
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X holds (\for (x,A)) \iff (\not (\ex (x,(\not A)))) in G
proof end;

theorem Th107: :: AOFA_L00:109
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct holds
(\for (x,(A \imp B))) \imp ((\for (x,A)) \imp B) in G
proof end;

theorem Th108: :: AOFA_L00:110
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X
for a being SortSymbol of J st x in X . a & x nin (vf A) . a & \for (x,(A \imp B)) in G holds
A \imp (\for (x,B)) in G
proof end;

:: x nin (vf A).a implies \for(x,A\impB)\imp(A\imp\for(x,B)) in G by AX2;
theorem Th109: :: AOFA_L00:111
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,(A \imp B))) \imp ((\for (x,A)) \imp (\for (x,B))) in G
proof end;

theorem Th110: :: AOFA_L00:112
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
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
proof end;

theorem Th111: :: AOFA_L00:113
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\ex (x,y,A)) \iff (\not (\for (x,y,(\not A)))) in G
proof end;

theorem Th112: :: AOFA_L00:114
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct holds
A \imp (\ex (x,A)) in G
proof end;

theorem Th113: :: AOFA_L00:115
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for A being Formula of L
for x being Element of Union X st L is vf-qc-correct holds
for a being SortSymbol of S1 st x in X . a holds
x nin (vf (\for (x,A))) . a
proof end;

theorem Th114: :: AOFA_L00:116
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for A being Formula of L
for x being Element of Union X st L is vf-qc-correct holds
for a being SortSymbol of S1 st x in X . a holds
x nin (vf (\ex (x,A))) . a
proof end;

theorem Th115: :: AOFA_L00:117
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \imp B in G holds
(\for (x,A)) \imp (\for (x,B)) in G
proof end;

theorem :: AOFA_L00:118
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,((\not A) \imp (\not B)))) \imp ((\for (x,B)) \imp (\for (x,A))) in G
proof end;

theorem Th117: :: AOFA_L00:119
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,(A \imp B))) \imp ((\for (x,(\not B))) \imp (\for (x,(\not A)))) in G
proof end;

theorem :: AOFA_L00:120
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds
(\for (x,A)) \iff (\for (x,B)) in G
proof end;

theorem :: AOFA_L00:121
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X holds (\ex (x,(\not A))) \iff (\not (\for (x,A))) in G by Def39;

theorem Th120: :: AOFA_L00:122
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
for a being SortSymbol of J st x in X . a & x nin (vf B) . a holds
(\for (x,(A \imp B))) \imp ((\ex (x,A)) \imp B) in G
proof end;

theorem Th121: :: AOFA_L00:123
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,(A \imp B))) \imp ((\ex (x,A)) \imp (\ex (x,B))) in G
proof end;

theorem Th122: :: AOFA_L00:124
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,(\not A))) \iff (\not (\ex (x,A))) in G
proof end;

theorem :: AOFA_L00:125
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,y,A)) \iff (\not (\ex (x,y,(\not A)))) in G
proof end;

theorem :: AOFA_L00:126
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,A)) \iff (\for (x,(\not (\not A)))) in G
proof end;

theorem Th125: :: AOFA_L00:127
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,(A \and B))) \imp ((\for (x,A)) \and (\for (x,B))) in G
proof end;

theorem Th126: :: AOFA_L00:128
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is vf-qc-correct & L is subst-correct holds
((\for (x,A)) \and (\for (x,B))) \imp (\for (x,(A \and B))) in G
proof end;

theorem Th127: :: AOFA_L00:129
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
((\for (x,A)) \or (\for (x,B))) \imp (\for (x,(A \or B))) in G
proof end;

theorem Th128: :: AOFA_L00:130
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \imp B in G holds
(\ex (x,A)) \imp (\ex (x,B)) in G
proof end;

theorem Th129: :: AOFA_L00:131
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds
(\ex (x,A)) \iff (\ex (x,B)) in G
proof end;

theorem :: AOFA_L00:132
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\ex (x,A)) \iff (\ex (x,(\not (\not A)))) in G
proof end;

theorem :: AOFA_L00:133
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
((\ex (x,A)) \or (\ex (x,B))) \iff (\ex (x,(A \or B))) in G
proof end;

theorem :: AOFA_L00:134
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct holds
for a being SortSymbol of J st x in X . a & x nin (vf A) . a holds
A \iff (\for (x,A)) in G
proof end;

theorem Th133: :: AOFA_L00:135
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X
for a being SortSymbol of J st L is subst-correct & L is vf-qc-correct & x in X . a & x nin (vf A) . a holds
(\for (x,(A \or B))) \imp (A \or (\for (x,B))) in G
proof end;

theorem Th134: :: AOFA_L00:136
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X
for a being SortSymbol of J st L is subst-correct & L is vf-qc-correct & x in X . a & x nin (vf A) . a holds
(\ex (x,(A \and B))) \imp (A \and (\ex (x,B))) in G
proof end;

theorem :: AOFA_L00:137
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X
for a being SortSymbol of J st L is subst-correct & L is vf-qc-correct & x in X . a & x nin (vf A) . a holds
(\ex (x,(A \and B))) \iff (A \and (\ex (x,B))) in G
proof end;

theorem :: AOFA_L00:138
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A, B being Formula of L
for x being Element of Union X
for a being SortSymbol of J st L is subst-correct & L is vf-qc-correct & x in X . a & x nin (vf A) . a holds
(\ex (x,(A \imp B))) \imp (A \imp (\ex (x,B))) in G
proof end;

theorem :: AOFA_L00:139
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is vf-qc-correct holds
(\for (x,A)) \imp (\for (x,x,A)) in G
proof end;

theorem Th138: :: AOFA_L00:140
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X st L is vf-qc-correct & L is subst-correct holds
(\for (x,y,A)) \imp (\for (y,x,A)) in G
proof end;

theorem :: AOFA_L00:141
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X st L is vf-qc-correct & L is subst-correct holds
(\ex (x,y,A)) \imp (\ex (y,x,A)) in G
proof end;

theorem :: AOFA_L00:142
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X st L is vf-qc-correct & L is subst-correct holds
(\ex (x,(\for (y,A)))) \imp (\for (y,(\ex (x,A)))) in G
proof end;

theorem :: AOFA_L00:143
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,(A \and A))) \iff (\for (x,A)) in G
proof end;

theorem :: AOFA_L00:144
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\for (x,(A \or A))) \iff (\for (x,A)) in G
proof end;

theorem :: AOFA_L00:145
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x being Element of Union X st L is subst-correct & L is vf-qc-correct holds
(\ex (x,(A \or A))) \iff (\ex (x,A)) in G
proof end;

theorem :: AOFA_L00:146
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for x0 being Element of Union (X extended_by ({}, the carrier of S1))
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for s, s1 being SortSymbol of S1
for t being Element of L,s
for t1, t2 being Element of L,s1 st L is subst-eq-correct & x0 in X . s & t1 '=' (t2,L) in G1 holds
(t1 / (x0,t)) '=' ((t2 / (x0,t)),L) in G1
proof end;

theorem ThOne: :: AOFA_L00:147
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for s1 being SortSymbol of S1
for t1, t2 being Element of L,s1 st L is subst-eq-correct & L is vf-finite & L is subst-correct2 & L is subst-correct3 & s1 in the carrier of J & X . s1 is infinite holds
(t1 '=' (t2,L)) \imp (t2 '=' (t1,L)) in G1
proof end;

theorem :: AOFA_L00:148
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for s1 being SortSymbol of S1
for t1, t2, t3 being Element of L,s1 st L is subst-eq-correct & L is vf-finite & L is subst-correct2 & L is subst-correct3 & s1 in the carrier of J & X . s1 is infinite holds
((t1 '=' (t2,L)) \and (t2 '=' (t3,L))) \imp (t1 '=' (t3,L)) in G1
proof end;

theorem :: AOFA_L00:149
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1))
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for A being Formula of L
for s being SortSymbol of S1 st L is subst-correct3 & L is vf-finite & L is subst-correct2 & L is subst-correct & L is subst-eq-correct & L is vf-qc-correct & L is vf-eq-correct & x = x0 & x0 in X . s & y = y0 & y0 in X . s & x <> y & y nin (vf A) . s & X . s is infinite holds
\for (x,(A \iff (\ex (y,((x '=' (y,L)) \and (A / (x0,y0))))))) in G1
proof end;

theorem :: AOFA_L00:150
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1))
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for A being Formula of L
for s being SortSymbol of S1 st L is subst-correct3 & L is vf-finite & L is subst-correct2 & L is subst-correct & L is subst-eq-correct & L is vf-qc-correct & L is vf-eq-correct & x = x0 & x0 in X . s & y = y0 & y0 in X . s & x <> y & y nin (vf A) . s & X . s is infinite holds
\for (x,(A \iff (\for (y,((x '=' (y,L)) \imp (A / (x0,y0))))))) in G1
proof end;

theorem :: AOFA_L00:151
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for x, y being Element of Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for s being SortSymbol of S1 st L is subst-correct & L is subst-eq-correct & L is subst-correct3 & L is vf-eq-correct & x in X . s & y in X . s & x <> y holds
\for (x,(\ex (y,(x '=' (y,L))))) in G1
proof end;

theorem ThTwo: :: AOFA_L00:152
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1))
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for A being Formula of L
for s being SortSymbol of S1 st L is subst-correct & x = x0 & x0 in X . s & y = y0 & y0 in X . s holds
(A \and (x '=' (y,L))) \imp (A / (x0,y0)) in G1
proof end;

theorem :: AOFA_L00:153
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S1 being non empty non void b2 -extension b1 PC-correct QC-correct QCLangSignature over Union X
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1))
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G1 being QC-theory_with_equality of L
for A being Formula of L
for s being SortSymbol of S1 st L is subst-correct & x = x0 & x0 in X . s & y = y0 & y0 in X . s holds
(A \and (\not (A / (x0,y0)))) \imp (\not (x '=' (y,L))) in G1
proof end;

theorem :: AOFA_L00:154
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M being Algorithm of L
for A, B, C, V being Formula of L
for H being AL-theory of V,L holds (M * ((A \and B) \and C)) \iff (((M * A) \and (M * B)) \and (M * C)) in H
proof end;

theorem :: AOFA_L00:155
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M being Algorithm of L
for A, B, C, V being Formula of L
for H being AL-theory of V,L holds (M * ((A \or B) \or C)) \iff (((M * A) \or (M * B)) \or (M * C)) in H
proof end;

theorem Th147: :: AOFA_L00:156
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M being Algorithm of L
for A, B, V being Formula of L
for H being AL-theory of V,L st A \iff B in H holds
(\Cup (M,A)) \iff (\Cup (M,B)) in H
proof end;

theorem Th148: :: AOFA_L00:157
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M being Algorithm of L
for A, B, V being Formula of L
for H being AL-theory of V,L st A \iff B in H holds
(\Cap (M,A)) \iff (\Cap (M,B)) in H
proof end;

theorem :: AOFA_L00:158
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M being Algorithm of L
for A, V being Formula of L
for H being AL-theory of V,L holds (\Cup (M,A)) \iff ((A \or (M * A)) \or (\Cup (M,((M \; M) * A)))) in H
proof end;

theorem :: AOFA_L00:159
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M being Algorithm of L
for A, V being Formula of L
for H being AL-theory of V,L holds (\Cap (M,A)) \iff ((A \and (M * A)) \and (\Cap (M,((M \; M) * A)))) in H
proof end;

theorem :: AOFA_L00:160
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for A, V being Formula of L
for H being AL-theory of V,L
for a being SortSymbol of J
for x, y being Element of X . a
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
proof end;

theorem :: AOFA_L00:161
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M, M1, M2 being Algorithm of L
for A, V being Formula of L
for H being AL-theory of V,L st ( ( M * V in H & M * (M1 * A) in H ) or ( M * (\not V) in H & M * (M2 * A) in H ) ) holds
(if-then-else (M,M1,M2)) * A in H
proof end;

theorem :: AOFA_L00:162
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being V2() GeneratorSet of T
for S being non empty non void b2 -extension b1 PC-correct QC-correct b1 AL-correct essential AlgLangSignature over Union X
for L being non empty IfWhileAlgebra of X,S
for M, M1 being Algorithm of L
for A, V being Formula of L
for H being AL-theory of V,L st ( ( M * (\not V) in H & A in H ) or ( M * V in H & M * (M1 * ((while (M,M1)) * A)) in H ) ) holds
(while (M,M1)) * A in H
proof end;