let S be non empty set ; :: thesis:
let T be Subset of S; :: thesis:
let A be free ECIW-strict preIfWhileAlgebra; :: thesis:
let f1, f2 be ExecutionFunction of A,S,T; :: thesis:
assume A1: f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] ; :: thesis:
set g = f1 | [:S,(ElementaryInstructions A):];
set TP1 = TerminatingPrograms A,S,T,f1;
set TP2 = TerminatingPrograms A,S,T,f2;
defpred S₁[ 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
S₁[I]

let I be Element of A; :: thesis:
assume A3: I in ElementaryInstructions A ; :: thesis:
let s be Element of S; :: thesis:
assume [s,I] in TerminatingPrograms A,S,T,f1 ; :: thesis:
thus [s,I] in TerminatingPrograms A,S,T,f2 by A3, Th94; :: thesis:
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:

end;

A5: S₁[ EmptyIns A]

let s be Element of S; :: thesis:
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 Th96, Def28; :: thesis:

end;

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

let I1, I2 be Element of A; :: thesis:
assume A7: ( S₁[I1] & S₁[I2] ) ; :: thesis:
let s be Element of S; :: thesis:
assume [s,(I1 \; I2)] in TerminatingPrograms A,S,T,f1 ; :: thesis:
then ( [s,I1] in TerminatingPrograms A,S,T,f1 & [(f1 . s,I1),I2] in TerminatingPrograms A,S,T,f1 ) by Th97;
then ( [s,I1] in TerminatingPrograms A,S,T,f2 & [(f1 . s,I1),I2] in TerminatingPrograms A,S,T,f2 & f1 . s,I1 = f2 . s,I1 & f1 . (f1 . s,I1),I2 = f2 . (f1 . s,I1),I2 & f1 . (f1 . s,I1),I2 = f1 . s,(I1 \; I2) ) by A7, Def29;
hence ( [s,(I1 \; I2)] in TerminatingPrograms A,S,T,f2 & f1 . s,(I1 \; I2) = f2 . s,(I1 \; I2) ) by Def35, Def29; :: thesis:

end;

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

let C, I1, I2 be Element of A; :: thesis:
assume A9: ( S₁[C] & S₁[I1] & S₁[I2] ) ; :: thesis:
A10: ( f1 complies_with_if_wrt T & f2 complies_with_if_wrt T ) by Def32;
set J = if-then-else C,I1,I2;
let s be Element of S; :: thesis:
assume [s,(if-then-else C,I1,I2)] in TerminatingPrograms A,S,T,f1 ; :: thesis:
then ( [s,C] in TerminatingPrograms A,S,T,f1 & ( f1 . s,C in T implies [(f1 . s,C),I1] in TerminatingPrograms A,S,T,f1 ) & ( f1 . s,C nin T implies [(f1 . s,C),I2] in TerminatingPrograms A,S,T,f1 ) ) by Th98;
then ( [s,C] in TerminatingPrograms A,S,T,f2 & f1 . s,C = f2 . s,C & ( 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 ) ) & ( 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 ) ) & ( f1 . s,C in T or f1 . s,C nin T ) ) by A9, A10, Def30;
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 Def35, A10, Def30; :: thesis:

end;

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

let C, I be Element of A; :: thesis:
assume A12: ( S₁[C] & S₁[I] ) ; :: thesis:
set J = while C,I;
let s be Element of S; :: thesis:
assume A13: [s,(while C,I)] in TerminatingPrograms A,S,T,f1 ; :: thesis:
then [s,C] in TerminatingPrograms A,S,T,f1 by Th99;
then A14: ( [s,C] in TerminatingPrograms A,S,T,f2 & f1 . s,C = f2 . s,C ) by A12;
consider r being non empty FinSequence of S such that
A15: ( r . 1 = f1 . s,C & r . (len r) nin T ) and
A16: 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 A13, 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 A16;
then A17: f1 . s,(while C,I) = r . (len r) by A15, Th86;
defpred S₂[ 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) ) );
A18: for i being Nat holds S₂[i]

let i be Nat; :: thesis:
assume A19: ( 1 <= i & i < len r ) ; :: thesis:
hence A20: r . i in T by A16; :: thesis:
then reconsider ri = r . i as Element of S ;
A21: [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f1 by A19, A16;
hence [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f2 by A12, A20, A6; :: thesis:
A22: ( [ri,I] in TerminatingPrograms A,S,T,f1 & [(f1 . ri,I),C] in TerminatingPrograms A,S,T,f1 ) by A21, Th97;
thus r . (i + 1) = f1 . (r . i),(I \; C) by A19, A16
.= f1 . (f1 . ri,I),C by Def29
.= f2 . (f1 . ri,I),C by A12, A22
.= f2 . (f2 . ri,I),C by A12, A22
.= f2 . (r . i),(I \; C) by Def29 ; :: thesis:

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 A14, A15, A17, A18, Th86, Def35; :: thesis:

end;

let I be Element of A; :: thesis:
thus S₁[I] from AOFA_000:sch 2(A2, A5, A6, A8, A11); :: thesis: