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):] holds
for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms A,S,T,f1 holds
( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I )
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):] holds
for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms A,S,T,f1 holds
( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I )
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):] holds
for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms A,S,T,f1 holds
( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I )
let f1, f2 be ExecutionFunction of A,S,T; :: thesis: ( f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] implies for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms A,S,T,f1 holds
( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I ) )
assume A1: f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] ; :: thesis: for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms A,S,T,f1 holds
( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I )
set g = f1 | [:S,(ElementaryInstructions A):];
set TP1 = TerminatingPrograms A,S,T,f1;
set TP2 = TerminatingPrograms A,S,T,f2;
defpred S1[ Element of A] means for s being Element of S st [s,$1] in TerminatingPrograms A,S,T,f1 holds
( [s,$1] in TerminatingPrograms A,S,T,f2 & f1 . s,$1 = f2 . s,$1 );
A2: 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 A3: I in ElementaryInstructions A ; :: thesis: S1[I]
let s be Element of S; :: thesis: ( [s,I] in TerminatingPrograms A,S,T,f1 implies ( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I ) )
assume [s,I] in TerminatingPrograms A,S,T,f1 ; :: thesis: ( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I )
thus [s,I] in TerminatingPrograms A,S,T,f2 by A3, Th94; :: thesis: f1 . s,I = f2 . s,I
A4: [s,I] in [:S,(ElementaryInstructions A):] by A3, ZFMISC_1:106;
hence f1 . s,I = (f1 | [:S,(ElementaryInstructions A):]) . [s,I] by FUNCT_1:72
.= f2 . s,I by A1, A4, FUNCT_1:72 ;
:: thesis: verum
end;
A5: S1[ EmptyIns A]
proof
let s be Element of S; :: thesis: ( [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f1 implies ( [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f2 & f1 . s,(EmptyIns A) = f2 . s,(EmptyIns A) ) )
f1 . s,(EmptyIns A) = s by Def28;
hence ( [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f1 implies ( [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f2 & f1 . s,(EmptyIns A) = f2 . s,(EmptyIns A) ) ) by Def28, Th96; :: thesis: verum
end;
A6: 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
A7: S1[I1] and
A8: S1[I2] ; :: thesis: S1[I1 \; I2]
let s be Element of S; :: thesis: ( [s,(I1 \; I2)] in TerminatingPrograms A,S,T,f1 implies ( [s,(I1 \; I2)] in TerminatingPrograms A,S,T,f2 & f1 . s,(I1 \; I2) = f2 . s,(I1 \; I2) ) )
assume A9: [s,(I1 \; I2)] in TerminatingPrograms A,S,T,f1 ; :: thesis: ( [s,(I1 \; I2)] in TerminatingPrograms A,S,T,f2 & f1 . s,(I1 \; I2) = f2 . s,(I1 \; I2) )
then A10: [s,I1] in TerminatingPrograms A,S,T,f1 by Th97;
A11: [(f1 . s,I1),I2] in TerminatingPrograms A,S,T,f1 by A9, Th97;
A12: [s,I1] in TerminatingPrograms A,S,T,f2 by A7, A10;
A13: [(f1 . s,I1),I2] in TerminatingPrograms A,S,T,f2 by A8, A11;
A14: f1 . s,I1 = f2 . s,I1 by A7, A10;
A15: f1 . (f1 . s,I1),I2 = f2 . (f1 . s,I1),I2 by A8, A11;
f1 . (f1 . s,I1),I2 = f1 . s,(I1 \; I2) by Def29;
hence ( [s,(I1 \; I2)] in TerminatingPrograms A,S,T,f2 & f1 . s,(I1 \; I2) = f2 . s,(I1 \; I2) ) by A12, A13, A14, A15, Def29, Def35; :: thesis: verum
end;
A16: 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
A17: S1[C] and
A18: S1[I1] and
A19: S1[I2] ; :: thesis: S1[ if-then-else C,I1,I2]
A20: f1 complies_with_if_wrt T by Def32;
A21: f2 complies_with_if_wrt T by Def32;
set J = if-then-else C,I1,I2;
let s be Element of S; :: thesis: ( [s,(if-then-else C,I1,I2)] in TerminatingPrograms A,S,T,f1 implies ( [s,(if-then-else C,I1,I2)] in TerminatingPrograms A,S,T,f2 & f1 . s,(if-then-else C,I1,I2) = f2 . s,(if-then-else C,I1,I2) ) )
assume A22: [s,(if-then-else C,I1,I2)] in TerminatingPrograms A,S,T,f1 ; :: thesis: ( [s,(if-then-else C,I1,I2)] in TerminatingPrograms A,S,T,f2 & f1 . s,(if-then-else C,I1,I2) = f2 . s,(if-then-else C,I1,I2) )
then A23: [s,C] in TerminatingPrograms A,S,T,f1 by Th98;
A24: ( f1 . s,C in T implies [(f1 . s,C),I1] in TerminatingPrograms A,S,T,f1 ) by A22, Th98;
A25: ( f1 . s,C nin T implies [(f1 . s,C),I2] in TerminatingPrograms A,S,T,f1 ) by A22, Th98;
A26: [s,C] in TerminatingPrograms A,S,T,f2 by A17, A23;
A27: f1 . s,C = f2 . s,C by A17, A23;
A28: ( f1 . s,C in T implies ( [(f1 . s,C),I1] in TerminatingPrograms A,S,T,f2 & f1 . (f1 . s,C),I1 = f2 . (f1 . s,C),I1 & f1 . s,(if-then-else C,I1,I2) = f1 . (f1 . s,C),I1 ) ) by A18, A20, A24, Def30;
A29: ( f1 . s,C nin T implies ( [(f1 . s,C),I2] in TerminatingPrograms A,S,T,f2 & f1 . (f1 . s,C),I2 = f2 . (f1 . s,C),I2 & f1 . s,(if-then-else C,I1,I2) = f1 . (f1 . s,C),I2 ) ) by A19, A20, A25, Def30;
( f1 . s,C in T or f1 . s,C nin T ) ;
hence ( [s,(if-then-else C,I1,I2)] in TerminatingPrograms A,S,T,f2 & f1 . s,(if-then-else C,I1,I2) = f2 . s,(if-then-else C,I1,I2) ) by A21, A26, A27, A28, A29, Def30, Def35; :: thesis: verum
end;
A30: 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
A31: S1[C] and
A32: S1[I] ; :: thesis: S1[ while C,I]
set J = while C,I;
let s be Element of S; :: thesis: ( [s,(while C,I)] in TerminatingPrograms A,S,T,f1 implies ( [s,(while C,I)] in TerminatingPrograms A,S,T,f2 & f1 . s,(while C,I) = f2 . s,(while C,I) ) )
assume A33: [s,(while C,I)] in TerminatingPrograms A,S,T,f1 ; :: thesis: ( [s,(while C,I)] in TerminatingPrograms A,S,T,f2 & f1 . s,(while C,I) = f2 . s,(while C,I) )
then A34: [s,C] in TerminatingPrograms A,S,T,f1 by Th99;
then A35: [s,C] in TerminatingPrograms A,S,T,f2 by A31;
A36: f1 . s,C = f2 . s,C by A31, A34;
consider r being non empty FinSequence of S such that
A37: r . 1 = f1 . s,C and
A38: r . (len r) nin T and
A39: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f1 & r . (i + 1) = f1 . (r . i),(I \; C) ) by A33, Th99;
for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f1 . (r . i),(I \; C) ) by A39;
then A40: f1 . s,(while C,I) = r . (len r) by A37, A38, Th86;
defpred S2[ Nat] means ( 1 <= $1 & $1 < len r implies ( r . $1 in T & [(r . $1),(I \; C)] in TerminatingPrograms A,S,T,f2 & r . ($1 + 1) = f2 . (r . $1),(I \; C) ) );
A41: for i being Nat holds S2[i]
proof
let i be Nat; :: thesis: S2[i]
assume that
A42: 1 <= i and
A43: i < len r ; :: thesis: ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f2 & r . (i + 1) = f2 . (r . i),(I \; C) )
thus A44: r . i in T by A39, A42, A43; :: thesis: ( [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f2 & r . (i + 1) = f2 . (r . i),(I \; C) )
then reconsider ri = r . i as Element of S ;
A45: [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f1 by A39, A42, A43;
hence [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f2 by A6, A31, A32, A44; :: thesis: r . (i + 1) = f2 . (r . i),(I \; C)
A46: [ri,I] in TerminatingPrograms A,S,T,f1 by A45, Th97;
A47: [(f1 . ri,I),C] in TerminatingPrograms A,S,T,f1 by A45, Th97;
thus r . (i + 1) = f1 . (r . i),(I \; C) by A39, A42, A43
.= f1 . (f1 . ri,I),C by Def29
.= f2 . (f1 . ri,I),C by A31, A47
.= f2 . (f2 . ri,I),C by A32, A46
.= f2 . (r . i),(I \; C) by Def29 ; :: thesis: verum
end;
then for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f2 . (r . i),(I \; C) ) ;
hence ( [s,(while C,I)] in TerminatingPrograms A,S,T,f2 & f1 . s,(while C,I) = f2 . s,(while C,I) ) by A35, A36, A37, A38, A40, A41, Def35, Th86; :: thesis: verum
end;
let I be Element of A; :: thesis: for s being Element of S st [s,I] in TerminatingPrograms A,S,T,f1 holds
( [s,I] in TerminatingPrograms A,S,T,f2 & f1 . s,I = f2 . s,I )
thus S1[I] from AOFA_000:sch 2(A2, A5, A6, A16, A30); :: thesis: verum