let A be preIfWhileAlgebra; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: according to AOFA_000:def 38,AOFA_000:def 39 :: thesis: I \; J is_terminating_wrt f,P
let s be Element of S; :: according to AOFA_000:def 38 :: thesis: ( s in P implies [s,(I \; J)] in TerminatingPrograms A,S,T,f )
assume s in P ; :: thesis: [s,(I \; J)] in TerminatingPrograms A,S,T,f
then A4: ( [s,I] in TerminatingPrograms A,S,T,f & f . s,I in P ) by A1, A3;
then [(f . s,I),J] in TerminatingPrograms A,S,T,f by A2;
hence [s,(I \; J)] in TerminatingPrograms A,S,T,f by A4, Def35; :: thesis: verum