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 I, J being Element of A st I is_terminating_wrt f & J is_terminating_wrt f holds
I \; J is_terminating_wrt f
let S be non empty set ; :: thesis: for T being Subset of S
for f being ExecutionFunction of A,S,T
for I, J being Element of A st I is_terminating_wrt f & J is_terminating_wrt f holds
I \; J is_terminating_wrt f
let T be Subset of S; :: thesis: for f being ExecutionFunction of A,S,T
for I, J being Element of A st I is_terminating_wrt f & J is_terminating_wrt f holds
I \; J is_terminating_wrt f
let f be ExecutionFunction of A,S,T; :: thesis: for I, J being Element of A st I is_terminating_wrt f & J is_terminating_wrt f holds
I \; J is_terminating_wrt f
let I, J be Element of A; :: thesis: ( I is_terminating_wrt f & J is_terminating_wrt f implies I \; J is_terminating_wrt f )
assume that
A1: for s being Element of S holds [s,I] in TerminatingPrograms (A,S,T,f) and
A2: for s being Element of S holds [s,J] in TerminatingPrograms (A,S,T,f) ; :: according to AOFA_000:def 37 :: thesis: I \; J is_terminating_wrt f
let s be Element of S; :: according to AOFA_000:def 37 :: thesis: [s,(I \; J)] in TerminatingPrograms (A,S,T,f)
A3: [s,I] in TerminatingPrograms (A,S,T,f) by A1;
[(f . (s,I)),J] in TerminatingPrograms (A,S,T,f) by A2;
hence [s,(I \; J)] in TerminatingPrograms (A,S,T,f) by A3, Def35; :: thesis: verum