let S be non empty set ; 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; 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; 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; ( 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):]
; 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)
XBOOLE_0:def 10 TerminatingPrograms (A,S,T,f2) c= TerminatingPrograms (A,S,T,f1)proof
let q,
I be
object ;
RELAT_1:def 3 ( [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)
;
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;
verum
end;
let q, I be object ; RELAT_1:def 3 ( [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)
; 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; verum