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
TerminatingPrograms A,S,T,f1 = TerminatingPrograms A,S,T,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):] holds
TerminatingPrograms A,S,T,f1 = TerminatingPrograms A,S,T,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):] holds
TerminatingPrograms A,S,T,f1 = TerminatingPrograms A,S,T,f2
let f1, f2 be ExecutionFunction of A,S,T; :: thesis: ( f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] implies TerminatingPrograms A,S,T,f1 = TerminatingPrograms A,S,T,f2 )
assume A1: f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] ; :: thesis: TerminatingPrograms A,S,T,f1 = TerminatingPrograms A,S,T,f2
set TP1 = TerminatingPrograms A,S,T,f1;
set TP2 = TerminatingPrograms A,S,T,f2;
thus TerminatingPrograms A,S,T,f1 c= TerminatingPrograms A,S,T,f2 :: according to XBOOLE_0:def 10 :: thesis: TerminatingPrograms A,S,T,f2 c= TerminatingPrograms A,S,T,f1

proof

let q, I be set ; :: according to RELAT_1:def 3 :: thesis: ( [q,I] nin TerminatingPrograms A,S,T,f1 or not [q,I] nin TerminatingPrograms A,S,T,f2 )
assume A2: [q,I] in TerminatingPrograms A,S,T,f1 ; :: thesis: not [q,I] nin TerminatingPrograms A,S,T,f2
then ( q is Element of S & I is Element of A ) by ZFMISC_1:106;
hence not [q,I] nin TerminatingPrograms A,S,T,f2 by A1, A2, Lm3; :: thesis: verum

end;

let q, I be set ; :: according to RELAT_1:def 3 :: thesis: ( [q,I] nin TerminatingPrograms A,S,T,f2 or not [q,I] nin TerminatingPrograms A,S,T,f1 )
assume A3: [q,I] in TerminatingPrograms A,S,T,f2 ; :: thesis: not [q,I] nin TerminatingPrograms A,S,T,f1
then ( q is Element of S & I is Element of A ) by ZFMISC_1:106;
hence not [q,I] nin TerminatingPrograms A,S,T,f1 by A1, A3, Lm3; :: thesis: verum