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 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]

proof

let I be Element of A; :: thesis: ( I in ElementaryInstructions A implies S₁[I] )
assume A3: I in ElementaryInstructions A ; :: thesis: S₁[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:87;
hence f1 . (s,I) = (f1 | [:S,(ElementaryInstructions A):]) . [s,I] by FUNCT_1:49
.= f2 . (s,I) by A1, A4, FUNCT_1:49 ;
:: thesis: verum

end;

A5: S₁[ 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 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
A7: S₁[I1] and
A8: S₁[I2] ; :: thesis: S₁[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 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
A17: S₁[C] and
A18: S₁[I1] and
A19: S₁[I2] ; :: thesis: S₁[ 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;
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;
( 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, Def35; :: thesis: verum

end;

A30: 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
A31: S₁[C] and
A32: S₁[I] ; :: thesis: S₁[ 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 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)) ) );
A41: for i being Nat holds S₂[i]

proof

let i be Nat; :: thesis: S₂[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 S₁[I] from AOFA_000:sch 2(A2, A5, A6, A16, A30); :: thesis: verum