set U = the infinite IfWhileAlgebra;

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

set A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #);

( ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) is partial & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) is quasi_total & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) is non-empty ) ;

then reconsider A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) as partial quasi_total non-empty strict ProgramAlgStr over J,T,X ;

( 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 partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction strict ProgramAlgStr over J,T,X ;

take A ; :: thesis: ( not A is degenerated & A is well_founded & A is ECIW-strict & A is infinite )

set W = the infinite IfWhileAlgebra;

then signature A = signature the infinite IfWhileAlgebra by Th42;

hence signature A = ECIW-signature by AOFA_000:def 27; :: according to AOFA_000:def 27 :: thesis: A is infinite

UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra #) ;

then ElementaryInstructions A = ElementaryInstructions the infinite IfWhileAlgebra by Th38;

hence ElementaryInstructions A is infinite ; :: according to AOFA_000:def 23 :: thesis: verum

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

set A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #);

( ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) is partial & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) is quasi_total & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) is non-empty ) ;

then reconsider A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra #) as partial quasi_total non-empty strict ProgramAlgStr over J,T,X ;

( 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 partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction strict ProgramAlgStr over J,T,X ;

take A ; :: thesis: ( not A is degenerated & A is well_founded & A is ECIW-strict & A is infinite )

set W = the infinite IfWhileAlgebra;

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 & A is infinite )

( b

( b

let I1, I2 be Element 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 infinite IfWhileAlgebra ;

( EmptyIns A = EmptyIns the infinite 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 infinite IfWhileAlgebra ;

( EmptyIns A = EmptyIns the infinite 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 & A is infinite )

( b

( b

let C, I1, I2 be Element of A; :: thesis: if-then-else (C,I1,I2) <> EmptyIns A

reconsider C1 = C, J1 = I1, J2 = I2 as Element of the infinite IfWhileAlgebra ;

( if-then-else (C,I1,I2) = if-then-else (C1,J1,J2) & EmptyIns the infinite 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 infinite IfWhileAlgebra ;

( if-then-else (C,I1,I2) = if-then-else (C1,J1,J2) & EmptyIns the infinite 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 & A is infinite )

( b

( b

let C, I be Element of A; :: thesis: while (C,I) <> EmptyIns A

reconsider C1 = C, J = I as Element of the infinite IfWhileAlgebra ;

( EmptyIns A = EmptyIns the infinite 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 infinite IfWhileAlgebra ;

( EmptyIns A = EmptyIns the infinite 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 & A is infinite )

( b

let I1, I2, C, J1, J2 be Element 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 infinite IfWhileAlgebra ;

( if-then-else (C,J1,J2) = if-then-else (C1,L1,L2) & I1 \; I2 = K1 \; K2 & EmptyIns the infinite 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 infinite IfWhileAlgebra ;

( if-then-else (C,J1,J2) = if-then-else (C1,L1,L2) & I1 \; I2 = K1 \; K2 & EmptyIns the infinite 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 & A is infinite )

let I1, I2, C, J be Element 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 infinite IfWhileAlgebra ;

( EmptyIns the infinite 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 infinite IfWhileAlgebra ;

( EmptyIns the infinite 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 & A is infinite )

thus
A is well_founded
:: thesis: ( A is ECIW-strict & A is infinite )let C1, I1, I2, C2, J be Element 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 infinite 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 infinite 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 infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra #)
;
A1:
UAStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra #) = UAStr(# the carrier of A, the charact of A #)
;

then ( ElementaryInstructions the infinite IfWhileAlgebra = ElementaryInstructions A & ElementaryInstructions the infinite IfWhileAlgebra is GeneratorSet of the infinite IfWhileAlgebra ) by Th38, AOFA_000:def 25;

hence ElementaryInstructions A is GeneratorSet of A by A1, Th41; :: according to AOFA_000:def 25 :: thesis: verum

end;then ( ElementaryInstructions the infinite IfWhileAlgebra = ElementaryInstructions A & ElementaryInstructions the infinite IfWhileAlgebra is GeneratorSet of the infinite IfWhileAlgebra ) by Th38, AOFA_000:def 25;

hence ElementaryInstructions A is GeneratorSet of A by A1, Th41; :: according to AOFA_000:def 25 :: thesis: verum

then signature A = signature the infinite IfWhileAlgebra by Th42;

hence signature A = ECIW-signature by AOFA_000:def 27; :: according to AOFA_000:def 27 :: thesis: A is infinite

UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the infinite IfWhileAlgebra, the charact of the infinite IfWhileAlgebra #) ;

then ElementaryInstructions A = ElementaryInstructions the infinite IfWhileAlgebra by Th38;

hence ElementaryInstructions A is infinite ; :: according to AOFA_000:def 23 :: thesis: verum