let A be preIfWhileAlgebra; :: thesis:
let C, I be Element of A; :: thesis:
let S be non empty set ; :: thesis:
let T be Subset of S; :: thesis:
let s be Element of S; :: thesis:
let f be ExecutionFunction of A,S,T; :: thesis:
set TP = TerminatingPrograms A,S,T,f;
set rr = s;
set IJ = while C,I;
assume A1: ( A is free & [s,(while C,I)] in TerminatingPrograms A,S,T,f ) ; :: thesis:
reconsider P = (TerminatingPrograms A,S,T,f) \ {[s,(while C,I)]} as Subset of [:S,the carrier of A:] ;
A2: [:S,(ElementaryInstructions A):] c= P

let x, y be set ; :: according to RELAT_1:def 3 :: thesis:
assume A3: [x,y] in [:S,(ElementaryInstructions A):] ; :: thesis:
then y in ElementaryInstructions A by ZFMISC_1:106;
then y <> while C,I by Th52;
then ( [:S,(ElementaryInstructions A):] c= TerminatingPrograms A,S,T,f & [x,y] <> [s,(while C,I)] ) by Def35, ZFMISC_1:33;
then ( [x,y] nin {[s,(while C,I)]} & [x,y] in TerminatingPrograms A,S,T,f ) by A3, TARSKI:def 1;
hence not [x,y] nin P by XBOOLE_0:def 5; :: thesis:

end;

A4: [:S,{(EmptyIns A)}:] c= P

let x, y be set ; :: according to RELAT_1:def 3 :: thesis:
assume A5: [x,y] in [:S,{(EmptyIns A)}:] ; :: thesis:
then y in {(EmptyIns A)} by ZFMISC_1:106;
then y = EmptyIns A by TARSKI:def 1;
then y <> while C,I by A1, Th72;
then ( [:S,{(EmptyIns A)}:] c= TerminatingPrograms A,S,T,f & [x,y] <> [s,(while C,I)] ) by Def35, ZFMISC_1:33;
then ( [x,y] nin {[s,(while C,I)]} & [x,y] in TerminatingPrograms A,S,T,f ) by A5, TARSKI:def 1;
hence not [x,y] nin P by XBOOLE_0:def 5; :: thesis:

end;

A6: now

let s be Element of S; :: thesis:
let C, I, J be Element of A; :: thesis:

hereby :: thesis:

assume ( [s,I] in P & [(f . s,I),J] in P ) ; :: thesis:
then ( [s,I] in TerminatingPrograms A,S,T,f & [(f . s,I),J] in TerminatingPrograms A,S,T,f & while C,I <> I \; J ) by A1, Th73, ZFMISC_1:64;
then ( [s,(I \; J)] in TerminatingPrograms A,S,T,f & [s,(while C,I)] <> [s,(I \; J)] ) by Def35, ZFMISC_1:33;
hence [s,(I \; J)] in P by ZFMISC_1:64; :: thesis:

end;

hereby :: thesis:

assume A7: ( [s,C] in P & [(f . s,C),I] in P & f . s,C in T ) ; :: thesis:
then ( [s,C] in TerminatingPrograms A,S,T,f & [(f . s,C),I] in TerminatingPrograms A,S,T,f & while C,I <> if-then-else C,I,J ) by A1, Th74, ZFMISC_1:64;
then ( [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f & [s,(while C,I)] <> [s,(if-then-else C,I,J)] ) by A7, Def35, ZFMISC_1:33;
hence [s,(if-then-else C,I,J)] in P by ZFMISC_1:64; :: thesis:

end;

hereby :: thesis:

assume A8: ( [s,C] in P & [(f . s,C),J] in P & f . s,C nin T ) ; :: thesis:
then ( [s,C] in TerminatingPrograms A,S,T,f & [(f . s,C),J] in TerminatingPrograms A,S,T,f & while C,I <> if-then-else C,I,J ) by A1, Th74, ZFMISC_1:64;
then ( [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f & [s,(while C,I)] <> [s,(if-then-else C,I,J)] ) by A8, Def35, ZFMISC_1:33;
hence [s,(if-then-else C,I,J)] in P by ZFMISC_1:64; :: thesis:

end;

hereby :: thesis:

assume A9: [s,C] nin TerminatingPrograms A,S,T,f ; :: thesis:

let s be Element of S; :: thesis:
let C', I', J be Element of A; :: thesis:
assume A10: [s,C'] in P ; :: thesis:
given r being non empty FinSequence of S such that A11: ( r . 1 = f . s,C' & r . (len r) nin T ) and
A12: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I' \; C')] in P & r . (i + 1) = f . (r . i),(I' \; C') ) ; :: thesis:

A13: now

let i be Nat; :: thesis:
assume ( 1 <= i & i < len r ) ; :: thesis:
then ( r . i in T & [(r . i),(I' \; C')] in P & r . (i + 1) = f . (r . i),(I' \; C') ) by A12;
hence ( r . i in T & [(r . i),(I' \; C')] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I' \; C') ) by ZFMISC_1:64; :: thesis:

end;

A14: [s,C'] in TerminatingPrograms A,S,T,f by A10, ZFMISC_1:64;
then ( while C',I' <> while C,I or s <> s ) by A9, A1, Th75;
then ( [s,(while C',I')] in TerminatingPrograms A,S,T,f & [s,(while C',I')] <> [s,(while C,I)] ) by A11, A13, A14, Def35, ZFMISC_1:33;
hence [s,(while C',I')] in P by ZFMISC_1:64; :: thesis:

end;

then for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . s,I),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . s,C),I] in P & f . s,C in T implies [s,(if-then-else C,I,J)] in P ) & ( [s,C] in P & [(f . s,C),J] in P & f . s,C nin T implies [s,(if-then-else C,I,J)] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . s,C & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . (r . i),(I \; C) ) ) ) implies [s,(while C,I)] in P ) ) by A6;
then TerminatingPrograms A,S,T,f c= P by A2, A4, Def35;
hence contradiction by A1, ZFMISC_1:64; :: thesis:

end;

assume A15: for r being non empty FinSequence of S holds
( not r . 1 = f . s,C or not r . (len r) nin T or ex i being Nat st
( 1 <= i & i < len r & not ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) ) ) ) ; :: thesis:

let s be Element of S; :: thesis:
let C', I', J be Element of A; :: thesis:
assume A16: [s,C'] in P ; :: thesis:
given r being non empty FinSequence of S such that A17: ( r . 1 = f . s,C' & r . (len r) nin T ) and
A18: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I' \; C')] in P & r . (i + 1) = f . (r . i),(I' \; C') ) ; :: thesis:

A19: now

let i be Nat; :: thesis:
assume ( 1 <= i & i < len r ) ; :: thesis:
then ( r . i in T & [(r . i),(I' \; C')] in P & r . (i + 1) = f . (r . i),(I' \; C') ) by A18;
hence ( r . i in T & [(r . i),(I' \; C')] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I' \; C') ) by ZFMISC_1:64; :: thesis:

end;

A20: [s,C'] in TerminatingPrograms A,S,T,f by A16, ZFMISC_1:64;
( I <> I' or C <> C' or s <> s ) by A15, A17, A19;
then ( while C',I' <> while C,I or s <> s ) by A1, Th75;
then ( [s,(while C',I')] in TerminatingPrograms A,S,T,f & [s,(while C',I')] <> [s,(while C,I)] ) by A17, A19, A20, Def35, ZFMISC_1:33;
hence [s,(while C',I')] in P by ZFMISC_1:64; :: thesis:

end;