let S be non empty set ; :: thesis: for T being Subset of S
for A being free ECIW-strict preIfWhileAlgebra
for g being Function of [:S,(ElementaryInstructions A):],S
for F being Function of (Funcs S,S),(Funcs S,S) st ( for h being Element of Funcs S,S holds (F . h) * h = F . h ) holds
ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) ) )
let T be Subset of S; :: thesis: for A being free ECIW-strict preIfWhileAlgebra
for g being Function of [:S,(ElementaryInstructions A):],S
for F being Function of (Funcs S,S),(Funcs S,S) st ( for h being Element of Funcs S,S holds (F . h) * h = F . h ) holds
ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) ) )
let A be free ECIW-strict preIfWhileAlgebra; :: thesis: for g being Function of [:S,(ElementaryInstructions A):],S
for F being Function of (Funcs S,S),(Funcs S,S) st ( for h being Element of Funcs S,S holds (F . h) * h = F . h ) holds
ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) ) )
let g be Function of [:S,(ElementaryInstructions A):],S; :: thesis: for F being Function of (Funcs S,S),(Funcs S,S) st ( for h being Element of Funcs S,S holds (F . h) * h = F . h ) holds
ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) ) )
consider s0 being Element of S;
let F be Function of (Funcs S,S),(Funcs S,S); :: thesis: ( ( for h being Element of Funcs S,S holds (F . h) * h = F . h ) implies ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) ) ) )
assume A1: for h being Element of Funcs S,S holds (F . h) * h = F . h ; :: thesis: ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) ) )
set Z = Funcs S,S;
deffunc H₁( Element of A) -> set = (curry' g) . $1;
A2: for I being Element of A st I in ElementaryInstructions A holds
H₁(I) in Funcs S,S

proof

let I be Element of A; :: thesis: ( I in ElementaryInstructions A implies H₁(I) in Funcs S,S )
assume A3: I in ElementaryInstructions A ; :: thesis: H₁(I) in Funcs S,S
then reconsider B = ElementaryInstructions A as non empty set ;
reconsider I = I as Element of B by A3;
reconsider g = g as Function of [:S,B:],S ;
(curry' g) . I is Element of Funcs S,S ;
hence H₁(I) in Funcs S,S ; :: thesis: verum

end;

reconsider idS = id S as Element of Funcs S,S by ALTCAT_1:2;
deffunc H₂( Element of Funcs S,S, Element of Funcs S,S) -> Element of Funcs S,S = $2 * $1;
deffunc H₃( Element of Funcs S,S, Element of Funcs S,S, Element of Funcs S,S) -> Element of Funcs S,S = ($2,T +* $3) * $1;
deffunc H₄( Element of Funcs S,S, Element of Funcs S,S) -> Element of Funcs S,S = (T,(F . ($1 * $2)) iter ($1 * $2)) * $1;
consider h being Function of the carrier of A,(Funcs S,S) such that
A4: for I being Element of A st I in ElementaryInstructions A holds
h . I = H₁(I) and
A5: h . (EmptyIns A) = idS and
A6: for I1, I2 being Element of A holds h . (I1 \; I2) = H₂(h . I1,h . I2) and
A7: for C, I1, I2 being Element of A holds h . (if-then-else C,I1,I2) = H₃(h . C,h . I1,h . I2) and
A8: for C, I being Element of A holds h . (while C,I) = H₄(h . C,h . I) from AOFA_000:sch 7(A2);
h in Funcs the carrier of A,(Funcs S,S) by FUNCT_2:11;
then uncurry' h in Funcs [:S,the carrier of A:],S by FUNCT_6:20;
then reconsider f = uncurry' h as Function of [:S,the carrier of A:],S by FUNCT_2:121;
A9: dom h = the carrier of A by FUNCT_2:def 1;
A10: dom idS = S by FUNCT_2:def 1;
A11: f is complying_with_empty-instruction

proof

let s be Element of S; :: according to AOFA_000:def 28 :: thesis: f . s,(EmptyIns A) = s
idS . s = s by FUNCT_1:35;
hence f . s,(EmptyIns A) = s by A5, A9, A10, FUNCT_5:46; :: thesis: verum

end;

A12: f is complying_with_catenation

proof

let s be Element of S; :: according to AOFA_000:def 29 :: thesis: for I1, I2 being Element of A holds f . s,(I1 \; I2) = f . (f . s,I1),I2
let I1, I2 be Element of A; :: thesis: f . s,(I1 \; I2) = f . (f . s,I1),I2
A13: dom (h . (I1 \; I2)) = S by FUNCT_2:def 1;
A14: dom (h . I1) = S by FUNCT_2:def 1;
A15: dom (h . I2) = S by FUNCT_2:def 1;
thus f . s,(I1 \; I2) = (h . (I1 \; I2)) . s by A9, A13, FUNCT_5:46
.= ((h . I2) * (h . I1)) . s by A6
.= (h . I2) . ((h . I1) . s) by FUNCT_2:21
.= (h . I2) . (f . s,I1) by A9, A14, FUNCT_5:46
.= f . (f . s,I1),I2 by A9, A15, FUNCT_5:46 ; :: thesis: verum

end;

A16: f complies_with_if_wrt T

proof

let s be Element of S; :: according to AOFA_000:def 30 :: thesis: for C, I1, I2 being Element of A holds
( ( f . s,C in T implies f . s,(if-then-else C,I1,I2) = f . (f . s,C),I1 ) & ( f . s,C nin T implies f . s,(if-then-else C,I1,I2) = f . (f . s,C),I2 ) )
let C, I1, I2 be Element of A; :: thesis: ( ( f . s,C in T implies f . s,(if-then-else C,I1,I2) = f . (f . s,C),I1 ) & ( f . s,C nin T implies f . s,(if-then-else C,I1,I2) = f . (f . s,C),I2 ) )
A17: dom (h . (if-then-else C,I1,I2)) = S by FUNCT_2:def 1;
A18: dom (h . C) = S by FUNCT_2:def 1;
A19: dom (h . I1) = S by FUNCT_2:def 1;
A20: dom (h . I2) = S by FUNCT_2:def 1;
A21: f . s,(if-then-else C,I1,I2) = (h . (if-then-else C,I1,I2)) . s by A9, A17, FUNCT_5:46
.= H₃(h . C,h . I1,h . I2) . s by A7
.= ((h . I1),T +* (h . I2)) . ((h . C) . s) by FUNCT_2:21 ;
A22: f . s,C = (h . C) . s by A9, A18, FUNCT_5:46;

hereby :: thesis: ( f . s,C nin T implies f . s,(if-then-else C,I1,I2) = f . (f . s,C),I2 )

assume f . s,C in T ; :: thesis: f . s,(if-then-else C,I1,I2) = f . (f . s,C),I1
hence f . s,(if-then-else C,I1,I2) = (h . I1) . (f . s,C) by A19, A21, A22, Th4
.= f . (f . s,C),I1 by A9, A19, FUNCT_5:46 ;
:: thesis: verum

end;

assume f . s,C nin T ; :: thesis: f . s,(if-then-else C,I1,I2) = f . (f . s,C),I2
hence f . s,(if-then-else C,I1,I2) = (h . I2) . (f . s,C) by A20, A21, A22, Th5
.= f . (f . s,C),I2 by A9, A20, FUNCT_5:46 ;
:: thesis: verum

end;

f complies_with_while_wrt T

proof

let s be Element of S; :: according to AOFA_000:def 31 :: thesis: for C, I being Element of A holds
( ( f . s,C in T implies f . s,(while C,I) = f . (f . (f . s,C),I),(while C,I) ) & ( f . s,C nin T implies f . s,(while C,I) = f . s,C ) )
let C, I be Element of A; :: thesis: ( ( f . s,C in T implies f . s,(while C,I) = f . (f . (f . s,C),I),(while C,I) ) & ( f . s,C nin T implies f . s,(while C,I) = f . s,C ) )
A23: dom (h . (while C,I)) = S by FUNCT_2:def 1;
A24: dom (h . C) = S by FUNCT_2:def 1;
A25: dom (h . I) = S by FUNCT_2:def 1;
A26: dom ((h . C) * (h . I)) = S by FUNCT_2:def 1;
A27: f . s,(while C,I) = (h . (while C,I)) . s by A9, A23, FUNCT_5:46
.= H₄(h . C,h . I) . s by A8
.= (T,(F . ((h . C) * (h . I))) iter ((h . C) * (h . I))) . ((h . C) . s) by FUNCT_2:21 ;
A28: f . s,C = (h . C) . s by A9, A24, FUNCT_5:46;
A29: rng ((h . C) * (h . I)) c= S ;
A30: (F . ((h . C) * (h . I))) * ((h . C) * (h . I)) = F . ((h . C) * (h . I)) by A1;

hereby :: thesis: ( f . s,C nin T implies f . s,(while C,I) = f . s,C )

assume f . s,C in T ; :: thesis: f . s,(while C,I) = f . (f . (f . s,C),I),(while C,I)
hence f . s,(while C,I) = (T,(F . ((h . C) * (h . I))) iter ((h . C) * (h . I))) . (((h . C) * (h . I)) . (f . s,C)) by A26, A27, A28, A29, A30, Th11
.= (T,(F . ((h . C) * (h . I))) iter ((h . C) * (h . I))) . ((h . C) . ((h . I) . (f . s,C))) by FUNCT_2:21
.= ((T,(F . ((h . C) * (h . I))) iter ((h . C) * (h . I))) * (h . C)) . ((h . I) . (f . s,C)) by FUNCT_2:21
.= ((T,(F . ((h . C) * (h . I))) iter ((h . C) * (h . I))) * (h . C)) . (f . (f . s,C),I) by A9, A25, FUNCT_5:46
.= (h . (while C,I)) . (f . (f . s,C),I) by A8
.= f . (f . (f . s,C),I),(while C,I) by A9, A23, FUNCT_5:46 ;
:: thesis: verum

end;

thus ( f . s,C nin T implies f . s,(while C,I) = f . s,C ) by A26, A27, A28, A29, Th12; :: thesis: verum

end;

then reconsider f = f as ExecutionFunction of A,S,T by A11, A12, A16, Def32;
take f ; :: thesis: ( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) ) )
dom f = [:S,the carrier of A:] by FUNCT_2:def 1;
then A31: [:S,(ElementaryInstructions A):] c= dom f by ZFMISC_1:118;
A32: dom g = [:S,(ElementaryInstructions A):] by FUNCT_2:def 1;
A33: (dom f) /\ [:S,(ElementaryInstructions A):] = [:S,(ElementaryInstructions A):] by A31, XBOOLE_1:28;

now

let a be set ; :: thesis: ( a in dom g implies g . a = f . a )
assume A34: a in dom g ; :: thesis: g . a = f . a
then consider s, I being set such that
A35: s in S and
A36: I in ElementaryInstructions A and
A37: a = [s,I] by ZFMISC_1:def 2;
reconsider s = s as Element of S by A35;
reconsider I = I as Element of A by A36;
reconsider EI = (curry' g) . I as Element of Funcs S,S by A2, A36;
g in Funcs [:S,(ElementaryInstructions A):],S by FUNCT_2:11;
then curry' g in Funcs (ElementaryInstructions A),(Funcs S,S) by A34, FUNCT_6:19;
then A38: dom (curry' g) = ElementaryInstructions A by FUNCT_2:169;
A39: dom EI = S by FUNCT_2:169;
A40: dom (h . I) = S by FUNCT_2:169;
thus g . a = g . s,I by A37
.= EI . s by A36, A38, A39, FUNCT_5:41
.= (h . I) . s by A4, A36
.= f . s,I by A9, A40, FUNCT_5:46
.= f . a by A37 ; :: thesis: verum

end;

hence f | [:S,(ElementaryInstructions A):] = g by A32, A33, FUNCT_1:68; :: thesis: for C, I being Element of A
for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C)
let C, I be Element of A; :: thesis: for s being Element of S st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C)
let s be Element of S; :: thesis: ( not f iteration_terminates_for I \; C,f . s,C implies f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) )
assume A41: not f iteration_terminates_for I \; C,f . s,C ; :: thesis: f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C)
A42: dom (h . (while C,I)) = S by FUNCT_2:def 1;
A43: dom (h . C) = S by FUNCT_2:def 1;
A44: dom ((h . C) * (h . I)) = S by FUNCT_2:def 1;
A45: f . s,(while C,I) = (h . (while C,I)) . s by A9, A42, FUNCT_5:46
.= H₄(h . C,h . I) . s by A8
.= (T,(F . ((h . C) * (h . I))) iter ((h . C) * (h . I))) . ((h . C) . s) by FUNCT_2:21 ;
A46: f . s,C = (h . C) . s by A9, A43, FUNCT_5:46;
A47: rng ((h . C) * (h . I)) c= S ;
rng h c= Funcs S,S ;
then h = curry' f by FUNCT_5:55;
then A48: (curry' f) . (I \; C) = (h . C) * (h . I) by A6;
then ((h . C) * (h . I)) orbit (f . s,C) c= T by A41, Th87;
hence f . s,(while C,I) = (F . ((curry' f) . (I \; C))) . (f . s,C) by A44, A45, A46, A47, A48, Def7; :: thesis: verum