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 S1[ 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
S1[I]
proof
let I be Element of A; :: thesis: ( I in ElementaryInstructions A implies S1[I] )
assume A4: I in ElementaryInstructions A ; :: thesis: S1[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:106;
hence f1 . s,I = (f1 | [:S,(ElementaryInstructions A):]) . [s,I] by FUNCT_1:72
.= f2 . s,I by A1, A5, FUNCT_1:72 ;
:: thesis: verum
end;
A6: S1[ 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 S1[I1] & S1[I2] holds
S1[I1 \; I2]
proof
let I1, I2 be Element of A; :: thesis: ( S1[I1] & S1[I2] implies S1[I1 \; I2] )
assume that
A8: S1[I1] and
A9: S1[I2] ; :: thesis: S1[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 S1[C] & S1[I1] & S1[I2] holds
S1[ if-then-else C,I1,I2]
proof
let C, I1, I2 be Element of A; :: thesis: ( S1[C] & S1[I1] & S1[I2] implies S1[ if-then-else C,I1,I2] )
assume that
A11: S1[C] and
A12: S1[I1] and
A13: S1[I2] ; :: thesis: S1[ 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, Def30
.= f2 . (f1 . s,C),I1 by A12
.= f2 . s,(if-then-else C,I1,I2) by A15, A16, A17, Def30 ;
:: 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, Def30
.= f2 . (f1 . s,C),I2 by A13
.= f2 . s,(if-then-else C,I1,I2) by A15, A16, A18, Def30 ;
:: thesis: verum
end;
end;
end;
A19: for C, I being Element of A st S1[C] & S1[I] holds
S1[ while C,I]
proof
let C, I be Element of A; :: thesis: ( S1[C] & S1[I] implies S1[ while C,I] )
assume that
A20: S1[C] and
A21: S1[I] ; :: thesis: S1[ while C,I]
let s be Element of S; :: thesis: f1 . s,(while C,I) = f2 . s,(while C,I)
now
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) ) by Def33;
A25: f1 . s,C = f2 . s,C by A20;
A26: now
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
let sI be Element of [:S,the carrier of A:]; :: thesis: f1 . sI = f2 . sI
consider s, I being set 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;
S1[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:113; :: thesis: verum