let A be preIfWhileAlgebra; for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for P being set
for I, J being Element of A st I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f holds
I \; J is_terminating_wrt f,P
let S be non empty set ; for T being Subset of S
for f being ExecutionFunction of A,S,T
for P being set
for I, J being Element of A st I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f holds
I \; J is_terminating_wrt f,P
let T be Subset of S; for f being ExecutionFunction of A,S,T
for P being set
for I, J being Element of A st I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f holds
I \; J is_terminating_wrt f,P
let f be ExecutionFunction of A,S,T; for P being set
for I, J being Element of A st I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f holds
I \; J is_terminating_wrt f,P
let P be set ; for I, J being Element of A st I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f holds
I \; J is_terminating_wrt f,P
let I, J be Element of A; ( I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f implies I \; J is_terminating_wrt f,P )
assume that
A1:
for s being Element of S st s in P holds
[s,I] in TerminatingPrograms (A,S,T,f)
and
A2:
for s being Element of S st s in P holds
[s,J] in TerminatingPrograms (A,S,T,f)
and
A3:
for s being Element of S st s in P holds
f . (s,I) in P
; AOFA_000:def 38,AOFA_000:def 39 I \; J is_terminating_wrt f,P
let s be Element of S; AOFA_000:def 38 ( s in P implies [s,(I \; J)] in TerminatingPrograms (A,S,T,f) )
assume A4:
s in P
; [s,(I \; J)] in TerminatingPrograms (A,S,T,f)
then A5:
[s,I] in TerminatingPrograms (A,S,T,f)
by A1;
[(f . (s,I)),J] in TerminatingPrograms (A,S,T,f)
by A2, A3, A4;
hence
[s,(I \; J)] in TerminatingPrograms (A,S,T,f)
by A5, Def35; verum