:: by Grzegorz Bancerek

::

:: Received September 15, 2014

:: Copyright (c) 2014-2017 Association of Mizar Users

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

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

registration

let I be set ;

let f be V2() ManySortedSet of I;

let i be set ;

let x be non empty set ;

coherence

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

end;
let f be V2() ManySortedSet of I;

let i be set ;

let x be non empty set ;

coherence

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

registration

let S be non empty non void ManySortedSign ;

existence

ex b_{1} being strict VarMSAlgebra over S st b_{1} is non-empty

end;
existence

ex b

proof end;

:: deftheorem defines -tolerating AOFA_L00:def 1 :

for f, g being Function holds

( g is f -tolerating iff f tolerates g );

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 )

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

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;

registration
end;

registration

let X be Function;

let J be set ;

let Y be ManySortedSet of J;

coherence

Y +* (X | J) is X -tolerating

end;
let J be set ;

let Y be ManySortedSet of J;

coherence

Y +* (X | J) is X -tolerating

proof end;

registration

let J be set ;

let X be Function;

existence

ex b_{1} being ManySortedSet of J st b_{1} is X -tolerating

end;
let X be Function;

existence

ex b

proof end;

registration

let J be set ;

let X be non-empty Function;

existence

ex b_{1} being V2() ManySortedSet of J st b_{1} is X -tolerating

end;
let X be non-empty Function;

existence

ex b

proof end;

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

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)

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

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)

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

hence
A is Function of I,(bool (Union A))
by A1, FUNCT_2:2; :: thesis: verum
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;
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

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)

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)

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

for S, E being Signature holds

( E is S -extension iff S is Subsignature of E );

registration

let S be Signature;

coherence

for b_{1} being Extension of S holds b_{1} is S -extension
by ALGSPEC1:def 5;

end;
coherence

for b

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

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

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

for X being Function

for J, Y being set holds X extended_by (Y,J) = (J --> Y) +* (X | J);

registration
end;

definition

attr c_{1} is strict ;

struct PCLangSignature -> ConnectivesSignature ;

aggr PCLangSignature(# carrier, carrier', Arity, ResultSort, formula-sort, connectives #) -> PCLangSignature ;

sel formula-sort c_{1} -> Element of the carrier of c_{1};

end;
struct PCLangSignature -> ConnectivesSignature ;

aggr PCLangSignature(# carrier, carrier', Arity, ResultSort, formula-sort, connectives #) -> PCLangSignature ;

sel formula-sort c

definition

let X be set ;

attr c_{2} 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 c_{2} -> set ;

sel quantifiers c_{2} -> Function of [: the quant-sort of c_{2},X:], the carrier' of c_{2};

end;
attr c

struct QCLangSignature over X -> PCLangSignature ;

aggr QCLangSignature(# carrier, carrier', Arity, ResultSort, formula-sort, connectives, quant-sort, quantifiers #) -> QCLangSignature over X;

sel quant-sort c

sel quantifiers c

definition

let X be set ;

attr c_{2} 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 c_{2} -> Element of the carrier of c_{2};

end;
attr c

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 c

definition

let n be Nat;

let L be PCLangSignature ;

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

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

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

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;

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

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

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

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;

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

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

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

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 ;

coherence

for b_{1} being PCLangSignature st b_{1} is n PC-correct holds

not b_{1} is void
;

end;
coherence

for b

not b

:: deftheorem Def7 defines incl AOFA_L00:def 7 :

for X, Y being set st Y c= X holds

incl (Y,X) = id Y;

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 ;

existence

ex b_{1} being QCLangSignature over X st

( not b_{1} is void & not b_{1} is empty & b_{1} is n PC-correct & b_{1} is QC-correct )

end;
let X be set ;

existence

ex b

( not b

proof end;

registration

let n be natural non empty number ;

existence

ex b_{1} being PCLangSignature st

( not b_{1} is void & not b_{1} is empty & b_{1} is n PC-correct )

end;
existence

ex b

( not b

proof end;

registration

let X be set ;

existence

ex b_{1} being strict AlgLangSignature over X st

( not b_{1} is void & not b_{1} is empty )

end;
existence

ex b

( not b

proof end;

registration
end;

theorem :: AOFA_L00:10

registration
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:] ) )

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;

ex b_{1} being non empty non void strict AlgLangSignature over X st

( b_{1} is J -extension & b_{1} is n PC-correct & b_{1} is QC-correct & b_{1} is n AL-correct )

end;
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 b

( b

proof end;

registration

let X be non empty set ;

let n be natural non empty number ;

ex b_{1} being non empty non void strict AlgLangSignature over X st

( b_{1} is n PC-correct & b_{1} is QC-correct & b_{1} is n AL-correct )

end;
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 b

( b

proof end;

definition

let J be non empty non void Signature;

let T be MSAlgebra over J;

ex b_{1} being set ex G being GeneratorSet of T st b_{1} = Union G

end;
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 G being GeneratorSet of T st it = Union G;

ex b

proof end;

:: deftheorem Def8 defines VariableSet AOFA_L00:def 8 :

for J being non empty non void Signature

for T being MSAlgebra over J

for b_{3} being set holds

( b_{3} is VariableSet of T iff ex G being GeneratorSet of T st b_{3} = Union G );

for J being non empty non void Signature

for T being MSAlgebra over J

for b

( b

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

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

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;

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

the free-vars of T is ManySortedMSSet of the Sorts of T,X;

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

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

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

for j being Element of J holds f .: [:(Q . j),Y:] c= Q . j;

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

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 ;

ex b_{1} being Function of [:(Union Q),Y:],(Union Q) st b_{1} is sort-preserving

end;
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 b

proof end;

definition

let J be non empty non void Signature;

let X be ManySortedSet of the carrier of J;

attr c_{3} is strict ;

struct SubstMSAlgebra over J,X -> MSAlgebra over J;

aggr SubstMSAlgebra(# Sorts, Charact, subst-op #) -> SubstMSAlgebra over J,X;

sel subst-op c_{3} -> sort-preserving Function of [:(Union the Sorts of c_{3}),(Union [|X, the Sorts of c_{3}|]):],(Union the Sorts of c_{3});

end;
let X be ManySortedSet of the carrier of J;

attr c

struct SubstMSAlgebra over J,X -> MSAlgebra over J;

aggr SubstMSAlgebra(# Sorts, Charact, subst-op #) -> SubstMSAlgebra over J,X;

sel subst-op c

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)

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;

coherence

x is Element of Union the Sorts of Q by A2;

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

coherence

x is Element of Union the Sorts of Q by A2;

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

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

coherence

the subst-op of Q . [A,[x,y]] is Element of Q,j

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

coherence

the subst-op of Q . [A,[x,y]] is Element of Q,j

proof 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]];

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

coherence

the subst-op of Q . [A,[x,t]] is Element of Q,j

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

coherence

the subst-op of Q . [A,[x,t]] is Element of Q,j

proof 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]];

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;

existence

ex b_{1} being SubstMSAlgebra over J,X st b_{1} is non-empty

end;
let X be ManySortedSet of the carrier of J;

existence

ex b

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

ex b_{1} 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 & b_{1} . i = A / (x,y) ) )

for b_{1}, b_{2} 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 & b_{1} . 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 & b_{2} . i = A / (x,y) ) ) ) holds

b_{1} = b_{2}

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

ex b

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 & b

proof end;

uniqueness for b

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & b

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & b

b

proof 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 b_{8} being Element of Args (o,Q) holds

( b_{8} = 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 & b_{8} . i = A / (x,y) ) ) );

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 b

( b

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & b

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;

coherence

z is Element of X . x

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

coherence

z is Element of X . x

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

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;

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

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;

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;

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

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

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)

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;

coherence

for b_{1} being Signature st b_{1} is J -extension holds

( not b_{1} is void & not b_{1} is empty )

end;
coherence

for b

( not b

proof end;

registration

let J be Signature;

existence

ex b_{1} being non empty non void Signature st b_{1} is J -extension

existence

ex b_{1} being non empty non void QCLangSignature over X st b_{1} is J -extension

ex b_{1} being non empty non void n PC-correct QC-correct QCLangSignature over X st b_{1} is J -extension

end;
existence

ex b

proof end;

let X be non empty set ;existence

ex b

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 b

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

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

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

:: 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 b_{1} -extension b_{3} 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 ) );

for J being Signature

for X being non empty set

for n being non empty Nat

for S being feasible b

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

ex b_{1} being non empty non void J -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X st b_{1} is essential

end;
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 b

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

ex b_{1} being V3() ManySortedSet of the carrier of S st b_{1} is X -tolerating

end;
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 b

proof end;

definition

let J, S be non empty Signature;

let T be MSAlgebra over J;

let Q be MSAlgebra over S;

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

Q | J = MSAlgebra(# the Sorts of T, the Charact of T #);

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

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 b_{1} -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

for S being b

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 b_{1} -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

for S being b

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 b_{1} -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 )

for S being b

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 b_{1} -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 )

for S being b

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;

existence

ex b_{1} being MSAlgebra over S st b_{1} is T -extension

end;
let S be J -extension Signature;

let T be MSAlgebra over J;

existence

ex b

proof end;

registration

let J be non empty non void Signature;

let S be J -extension Signature;

let T be non-empty MSAlgebra over J;

existence

ex b_{1} being non-empty MSAlgebra over S st b_{1} is T -extension

end;
let S be J -extension Signature;

let T be non-empty MSAlgebra over J;

existence

ex b

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

E2 is Extension of S2

proof 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

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

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 b_{1} 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 )

for X being set

for J being non empty Signature ex Q being non empty non void b

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

existence

ex b_{1} being non empty non void Signature st b_{1} is J -extension

existence

ex b_{1} being non empty non void QCLangSignature over X st b_{1} is J -extension

ex b_{1} being non empty non void n PC-correct QC-correct QCLangSignature over X st b_{1} is J -extension

end;
existence

ex b

proof end;

let X be set ;existence

ex b

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 b

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 c_{6} 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 c_{6} -> Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of c_{6} . the formula-sort of S);

end;
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 c

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 c

definition

let S be non empty PCLangSignature ;

let L be MSAlgebra over S;

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

not the Sorts of L . the formula-sort of S is empty ;

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

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 ;

coherence

for b_{1} being MSAlgebra over S st b_{1} is non-empty holds

b_{1} is language
;

existence

ex b_{1} being MSAlgebra over S st b_{1} is language

end;
coherence

for b

b

existence

ex b

proof end;

theorem Th22: :: AOFA_L00:23

for J being non void Signature

for S being non void b_{1} -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

for S being non void b

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;

ex b_{1} being V3() ManySortedSet of the carrier of S st b_{1} is X -tolerating

end;
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 b

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;

let Y be V3() X -tolerating ManySortedSet of the carrier of S;

existence

ex b_{1} being LanguageStr over T,Y,S st

( b_{1} is non-empty & b_{1} is language & b_{1} is T -extension )

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

existence

ex b

( b

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 V3() X -tolerating ManySortedSet of the carrier of S;

let L be non-empty LanguageStr over T,Y,S;

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

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

:: 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 b_{1} -extension QCLangSignature over Union X

for Y being V3() b_{3} -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 ) ) );

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 b

for Y being V3() b

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 ;

coherence

not X extended_by (Y, the carrier of S) is empty-yielding

end;
let S be non empty J -extension Signature;

let X be V3() ManySortedSet of the carrier of J;

let Y be set ;

coherence

not X extended_by (Y, the carrier of S) is empty-yielding

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;

ex b_{1} being LanguageStr over T,X extended_by ({}, the carrier of S),S st

( b_{1} is X extended_by ({}, the carrier of S) -vf-yielding & b_{1} is non-empty & b_{1} is language & b_{1} is T -extension )

end;
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 b

( b

proof end;

registration

let X be set ;

let S be non empty QCLangSignature over X;

let L be language MSAlgebra over S;

coherence

not the Sorts of L . the formula-sort of S is empty by Def18;

end;
let S be non empty QCLangSignature over X;

let L be language MSAlgebra over S;

coherence

not the Sorts of L . the formula-sort of S is empty by Def18;

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

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;
let L be language MSAlgebra over S;

mode Formula of L is Element of the Sorts of L . the formula-sort of S;

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;

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

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

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

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

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

(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;
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)) . {};

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

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

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

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

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

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

:: deftheorem defines \true_ AOFA_L00:def 22 :

for n being natural non empty number

for S being non empty non void b_{1} 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)) . {};

for n being natural non empty number

for S being non empty non void b

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 b_{1} 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*>;

for n being natural non empty number

for S being non empty non void b

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 b_{1} 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*>;

for n being natural non empty number

for S being non empty non void b

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 b_{1} 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*>;

for n being natural non empty number

for S being non empty non void b

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 b_{1} 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*>;

for n being natural non empty number

for S being non empty non void b

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 b_{1} 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*>;

for n being natural non empty number

for S being non empty non void b

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;

existence

not for b_{1} being VariableSet of T holds b_{1} is empty

end;
let T be non-empty MSAlgebra over J;

existence

not for b

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

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

(Den ((In (( the quantifiers of S . (2,x)), the carrier' of S)),L)) . <*A*> is Formula of L by A4, AOFA_A00:32;

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

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

(Den ((In (( the quantifiers of S . (2,x)), the carrier' of S)),L)) . <*A*> is Formula of L by A4, AOFA_A00:32;

:: 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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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*>;

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 b

for Y being V3() b

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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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*>;

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 b

for Y being V3() b

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;

coherence

\for (x,(\for (y,A))) is Formula of L ;

coherence

\ex (x,(\ex (y,A))) is Formula of L ;

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

coherence

\for (x,(\for (y,A))) is Formula of L ;

coherence

\ex (x,(\ex (y,A))) is Formula of L ;

:: 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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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)));

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 b

for Y being V3() b

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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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)));

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 b

for Y being V3() b

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;

coherence

\for (x,y,(\for (z,A))) is Formula of L ;

coherence

\ex (x,y,(\ex (z,A))) is Formula of L ;

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

coherence

\for (x,y,(\for (z,A))) is Formula of L ;

coherence

\ex (x,y,(\ex (z,A))) is Formula of L ;

:: 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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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)));

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 b

for Y being V3() b

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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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)));

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 b

for Y being V3() b

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

coherence

the equality of L . (t1,t2) is Formula of L

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

coherence

the equality of L . (t1,t2) is Formula of L

proof 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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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);

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 b

for Y being V3() b

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;

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

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

:: 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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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) ) ) ) );

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 b

for Y being V3() b

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;

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

for s being SortSymbol of S

for t being Element of L,s holds vf t is V31();

:: 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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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() );

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 b

for Y being V3() b

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;

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

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

:: 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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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))) ) ) ) );

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 b

for Y being V3() b

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 b_{1} -extension Signature

for Q being b_{2} -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

for T being MSAlgebra over J

for X being ManySortedSubset of the Sorts of T

for S being non void b

for Q being b

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 b_{1} -extension Signature holds Union (X extended_by ({}, the carrier of S)) = Union X

for T being MSAlgebra over J

for X being ManySortedSubset of the Sorts of T

for S being non void b

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 b_{1} 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) ) ) ) ) ) ) )

for X being non empty set

for S being non empty non void b

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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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))*> ) ) ) ) ) ) ) )

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 b

for Y being V3() b

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 b_{2} -extension b_{1} PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{4} -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 ) ) )

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 b

for Y being V3() b

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 c_{6} 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;
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 c

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;

registration

let J be non empty non void Signature;

let T be non-empty MSAlgebra over J;

let X be V3() GeneratorSet of T;

existence

ex b_{1} being non empty non void AlgLangSignature over Union X st b_{1} is J -extension

end;
let T be non-empty MSAlgebra over J;

let X be V3() GeneratorSet of T;

existence

ex b

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 AlgLangSignature over Union X;

let Y be X -tolerating ManySortedSet of the carrier of S;

let L be BialgebraStr over S,Y;

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

the carrier of L = the Sorts of L . the program-sort of S;

:: 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 b_{1} -extension AlgLangSignature over Union X

for Y being b_{3} -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 );

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 b

for Y being b

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

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;

existence

not for b_{1} being strict BialgebraStr over S,Y holds b_{1} is 1s-empty

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

existence

not for b

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

ex b_{1} being non 1s-empty strict BialgebraStr over S,Y st

( b_{1} is non-empty & b_{1} is language & b_{1} is AL-correct & b_{1} is quasi_total & b_{1} is partial & b_{1} is ua-non-empty & b_{1} is with_empty-instruction & b_{1} is with_catenation & b_{1} is with_if-instruction & b_{1} is with_while-instruction & b_{1} is T -extension )

end;
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 b

( b

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

( 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

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 ;

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

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

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

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;

ex b_{1} 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

( b_{1} is AL-correct & b_{1} is vf-qc-correct & b_{1} is vf-correct & b_{1} is vf-finite & b_{1} is subst-correct & b_{1} is subst-forex & not b_{1} is degenerated & b_{1} is well_founded & b_{1} is ECIW-strict )

end;
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 b

( b

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

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;

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

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

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

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

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

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

:: 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 b_{2} -extension b_{1} PC-correct QC-correct b_{1} 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*>;

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 b

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 b_{2} -extension b_{1} PC-correct QC-correct b_{1} 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*>;

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 b

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 b_{2} -extension b_{1} PC-correct QC-correct b_{1} 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*>;

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 b

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

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

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

:: deftheorem Def38 defines PC-closed AOFA_L00:def 42 :

for n being non empty Nat

for S being non empty non void b_{1} 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 ) ) );

for n being non empty Nat

for S being non empty non void b

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

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

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

:: 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 b_{2} -extension b_{1} 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 ) ) );

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 b

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;

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

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

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

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

:: 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 b_{2} -extension b_{1} 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) );

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 b

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 b_{2} -extension b_{1} 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 ) ) );

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 b

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 b_{2} -extension b_{1} 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 ) ) ) ) );

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 b

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

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

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

:: 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 b_{2} -extension b_{1} PC-correct QC-correct b_{1} 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 ) ) ) );

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 b

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;

coherence

[#] ( the Sorts of L . the formula-sort of S) is PC-closed

for b_{1} being Subset of ( the Sorts of L . the formula-sort of S) st b_{1} is PC-closed holds

not b_{1} is empty
;

existence

ex b_{1} being Subset of ( the Sorts of L . the formula-sort of S) st b_{1} is PC-closed

end;
let S be non empty non void n PC-correct PCLangSignature ;

let L be language MSAlgebra over S;

coherence

[#] ( the Sorts of L . the formula-sort of S) is PC-closed

proof end;

coherence for b

not b

existence

ex b

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

coherence

[#] ( the Sorts of L . the formula-sort of S) is QC-closed

ex b_{1} being Subset of ( the Sorts of L . the formula-sort of S) st

( b_{1} is QC-closed & b_{1} is PC-closed )

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

coherence

[#] ( the Sorts of L . the formula-sort of S) is QC-closed

proof end;

existence ex b

( b

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

coherence

[#] ( the Sorts of L . the formula-sort of S) is with_equality

ex b_{1} being Subset of ( the Sorts of L . the formula-sort of S) st

( b_{1} is QC-closed & b_{1} is PC-closed & b_{1} is with_equality )

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

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 b

( b

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

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

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

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;

ex b_{1} being PC-closed QC-closed with_equality Subset of ( the Sorts of L . the formula-sort of S) st b_{1} is V AL-closed

end;
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 b

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

theorem Th34: :: AOFA_L00:35

for n being non empty Nat

for S being non empty non void b_{1} 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

for S being non empty non void b

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 b_{1} 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 ) )

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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 ) )

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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 )

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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 )

for S being non empty non void b

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 b_{1} 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 )

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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 )

for S being non empty non void b

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 b_{1} 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 )

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{1} 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

for S being non empty non void b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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;

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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 b_{2} -extension b_{1} 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

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 b

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;