let S be non empty set ; :: thesis: for T being Subset of S
for A being free ECIW-strict preIfWhileAlgebra
for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] & ( for s being Element of S
for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . (s,C) holds
f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) holds
f1 = f2
let T be Subset of S; :: thesis: for A being free ECIW-strict preIfWhileAlgebra
for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] & ( for s being Element of S
for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . (s,C) holds
f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) holds
f1 = f2
let A be free ECIW-strict preIfWhileAlgebra; :: thesis: for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] & ( for s being Element of S
for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . (s,C) holds
f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) holds
f1 = f2
let f1, f2 be ExecutionFunction of A,S,T; :: thesis: ( f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] & ( for s being Element of S
for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . (s,C) holds
f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) implies f1 = f2 )
assume A1: f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] ; :: thesis: ( ex s being Element of S ex C, I being Element of A st
( not f1 iteration_terminates_for I \; C,f1 . (s,C) & not f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) or f1 = f2 )
set g = f1 | [:S,(ElementaryInstructions A):];
assume A2: for s being Element of S
for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . (s,C) holds
f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ; :: thesis: f1 = f2
defpred S₁[ set ] means for s being Element of S holds f1 . (s,$1) = f2 . (s,$1);
A3: for I being Element of A st I in ElementaryInstructions A holds
S₁[I]

proof

let I be Element of A; :: thesis: ( I in ElementaryInstructions A implies S₁[I] )
assume A4: I in ElementaryInstructions A ; :: thesis: S₁[I]
let s be Element of S; :: thesis: f1 . (s,I) = f2 . (s,I)
A5: [s,I] in [:S,(ElementaryInstructions A):] by A4, ZFMISC_1:87;
hence f1 . (s,I) = (f1 | [:S,(ElementaryInstructions A):]) . [s,I] by FUNCT_1:49
.= f2 . (s,I) by A1, A5, FUNCT_1:49 ;
:: thesis: verum

end;

A6: S₁[ EmptyIns A]

proof

let s be Element of S; :: thesis: f1 . (s,(EmptyIns A)) = f2 . (s,(EmptyIns A))
thus f1 . (s,(EmptyIns A)) = s by Def28
.= f2 . (s,(EmptyIns A)) by Def28 ; :: thesis: verum

end;

A7: for I1, I2 being Element of A st S₁[I1] & S₁[I2] holds
S₁[I1 \; I2]

proof

let I1, I2 be Element of A; :: thesis: ( S₁[I1] & S₁[I2] implies S₁[I1 \; I2] )
assume that
A8: S₁[I1] and
A9: S₁[I2] ; :: thesis: S₁[I1 \; I2]
let s be Element of S; :: thesis: f1 . (s,(I1 \; I2)) = f2 . (s,(I1 \; I2))
thus f1 . (s,(I1 \; I2)) = f1 . ((f1 . (s,I1)),I2) by Def29
.= f1 . ((f2 . (s,I1)),I2) by A8
.= f2 . ((f2 . (s,I1)),I2) by A9
.= f2 . (s,(I1 \; I2)) by Def29 ; :: thesis: verum

end;

A10: for C, I1, I2 being Element of A st S₁[C] & S₁[I1] & S₁[I2] holds
S₁[ if-then-else (C,I1,I2)]

proof

let C, I1, I2 be Element of A; :: thesis: ( S₁[C] & S₁[I1] & S₁[I2] implies S₁[ if-then-else (C,I1,I2)] )
assume that
A11: S₁[C] and
A12: S₁[I1] and
A13: S₁[I2] ; :: thesis: S₁[ if-then-else (C,I1,I2)]
let s be Element of S; :: thesis: f1 . (s,(if-then-else (C,I1,I2))) = f2 . (s,(if-then-else (C,I1,I2)))
A14: f1 complies_with_if_wrt T by Def32;
A15: f2 complies_with_if_wrt T by Def32;
A16: f1 . (s,C) = f2 . (s,C) by A11;

per cases ( f1 . (s,C) in T or f1 . (s,C) nin T ) ;

suppose A17: f1 . (s,C) in T ; :: thesis: f1 . (s,(if-then-else (C,I1,I2))) = f2 . (s,(if-then-else (C,I1,I2)))

hence f1 . (s,(if-then-else (C,I1,I2))) = f1 . ((f1 . (s,C)),I1) by A14
.= f2 . ((f1 . (s,C)),I1) by A12
.= f2 . (s,(if-then-else (C,I1,I2))) by A15, A16, A17 ;
:: thesis: verum

end;

suppose A18: f1 . (s,C) nin T ; :: thesis: f1 . (s,(if-then-else (C,I1,I2))) = f2 . (s,(if-then-else (C,I1,I2)))

hence f1 . (s,(if-then-else (C,I1,I2))) = f1 . ((f1 . (s,C)),I2) by A14
.= f2 . ((f1 . (s,C)),I2) by A13
.= f2 . (s,(if-then-else (C,I1,I2))) by A15, A16, A18 ;
:: thesis: verum

end;

end;

end;

A19: for C, I being Element of A st S₁[C] & S₁[I] holds
S₁[ while (C,I)]

proof

let C, I be Element of A; :: thesis: ( S₁[C] & S₁[I] implies S₁[ while (C,I)] )
assume that
A20: S₁[C] and
A21: S₁[I] ; :: thesis: S₁[ while (C,I)]
let s be Element of S; :: thesis: f1 . (s,(while (C,I))) = f2 . (s,(while (C,I)))

now :: thesis: ( f1 iteration_terminates_for I \; C,f1 . (s,C) implies f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) )

assume f1 iteration_terminates_for I \; C,f1 . (s,C) ; :: thesis: f1 . (s,(while (C,I))) = f2 . (s,(while (C,I)))
then consider r being non empty FinSequence of S such that
A22: r . 1 = f1 . (s,C) and
A23: r . (len r) nin T and
A24: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f1 . ((r . i),(I \; C)) ) ;
A25: f1 . (s,C) = f2 . (s,C) by A20;

A26: now :: thesis: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f2 . ((r . i),(I \; C)) )

let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in T & r . (i + 1) = f2 . ((r . i),(I \; C)) ) )
assume that
A27: 1 <= i and
A28: i < len r ; :: thesis: ( r . i in T & r . (i + 1) = f2 . ((r . i),(I \; C)) )
thus r . i in T by A24, A27, A28; :: thesis: r . (i + 1) = f2 . ((r . i),(I \; C))
then reconsider si = r . i as Element of S ;
thus r . (i + 1) = f1 . (si,(I \; C)) by A24, A27, A28
.= f1 . ((f1 . (si,I)),C) by Def29
.= f1 . ((f2 . (si,I)),C) by A21
.= f2 . ((f2 . (si,I)),C) by A20
.= f2 . ((r . i),(I \; C)) by Def29 ; :: thesis: verum

end;

thus f1 . (s,(while (C,I))) = r . (len r) by A22, A23, A24, Th86
.= f2 . (s,(while (C,I))) by A22, A23, A25, A26, Th86 ; :: thesis: verum

end;

hence f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) by A2; :: thesis: verum

end;

now :: thesis: for sI being Element of [:S, the carrier of A:] holds f1 . sI = f2 . sI

let sI be Element of [:S, the carrier of A:]; :: thesis: f1 . sI = f2 . sI
consider s, I being object such that
A29: s in S and
A30: I in the carrier of A and
A31: sI = [s,I] by ZFMISC_1:def 2;
reconsider I = I as Element of A by A30;
reconsider s = s as Element of S by A29;
S₁[I] from AOFA_000:sch 2(A3, A6, A7, A10, A19);
then f1 . (s,I) = f2 . (s,I) ;
hence f1 . sI = f2 . sI by A31; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum