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_{1}( object , object , object ) -> set = {} ;

deffunc H_{2}( object ) -> object = n `1 ;

consider g being Function such that

A2: dom g = [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):] and

A3: for x being object st x in [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):] holds

g . x = H_{2}(x)
from FUNCT_1:sch 3();

rng g c= Union the Sorts of Q

g is sort-preserving

set a = the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra;

set f = the ManySortedMSSet of the Sorts of Q, the Sorts of Q;

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, the ManySortedMSSet of the Sorts of Q, the Sorts of Q,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, the ManySortedMSSet of the Sorts of Q, the Sorts of Q,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 strict BialgebraStr over S,Y ;

take A ; :: thesis: ( A is non-empty & A is language & A is AL-correct & 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 & A is T -extension )

thus the Sorts of A is V2() ; :: according to MSUALG_1:def 3 :: thesis: ( A is language & A is AL-correct & 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 & A is T -extension )

thus not the Sorts of A . the formula-sort of S is empty ; :: according to AOFA_L00:def 20 :: thesis: ( A is AL-correct & 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 & A is T -extension )

A8: 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, A8, FUNCT_1:49 ;

:: according to AOFA_L00:def 38 :: thesis: ( 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 & A is T -extension )

thus the charact of A is quasi_total ; :: according to UNIALG_1:def 2 :: thesis: ( 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 & A is T -extension )

thus the charact of A is homogeneous ; :: according to UNIALG_1:def 1 :: thesis: ( A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( the charact of A <> {} & the charact of A is non-empty ) ; :: according to UNIALG_1:def 3 :: thesis: ( A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( 1 in dom the charact of A & the charact of A . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 10; :: according to AOFA_000:def 10 :: thesis: ( A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( 2 in dom the charact of A & the charact of A . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 11; :: according to AOFA_000:def 11 :: thesis: ( A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( 3 in dom the charact of A & the charact of A . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 12; :: according to AOFA_000:def 12 :: thesis: ( A is with_while-instruction & A is T -extension )

thus ( 4 in dom the charact of A & the charact of A . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 13; :: according to AOFA_000:def 13 :: thesis: A is T -extension

MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of Q, the Charact of Q #) ;

hence A is T -extension by A1, Th15; :: thesis: verum

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

deffunc H

consider g being Function such that

A2: dom g = [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):] and

A3: for x being object st x in [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):] holds

g . x = H

rng g c= Union the Sorts of Q

proof

then reconsider g = g as Function of [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):],(Union the Sorts of Q) by A2, FUNCT_2:2;
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

A4: ( y in dom g & x = g . y ) by FUNCT_1:def 3;

consider y1, y2 being object such that

A5: ( y1 in Union the Sorts of Q & y2 in Union [|Y, the Sorts of Q|] & y = [y1,y2] ) by A2, A4, ZFMISC_1:def 2;

x = [y1,y2] `1 by A5, A2, A3, A4

.= y1 ;

hence x in Union the Sorts of Q by A5; :: thesis: verum

end;assume x in rng g ; :: thesis: x in Union the Sorts of Q

then consider y being object such that

A4: ( y in dom g & x = g . y ) by FUNCT_1:def 3;

consider y1, y2 being object such that

A5: ( y1 in Union the Sorts of Q & y2 in Union [|Y, the Sorts of Q|] & y = [y1,y2] ) by A2, A4, ZFMISC_1:def 2;

x = [y1,y2] `1 by A5, A2, A3, A4

.= y1 ;

hence x in Union the Sorts of Q by A5; :: thesis: verum

g is sort-preserving

proof

then reconsider g = g as sort-preserving Function of [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):],(Union the Sorts of Q) ;
let j be SortSymbol of S; :: according to AOFA_L00:def 10 :: thesis: g .: [:( the Sorts of Q . j),(Union [|Y, 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 [|Y, the Sorts of Q|]):] or x in the Sorts of Q . j )

assume x in g .: [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] ; :: thesis: x in the Sorts of Q . j

then consider y being object such that

A6: ( y in dom g & y in [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] & x = g . y ) by FUNCT_1:def 6;

consider a, b being object such that

A7: ( a in the Sorts of Q . j & b in Union [|Y, the Sorts of Q|] & y = [a,b] ) by A6, ZFMISC_1:def 2;

x = [a,b] `1 by A3, A6, A7

.= a ;

hence x in the Sorts of Q . j by A7; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] or x in the Sorts of Q . j )

assume x in g .: [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] ; :: thesis: x in the Sorts of Q . j

then consider y being object such that

A6: ( y in dom g & y in [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] & x = g . y ) by FUNCT_1:def 6;

consider a, b being object such that

A7: ( a in the Sorts of Q . j & b in Union [|Y, the Sorts of Q|] & y = [a,b] ) by A6, ZFMISC_1:def 2;

x = [a,b] `1 by A3, A6, A7

.= a ;

hence x in the Sorts of Q . j by A7; :: thesis: verum

set a = the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra;

set f = the ManySortedMSSet of the Sorts of Q, the Sorts of Q;

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, the ManySortedMSSet of the Sorts of Q, the Sorts of Q,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, the ManySortedMSSet of the Sorts of Q, the Sorts of Q,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 strict BialgebraStr over S,Y ;

take A ; :: thesis: ( A is non-empty & A is language & A is AL-correct & 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 & A is T -extension )

thus the Sorts of A is V2() ; :: according to MSUALG_1:def 3 :: thesis: ( A is language & A is AL-correct & 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 & A is T -extension )

thus not the Sorts of A . the formula-sort of S is empty ; :: according to AOFA_L00:def 20 :: thesis: ( A is AL-correct & 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 & A is T -extension )

A8: 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, A8, FUNCT_1:49 ;

:: according to AOFA_L00:def 38 :: thesis: ( 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 & A is T -extension )

thus the charact of A is quasi_total ; :: according to UNIALG_1:def 2 :: thesis: ( 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 & A is T -extension )

thus the charact of A is homogeneous ; :: according to UNIALG_1:def 1 :: thesis: ( A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( the charact of A <> {} & the charact of A is non-empty ) ; :: according to UNIALG_1:def 3 :: thesis: ( A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( 1 in dom the charact of A & the charact of A . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 10; :: according to AOFA_000:def 10 :: thesis: ( A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( 2 in dom the charact of A & the charact of A . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 11; :: according to AOFA_000:def 11 :: thesis: ( A is with_if-instruction & A is with_while-instruction & A is T -extension )

thus ( 3 in dom the charact of A & the charact of A . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 12; :: according to AOFA_000:def 12 :: thesis: ( A is with_while-instruction & A is T -extension )

thus ( 4 in dom the charact of A & the charact of A . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 13; :: according to AOFA_000:def 13 :: thesis: A is T -extension

MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of Q, the Charact of Q #) ;

hence A is T -extension by A1, Th15; :: thesis: verum