set Y = X extended_by ({}, the carrier of S);
set W = the IfWhileAlgebra;
set I = { the program-sort of S};
set p = the program-sort of S;
set f = the formula-sort of S;
( the program-sort of S in { the formula-sort of S, the program-sort of S} & { the formula-sort of S, the program-sort of S} misses the carrier of J ) by ;
then the program-sort of S nin the carrier of J by XBOOLE_0:3;
then the program-sort of S in the carrier of S \ the carrier of J by XBOOLE_0:def 5;
then consider Q being non-empty MSAlgebra over S such that
A1: ( Q is T -extension & the Sorts of Q | { the program-sort of S} = { the program-sort of S} --> the carrier of the IfWhileAlgebra ) by ;
set U2 = the Sorts of Q;
set C = the Charact of Q;
deffunc H1( object , object , object ) -> set = {} ;
A2: for s, r being Element of the carrier of S
for t being Element of the Sorts of Q . s holds H1(s,r,t) is Subset of ( the Sorts of Q . r) by XBOOLE_1:2;
consider f being ManySortedMSSet of the Sorts of Q, the Sorts of Q such that
A3: for s, r being Element of the carrier of S
for t being Element of the Sorts of Q . s holds ((f . s) . t) . r = H1(s,r,t) from deffunc H2( object ) -> object = n `1 ;
consider g being Function such that
A4: dom g = [:(Union the Sorts of Q),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):] and
A5: for x being object st x in [:(Union the Sorts of Q),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):] holds
g . x = H2(x) from rng g c= Union the Sorts of Q
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in Union the Sorts of Q )
assume x in rng g ; :: thesis: x in Union the Sorts of Q
then consider y being object such that
A6: ( y in dom g & x = g . y ) by FUNCT_1:def 3;
consider y1, y2 being object such that
A7: ( y1 in Union the Sorts of Q & y2 in Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|] & y = [y1,y2] ) by ;
x = [y1,y2] `1 by A7, A4, A5, A6
.= y1 ;
hence x in Union the Sorts of Q by A7; :: thesis: verum
end;
then reconsider g = g as Function of [:(Union the Sorts of Q),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):],(Union the Sorts of Q) by ;
g is sort-preserving
proof
let j be SortSymbol of S; :: according to AOFA_L00:def 10 :: thesis: g .: [:( the Sorts of Q . j),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):] c= the Sorts of Q . j
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: [:( the Sorts of Q . j),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):] or x in the Sorts of Q . j )
assume x in g .: [:( the Sorts of Q . j),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):] ; :: thesis: x in the Sorts of Q . j
then consider y being object such that
A8: ( y in dom g & y in [:( the Sorts of Q . j),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):] & x = g . y ) by FUNCT_1:def 6;
consider a, b being object such that
A9: ( a in the Sorts of Q . j & b in Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|] & y = [a,b] ) by ;
x = [a,b] `1 by A5, A8, A9
.= a ;
hence x in the Sorts of Q . j by A9; :: thesis: verum
end;
then reconsider g = g as sort-preserving Function of [:(Union the Sorts of Q),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):],(Union the Sorts of Q) ;
set a = the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra;
set eq = the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of Q . the formula-sort of S);
set A = BialgebraStr(# the Sorts of Q, the Charact of Q,f,g, the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of Q . the formula-sort of S), the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #);
reconsider A = BialgebraStr(# the Sorts of Q, the Charact of Q,f,g, the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of Q . the formula-sort of S), the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) as non 1s-empty BialgebraStr over S,X extended_by ({}, the carrier of S) ;
A is language ;
then reconsider A = A as non 1s-empty language BialgebraStr over S,X extended_by ({}, the carrier of S) ;
A10: now :: thesis: for s being SortSymbol of S
for B being Element of the Sorts of A . s
for x, y being Element of Union (X extended_by ({}, the carrier of S))
for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in (X extended_by ({}, the carrier of S)) . a holds
B / (x,y) = B
let s be SortSymbol of S; :: thesis: for B being Element of the Sorts of A . s
for x, y being Element of Union (X extended_by ({}, the carrier of S))
for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in (X extended_by ({}, the carrier of S)) . a holds
B / (x,y) = B

let B be Element of the Sorts of A . s; :: thesis: for x, y being Element of Union (X extended_by ({}, the carrier of S))
for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in (X extended_by ({}, the carrier of S)) . a holds
B / (x,y) = B

let x, y be Element of Union (X extended_by ({}, the carrier of S)); :: thesis: for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in (X extended_by ({}, the carrier of S)) . a holds
B / (x,y) = B

let a be SortSymbol of S; :: thesis: ( x in (X extended_by ({}, the carrier of S)) . a & y in (X extended_by ({}, the carrier of S)) . a implies B / (x,y) = B )
assume A11: ( x in (X extended_by ({}, the carrier of S)) . a & y in (X extended_by ({}, the carrier of S)) . a ) ; :: thesis: B / (x,y) = B
A12: X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q by ;
then (X extended_by ({}, the carrier of S)) . a is Subset of ( the Sorts of A . a) by Th13;
then A13: [x,y] in [:((X extended_by ({}, the carrier of S)) . a),( the Sorts of A . a):] by ;
A14: [|(X extended_by ({}, the carrier of S)), the Sorts of A|] . a = [:((X extended_by ({}, the carrier of S)) . a),( the Sorts of A . a):] by PBOOLE:def 16;
( dom the Sorts of Q = the carrier of S & dom [|(X extended_by ({}, the carrier of S)), the Sorts of A|] = the carrier of S ) by PARTFUN1:def 2;
then A15: ( B in Union the Sorts of Q & [x,y] in Union [|(X extended_by ({}, the carrier of S)), the Sorts of A|] ) by ;
thus B / (x,y) = g . [B,[x,y]] by
.= [B,[x,y]] `1 by
.= B ; :: thesis: verum
end;
A16: now :: thesis: for s being SortSymbol of S
for B being Element of the Sorts of A . s
for x being Element of Union (X extended_by ({}, the carrier of S))
for y being Element of Union the Sorts of A
for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a holds
B / (x,y) = B
let s be SortSymbol of S; :: thesis: for B being Element of the Sorts of A . s
for x being Element of Union (X extended_by ({}, the carrier of S))
for y being Element of Union the Sorts of A
for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a holds
B / (x,y) = B

let B be Element of the Sorts of A . s; :: thesis: for x being Element of Union (X extended_by ({}, the carrier of S))
for y being Element of Union the Sorts of A
for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a holds
B / (x,y) = B

let x be Element of Union (X extended_by ({}, the carrier of S)); :: thesis: for y being Element of Union the Sorts of A
for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a holds
B / (x,y) = B

let y be Element of Union the Sorts of A; :: thesis: for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a holds
B / (x,y) = B

let a be SortSymbol of S; :: thesis: ( x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a implies B / (x,y) = B )
assume A17: ( x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a ) ; :: thesis: B / (x,y) = B
then A18: [x,y] in [:((X extended_by ({}, the carrier of S)) . a),( the Sorts of A . a):] by ZFMISC_1:87;
A19: [|(X extended_by ({}, the carrier of S)), the Sorts of A|] . a = [:((X extended_by ({}, the carrier of S)) . a),( the Sorts of A . a):] by PBOOLE:def 16;
( dom the Sorts of Q = the carrier of S & dom [|(X extended_by ({}, the carrier of S)), the Sorts of A|] = the carrier of S ) by PARTFUN1:def 2;
then A20: ( B in Union the Sorts of Q & [x,y] in Union [|(X extended_by ({}, the carrier of S)), the Sorts of A|] ) by ;
thus B / (x,y) = g . [B,[x,y]] by
.= [B,[x,y]] `1 by
.= B ; :: thesis: verum
end;
A21: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of Q, the Charact of Q #) ;
( A is non-empty & A is quasi_total & A is partial & A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction ) by ;
then reconsider A = A as 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) by ;
take A ; :: thesis: ( A is AL-correct & A is vf-qc-correct & A is vf-correct & A is vf-finite & A is subst-correct & A is subst-forex & not A is degenerated & A is well_founded & A is ECIW-strict )
A22: the program-sort of S in { the program-sort of S} by TARSKI:def 1;
hence the carrier of A = ({ the program-sort of S} --> the carrier of the IfWhileAlgebra) . the program-sort of S by FUNCOP_1:7
.= the Sorts of A . the program-sort of S by ;
:: according to AOFA_L00:def 38 :: thesis: ( A is vf-qc-correct & A is vf-correct & A is vf-finite & A is subst-correct & A is subst-forex & not A is degenerated & A is well_founded & A is ECIW-strict )
thus A is vf-qc-correct :: thesis: ( A is vf-correct & A is vf-finite & A is subst-correct & A is subst-forex & not A is degenerated & A is well_founded & A is ECIW-strict )
proof
let C, B be Formula of A; :: according to AOFA_L00:def 35 :: thesis: ( vf (\not C) = vf C & vf (C \and B) = (vf C) (\/) (vf B) & vf (C \or B) = (vf C) (\/) (vf B) & vf (C \imp B) = (vf C) (\/) (vf B) & vf (C \iff B) = (vf C) (\/) (vf B) & vf () = 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,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () ) ) )

A23: ( vf C = EmptyMS the carrier of S & vf B = EmptyMS the carrier of S & vf (\not C) = EmptyMS the carrier of S & vf (C \and B) = EmptyMS the carrier of S & vf (C \or B) = EmptyMS the carrier of S & vf (C \imp B) = EmptyMS the carrier of S & vf (C \iff B) = EmptyMS the carrier of S ) by A3;
thus ( vf (\not C) = vf C & vf (C \and B) = (vf C) (\/) (vf B) ) by A23; :: thesis: ( vf (C \or B) = (vf C) (\/) (vf B) & vf (C \imp B) = (vf C) (\/) (vf B) & vf (C \iff B) = (vf C) (\/) (vf B) & vf () = 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,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () ) ) )

thus ( vf (C \or B) = (vf C) (\/) (vf B) & vf (C \imp B) = (vf C) (\/) (vf B) & vf (C \iff B) = (vf C) (\/) (vf B) ) by A23; :: thesis: ( vf () = 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,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () ) ) )

thus vf () = EmptyMS the carrier of S by A3; :: thesis: for x being Element of Union X
for a being SortSymbol of S st x in X . a holds
( vf (\for (x,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () )

let x be Element of Union X; :: thesis: for a being SortSymbol of S st x in X . a holds
( vf (\for (x,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () )

let a be SortSymbol of S; :: thesis: ( x in X . a implies ( vf (\for (x,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () ) )
assume x in X . a ; :: thesis: ( vf (\for (x,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () )
( vf (\for (x,C)) = EmptyMS the carrier of S & vf (\ex (x,C)) = EmptyMS the carrier of S ) by A3;
hence ( vf (\for (x,C)) = (vf C) (\) () & vf (\ex (x,C)) = (vf C) (\) () ) by ; :: thesis: verum
end;
thus A is vf-correct :: thesis: ( A is vf-finite & A is subst-correct & A is subst-forex & not A is degenerated & A is well_founded & A is ECIW-strict )
proof
let o be OperSymbol of S; :: according to AOFA_A00:def 10 :: thesis: for b1 being set holds
( not b1 in Args (o,A) or for b2 being Element of the Sorts of A . holds
( not b2 = (Den (o,A)) . b1 or for b3 being Element of the carrier of S holds (vf b2) . b3 c= union { ((vf b5) . b3) where b4 is Element of the carrier of S, b5 is Element of the Sorts of A . b4 : ex b6 being set st
( b6 in dom () & b4 = () . b6 & b5 = b1 . b6 )
}
) )

let p be FinSequence; :: thesis: ( not p in Args (o,A) or for b1 being Element of the Sorts of A . holds
( not b1 = (Den (o,A)) . p or for b2 being Element of the carrier of S holds (vf b1) . b2 c= union { ((vf b4) . b2) where b3 is Element of the carrier of S, b4 is Element of the Sorts of A . b3 : ex b5 being set st
( b5 in dom () & b3 = () . b5 & b4 = p . b5 )
}
) )

assume p in Args (o,A) ; :: thesis: for b1 being Element of the Sorts of A . holds
( not b1 = (Den (o,A)) . p or for b2 being Element of the carrier of S holds (vf b1) . b2 c= union { ((vf b4) . b2) where b3 is Element of the carrier of S, b4 is Element of the Sorts of A . b3 : ex b5 being set st
( b5 in dom () & b3 = () . b5 & b4 = p . b5 )
}
)

let b be Element of A,; :: thesis: ( not b = (Den (o,A)) . p or for b1 being Element of the carrier of S holds (vf b) . b1 c= union { ((vf b3) . b1) where b2 is Element of the carrier of S, b3 is Element of the Sorts of A . b2 : ex b4 being set st
( b4 in dom () & b2 = () . b4 & b3 = p . b4 )
}
)

assume b = (Den (o,A)) . p ; :: thesis: for b1 being Element of the carrier of S holds (vf b) . b1 c= union { ((vf b3) . b1) where b2 is Element of the carrier of S, b3 is Element of the Sorts of A . b2 : ex b4 being set st
( b4 in dom () & b2 = () . b4 & b3 = p . b4 )
}

let s be SortSymbol of S; :: thesis: (vf b) . s c= union { ((vf b2) . s) where b1 is Element of the carrier of S, b2 is Element of the Sorts of A . b1 : ex b3 being set st
( b3 in dom () & b1 = () . b3 & b2 = p . b3 )
}

(vf b) . s = {} by A3;
hence (vf b) . s c= union { ((vf b2) . s) where b1 is Element of the carrier of S, b2 is Element of the Sorts of A . b1 : ex b3 being set st
( b3 in dom () & b1 = () . b3 & b2 = p . b3 )
}
; :: thesis: verum
end;
thus A is vf-finite :: thesis: ( A is subst-correct & A is subst-forex & not A is degenerated & A is well_founded & A is ECIW-strict )
proof
let s be SortSymbol of S; :: according to AOFA_L00:def 36 :: thesis: for t being Element of A,s holds vf t is V31()
let t be Element of A,s; :: thesis: vf t is V31()
let a be object ; :: according to FINSET_1:def 5 :: thesis: ( not a in the carrier of S or (vf t) . a is finite )
assume a in the carrier of S ; :: thesis: (vf t) . a is finite
hence (vf t) . a is finite by A3; :: thesis: verum
end;
thus A is subst-correct :: thesis: ( A is subst-forex & not A is degenerated & A is well_founded & A is ECIW-strict )
proof
let x be Element of Union (X extended_by ({}, the carrier of S)); :: according to AOFA_L00:def 16 :: thesis: for a being SortSymbol of S st x in (X extended_by ({}, the carrier of S)) . a holds
( ( for j being SortSymbol of S
for A being Element of A,j holds A / (x,x) = A ) & ( for y being Element of Union the Sorts of A st y in the Sorts of A . a holds
for o being OperSymbol of S
for p being Element of Args (o,A)
for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y)) ) )

let a be SortSymbol of S; :: thesis: ( x in (X extended_by ({}, the carrier of S)) . a implies ( ( for j being SortSymbol of S
for A being Element of A,j holds A / (x,x) = A ) & ( for y being Element of Union the Sorts of A st y in the Sorts of A . a holds
for o being OperSymbol of S
for p being Element of Args (o,A)
for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y)) ) ) )

assume A24: x in (X extended_by ({}, the carrier of S)) . a ; :: thesis: ( ( for j being SortSymbol of S
for A being Element of A,j holds A / (x,x) = A ) & ( for y being Element of Union the Sorts of A st y in the Sorts of A . a holds
for o being OperSymbol of S
for p being Element of Args (o,A)
for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y)) ) )

hereby :: thesis: for y being Element of Union the Sorts of A st y in the Sorts of A . a holds
for o being OperSymbol of S
for p being Element of Args (o,A)
for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y))
let j be SortSymbol of S; :: thesis: for C being Element of A,j holds C / (x,x) = C
let C be Element of A,j; :: thesis: C / (x,x) = C
thus C / (x,x) = C by ; :: thesis: verum
end;
let y be Element of Union the Sorts of A; :: thesis: ( y in the Sorts of A . a implies for o being OperSymbol of S
for p being Element of Args (o,A)
for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y)) )

assume A25: y in the Sorts of A . a ; :: thesis: for o being OperSymbol of S
for p being Element of Args (o,A)
for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y))

let o be OperSymbol of S; :: thesis: for p being Element of Args (o,A)
for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y))

let p be Element of Args (o,A); :: thesis: for A being Element of A, st A = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,A)) . (p / (x,y))

now :: thesis: for i being Nat st i in dom () holds
ex j being Element of the carrier of S st
( j = () . i & ex B being Element of the Sorts of A . j st
( B = p . i & p . i = B / (x,y) ) )
let i be Nat; :: thesis: ( i in dom () implies ex j being Element of the carrier of S st
( j = () . i & ex B being Element of the Sorts of A . j st
( B = p . i & p . i = B / (x,y) ) ) )

assume A26: i in dom () ; :: thesis: ex j being Element of the carrier of S st
( j = () . i & ex B being Element of the Sorts of A . j st
( B = p . i & p . i = B / (x,y) ) )

take j = () /. i; :: thesis: ( j = () . i & ex B being Element of the Sorts of A . j st
( B = p . i & p . i = B / (x,y) ) )

thus j = () . i by ; :: thesis: ex B being Element of the Sorts of A . j st
( B = p . i & p . i = B / (x,y) )

take B = In ((p . i),( the Sorts of A . j)); :: thesis: ( B = p . i & p . i = B / (x,y) )
thus B = p . i by ; :: thesis: p . i = B / (x,y)
hence p . i = B / (x,y) by ; :: thesis: verum
end;
then A27: p / (x,y) = p by Def14;
let C be Element of A,; :: thesis: ( C = (Den (o,A)) . p & ( for S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) implies C / (x,y) = (Den (o,A)) . (p / (x,y)) )

assume A28: C = (Den (o,A)) . p ; :: thesis: ( ex S being QCLangSignature over Union (X extended_by ({}, the carrier of S)) st
( S = S & ex z being Element of Union (X extended_by ({}, the carrier of S)) ex q being Element of {1,2} st o = the quantifiers of S . (q,z) ) or C / (x,y) = (Den (o,A)) . (p / (x,y)) )

assume for S1 being QCLangSignature over Union (X extended_by ({}, the carrier of S)) holds
( not S = S1 or for z being Element of Union (X extended_by ({}, the carrier of S))
for q being Element of {1,2} holds not o = the quantifiers of S1 . (q,z) ) ; :: thesis: C / (x,y) = (Den (o,A)) . (p / (x,y))
thus C / (x,y) = (Den (o,A)) . (p / (x,y)) by A27, A28, A24, A25, A16; :: thesis: verum
end;
thus A is subst-forex :: thesis: ( not A is degenerated & A is well_founded & A is ECIW-strict )
proof
let B be Formula of A; :: according to AOFA_L00:def 37 :: thesis: for x being Element of Union X
for s, s1 being SortSymbol of S
for t being Element of A,s st x in X . s1 holds
for y being Element of Union (X extended_by ({}, the carrier of S)) st y in (X extended_by ({}, the carrier of S)) . s holds
( ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) )

let x be Element of Union X; :: thesis: for s, s1 being SortSymbol of S
for t being Element of A,s st x in X . s1 holds
for y being Element of Union (X extended_by ({}, the carrier of S)) st y in (X extended_by ({}, the carrier of S)) . s holds
( ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) )

let s, s1 be SortSymbol of S; :: thesis: for t being Element of A,s st x in X . s1 holds
for y being Element of Union (X extended_by ({}, the carrier of S)) st y in (X extended_by ({}, the carrier of S)) . s holds
( ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) )

let t be Element of A,s; :: thesis: ( x in X . s1 implies for y being Element of Union (X extended_by ({}, the carrier of S)) st y in (X extended_by ({}, the carrier of S)) . s holds
( ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) ) )

assume x in X . s1 ; :: thesis: for y being Element of Union (X extended_by ({}, the carrier of S)) st y in (X extended_by ({}, the carrier of S)) . s holds
( ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) )

let y be Element of Union (X extended_by ({}, the carrier of S)); :: thesis: ( y in (X extended_by ({}, the carrier of S)) . s implies ( ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) ) )

assume C2: y in (X extended_by ({}, the carrier of S)) . s ; :: thesis: ( ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) )

thus ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) by ; :: thesis: ( ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) ) )

thus ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union (X extended_by ({}, the carrier of S)) st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf B) . s1) & (\for (x,B)) / (y,t) = \for (z,((B / (x0,z0)) / (y,t))) & (\ex (x,B)) / (y,t) = \ex (z,((B / (x0,z0)) / (y,t))) ) ) by A3; :: thesis: ( x <> y & x nin (vf t) . s implies ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) ) )
assume ( x <> y & x nin (vf t) . s ) ; :: thesis: ( (\for (x,B)) / (y,t) = \for (x,(B / (y,t))) & (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t))) )
thus (\for (x,B)) / (y,t) = \for (x,B) by
.= \for (x,(B / (y,t))) by ; :: thesis: (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t)))
thus (\ex (x,B)) / (y,t) = \ex (x,B) by
.= \ex (x,(B / (y,t))) by ; :: thesis: verum
end;
hereby :: according to AOFA_000:def 24 :: thesis: ( ( for b1, b2, b3 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = EmptyIns A ) & ( for b1, b2 being Element of the carrier of A holds not while (b1,b2) = EmptyIns A ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = if-then-else (b3,b4,b5) ) ) & ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict )
let I1, I2 be Element of the carrier of A; :: thesis: ( ( I1 <> EmptyIns A implies I1 \; I2 <> I2 ) & ( I2 <> EmptyIns A implies I1 \; I2 <> I1 ) & ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) implies I1 \; I2 <> EmptyIns A ) )
reconsider J1 = I1, J2 = I2 as Element of the IfWhileAlgebra ;
( EmptyIns A = EmptyIns the IfWhileAlgebra & I1 \; I2 = J1 \; J2 ) ;
hence ( ( I1 <> EmptyIns A implies I1 \; I2 <> I2 ) & ( I2 <> EmptyIns A implies I1 \; I2 <> I1 ) & ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) implies I1 \; I2 <> EmptyIns A ) ) by AOFA_000:def 24; :: thesis: verum
end;
hereby :: thesis: ( ( for b1, b2 being Element of the carrier of A holds not while (b1,b2) = EmptyIns A ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = if-then-else (b3,b4,b5) ) ) & ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict )
let C, I1, I2 be Element of the carrier of A; :: thesis: if-then-else (C,I1,I2) <> EmptyIns A
reconsider C1 = C, J1 = I1, J2 = I2 as Element of the IfWhileAlgebra ;
( if-then-else (C,I1,I2) = if-then-else (C1,J1,J2) & EmptyIns the IfWhileAlgebra = EmptyIns A ) ;
hence if-then-else (C,I1,I2) <> EmptyIns A by AOFA_000:def 24; :: thesis: verum
end;
hereby :: thesis: ( ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = if-then-else (b3,b4,b5) ) ) & ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict )
let C, I be Element of the carrier of A; :: thesis: while (C,I) <> EmptyIns A
reconsider C1 = C, J = I as Element of the IfWhileAlgebra ;
( EmptyIns A = EmptyIns the IfWhileAlgebra & while (C,I) = while (C1,J) ) ;
hence while (C,I) <> EmptyIns A by AOFA_000:def 24; :: thesis: verum
end;
hereby :: thesis: ( ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict )
let I1, I2, C, J1, J2 be Element of the carrier of A; :: thesis: ( I1 = EmptyIns A or I2 = EmptyIns A or I1 \; I2 <> if-then-else (C,J1,J2) )
reconsider C1 = C, K1 = I1, K2 = I2, L1 = J1, L2 = J2 as Element of the IfWhileAlgebra ;
( if-then-else (C,J1,J2) = if-then-else (C1,L1,L2) & I1 \; I2 = K1 \; K2 & EmptyIns the IfWhileAlgebra = EmptyIns A ) ;
hence ( I1 = EmptyIns A or I2 = EmptyIns A or I1 \; I2 <> if-then-else (C,J1,J2) ) by AOFA_000:def 24; :: thesis: verum
end;
hereby :: thesis: ( ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict )
let I1, I2, C, J be Element of the carrier of A; :: thesis: ( I1 <> EmptyIns A & I2 <> EmptyIns A implies I1 \; I2 <> while (C,J) )
reconsider C1 = C, K1 = I1, K2 = I2, L = J as Element of the IfWhileAlgebra ;
( EmptyIns the IfWhileAlgebra = EmptyIns A & I1 \; I2 = K1 \; K2 & while (C,J) = while (C1,L) ) ;
hence ( I1 <> EmptyIns A & I2 <> EmptyIns A implies I1 \; I2 <> while (C,J) ) by AOFA_000:def 24; :: thesis: verum
end;
hereby :: thesis: ( A is well_founded & A is ECIW-strict )
let C1, I1, I2, C2, J be Element of the carrier of A; :: thesis: if-then-else (C1,I1,I2) <> while (C2,J)
reconsider C3 = C1, K1 = I1, K2 = I2, C4 = C2, L = J as Element of the IfWhileAlgebra ;
( while (C2,J) = while (C4,L) & if-then-else (C1,I1,I2) = if-then-else (C3,K1,K2) ) ;
hence if-then-else (C1,I1,I2) <> while (C2,J) by AOFA_000:def 24; :: thesis: verum
end;
thus A is well_founded :: thesis: A is ECIW-strict
proof end;
UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra #) ;
then signature A = signature the IfWhileAlgebra by Th33;
hence signature A = ECIW-signature by AOFA_000:def 27; :: according to AOFA_000:def 27 :: thesis: verum