let A be preIfWhileAlgebra; :: thesis: for C, I being Element of A
for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T holds
[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
let C, I be Element of A; :: thesis: for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T holds
[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
let S be non empty set ; :: thesis: for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T holds
[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T holds
[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T holds
[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
let f be ExecutionFunction of A,S,T; :: thesis: ( A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T implies [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) )
set TP = TerminatingPrograms (A,S,T,f);
set IJ = while (C,I);
assume that
A1: A is free and
A2: [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) and
A3: f . (s,C) in T ; :: thesis: [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
consider r being non empty FinSequence of S such that
A4: r . 1 = f . (s,C) and
A5: r . (len r) nin T and
A6: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) by A1, A2, Th99;
len r >= 1 by NAT_1:14;
then 1 < len r by A3, A4, A5, XXREAL_0:1;
then [(r . 1),(I \; C)] in TerminatingPrograms (A,S,T,f) by A6;
hence [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) by A1, A4, Th97; :: thesis: verum