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_{1}( 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_{1}(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_{1}(s,r,t)
from AOFA_A00:sch 1(A2);

deffunc H_{2}( 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_{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 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) ;

( 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: ( 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 A1, A22, FUNCT_1:49 ;

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

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

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

A2: for s, r being Element of the carrier of S

for t being Element of the Sorts of Q . s holds H

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

deffunc H

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

rng g c= Union the Sorts of Q

proof

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

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

g is sort-preserving

proof

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

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

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

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 A1, Th23;

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 A11, ZFMISC_1:87;

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 A13, A14, CARD_5:2;

thus B / (x,y) = g . [B,[x,y]] by A12, A11, Def12

.= [B,[x,y]] `1 by A5, A15, ZFMISC_1:87

.= B ; :: thesis: verum

end;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 A1, Th23;

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 A11, ZFMISC_1:87;

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 A13, A14, CARD_5:2;

thus B / (x,y) = g . [B,[x,y]] by A12, A11, Def12

.= [B,[x,y]] `1 by A5, A15, ZFMISC_1:87

.= B ; :: thesis: verum

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

A21:
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of Q, the Charact of Q #)
;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 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: verum

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

( 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: ( 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 A1, A22, FUNCT_1:49 ;

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

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 )
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 (\true_ A) = 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) ) )

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 (\true_ A) = 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) ) )

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 (\true_ A) = 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) ) )

thus vf (\true_ A) = 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) )

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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) )

let a be SortSymbol of S; :: thesis: ( x in X . a implies ( vf (\for (x,C)) = (vf C) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) )

assume x in X . a ; :: thesis: ( vf (\for (x,C)) = (vf C) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) )

( 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: verum

end;for a being SortSymbol of S st x in X . a holds

( vf (\for (x,C)) = (vf C) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) ) )

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 (\true_ A) = 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) ) )

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 (\true_ A) = 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) ) )

thus vf (\true_ A) = 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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) )

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) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) )

let a be SortSymbol of S; :: thesis: ( x in X . a implies ( vf (\for (x,C)) = (vf C) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) ) )

assume x in X . a ; :: thesis: ( vf (\for (x,C)) = (vf C) (\) (a -singleton x) & vf (\ex (x,C)) = (vf C) (\) (a -singleton x) )

( 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: verum

proof

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 )
let o be OperSymbol of S; :: according to AOFA_A00:def 10 :: thesis: for b_{1} being set holds

( not b_{1} in Args (o,A) or for b_{2} being Element of the Sorts of A . (the_result_sort_of o) holds

( not b_{2} = (Den (o,A)) . b_{1} or for b_{3} being Element of the carrier of S holds (vf b_{2}) . b_{3} c= union { ((vf b_{5}) . b_{3}) where b_{4} is Element of the carrier of S, b_{5} is Element of the Sorts of A . b_{4} : ex b_{6} being set st

( b_{6} in dom (the_arity_of o) & b_{4} = (the_arity_of o) . b_{6} & b_{5} = b_{1} . b_{6} ) } ) )

let p be FinSequence; :: thesis: ( not p in Args (o,A) or for b_{1} being Element of the Sorts of A . (the_result_sort_of o) holds

( not b_{1} = (Den (o,A)) . p or for b_{2} being Element of the carrier of S holds (vf b_{1}) . b_{2} c= union { ((vf b_{4}) . b_{2}) where b_{3} is Element of the carrier of S, b_{4} is Element of the Sorts of A . b_{3} : ex b_{5} being set st

( b_{5} in dom (the_arity_of o) & b_{3} = (the_arity_of o) . b_{5} & b_{4} = p . b_{5} ) } ) )

assume p in Args (o,A) ; :: thesis: for b_{1} being Element of the Sorts of A . (the_result_sort_of o) holds

( not b_{1} = (Den (o,A)) . p or for b_{2} being Element of the carrier of S holds (vf b_{1}) . b_{2} c= union { ((vf b_{4}) . b_{2}) where b_{3} is Element of the carrier of S, b_{4} is Element of the Sorts of A . b_{3} : ex b_{5} being set st

( b_{5} in dom (the_arity_of o) & b_{3} = (the_arity_of o) . b_{5} & b_{4} = p . b_{5} ) } )

let b be Element of A,(the_result_sort_of o); :: thesis: ( not b = (Den (o,A)) . p or for b_{1} being Element of the carrier of S holds (vf b) . b_{1} c= union { ((vf b_{3}) . b_{1}) where b_{2} is Element of the carrier of S, b_{3} is Element of the Sorts of A . b_{2} : ex b_{4} being set st

( b_{4} in dom (the_arity_of o) & b_{2} = (the_arity_of o) . b_{4} & b_{3} = p . b_{4} ) } )

assume b = (Den (o,A)) . p ; :: thesis: for b_{1} being Element of the carrier of S holds (vf b) . b_{1} c= union { ((vf b_{3}) . b_{1}) where b_{2} is Element of the carrier of S, b_{3} is Element of the Sorts of A . b_{2} : ex b_{4} being set st

( b_{4} in dom (the_arity_of o) & b_{2} = (the_arity_of o) . b_{4} & b_{3} = p . b_{4} ) }

let s be SortSymbol of S; :: thesis: (vf b) . s c= union { ((vf b_{2}) . s) where b_{1} is Element of the carrier of S, b_{2} is Element of the Sorts of A . b_{1} : ex b_{3} being set st

( b_{3} in dom (the_arity_of o) & b_{1} = (the_arity_of o) . b_{3} & b_{2} = p . b_{3} ) }

(vf b) . s = {} by A3;

hence (vf b) . s c= union { ((vf b_{2}) . s) where b_{1} is Element of the carrier of S, b_{2} is Element of the Sorts of A . b_{1} : ex b_{3} being set st

( b_{3} in dom (the_arity_of o) & b_{1} = (the_arity_of o) . b_{3} & b_{2} = p . b_{3} ) }
; :: thesis: verum

end;( not b

( not b

( b

let p be FinSequence; :: thesis: ( not p in Args (o,A) or for b

( not b

( b

assume p in Args (o,A) ; :: thesis: for b

( not b

( b

let b be Element of A,(the_result_sort_of o); :: thesis: ( not b = (Den (o,A)) . p or for b

( b

assume b = (Den (o,A)) . p ; :: thesis: for b

( b

let s be SortSymbol of S; :: thesis: (vf b) . s c= union { ((vf b

( b

(vf b) . s = {} by A3;

hence (vf b) . s c= union { ((vf b

( b

proof

thus
A is subst-correct
:: thesis: ( A is subst-forex & not A is degenerated & A is well_founded & A is ECIW-strict )
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;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

proof

thus
A is subst-forex
:: thesis: ( not A is degenerated & A is well_founded & A is ECIW-strict )
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,(the_result_sort_of o) 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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)) ) )

for p being Element of Args (o,A)

for A being Element of A,(the_result_sort_of o) 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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 C be Element of A,(the_result_sort_of o); :: 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;( ( 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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 y be Element of Union the Sorts of A; :: thesis: ( y in the Sorts of A . a implies for o being OperSymbol of Sfor o being OperSymbol of S

for p being Element of Args (o,A)

for A being Element of A,(the_result_sort_of o) 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 A24, A10; :: thesis: verum

end;let C be Element of A,j; :: thesis: C / (x,x) = C

thus C / (x,x) = C by A24, A10; :: thesis: verum

for p being Element of Args (o,A)

for A being Element of A,(the_result_sort_of o) 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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,(the_result_sort_of o) 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 (the_arity_of o) holds

ex j being Element of the carrier of S st

( j = (the_arity_of o) . i & ex B being Element of the Sorts of A . j st

( B = p . i & p . i = B / (x,y) ) )

then A27:
p / (x,y) = p
by Def14;ex j being Element of the carrier of S st

( j = (the_arity_of o) . 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 (the_arity_of o) implies ex j being Element of the carrier of S st

( j = (the_arity_of o) . 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 (the_arity_of o) ; :: thesis: ex j being Element of the carrier of S st

( j = (the_arity_of o) . i & ex B being Element of the Sorts of A . j st

( B = p . i & p . i = B / (x,y) ) )

take j = (the_arity_of o) /. i; :: thesis: ( j = (the_arity_of o) . i & ex B being Element of the Sorts of A . j st

( B = p . i & p . i = B / (x,y) ) )

thus j = (the_arity_of o) . i by A26, PARTFUN1:def 6; :: 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 A26, MSUALG_6:2, SUBSET_1:def 8; :: thesis: p . i = B / (x,y)

hence p . i = B / (x,y) by A24, A25, A16; :: thesis: verum

end;( j = (the_arity_of o) . 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 (the_arity_of o) ; :: thesis: ex j being Element of the carrier of S st

( j = (the_arity_of o) . i & ex B being Element of the Sorts of A . j st

( B = p . i & p . i = B / (x,y) ) )

take j = (the_arity_of o) /. i; :: thesis: ( j = (the_arity_of o) . i & ex B being Element of the Sorts of A . j st

( B = p . i & p . i = B / (x,y) ) )

thus j = (the_arity_of o) . i by A26, PARTFUN1:def 6; :: 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 A26, MSUALG_6:2, SUBSET_1:def 8; :: thesis: p . i = B / (x,y)

hence p . i = B / (x,y) by A24, A25, A16; :: thesis: verum

let C be Element of A,(the_result_sort_of o); :: 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

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 C2, A16; :: 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 C2, A16

.= \for (x,(B / (y,t))) by C2, A16 ; :: thesis: (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t)))

thus (\ex (x,B)) / (y,t) = \ex (x,B) by C2, A16

.= \ex (x,(B / (y,t))) by C2, A16 ; :: thesis: verum

end;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 C2, A16; :: 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 C2, A16

.= \for (x,(B / (y,t))) by C2, A16 ; :: thesis: (\ex (x,B)) / (y,t) = \ex (x,(B / (y,t)))

thus (\ex (x,B)) / (y,t) = \ex (x,B) by C2, A16

.= \ex (x,(B / (y,t))) by C2, A16 ; :: thesis: verum

hereby :: according to AOFA_000:def 24 :: thesis: ( ( for b_{1}, b_{2}, b_{3} being Element of the carrier of A holds not if-then-else (b_{1},b_{2},b_{3}) = EmptyIns A ) & ( for b_{1}, b_{2} being Element of the carrier of A holds not while (b_{1},b_{2}) = EmptyIns A ) & ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds

( b_{1} = EmptyIns A or b_{2} = EmptyIns A or not b_{1} \; b_{2} = if-then-else (b_{3},b_{4},b_{5}) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being Element of the carrier of A holds

( b_{1} = EmptyIns A or b_{2} = EmptyIns A or not b_{1} \; b_{2} = while (b_{3},b_{4}) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds not if-then-else (b_{1},b_{2},b_{3}) = while (b_{4},b_{5}) ) & A is well_founded & A is ECIW-strict )

( b

( b

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

hereby :: thesis: ( ( for b_{1}, b_{2} being Element of the carrier of A holds not while (b_{1},b_{2}) = EmptyIns A ) & ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds

( b_{1} = EmptyIns A or b_{2} = EmptyIns A or not b_{1} \; b_{2} = if-then-else (b_{3},b_{4},b_{5}) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being Element of the carrier of A holds

( b_{1} = EmptyIns A or b_{2} = EmptyIns A or not b_{1} \; b_{2} = while (b_{3},b_{4}) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds not if-then-else (b_{1},b_{2},b_{3}) = while (b_{4},b_{5}) ) & A is well_founded & A is ECIW-strict )

( b

( b

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

hereby :: thesis: ( ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds

( b_{1} = EmptyIns A or b_{2} = EmptyIns A or not b_{1} \; b_{2} = if-then-else (b_{3},b_{4},b_{5}) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being Element of the carrier of A holds

( b_{1} = EmptyIns A or b_{2} = EmptyIns A or not b_{1} \; b_{2} = while (b_{3},b_{4}) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds not if-then-else (b_{1},b_{2},b_{3}) = while (b_{4},b_{5}) ) & A is well_founded & A is ECIW-strict )

( b

( b

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

hereby :: thesis: ( ( for b_{1}, b_{2}, b_{3}, b_{4} being Element of the carrier of A holds

( b_{1} = EmptyIns A or b_{2} = EmptyIns A or not b_{1} \; b_{2} = while (b_{3},b_{4}) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds not if-then-else (b_{1},b_{2},b_{3}) = while (b_{4},b_{5}) ) & A is well_founded & A is ECIW-strict )

( b

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

hereby :: thesis: ( ( for b_{1}, b_{2}, b_{3}, b_{4}, b_{5} being Element of the carrier of A holds not if-then-else (b_{1},b_{2},b_{3}) = while (b_{4},b_{5}) ) & 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;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

hereby :: thesis: ( A is well_founded & A is ECIW-strict )

thus
A is well_founded
:: thesis: 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;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

proof

UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra #)
;
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: verum

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

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