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