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