set W = the infinite IfWhileAlgebra of the generators of G;
set f = the Function of (Union [| the generators of G, the Sorts of T|]),(ElementaryInstructions the infinite IfWhileAlgebra of the generators of G);
reconsider f = the Function of (Union [| the generators of G, the Sorts of T|]),(ElementaryInstructions the infinite IfWhileAlgebra of the generators of G) as Function of (Union [| the generators of G, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra of the generators of G by FUNCT_2:7;
set A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #);
set X = the generators of G;
set J = S;
( ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is partial & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is quasi_total & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is non-empty & not ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is empty )
;
then reconsider A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) as non empty partial quasi_total non-empty strict ProgramAlgStr over S,T, the generators of G ;
( 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 empty partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction strict ProgramAlgStr over S,T, the generators of G ;
( not A is degenerated & A is well_founded & A is ECIW-strict & A is infinite )
proof
hereby AOFA_000:def 24 ( ( for b1, b2, b3 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = EmptyIns A ) & ( for b1, b2 being Element of the carrier of A holds not while (b1,b2) = EmptyIns A ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = if-then-else (b3,b4,b5) ) ) & ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict & A is infinite )
end;
hereby ( ( for b1, b2 being Element of the carrier of A holds not while (b1,b2) = EmptyIns A ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = if-then-else (b3,b4,b5) ) ) & ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict & A is infinite )
let C,
I1,
I2 be
Element of
A;
if-then-else (C,I1,I2) <> EmptyIns Areconsider C1 =
C,
J1 =
I1,
J2 =
I2 as
Element of the
infinite IfWhileAlgebra of the
generators of
G ;
(
if-then-else (
C,
I1,
I2)
= if-then-else (
C1,
J1,
J2) &
EmptyIns the
infinite IfWhileAlgebra of the
generators of
G = EmptyIns A )
;
hence
if-then-else (
C,
I1,
I2)
<> EmptyIns A
by AOFA_000:def 24;
verum
end;
hereby ( ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = if-then-else (b3,b4,b5) ) ) & ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict & A is infinite )
end;
hereby ( ( for b1, b2, b3, b4 being Element of the carrier of A holds
( b1 = EmptyIns A or b2 = EmptyIns A or not b1 \; b2 = while (b3,b4) ) ) & ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict & A is infinite )
let I1,
I2,
C,
J1,
J2 be
Element of
A;
( 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 of the
generators of
G ;
(
if-then-else (
C,
J1,
J2)
= if-then-else (
C1,
L1,
L2) &
I1 \; I2 = K1 \; K2 &
EmptyIns the
infinite IfWhileAlgebra of the
generators of
G = EmptyIns A )
;
hence
(
I1 = EmptyIns A or
I2 = EmptyIns A or
I1 \; I2 <> if-then-else (
C,
J1,
J2) )
by AOFA_000:def 24;
verum
end;
hereby ( ( for b1, b2, b3, b4, b5 being Element of the carrier of A holds not if-then-else (b1,b2,b3) = while (b4,b5) ) & A is well_founded & A is ECIW-strict & A is infinite )
let I1,
I2,
C,
J be
Element of
A;
( 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 of the
generators of
G ;
(
EmptyIns the
infinite IfWhileAlgebra of the
generators of
G = 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;
verum
end;
hereby ( A is well_founded & A is ECIW-strict & A is infinite )
let C1,
I1,
I2,
C2,
J be
Element of
A;
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 of the
generators of
G ;
(
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;
verum
end;
thus
A is
well_founded
( A is ECIW-strict & A is infinite )
UAStr(# the
carrier of
A, the
charact of
A #)
= UAStr(# the
carrier of the
infinite IfWhileAlgebra of the
generators of
G, the
charact of the
infinite IfWhileAlgebra of the
generators of
G #)
;
then
signature A = signature the
infinite IfWhileAlgebra of the
generators of
G
by AOFA_A00:47;
hence
signature A = ECIW-signature
by AOFA_000:def 27;
AOFA_000:def 27 A is infinite
UAStr(# the
carrier of
A, the
charact of
A #)
= UAStr(# the
carrier of the
infinite IfWhileAlgebra of the
generators of
G, the
charact of the
infinite IfWhileAlgebra of the
generators of
G #)
;
hence
ElementaryInstructions A is
infinite
by AOFA_A00:43;
AOFA_000:def 23 verum
end;
then reconsider A = A as infinite strict IfWhileAlgebra of the generators of G ;
take
A
; A is elementary
UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G #)
;
then
ElementaryInstructions A = ElementaryInstructions the infinite IfWhileAlgebra of the generators of G
by AOFA_A00:43;
hence
rng the assignments of A c= ElementaryInstructions A
by RELAT_1:def 19; AOFA_A01:def 13 verum