AOFA_L00: Algebraic Approach to Algorithmic Logic

proof end;

end;

definition

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

proof end;

end;

registration

let I be set ;
let f be V2() ManySortedSet of I;
let i be set ;
let x be non empty set ;

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

end;

registration

let S be non empty non void ManySortedSign ;

cluster non-empty strict for VarMSAlgebra over S;

proof end;

end;

definition

let f, g be Function;

attr g is f -tolerating means :: AOFA_L00:def 1
f tolerates g;

end;

:: deftheorem defines -tolerating AOFA_L00:def 1 :

theorem Th1: :: AOFA_L00:1

for f, g being Function holds
( g is f -tolerating iff for x being object st x in dom f & x in dom g holds
f . x = g . x )

proof end;

theorem Th2: :: AOFA_L00:2

for I, J being set
for f being ManySortedSet of I
for g being ManySortedSet of J holds
( g is f -tolerating iff for x being object st x in I & x in J holds
f . x = g . x )

proof end;

theorem Th3: :: AOFA_L00:3

for f, g being Function holds f tolerates g +* f

proof end;

registration

let X, Y be Function;

cluster Y +* X -> X -tolerating ;

coherence by Th3;

end;

registration

let X be Function;
let J be set ;
let Y be ManySortedSet of J;

cluster Y +* (X | J) -> X -tolerating ;

proof end;

end;

registration

let J be set ;
let X be Function;

cluster Relation-like J -defined Function-like total X -tolerating for set ;

proof end;

end;

registration

let J be set ;
let X be non-empty Function;

cluster Relation-like V2() J -defined Function-like total X -tolerating for set ;

proof end;

end;

registration

let I be non empty set ;
let X be V3() ManySortedSet of I;

cluster Union X -> non empty ;

end;

theorem Th4: :: AOFA_L00:4

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type {} ,r holds
{} in Args (o,T)

proof end;

theorem Th5: :: AOFA_L00:5

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

proof end;

Lm1: now :: thesis:

let I be set ; :: thesis:
let A be ManySortedSet of I; :: thesis:
A1: dom A = I by PARTFUN1:def 2;
rng A c= bool (Union A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider X = x as set by TARSKI:1;
assume x in rng A ; :: thesis:
then ( X c= union (rng A) & union (rng A) = Union A ) by ZFMISC_1:74;
hence x in bool (Union A) ; :: thesis:

end;

hence A is Function of I,(bool (Union A)) by A1, FUNCT_2:2; :: thesis:

end;

theorem Th6: :: AOFA_L00:6

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

proof end;

theorem :: AOFA_L00:7

for x, y, z being object
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s1, s2, s3, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s1,s2,s3*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 & z in the Sorts of T . s3 holds
<*x,y,z*> in Args (o,T)

proof end;

definition

let S, E be Signature;

attr E is S -extension means :Def2: :: AOFA_L00:def 2
S is Subsignature of E;

end;

:: deftheorem Def2 defines -extension AOFA_L00:def 2 :

registration

let S be Signature;

cluster -> S -extension for Extension of S;

coherence by ALGSPEC1:def 5;

end;

theorem Th8: :: AOFA_L00:8

for S, E being non empty Signature st E is S -extension holds
for a being SortSymbol of S holds a is SortSymbol of E

proof end;

theorem Th9: :: AOFA_L00:9

for S, E being non void Signature st E is S -extension holds
for o being OperSymbol of S
for a being set
for r being Element of S
for r1 being Element of E st r = r1 & o is_of_type a,r holds
o is_of_type a,r1

proof end;

definition

let X be Function;
let J, Y be set ;

func X extended_by (Y,J) -> ManySortedSet of J equals :: AOFA_L00:def 3
(J --> Y) +* (X | J);

end;

:: deftheorem defines extended_by AOFA_L00:def 3 :

registration

let X be Function;
let J, Y be set ;

cluster X extended_by (Y,J) -> X -tolerating ;

end;

definition

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

end;

definition

let X be set ;
attr c₂ 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₂ -> set ;
sel quantifiers c₂ -> Function of [: the quant-sort of c₂,X:], the carrier' of c₂;

end;

definition

let X be set ;
attr c₂ 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₂ -> Element of the carrier of c₂;

end;

definition

let n be Nat;
let L be PCLangSignature ;

attr L is n PC-correct means :Def4: :: AOFA_L00:def 4
( len the connectives of L >= n + 5 & the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one & the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L & the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L );

end;

:: deftheorem Def4 defines PC-correct AOFA_L00:def 4 :

definition

let X be set ;
let L be QCLangSignature over X;

attr L is QC-correct means :Def5: :: AOFA_L00:def 5
( the quant-sort of L = {1,2} & the quantifiers of L is one-to-one & rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) );

end;

:: deftheorem Def5 defines QC-correct AOFA_L00:def 5 :

definition

let n be Nat;
let X be set ;
let L be AlgLangSignature over X;

attr L is n AL-correct means :Def6: :: AOFA_L00:def 6
( the program-sort of L <> the formula-sort of L & len the connectives of L >= n + 8 & the connectives of L . (n + 6) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 8) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L );

end;

:: deftheorem Def6 defines AL-correct AOFA_L00:def 6 :

registration

let n be natural number ;

cluster n PC-correct -> non void for PCLangSignature ;

end;

definition

let X, Y be set ;
assume A1: Y c= X ;

func incl (Y,X) -> Function of Y,X equals :Def7: :: AOFA_L00:def 7
id Y;

proof end;

end;

:: deftheorem Def7 defines incl AOFA_L00:def 7 :

registration

let n be natural non empty number ;
let X be set ;

cluster non empty non void n PC-correct QC-correct for QCLangSignature over X;

proof end;

end;

registration

let n be natural non empty number ;

cluster non empty non void n PC-correct for PCLangSignature ;

proof end;

end;

registration

let X be set ;

cluster non empty non void strict for AlgLangSignature over X;

proof end;

end;

registration

cluster ordinal -> non pair for set ;

proof end;

end;

theorem :: AOFA_L00:10

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

registration

let R be non empty Relation;

cluster -> pair for Element of R;

end;

theorem Th11: :: AOFA_L00:11

for n being natural non empty number
for X being non empty set
for J being Signature ex S being non empty non void strict AlgLangSignature over X st
( S is n PC-correct & S is QC-correct & S is n AL-correct & S is J -extension & ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of S . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of S . (1,x) = [ the carrier' of J,1,x] & the quantifiers of S . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of S = sup the carrier of J & the program-sort of S = (sup the carrier of J) +^ 1 & the carrier of S = the carrier of J \/ { the formula-sort of S, the program-sort of S} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of S = ( the carrier' of J \/ {(w +^ 0),(w +^ 1),(w +^ 2),(w +^ 3),(w +^ 4),(w +^ 5),(w +^ 6),(w +^ 7),(w +^ 8)}) \/ [:{ the carrier' of J},{1,2},X:] ) )

proof end;

registration

let n be natural non empty number ;
let X be non empty set ;
let J be Signature;

cluster non empty non void feasible feasible J -extension strict n PC-correct QC-correct n AL-correct for AlgLangSignature over X;

proof end;

end;

registration

let X be non empty set ;
let n be natural non empty number ;

cluster non empty non void feasible feasible strict n PC-correct QC-correct n AL-correct for AlgLangSignature over X;

proof end;

end;

definition

let J be non empty non void Signature;
let T be MSAlgebra over J;

mode VariableSet of T -> set means :Def8: :: AOFA_L00:def 8
ex G being GeneratorSet of T st it = Union G;

proof end;

end;

:: deftheorem Def8 defines VariableSet AOFA_L00:def 8 :

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

end;

theorem :: AOFA_L00:12

for J being non empty non void Signature
for T being MSAlgebra over J
for X being VariableSet of T holds X c= Union the Sorts of T

proof end;

definition

let S be non empty non void Signature;
let X be ManySortedSet of the carrier of S;
let T be VarMSAlgebra over S;

attr T is X -vf-yielding means :: AOFA_L00:def 9
the free-vars of T is ManySortedMSSet of the Sorts of T,X;

end;

:: deftheorem defines -vf-yielding AOFA_L00:def 9 :

definition

let J be non empty set ;
let Q be ManySortedSet of J;
let Y be set ;
let f be Function of [:(Union Q),Y:],(Union Q);

attr f is sort-preserving means :Def10: :: AOFA_L00:def 10
for j being Element of J holds f .: [:(Q . j),Y:] c= Q . j;

end;

:: deftheorem Def10 defines sort-preserving AOFA_L00:def 10 :

registration

let J be non empty set ;
let Q be ManySortedSet of J;
let Y be set ;

cluster Relation-like [:(Union Q),Y:] -defined Union Q -valued Function-like quasi_total sort-preserving for Element of bool [:[:(Union Q),Y:],(Union Q):];

proof end;

end;

definition

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

end;

theorem Th13: :: AOFA_L00:13

for I being set
for X being ManySortedSet of I
for S being ManySortedSubset of X
for x being object holds S . x is Subset of (X . x)

proof end;

definition

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

func @ (x,Q) -> Element of Union the Sorts of Q equals :: AOFA_L00:def 11
x;

coherence by A2;

end;

:: deftheorem defines @ AOFA_L00:def 11 :

definition

let J be non empty non void Signature;
let X be V3() ManySortedSet of the carrier of J;
let Q be SubstMSAlgebra over J,X;
assume A1: X is ManySortedSubset of the Sorts of Q ;
let j be SortSymbol of J;
assume A2: the Sorts of Q . j <> {} ;
let A be Element of Q,j;
let x, y be Element of Union X;
given a being SortSymbol of J such that A3: ( x in X . a & y in X . a ) ;

func A / (x,y) -> Element of Q,j equals :Def12: :: AOFA_L00:def 12
the subst-op of Q . [A,[x,y]];

proof end;

end;

:: deftheorem Def12 defines / AOFA_L00:def 12 :

definition

let J be non empty non void Signature;
let X be V3() ManySortedSet of the carrier of J;
let Q be SubstMSAlgebra over J,X;
let j be SortSymbol of J;
let A be Element of Q,j;
assume A1: the Sorts of Q . j <> {} ;
let x be Element of Union X;
let t be Element of Union the Sorts of Q;
given a being SortSymbol of J such that A2: ( x in X . a & t in the Sorts of Q . a ) ;

func A / (x,t) -> Element of Q,j equals :Def13: :: AOFA_L00:def 13
the subst-op of Q . [A,[x,t]];

proof end;

end;

:: deftheorem Def13 defines / AOFA_L00:def 13 :

registration

let J be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of J;

cluster non-empty for SubstMSAlgebra over J,X;

proof end;

end;

definition

let J be non empty non void Signature;
let X be V3() ManySortedSet of the carrier of J;
let Q be non-empty SubstMSAlgebra over J,X;
let o be OperSymbol of J;
let p be Element of Args (o,Q);
let x be Element of Union X;
let y be Element of Union the Sorts of Q;

func p / (x,y) -> Element of Args (o,Q) means :Def14: :: AOFA_L00:def 14
for i being Nat st i in dom (the_arity_of o) holds
ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & it . i = A / (x,y) ) );

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines / AOFA_L00:def 14 :

definition

let I be non empty set ;
let X be V2() ManySortedSet of I;
let S be V2() ManySortedSubset of X;
let x be Element of I;
let z be Element of S . x;

func @ z -> Element of X . x equals :: AOFA_L00:def 15
z;

proof end;

end;

:: deftheorem defines @ AOFA_L00:def 15 :

definition

let J be non empty non void Signature;
let X be V3() ManySortedSet of the carrier of J;
let Q be non-empty SubstMSAlgebra over J,X;

attr Q is subst-correct means :: AOFA_L00:def 16
for x being Element of Union X
for a being SortSymbol of J st x in X . a holds
( ( for j being SortSymbol of J
for A being Element of Q,j holds A / (x,x) = A ) & ( for y being Element of Union the Sorts of Q st y in the Sorts of Q . a holds
for o being OperSymbol of J
for p being Element of Args (o,Q)
for A being Element of Q,(the_result_sort_of o) st A = (Den (o,Q)) . p & ( for S being QCLangSignature over Union X holds
( not J = S or for z being Element of Union X
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,Q)) . (p / (x,y)) ) );

attr Q is subst-correct2 means :: AOFA_L00:def 17
for j being SortSymbol of J
for q, t being Element of Q,j
for x being Element of Union X st t = x & x in X . j holds
t / (x,q) = q;

end;

:: deftheorem defines subst-correct AOFA_L00:def 16 :

:: deftheorem defines subst-correct2 AOFA_L00:def 17 :

theorem Th14: :: AOFA_L00:14

for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for a being SortSymbol of J st the Sorts of Q . a <> {} holds
for A being Element of Q,a
for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)

proof end;

registration

let J be non void Signature;

cluster feasible J -extension -> non empty non void for ManySortedSign ;

proof end;

end;

registration

let J be Signature;

cluster non empty non void feasible feasible J -extension for ManySortedSign ;

proof end;

let X be non empty set ;

cluster non empty non void feasible feasible J -extension for QCLangSignature over X;

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;

proof end;

end;

definition

let J be Signature;
let X be non empty set ;
let n be non empty Nat;
let S be feasible J -extension n PC-correct AlgLangSignature over X;

attr S is essential means :Def16: :: AOFA_L00:def 18
( the connectives of S .: ((n + 9) \ n) misses the carrier' of J & rng the quantifiers of S misses the carrier' of J & { the formula-sort of S, the program-sort of S} misses the carrier of J );

end;

:: deftheorem Def16 defines essential AOFA_L00:def 18 :

registration

let n be natural non empty number ;
let X be non empty set ;
let J be Signature;

cluster non empty non void feasible feasible J -extension strict n PC-correct QC-correct n AL-correct essential for AlgLangSignature over X;

proof end;

end;

registration

let J be non empty Signature;
let S be non empty J -extension Signature;
let X be V3() ManySortedSet of the carrier of J;

cluster Relation-like V3() the carrier of S -defined Function-like non empty total X -tolerating for set ;

proof end;

end;

definition

let J, S be non empty Signature;
let T be MSAlgebra over J;
let Q be MSAlgebra over S;

attr Q is T -extension means :Def17: :: AOFA_L00:def 19
Q | J = MSAlgebra(# the Sorts of T, the Charact of T #);

end;

:: deftheorem Def17 defines -extension AOFA_L00:def 19 :

theorem Th15: :: AOFA_L00:15

for J being non empty non void Signature
for S being b₁ -extension Signature
for T being MSAlgebra over J
for Q1, Q2 being MSAlgebra over S st MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) & Q1 is T -extension holds
Q2 is T -extension

proof end;

theorem Th16: :: AOFA_L00:16

for J being non empty non void Signature
for S being b₁ -extension Signature
for T being MSAlgebra over J
for Q being MSAlgebra over S st Q is T -extension holds
for x being object st x in the carrier of J holds
the Sorts of T . x = the Sorts of Q . x

proof end;

theorem Th17: :: AOFA_L00:17

for J being non empty non void Signature
for S being b₁ -extension Signature
for T being MSAlgebra over J
for I being set st I c= the carrier of S \ the carrier of J holds
for X being ManySortedSet of I ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )

proof end;

theorem Th18: :: AOFA_L00:18

for J being non empty non void Signature
for S being b₁ -extension Signature
for T being non-empty MSAlgebra over J
for I being set st I c= the carrier of S \ the carrier of J holds
for X being V2() ManySortedSet of I ex Q being non-empty MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )

proof end;

registration

let J be non empty non void Signature;
let S be J -extension Signature;
let T be MSAlgebra over J;

cluster T -extension for MSAlgebra over S;

proof end;

end;

registration

let J be non empty non void Signature;
let S be J -extension Signature;
let T be non-empty MSAlgebra over J;

cluster non-empty non empty T -extension for MSAlgebra over S;

proof end;

end;

theorem Th19: :: AOFA_L00:19

for I being set
for a being object holds pr1 (I,{a}) is one-to-one

proof end;

theorem Th20: :: AOFA_L00:20

for S1, S2, E1, E2 being Signature st ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) & ManySortedSign(# the carrier of E1, the carrier' of E1, the Arity of E1, the ResultSort of E1 #) = ManySortedSign(# the carrier of E2, the carrier' of E2, the Arity of E2, the ResultSort of E2 #) & E1 is Extension of S1 holds
E2 is Extension of S2

proof end;

registration

let I be set ;
let a be object ;

cluster pr1 (I,{a}) -> one-to-one ;

coherence by Th19;

end;

definition

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

proof end;

end;

theorem Lem6: :: AOFA_L00:21

for X, Y being set
for f being one-to-one Function st X misses Y holds
f .: X misses f .: Y

proof end;

theorem Th21: :: AOFA_L00:22

for n being natural non empty number
for X being set
for J being non empty Signature ex Q being non empty non void b₁ PC-correct QC-correct QCLangSignature over X st
( the carrier of Q misses the carrier of J & the carrier' of Q misses the carrier' of J )

proof end;

registration

let J be non empty Signature;

cluster non empty non void feasible feasible J -extension for ManySortedSign ;

proof end;

let X be set ;

cluster non empty non void feasible feasible J -extension for QCLangSignature over X;

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;

proof end;

end;

definition

let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;
let Y be X -tolerating ManySortedSet of the carrier of S;
attr c₆ 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₆ -> Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of c₆ . the formula-sort of S);

end;

definition

let S be non empty PCLangSignature ;
let L be MSAlgebra over S;

attr L is language means :Def18: :: AOFA_L00:def 20
not the Sorts of L . the formula-sort of S is empty ;

end;

:: deftheorem Def18 defines language AOFA_L00:def 20 :

registration

let S be non empty PCLangSignature ;

cluster non-empty -> language for MSAlgebra over S;

coherence ;

cluster language for MSAlgebra over S;

proof end;

end;

theorem Th22: :: AOFA_L00:23

for J being non void Signature
for S being non void b₁ -extension Signature
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
A1 | J = A2 | J

proof end;

registration

let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;

cluster Relation-like V3() the carrier of S -defined Function-like non empty total X -tolerating for set ;

proof end;

end;

registration

cluster non-empty T -extension language for LanguageStr over T,Y,S;

proof end;

end;

definition

attr L is subst-correct3 means :: AOFA_L00:def 21
for s, s1 being SortSymbol of S
for t being Element of L,s
for t1 being Element of L,s1
for y being Element of Union Y st y in Y . s holds
( y nin (vf t1) . s & ( y nin (vf t1) . s implies t1 / (y,t) = t1 ) & ( t1 = y & y in Y . s1 implies t1 / (y,t) = t ) & ( for x being Element of Union Y st x in Y . s holds
(t1 / (x,y)) / (y,x) = t1 ) );

end;

:: deftheorem defines subst-correct3 AOFA_L00:def 21 :

registration

let J be non empty Signature;
let S be non empty J -extension Signature;
let X be V3() ManySortedSet of the carrier of J;
let Y be set ;

cluster X extended_by (Y, the carrier of S) -> V3() ;

proof end;

end;

registration

let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension QCLangSignature over Union X;

cluster non-empty X extended_by ({}, the carrier of S) -vf-yielding T -extension language for LanguageStr over T,X extended_by ({}, the carrier of S),S;

proof end;

end;

registration

let X be set ;
let S be non empty QCLangSignature over X;
let L be language MSAlgebra over S;

cluster the Sorts of L . the formula-sort of S -> non empty ;

coherence by Def18;

end;

definition

end;

definition

let S be non empty PCLangSignature ;
let L be language MSAlgebra over S;
mode Formula of L is Element of the Sorts of L . the formula-sort of S;

end;

definition

let n be natural non empty number ;
let S be non empty non void n PC-correct PCLangSignature ;
let L be language MSAlgebra over S;
set f = the formula-sort of S;
A1: the Sorts of L . the formula-sort of S <> {} by Def18;
A2: the connectives of S . n is_of_type <* the formula-sort of S*>, the formula-sort of S by Def4;
A3: the connectives of S . (n + 5) is_of_type {} , the formula-sort of S by Def4;
A4: len the connectives of S >= n + 5 by Def4;
n + 1 <= n + 5 & ... & n + 5 <= n + 5 by XREAL_1:6;
then ( 1 <= n + 1 & n + 1 <= len the connectives of S ) & ... & ( 1 <= n + 5 & n + 5 <= len the connectives of S ) by A4, NAT_1:12, XXREAL_0:2;
then A5: n + 1 in dom the connectives of S & ... & n + 5 in dom the connectives of S by FINSEQ_3:25;
A6: the connectives of S . (n + 1) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & ... & the connectives of S . (n + 4) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S by Def4;
A7: ( the connectives of S . (n + 5) in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by A5, FUNCT_1:def 3;

func \true_ L -> Formula of L equals :: AOFA_L00:def 22
(Den ((In (( the connectives of S . (n + 5)), the carrier' of S)),L)) . {};

coherence 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 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 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 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 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 by A1, A6, AOFA_A00:33;

end;

:: deftheorem defines \true_ AOFA_L00:def 22 :

:: deftheorem defines \not AOFA_L00:def 23 :

:: deftheorem defines \and AOFA_L00:def 24 :

:: deftheorem defines \or AOFA_L00:def 25 :

:: deftheorem defines \imp AOFA_L00:def 26 :

:: deftheorem defines \iff AOFA_L00:def 27 :

registration

let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;

cluster non empty for VariableSet of T;

proof end;

end;

definition

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

func \for (x,A) -> Formula of L equals :: AOFA_L00:def 28
(Den ((In (( the quantifiers of S . (1,x)), the carrier' of S)),L)) . <*A*>;

coherence 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 by A4, AOFA_A00:32;

end;

:: deftheorem defines \for AOFA_L00:def 28 :

:: deftheorem defines \ex AOFA_L00:def 29 :

definition

func \for (x,y,A) -> Formula of L equals :: AOFA_L00:def 30
\for (x,(\for (y,A)));

func \ex (x,y,A) -> Formula of L equals :: AOFA_L00:def 31
\ex (x,(\ex (y,A)));

end;

:: deftheorem defines \for AOFA_L00:def 30 :

:: deftheorem defines \ex AOFA_L00:def 31 :

definition

func \for (x,y,z,A) -> Formula of L equals :: AOFA_L00:def 32
\for (x,y,(\for (z,A)));

func \ex (x,y,z,A) -> Formula of L equals :: AOFA_L00:def 33
\ex (x,y,(\ex (z,A)));

end;

:: deftheorem defines \for AOFA_L00:def 32 :

:: deftheorem defines \ex AOFA_L00:def 33 :

definition

func t1 '=' (t2,L) -> Formula of L equals :: AOFA_L00:def 34
the equality of L . (t1,t2);

proof end;

end;

:: deftheorem defines '=' AOFA_L00:def 34 :

definition

attr L is vf-qc-correct means :: AOFA_L00:def 35
for A, B being Formula of L holds
( vf (\not A) = vf A & vf (A \and B) = (vf A) (\/) (vf B) & vf (A \or B) = (vf A) (\/) (vf B) & vf (A \imp B) = (vf A) (\/) (vf B) & vf (A \iff B) = (vf A) (\/) (vf B) & vf (\true_ L) = EmptyMS the carrier of S & ( for x being Element of Union X
for a being SortSymbol of S st x in X . a holds
( vf (\for (x,A)) = (vf A) (\) (a -singleton x) & vf (\ex (x,A)) = (vf A) (\) (a -singleton x) ) ) );

end;

:: deftheorem defines vf-qc-correct AOFA_L00:def 35 :

definition

attr L is vf-finite means :: AOFA_L00:def 36
for s being SortSymbol of S
for t being Element of L,s holds vf t is V31();

end;

:: deftheorem defines vf-finite AOFA_L00:def 36 :

definition

attr L is subst-forex means :: AOFA_L00:def 37
for A being Formula of L
for x being Element of Union X
for s, s1 being SortSymbol of S
for t being Element of L,s st x in X . s1 holds
for y being Element of Union Y st y in Y . s holds
( ( x = y implies ( (\for (x,A)) / (y,t) = \for (x,A) & (\ex (x,A)) / (y,t) = \ex (x,A) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union Y st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf A) . s1) & (\for (x,A)) / (y,t) = \for (z,((A / (x0,z0)) / (y,t))) & (\ex (x,A)) / (y,t) = \ex (z,((A / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,A)) / (y,t) = \for (x,(A / (y,t))) & (\ex (x,A)) / (y,t) = \ex (x,(A / (y,t))) ) ) );

end;

:: deftheorem defines subst-forex AOFA_L00:def 37 :

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₁ -extension Signature
for Q being b₂ -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

proof end;

theorem Th24: :: AOFA_L00:25

for J being non void Signature
for T being MSAlgebra over J
for X being ManySortedSubset of the Sorts of T
for S being non void b₁ -extension Signature holds Union (X extended_by ({}, the carrier of S)) = Union X

proof end;

theorem Th25: :: AOFA_L00:26

for n being natural non empty number
for X being non empty set
for S being non empty non void b₁ PC-correct QC-correct QCLangSignature over X
for Q being language MSAlgebra over S holds
( {} in Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),Q) & ( for A being Formula of Q holds
( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) ) ) )

proof end;

theorem Th26: :: AOFA_L00:27

for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b₂ -extension b₁ PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b₄ -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S
for x being Element of Union Y
for t being Element of Union the Sorts of L
for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds
( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds
a / (x,t) = {} ) & ( for A being Formula of L holds
( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds
a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds
( ( for a being Element of Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),L) st <*A,B*> = a holds
a / (x,t) = <*(A / (x,t)),(B / (x,t))*> ) & ... & ( for a being Element of Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),L) st <*A,B*> = a holds
a / (x,t) = <*(A / (x,t)),(B / (x,t))*> ) & ( for z being Element of Union X holds
( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds
a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds
a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

proof end;

theorem Th27: :: AOFA_L00:28

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₆ is strict ;
struct BialgebraStr over S,Y -> LanguageStr over T,Y,S, ProgramAlgStr over J,T,X;
aggr BialgebraStr(# Sorts, Charact, free-vars, subst-op, equality, carrier, charact, assignments #) -> BialgebraStr over S,Y;

end;

registration

let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;

cluster non empty non void feasible feasible J -extension for AlgLangSignature over Union X;

proof end;

end;

definition

let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension AlgLangSignature over Union X;
let Y be X -tolerating ManySortedSet of the carrier of S;
let L be BialgebraStr over S,Y;

attr L is AL-correct means :Def34: :: AOFA_L00:def 38
the carrier of L = the Sorts of L . the program-sort of S;

end;

:: deftheorem Def34 defines AL-correct AOFA_L00:def 38 :

notation

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

end;

notation

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

end;

registration

cluster non 1s-empty strict for BialgebraStr over S,Y;

proof end;

end;

registration

let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void feasible J -extension n PC-correct essential AlgLangSignature over Union X;
let Y be X -tolerating ManySortedSet of the carrier of S;

cluster non 1s-empty partial quasi_total ua-non-empty non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction T -extension language strict AL-correct for BialgebraStr over S,Y;

proof end;

end;

theorem :: AOFA_L00:29

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

theorem Th29: :: AOFA_L00:30

for U1, U2 being preIfWhileAlgebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
ElementaryInstructions U1 = ElementaryInstructions U2

proof end;

theorem :: AOFA_L00:31

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

theorem Th31: :: AOFA_L00:32

proof end;

theorem Th32: :: AOFA_L00:33

for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
for G being GeneratorSet of U1 holds G is GeneratorSet of U2

proof end;

theorem Th33: :: AOFA_L00:34

for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
signature U1 = signature U2

proof end;

registration

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

proof end;

end;

definition

let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X;
mode IfWhileAlgebra of X,S is non 1s-empty partial quasi_total ua-non-empty non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction non degenerated well_founded ECIW-strict vf-correct subst-correct T -extension language vf-qc-correct subst-forex AL-correct BialgebraStr over S,X extended_by ({}, the carrier of S);

end;

definition

let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X;
let L be IfWhileAlgebra of X,S;
set f = the formula-sort of S;
set p = the program-sort of S;
A1: the connectives of S . (n + 6) is_of_type <* the program-sort of S, the formula-sort of S*>, the formula-sort of S & ... & the connectives of S . (n + 8) is_of_type <* the program-sort of S, the formula-sort of S*>, the formula-sort of S by Def6;
A2: the Sorts of L . the program-sort of S = the carrier of L by Def34;
let K be Formula of L;
let P be Algorithm of L;

func P * K -> Formula of L equals :: AOFA_L00:def 39
(Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),L)) . <*P,K*>;

coherence 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 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 by A1, A2, AOFA_A00:33;

end;

:: deftheorem defines * AOFA_L00:def 39 :

:: deftheorem defines \Cup AOFA_L00:def 40 :

:: deftheorem defines \Cap AOFA_L00:def 41 :

definition

let n be non empty Nat;
let S be non empty non void n PC-correct PCLangSignature ;
let L be language MSAlgebra over S;
let F be Subset of ( the Sorts of L . the formula-sort of S);

attr F is PC-closed means :Def38: :: AOFA_L00:def 42
for A, B, C being Formula of L holds
( A \imp (B \imp A) in F & (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) in F & ((\not A) \imp (\not B)) \imp (B \imp A) in F & A \imp (A \or B) in F & A \imp (B \or A) in F & (A \imp C) \imp ((B \imp C) \imp ((A \or B) \imp C)) in F & (A \and B) \imp A in F & (A \and B) \imp B in F & A \imp (B \imp (A \and B)) in F & (A \and (\not A)) \imp B in F & (A \imp B) \imp ((A \imp (\not B)) \imp (\not A)) in F & A \or (\not A) in F & (A \iff B) \imp (A \imp B) in F & (A \iff B) \imp (B \imp A) in F & ((A \imp B) \and (B \imp A)) \imp (A \iff B) in F & \true_ L in F & ((\true_ L) \and A) \iff A in F & ((\true_ L) \or A) \iff (\true_ L) in F & ( A in F & A \imp B in F implies B in F ) );

end;

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

definition

let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let L be non-empty Language of X extended_by ({}, the carrier of S),S;
let F be Subset of ( the Sorts of L . the formula-sort of S);

attr F is QC-closed means :Def39: :: AOFA_L00:def 43
for A, B being Element of the Sorts of L . the formula-sort of S
for x being Element of Union X holds
( ( for a being SortSymbol of J holds
( ( for t being Element of Union the Sorts of L st x in (X extended_by ({}, the carrier of S)) . a & t in the Sorts of L . a holds
for y being Element of Union (X extended_by ({}, the carrier of S)) st x = y holds
(\for (x,A)) \imp (A / (y,t)) in F ) & ( x in X . a & x nin (vf A) . a implies (\for (x,(A \imp B))) \imp (A \imp (\for (x,B))) in F ) ) ) & (\not (\ex (x,A))) \iff (\for (x,(\not A))) in F & (\ex (x,(\not A))) \iff (\not (\for (x,A))) in F & ( A in F implies \for (x,A) in F ) );

end;

:: deftheorem Def39 defines QC-closed AOFA_L00:def 43 :

definition

attr L is subst-eq-correct means :: AOFA_L00:def 44
for x0 being Element of Union (X extended_by ({}, the carrier of S))
for s, s1 being SortSymbol of S st x0 in X . s holds
for t being Element of L,s
for t1, t2 being Element of L,s1 holds (t1 '=' (t2,L)) / (x0,t) = (t1 / (x0,t)) '=' ((t2 / (x0,t)),L);

attr L is vf-eq-correct means :: AOFA_L00:def 45
for s being SortSymbol of S holds
( ( for t1, t2 being Element of L,s holds vf (t1 '=' (t2,L)) = (vf t1) (\/) (vf t2) ) & ( for s being SortSymbol of S
for t being Element of L,s st t in X . s holds
vf t = s -singleton t ) );

let F be Subset of ( the Sorts of L . the formula-sort of S);

attr F is with_equality means :Def42: :: AOFA_L00:def 46
( ( for t being Element of T holds t '=' (t,L) in F ) & ( for b being SortSymbol of S
for t1, t2 being Element of L,b
for x being Element of Union (X extended_by ({}, the carrier of S)) st x in X . b holds
( ( for c being SortSymbol of S st c in the carrier of J holds
for t being Element of L,c holds (t1 '=' (t2,L)) \imp ((t / (x,t1)) '=' ((t / (x,t2)),L)) in F ) & ( for A being Formula of L holds (t1 '=' (t2,L)) \imp ((A / (x,t1)) \imp (A / (x,t2))) in F ) ) ) );

end;

:: deftheorem defines subst-eq-correct AOFA_L00:def 44 :

:: deftheorem defines vf-eq-correct AOFA_L00:def 45 :

:: deftheorem Def42 defines with_equality AOFA_L00:def 46 :

definition

let n be natural non empty number ;
let J be non empty non void Signature;
let T be non-empty VarMSAlgebra over J;
let X be V2() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X;
let L be IfWhileAlgebra of X,S;
let V be Formula of L;
let F be Subset of ( the Sorts of L . the formula-sort of S);

attr F is V AL-closed means :Def43: :: AOFA_L00:def 47
for A, B being Formula of L holds
( ( for M being Algorithm of L holds
( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \iff ((M * A) \or (M * B)) in F & (\Cup (M,A)) \iff (A \or (\Cup (M,(M * A)))) in F & (\Cap (M,A)) \iff (A \and (\Cap (M,(M * A)))) in F & ( A \imp B in F implies ( (\Cup (M,A)) \imp (\Cup (M,B)) in F & (\Cap (M,A)) \imp (\Cap (M,B)) in F ) ) ) ) & ( for a being SortSymbol of J
for x being Element of X . a
for x0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 holds
for t being Element of the Sorts of T . a
for t1 being Element of Union the Sorts of L st t1 = t holds
( ((x := (t,L)) * A) \iff (A / (x0,t1)) in F & ( for y being Element of X . a st y nin (vf t) . a holds
for y0 being Element of Union (X extended_by ({}, the carrier of S)) st y = y0 holds
((x := (t,L)) * (\ex (x,A))) \iff (\ex (y,((x := (t,L)) * ((y := ((@ x),L)) * (A / (x0,y0)))))) in F ) & ((x := (t,L)) * A) \imp (\ex (x,A)) in F ) ) & ( for M, M1, M2 being Algorithm of L holds
( ((M \; M1) * A) \iff (M * (M1 * A)) in F & ((if-then-else (M,M1,M2)) * A) \iff (((M * V) \and (M * (M1 * A))) \or ((M * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) );

end;

:: deftheorem Def43 defines AL-closed AOFA_L00:def 47 :

registration

let n be non empty Nat;
let S be non empty non void n PC-correct PCLangSignature ;
let L be language MSAlgebra over S;

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

proof end;

cluster PC-closed -> non empty for Element of bool ( the Sorts of L . the formula-sort of S);

coherence ;

cluster PC-closed for Element of bool ( the Sorts of L . the formula-sort of S);

proof end;

end;

registration

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

proof end;

cluster PC-closed QC-closed for Element of bool ( the Sorts of L . the formula-sort of S);

proof end;

end;

registration

cluster [#] ( the Sorts of L . the formula-sort of S) -> with_equality ;

proof end;

cluster PC-closed QC-closed with_equality for Element of bool ( the Sorts of L . the formula-sort of S);

proof end;

end;

definition

let n be non empty Nat;
let S be non empty non void n PC-correct PCLangSignature ;
let L be language MSAlgebra over S;
mode PC-theory of L is PC-closed Subset of ( the Sorts of L . the formula-sort of S);

end;

definition

let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let L be non-empty Language of X extended_by ({}, the carrier of S),S;
mode QC-theory of L is PC-closed QC-closed Subset of ( the Sorts of L . the formula-sort of S);

end;

definition

let n be non empty Nat;
let J be non empty non void Signature;
let T be non-empty MSAlgebra over J;
let X be V3() GeneratorSet of T;
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X;
let L be non-empty Language of X extended_by ({}, the carrier of S),S;
mode QC-theory_with_equality of L is PC-closed QC-closed with_equality Subset of ( the Sorts of L . the formula-sort of S);

end;

registration

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