let S be non empty set ; AOFA_000:def 36 for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f)
let s be Element of S; for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f)
let T be Subset of S; for f being ExecutionFunction of A,S,T holds [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f)
let f be ExecutionFunction of A,S,T; [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f)
A1:
[s,C] in TerminatingPrograms (A,S,T,f)
by Def36;
A2:
( f . (s,C) in T or f . (s,C) nin T )
;
A3:
[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
by Def36;
[(f . (s,C)),J] in TerminatingPrograms (A,S,T,f)
by Def36;
hence
[s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f)
by A1, A2, A3, Def35; verum