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 s0 being Element of S ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0 ) )
let T be Subset of S; :: thesis: for A being free ECIW-strict preIfWhileAlgebra
for g being Function of [:S,(ElementaryInstructions A):],S
for s0 being Element of S ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0 ) )
let A be free ECIW-strict preIfWhileAlgebra; :: thesis: for g being Function of [:S,(ElementaryInstructions A):],S
for s0 being Element of S ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0 ) )
let g be Function of [:S,(ElementaryInstructions A):],S; :: thesis: for s0 being Element of S ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0 ) )
let s0 be Element of S; :: thesis: ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0 ) )
reconsider Ss0 = S --> s0 as Element of Funcs (S,S) by FUNCT_2:9;
set Z = Funcs (S,S);
deffunc H1( Element of A) -> set = (curry' g) . $1;
A1: for I being Element of A st I in ElementaryInstructions A holds
H1(I) in Funcs (S,S)
proof
let I be Element of A; :: thesis: ( I in ElementaryInstructions A implies H1(I) in Funcs (S,S) )
assume A2: I in ElementaryInstructions A ; :: thesis: H1(I) in Funcs (S,S)
then reconsider B = ElementaryInstructions A as non empty set ;
reconsider I = I as Element of B by A2;
reconsider g = g as Function of [:S,B:],S ;
(curry' g) . I is Element of Funcs (S,S) ;
hence H1(I) in Funcs (S,S) ; :: thesis: verum
end;
reconsider idS = id S as Element of Funcs (S,S) by FUNCT_2:126;
deffunc H2( Element of Funcs (S,S), Element of Funcs (S,S)) -> Element of Funcs (S,S) = $2 * $1;
deffunc H3( 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 H4( Element of Funcs (S,S), Element of Funcs (S,S)) -> Element of Funcs (S,S) = ((T,Ss0) iter ($1 * $2)) * $1;
consider h being Function of the carrier of A,(Funcs (S,S)) such that
A3: for I being Element of A st I in ElementaryInstructions A holds
h . I = H1(I) and
A4: h . (EmptyIns A) = idS and
A5: for I1, I2 being Element of A holds h . (I1 \; I2) = H2(h . I1,h . I2) and
A6: for C, I1, I2 being Element of A holds h . (if-then-else (C,I1,I2)) = H3(h . C,h . I1,h . I2) and
A7: for C, I being Element of A holds h . (while (C,I)) = H4(h . C,h . I) from AOFA_000:sch 7(A1);
 h in Funcs ( the carrier of A,(Funcs (S,S))) by FUNCT_2:8;
then uncurry' h in Funcs ([:S, the carrier of A:],S) by FUNCT_6:11;
then reconsider f = uncurry' h as Function of [:S, the carrier of A:],S by FUNCT_2:66;
A8: dom h = the carrier of A by FUNCT_2:def 1;
A9: 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 ;
hence f . (s,(EmptyIns A)) = s by A4, A8, FUNCT_5:39; :: thesis: verum
end;
A10: 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)
A11: dom (h . (I1 \; I2)) = S by FUNCT_2:def 1;
A12: dom (h . I1) = S by FUNCT_2:def 1;
A13: dom (h . I2) = S by FUNCT_2:def 1;
thus f . (s,(I1 \; I2)) = (h . (I1 \; I2)) . s by A8, A11, FUNCT_5:39
.= ((h . I2) * (h . I1)) . s by A5
.= (h . I2) . ((h . I1) . s) by FUNCT_2:15
.= (h . I2) . (f . (s,I1)) by A8, A12, FUNCT_5:39
.= f . ((f . (s,I1)),I2) by A8, A13, FUNCT_5:39 ; :: thesis: verum
end;
A14: 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) ) )
A15: dom (h . (if-then-else (C,I1,I2))) = S by FUNCT_2:def 1;
A16: dom (h . C) = S by FUNCT_2:def 1;
A17: dom (h . I1) = S by FUNCT_2:def 1;
A18: dom (h . I2) = S by FUNCT_2:def 1;
A19: f . (s,(if-then-else (C,I1,I2))) = (h . (if-then-else (C,I1,I2))) . s by A8, A15, FUNCT_5:39
.= H3(h . C,h . I1,h . I2) . s by A6
.= (((h . I1),T) +* (h . I2)) . ((h . C) . s) by FUNCT_2:15 ;
A20: f . (s,C) = (h . C) . s by A8, A16, FUNCT_5:39;
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 A17, A19, A20, Th4
.= f . ((f . (s,C)),I1) by A8, A17, FUNCT_5:39 ;
:: 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 A18, A19, A20, Th5
.= f . ((f . (s,C)),I2) by A8, A18, FUNCT_5:39 ;
:: 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) ) )
A21: dom (h . (while (C,I))) = S by FUNCT_2:def 1;
A22: dom (h . C) = S by FUNCT_2:def 1;
A23: dom (h . I) = S by FUNCT_2:def 1;
A24: dom ((h . C) * (h . I)) = S by FUNCT_2:def 1;
A25: f . (s,(while (C,I))) = (h . (while (C,I))) . s by A8, A21, FUNCT_5:39
.= H4(h . C,h . I) . s by A7
.= ((T,Ss0) iter ((h . C) * (h . I))) . ((h . C) . s) by FUNCT_2:15 ;
A26: f . (s,C) = (h . C) . s by A8, A22, FUNCT_5:39;
A27: rng ((h . C) * (h . I)) c= S ;
A28: now :: thesis: for z being Element of S holds (Ss0 * ((h . C) * (h . I))) . z = Ss0 . z
let z be Element of S; :: thesis: (Ss0 * ((h . C) * (h . I))) . z = Ss0 . z
thus (Ss0 * ((h . C) * (h . I))) . z = Ss0 . (((h . C) * (h . I)) . z) by FUNCT_2:15
.= s0 by FUNCOP_1:7
.= Ss0 . z by FUNCOP_1:7 ; :: thesis: verum
end;
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,Ss0) iter ((h . C) * (h . I))) . (((h . C) * (h . I)) . (f . (s,C))) by A24, A25, A26, A27, A28, Th11, FUNCT_2:63
.= ((T,Ss0) iter ((h . C) * (h . I))) . ((h . C) . ((h . I) . (f . (s,C)))) by FUNCT_2:15
.= (((T,Ss0) iter ((h . C) * (h . I))) * (h . C)) . ((h . I) . (f . (s,C))) by FUNCT_2:15
.= (((T,Ss0) iter ((h . C) * (h . I))) * (h . C)) . (f . ((f . (s,C)),I)) by A8, A23, FUNCT_5:39
.= (h . (while (C,I))) . (f . ((f . (s,C)),I)) by A7
.= f . ((f . ((f . (s,C)),I)),(while (C,I))) by A8, A21, FUNCT_5:39 ;
:: thesis: verum
end;
thus ( f . (s,C) nin T implies f . (s,(while (C,I))) = f . (s,C) ) by A24, A25, A26, A27, Th12; :: thesis: verum
end;
then reconsider f = f as ExecutionFunction of A,S,T by A9, A10, A14, Def32;
take f ; :: thesis: ( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0 ) )
dom f = [:S, the carrier of A:] by FUNCT_2:def 1;
then A29: [:S,(ElementaryInstructions A):] c= dom f by ZFMISC_1:95;
A30: dom g = [:S,(ElementaryInstructions A):] by FUNCT_2:def 1;
A31: (dom f) /\ [:S,(ElementaryInstructions A):] = [:S,(ElementaryInstructions A):] by A29, XBOOLE_1:28;
now :: thesis: for a being object st a in dom g holds
g . a = f . a
let a be object ; :: thesis: ( a in dom g implies g . a = f . a )
assume A32: a in dom g ; :: thesis: g . a = f . a
then consider s, I being object such that
A33: s in S and
A34: I in ElementaryInstructions A and
A35: a = [s,I] by ZFMISC_1:def 2;
reconsider s = s as Element of S by A33;
reconsider I = I as Element of A by A34;
reconsider EI = (curry' g) . I as Element of Funcs (S,S) by A1, A34;
g in Funcs ([:S,(ElementaryInstructions A):],S) by FUNCT_2:8;
then curry' g in Funcs ((ElementaryInstructions A),(Funcs (S,S))) by A32, FUNCT_6:10;
then A36: dom (curry' g) = ElementaryInstructions A by FUNCT_2:92;
A37: dom EI = S by FUNCT_2:92;
A38: dom (h . I) = S by FUNCT_2:92;
thus g . a = g . (s,I) by A35
.= EI . s by A34, A36, A37, FUNCT_5:34
.= (h . I) . s by A3, A34
.= f . (s,I) by A8, A38, FUNCT_5:39
.= f . a by A35 ; :: thesis: verum
end;
hence f | [:S,(ElementaryInstructions A):] = g by A30, A31, FUNCT_1:46; :: thesis: for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0
let s be Element of S; :: thesis: for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0
let C, I be Element of A; :: thesis: ( not f iteration_terminates_for I \; C,f . (s,C) implies f . (s,(while (C,I))) = s0 )
assume A39: not f iteration_terminates_for I \; C,f . (s,C) ; :: thesis: f . (s,(while (C,I))) = s0
A40: dom (h . (while (C,I))) = S by FUNCT_2:def 1;
A41: dom (h . C) = S by FUNCT_2:def 1;
A42: dom ((h . C) * (h . I)) = S by FUNCT_2:def 1;
A43: f . (s,(while (C,I))) = (h . (while (C,I))) . s by A8, A40, FUNCT_5:39
.= H4(h . C,h . I) . s by A7
.= ((T,Ss0) iter ((h . C) * (h . I))) . ((h . C) . s) by FUNCT_2:15 ;
A44: f . (s,C) = (h . C) . s by A8, A41, FUNCT_5:39;
A45: rng ((h . C) * (h . I)) c= S ;
rng h c= Funcs (S,S) ;
then h = curry' f by FUNCT_5:48;
then (curry' f) . (I \; C) = (h . C) * (h . I) by A5;
then ((h . C) * (h . I)) orbit (f . (s,C)) c= T by A39, Th87;
hence f . (s,(while (C,I))) = Ss0 . (f . (s,C)) by A42, A43, A44, A45, Def7
.= s0 by FUNCOP_1:7 ;
:: thesis: verum