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 object ; :: 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 A3: q is Element of S by ZFMISC_1:87;
I is Element of A by A2, ZFMISC_1:87;
hence not [q,I] nin TerminatingPrograms (A,S,T,f2) by A1, A2, A3, Lm3; :: thesis: verum

end;

let q, I be object ; :: 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 A4: [q,I] in TerminatingPrograms (A,S,T,f2) ; :: thesis: not [q,I] nin TerminatingPrograms (A,S,T,f1)
then A5: q is Element of S by ZFMISC_1:87;
I is Element of A by A4, ZFMISC_1:87;
hence not [q,I] nin TerminatingPrograms (A,S,T,f1) by A1, A4, A5, Lm3; :: thesis: verum