set C = F₇() leq F₈();
set S = Funcs (F₂(),INT);
reconsider s1 = F₆() . (F₉(),(F₇() := F₁₀())) as Element of Funcs (F₂(),INT) ;
reconsider s2 = F₆() . (s1,(F₇() leq F₈())) as Element of Funcs (F₂(),INT) ;
A6: P₁[s2] by A2, A3;
defpred S₁[ Element of Funcs (F₂(),INT)] means ( P₁[$1] & ( F₁₀() . F₉() <= F₉() . F₈() implies ($1 . F₇()) - 1 <= F₉() . F₈() ) & $1 . F₈() = F₉() . F₈() );
A7: s1 . F₇() = F₁₀() . F₉() by Th26;
then A8: s2 . F₇() = F₁₀() . F₉() by A5, Th35;
defpred S₂[ Element of Funcs (F₂(),INT)] means $1 . F₇() <= $1 . F₈();
set T = (Funcs (F₂(),INT)) \ (F₃(),0);
A9: F₆() complies_with_while_wrt (Funcs (F₂(),INT)) \ (F₃(),0) by AOFA_000:def 32;
set II = F₄() \; (F₇() += 1);
A10: F₆() . (F₉(),F₅()) = F₆() . (s1,(while ((F₇() leq F₈()),(F₄() \; (F₇() += 1))))) by A1, AOFA_000:def 29;
(F₁₀() . F₉()) - 1 < F₁₀() . F₉() by XREAL_1:44;
then A11: S₁[s1] by A2, A5, A7, Th26, XXREAL_0:2;
A12: s1 . F₈() = F₉() . F₈() by A5, Th26;
then A13: s2 . F₈() = F₉() . F₈() by A5, Th35;

per cases ( F₁₀() . F₉() <= F₉() . F₈() or F₁₀() . F₉() > F₉() . F₈() ) ;

suppose A14: F₁₀() . F₉() <= F₉() . F₈() ; :: thesis: ( P₁[F₆() . (F₉(),F₅())] & ( F₁₀() . F₉() <= F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = (F₉() . F₈()) + 1 ) & ( F₁₀() . F₉() > F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = F₁₀() . F₉() ) & (F₆() . (F₉(),F₅())) . F₈() = F₉() . F₈() )

deffunc H₁( Element of Funcs (F₂(),INT)) -> Element of NAT = In (((($1 . F₈()) + 1) - ($1 . F₇())),NAT);
defpred S₃[ Element of Funcs (F₂(),INT)] means ( P₁[$1] & S₂[$1] );
A15: for s being Element of Funcs (F₂(),INT) st S₁[s] & s in (Funcs (F₂(),INT)) \ (F₃(),0) & S₂[s] holds
S₁[F₆() . (s,(F₄() \; (F₇() += 1)))]

proof

let s be Element of Funcs (F₂(),INT); :: thesis: ( S₁[s] & s in (Funcs (F₂(),INT)) \ (F₃(),0) & S₂[s] implies S₁[F₆() . (s,(F₄() \; (F₇() += 1)))] )
assume that
A16: S₁[s] and
s in (Funcs (F₂(),INT)) \ (F₃(),0) and
A17: S₂[s] ; :: thesis: S₁[F₆() . (s,(F₄() \; (F₇() += 1)))]
thus P₁[F₆() . (s,(F₄() \; (F₇() += 1)))] by A3, A16; :: thesis: ( ( F₁₀() . F₉() <= F₉() . F₈() implies ((F₆() . (s,(F₄() \; (F₇() += 1)))) . F₇()) - 1 <= F₉() . F₈() ) & (F₆() . (s,(F₄() \; (F₇() += 1)))) . F₈() = F₉() . F₈() )
reconsider s9 = F₆() . (s,F₄()) as Element of Funcs (F₂(),INT) ;
reconsider s99 = F₆() . (s9,(F₇() += 1)) as Element of Funcs (F₂(),INT) ;
A18: s99 = F₆() . (s,(F₄() \; (F₇() += 1))) by AOFA_000:def 29;
A19: s99 . F₇() = (s9 . F₇()) + 1 by Th28;
s9 . F₈() = s . F₈() by A4, A16;
hence ( ( F₁₀() . F₉() <= F₉() . F₈() implies ((F₆() . (s,(F₄() \; (F₇() += 1)))) . F₇()) - 1 <= F₉() . F₈() ) & (F₆() . (s,(F₄() \; (F₇() += 1)))) . F₈() = F₉() . F₈() ) by A4, A5, A16, A17, A19, A18, Th28; :: thesis: verum

end;

A20: for s being Element of Funcs (F₂(),INT) st S₃[s] holds
( ( S₃[F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))] implies F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) in (Funcs (F₂(),INT)) \ (F₃(),0) ) & ( F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₃[F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))] ) & H₁(F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))) < H₁(s) )

proof

let s be Element of Funcs (F₂(),INT); :: thesis: ( S₃[s] implies ( ( S₃[F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))] implies F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) in (Funcs (F₂(),INT)) \ (F₃(),0) ) & ( F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₃[F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))] ) & H₁(F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))) < H₁(s) ) )
reconsider s9 = F₆() . (s,F₄()) as Element of Funcs (F₂(),INT) ;
reconsider s99 = F₆() . (s9,(F₇() += 1)) as Element of Funcs (F₂(),INT) ;
reconsider s999 = F₆() . (s99,(F₇() leq F₈())) as Element of Funcs (F₂(),INT) ;
A21: F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) = F₆() . ((F₆() . (s,(F₄() \; (F₇() += 1)))),(F₇() leq F₈())) by AOFA_000:def 29;
A22: s99 . F₈() = s9 . F₈() by A5, Th28;
A23: ( s99 . F₇() <= s99 . F₈() implies s999 . F₃() = 1 ) by Th35;
A24: ( s99 . F₇() > s99 . F₈() implies s999 . F₃() = 0 ) by Th35;
assume A25: S₃[s] ; :: thesis: ( ( S₃[F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))] implies F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) in (Funcs (F₂(),INT)) \ (F₃(),0) ) & ( F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₃[F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))] ) & H₁(F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))) < H₁(s) )
then reconsider j = (s . F₈()) - (s . F₇()) as Element of NAT by INT_1:5;
A26: s999 . F₇() = s99 . F₇() by A5, Th35;
A27: s99 = F₆() . (s,(F₄() \; (F₇() += 1))) by AOFA_000:def 29;
then P₁[s99] by A3, A25;
hence ( S₃[F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))] iff F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) in (Funcs (F₂(),INT)) \ (F₃(),0) ) by A3, A5, A21, A27, A26, A24, A23, Th2, Th35; :: thesis: H₁(F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))) < H₁(s)
A28: s99 . F₇() = (s9 . F₇()) + 1 by Th28;
A29: s9 . F₈() = s . F₈() by A4, A25;
A30: s9 . F₇() = s . F₇() by A4, A25;
s999 . F₈() = s99 . F₈() by A5, Th35;
then H₁(s999) = j by A26, A30, A29, A28, A22;
then H₁(s999) + 1 = H₁(s) ;
hence H₁(F₆() . (s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())))) < H₁(s) by A21, A27, NAT_1:13; :: thesis: verum

end;

A31: for s being Element of Funcs (F₂(),INT) st S₁[s] holds
( S₁[F₆() . (s,(F₇() leq F₈()))] & ( F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₂[F₆() . (s,(F₇() leq F₈()))] ) & ( S₂[F₆() . (s,(F₇() leq F₈()))] implies F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) ) )

proof

let s be Element of Funcs (F₂(),INT); :: thesis: ( S₁[s] implies ( S₁[F₆() . (s,(F₇() leq F₈()))] & ( F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₂[F₆() . (s,(F₇() leq F₈()))] ) & ( S₂[F₆() . (s,(F₇() leq F₈()))] implies F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) ) ) )
A32: ( s . F₇() > s . F₈() implies (F₆() . (s,(F₇() leq F₈()))) . F₃() = 0 ) by Th35;
assume A33: S₁[s] ; :: thesis: ( S₁[F₆() . (s,(F₇() leq F₈()))] & ( F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₂[F₆() . (s,(F₇() leq F₈()))] ) & ( S₂[F₆() . (s,(F₇() leq F₈()))] implies F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) ) )
hence P₁[F₆() . (s,(F₇() leq F₈()))] by A3; :: thesis: ( ( F₁₀() . F₉() <= F₉() . F₈() implies ((F₆() . (s,(F₇() leq F₈()))) . F₇()) - 1 <= F₉() . F₈() ) & (F₆() . (s,(F₇() leq F₈()))) . F₈() = F₉() . F₈() & ( F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₂[F₆() . (s,(F₇() leq F₈()))] ) & ( S₂[F₆() . (s,(F₇() leq F₈()))] implies F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) ) )
A34: ( s . F₇() <= s . F₈() implies (F₆() . (s,(F₇() leq F₈()))) . F₃() = 1 ) by Th35;
(F₆() . (s,(F₇() leq F₈()))) . F₇() = s . F₇() by A5, Th35;
hence ( ( F₁₀() . F₉() <= F₉() . F₈() implies ((F₆() . (s,(F₇() leq F₈()))) . F₇()) - 1 <= F₉() . F₈() ) & (F₆() . (s,(F₇() leq F₈()))) . F₈() = F₉() . F₈() & ( F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) implies S₂[F₆() . (s,(F₇() leq F₈()))] ) & ( S₂[F₆() . (s,(F₇() leq F₈()))] implies F₆() . (s,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) ) ) by A5, A33, A32, A34, Th2, Th35; :: thesis: verum

end;

s2 . F₃() = 1 by A7, A12, A14, Th35;
then A35: ( F₆() . (s1,(F₇() leq F₈())) in (Funcs (F₂(),INT)) \ (F₃(),0) iff S₃[F₆() . (s1,(F₇() leq F₈()))] ) by A2, A3, A5, A12, A8, A14, Th35;
A36: F₆() iteration_terminates_for (F₄() \; (F₇() += 1)) \; (F₇() leq F₈()),F₆() . (s1,(F₇() leq F₈())) from AOFA_000:sch 3(A35, A20);
A37: ( S₁[F₆() . (s1,(while ((F₇() leq F₈()),(F₄() \; (F₇() += 1)))))] & not S₂[F₆() . (s1,(while ((F₇() leq F₈()),(F₄() \; (F₇() += 1)))))] ) from AOFA_000:sch 5(A11, A36, A15, A31);
then (F₆() . (F₉(),F₅())) . F₇() >= (F₉() . F₈()) + 1 by A10, INT_1:7;
then ((F₆() . (F₉(),F₅())) . F₇()) - 1 >= ((F₉() . F₈()) + 1) - 1 by XREAL_1:13;
then ((F₆() . (F₉(),F₅())) . F₇()) - 1 = F₉() . F₈() by A10, A14, A37, XXREAL_0:1;
hence ( P₁[F₆() . (F₉(),F₅())] & ( F₁₀() . F₉() <= F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = (F₉() . F₈()) + 1 ) & ( F₁₀() . F₉() > F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = F₁₀() . F₉() ) & (F₆() . (F₉(),F₅())) . F₈() = F₉() . F₈() ) by A1, A14, A37, AOFA_000:def 29; :: thesis: verum

end;

suppose A38: F₁₀() . F₉() > F₉() . F₈() ; :: thesis: ( P₁[F₆() . (F₉(),F₅())] & ( F₁₀() . F₉() <= F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = (F₉() . F₈()) + 1 ) & ( F₁₀() . F₉() > F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = F₁₀() . F₉() ) & (F₆() . (F₉(),F₅())) . F₈() = F₉() . F₈() )

then s2 . F₃() = 0 by A7, A12, Th35;
then s2 nin (Funcs (F₂(),INT)) \ (F₃(),0) by Th2;
hence ( P₁[F₆() . (F₉(),F₅())] & ( F₁₀() . F₉() <= F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = (F₉() . F₈()) + 1 ) & ( F₁₀() . F₉() > F₉() . F₈() implies (F₆() . (F₉(),F₅())) . F₇() = F₁₀() . F₉() ) & (F₆() . (F₉(),F₅())) . F₈() = F₉() . F₈() ) by A9, A8, A13, A10, A6, A38; :: thesis: verum

end;

end;