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 Def16, TARSKI:def 2;
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 Th18, ZFMISC_1:31;
set U2 = the Sorts of Q;
set C = the Charact of Q;
deffunc H₁( 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 H₁(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 = H₁(s,r,t) from AOFA_A00:sch 1(A2);
deffunc H₂( 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 = H₂(x) from FUNCT_1:sch 3();
rng g c= Union the Sorts of Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g ; :: thesis:
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 A4, A6, ZFMISC_1:def 2;
x = [y1,y2] `1 by A7, A4, A5, A6
.= y1 ;
hence x in Union the Sorts of Q by A7; :: thesis:

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 A4, FUNCT_2:2;
g is sort-preserving

proof

let j be SortSymbol of S; :: according to AOFA_L00:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in g .: [:( the Sorts of Q . j),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of Q|]):] ; :: thesis:
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 A8, ZFMISC_1:def 2;
x = [a,b] `1 by A5, A8, A9
.= a ;
hence x in the Sorts of Q . j by A9; :: thesis:

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:

end;

A16: now :: thesis:

let s be SortSymbol of S; :: thesis:
let B be Element of the Sorts of A . s; :: thesis:
let x be Element of Union (X extended_by ({}, the carrier of S)); :: thesis:
let y be Element of Union the Sorts of A; :: thesis:
let a be SortSymbol of S; :: thesis:
assume A17: ( x in (X extended_by ({}, the carrier of S)) . a & y in the Sorts of A . a ) ; :: thesis:
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 A18, A19, CARD_5:2;
thus B / (x,y) = g . [B,[x,y]] by A17, Def13
.= [B,[x,y]] `1 by A5, A20, ZFMISC_1:87
.= B ; :: thesis:

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 AOFA_000:def 10, AOFA_000:def 11, AOFA_000:def 12, AOFA_000:def 13;
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 A21, A1, Th15;
take A ; :: thesis:
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 A1, A22, FUNCT_1:49 ;
:: according to AOFA_L00:def 38 :: thesis:
thus A is vf-qc-correct :: thesis:

proof

let C, B be Formula of A; :: according to AOFA_L00:def 35 :: thesis:
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:
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:
thus vf (\true_ A) = EmptyMS the carrier of S by A3; :: thesis:
let x be Element of Union X; :: thesis:
let a be SortSymbol of S; :: thesis:
assume x in X . a ; :: thesis:
( 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) by A23, PBOOLE:60; :: thesis:

end;

thus A is vf-correct :: thesis:

proof

let o be OperSymbol of S; :: according to AOFA_A00:def 10 :: thesis:
let p be FinSequence; :: thesis:
assume p in Args (o,A) ; :: thesis:
let b be Element of A,(the_result_sort_of o); :: thesis:
assume b = (Den (o,A)) . p ; :: thesis:
let s be SortSymbol of S; :: thesis:
(vf b) . s = {} by A3;
hence (vf b) . s c= union { ((vf b₂) . s) where b₁ is Element of the carrier of S, b₂ is Element of the Sorts of A . b₁ : ex b₃ being set st
( b₃ in dom (the_arity_of o) & b₁ = (the_arity_of o) . b₃ & b₂ = p . b₃ ) } ; :: thesis:

end;

thus A is vf-finite :: thesis:

proof

let s be SortSymbol of S; :: according to AOFA_L00:def 36 :: thesis:
let t be Element of A,s; :: thesis:
let a be object ; :: according to FINSET_1:def 5 :: thesis:
assume a in the carrier of S ; :: thesis:
hence (vf t) . a is finite by A3; :: thesis:

end;

thus A is subst-correct :: thesis:

proof

let x be Element of Union (X extended_by ({}, the carrier of S)); :: according to AOFA_L00:def 16 :: thesis:
let a be SortSymbol of S; :: thesis:
assume A24: x in (X extended_by ({}, the carrier of S)) . a ; :: thesis:
thus for j being SortSymbol of S
for C being Element of A,j holds C / (x,x) = C by A24, A10; :: thesis:
let y be Element of Union the Sorts of A; :: thesis:
assume A25: y in the Sorts of A . a ; :: thesis:
let o be OperSymbol of S; :: thesis:
let p be Element of Args (o,A); :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume A26: i in dom (the_arity_of o) ; :: thesis:
take j = (the_arity_of o) /. i; :: thesis:
thus j = (the_arity_of o) . i by A26, PARTFUN1:def 6; :: thesis:
take B = In ((p . i),( the Sorts of A . j)); :: thesis:
thus B = p . i by A26, MSUALG_6:2, SUBSET_1:def 8; :: thesis:
hence p . i = B / (x,y) by A24, A25, A16; :: thesis:

end;

then A27: p / (x,y) = p by Def14;
let C be Element of A,(the_result_sort_of o); :: thesis:
assume A28: C = (Den (o,A)) . p ; :: thesis:
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:
thus C / (x,y) = (Den (o,A)) . (p / (x,y)) by A27, A28, A24, A25, A16; :: thesis:

end;

thus A is subst-forex :: thesis:

proof

let B be Formula of A; :: according to AOFA_L00:def 37 :: thesis:
let x be Element of Union X; :: thesis:
let s, s1 be SortSymbol of S; :: thesis:
let t be Element of A,s; :: thesis:
assume x in X . s1 ; :: thesis:
let y be Element of Union (X extended_by ({}, the carrier of S)); :: thesis:
assume C2: y in (X extended_by ({}, the carrier of S)) . s ; :: thesis:
thus ( x = y implies ( (\for (x,B)) / (y,t) = \for (x,B) & (\ex (x,B)) / (y,t) = \ex (x,B) ) ) by C2, A16; :: thesis:
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:
assume ( x <> y & x nin (vf t) . s ) ; :: thesis:
thus (\for (x,B)) / (y,t) = \for (x,B) by C2, A16
.= \for (x,(B / (y,t))) by C2, A16 ; :: thesis:
thus (\ex (x,B)) / (y,t) = \ex (x,B) by C2, A16
.= \ex (x,(B / (y,t))) by C2, A16 ; :: thesis:

end;

hereby :: according to AOFA_000:def 24 :: thesis:

let I1, I2 be Element of the carrier of A; :: thesis:
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:

end;

hereby :: thesis:

let C, I1, I2 be Element of the carrier of A; :: thesis:
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:

end;

hereby :: thesis:

let C, I be Element of the carrier of A; :: thesis:
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:

end;

hereby :: thesis:

let I1, I2, C, J1, J2 be Element of the carrier of A; :: thesis:
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:

end;

hereby :: thesis:

let I1, I2, C, J be Element of the carrier of A; :: thesis:
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:

end;

hereby :: thesis:

let C1, I1, I2, C2, J be Element of the carrier of A; :: thesis:
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:

end;

thus A is well_founded :: thesis:

proof

A29: UAStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra #) = UAStr(# the carrier of A, the charact of A #) ;
then ( ElementaryInstructions the IfWhileAlgebra = ElementaryInstructions A & ElementaryInstructions the IfWhileAlgebra is GeneratorSet of the IfWhileAlgebra ) by Th29, AOFA_000:def 25;
hence ElementaryInstructions A is GeneratorSet of A by A29, Th32; :: according to AOFA_000:def 25 :: thesis:

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: