set S = Funcs F₂(),INT ;
set T = (Funcs F₂(),INT ) \ F₃(),0 ;
set C = F₇() leq F₈();
set II = F₄() \; (F₇() += 1);
Z0: ( F₆() is complying_with_catenation & F₆() complies_with_while_wrt (Funcs F₂(),INT ) \ F₃(),0 ) by AOFA_000:def 32;
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 ;
S1: ( s1 . F₇() = F₁₀() . F₉() & s1 . F₈() = F₉() . F₈() ) by D, Th111;
then S2: ( s2 . F₇() = F₁₀() . F₉() & s2 . F₈() = F₉() . F₈() ) by D, Th114;
Sn: F₆() . F₉(),F₅() = F₆() . s1,(while (F₇() leq F₈()),(F₄() \; (F₇() += 1))) by F, AOFA_000:def 29;
defpred S₁[ Element of Funcs F₂(),INT ] means $1 . F₇() <= $1 . F₈();
defpred S₂[ Element of Funcs F₂(),INT ] means ( P₁[$1] & ( F₁₀() . F₉() <= F₉() . F₈() implies ($1 . F₇()) - 1 <= F₉() . F₈() ) & $1 . F₈() = F₉() . F₈() );
(F₁₀() . F₉()) - 1 < F₁₀() . F₉() by XREAL_1:46;
then A1: S₂[s1] by A, S1, XXREAL_0:2;
A2: P₁[s2] by B, A;

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

suppose C1: 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 B': s2 . F₃() = 1 by S1, Th114;
defpred S₃[ Element of Funcs F₂(),INT ] means ( P₁[$1] & S₁[$1] );
BB: ( F₆() . s1,(F₇() leq F₈()) in (Funcs F₂(),INT ) \ F₃(),0 iff S₃[F₆() . s1,(F₇() leq F₈())] ) by A, B, C1, S2, B';
deffunc H₁( Element of Funcs F₂(),INT ) -> Element of NAT = In ((($1 . F₈()) + 1) - ($1 . F₇())),NAT ;
Ct: 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) ) )
assume 00: 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) )
reconsider s' = F₆() . s,F₄() as Element of Funcs F₂(),INT ;
reconsider s'' = F₆() . s',(F₇() += 1) as Element of Funcs F₂(),INT ;
reconsider s''' = F₆() . s'',(F₇() leq F₈()) as Element of Funcs F₂(),INT ;
01: ( F₆() . s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈())) = F₆() . (F₆() . s,(F₄() \; (F₇() += 1))),(F₇() leq F₈()) & s'' = F₆() . s,(F₄() \; (F₇() += 1)) ) by AOFA_000:def 29;
02: ( s''' . F₇() = s'' . F₇() & s''' . F₈() = s'' . F₈() & ( s'' . F₇() > s'' . F₈() implies s''' . F₃() = 0 ) & ( s'' . F₇() <= s'' . F₈() implies s''' . F₃() = 1 ) ) by D, Th114;
03: ( s' . F₇() = s . F₇() & s' . F₈() = s . F₈() ) by C, 00;
04: ( s'' . F₇() = (s' . F₇()) + 1 & s'' . F₈() = s' . F₈() & P₁[s''] ) by 00, 01, B, D, Th012;
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 01, 02, B, LemTS; :: thesis: H₁(F₆() . s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) < H₁(s)
reconsider j = (s . F₈()) - (s . F₇()) as Element of NAT by 00, INT_1:18;
H₁(s''') = j by 02, 03, 04, FUNCT_7:def 1;
then H₁(s''') + 1 = H₁(s) by FUNCT_7:def 1;
hence H₁(F₆() . s,((F₄() \; (F₇() += 1)) \; (F₇() leq F₈()))) < H₁(s) by 01, NAT_1:13; :: thesis: verum

end;

C': F₆() iteration_terminates_for (F₄() \; (F₇() += 1)) \; (F₇() leq F₈()),F₆() . s1,(F₇() leq F₈()) from AOFA_000:sch 3(BB, Ct);
D': 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 01: ( S₂[s] & s in (Funcs F₂(),INT ) \ F₃(),0 & S₁[s] ) ; :: thesis: S₂[F₆() . s,(F₄() \; (F₇() += 1))]
thus P₁[F₆() . s,(F₄() \; (F₇() += 1))] by B, 01; :: thesis: ( ( F₁₀() . F₉() <= F₉() . F₈() implies ((F₆() . s,(F₄() \; (F₇() += 1))) . F₇()) - 1 <= F₉() . F₈() ) & (F₆() . s,(F₄() \; (F₇() += 1))) . F₈() = F₉() . F₈() )
reconsider s' = F₆() . s,F₄() as Element of Funcs F₂(),INT ;
reconsider s'' = F₆() . s',(F₇() += 1) as Element of Funcs F₂(),INT ;
03: ( s' . F₇() = s . F₇() & s' . F₈() = s . F₈() & s'' . F₇() = (s' . F₇()) + 1 & s'' . F₈() = s' . F₈() ) by 01, C, D, Th012;
s'' = F₆() . s,(F₄() \; (F₇() += 1)) by AOFA_000:def 29;
hence ( ( F₁₀() . F₉() <= F₉() . F₈() implies ((F₆() . s,(F₄() \; (F₇() += 1))) . F₇()) - 1 <= F₉() . F₈() ) & (F₆() . s,(F₄() \; (F₇() += 1))) . F₈() = F₉() . F₈() ) by 01, 03; :: thesis: verum

end;

E': 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 ) ) )
assume 01: 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 B; :: 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 ) )
( (F₆() . s,(F₇() leq F₈())) . F₇() = s . F₇() & (F₆() . s,(F₇() leq F₈())) . F₈() = s . F₈() & ( s . F₇() > s . F₈() implies (F₆() . s,(F₇() leq F₈())) . F₃() = 0 ) & ( s . F₇() <= s . F₈() implies (F₆() . s,(F₇() leq F₈())) . F₃() = 1 ) ) by D, Th114;
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 01, LemTS; :: thesis: verum

end;

F': ( 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(A1, C', D', E');
then (F₆() . F₉(),F₅()) . F₇() >= (F₉() . F₈()) + 1 by Sn, INT_1:20;
then ((F₆() . F₉(),F₅()) . F₇()) - 1 >= ((F₉() . F₈()) + 1) - 1 by XREAL_1:15;
then ((F₆() . F₉(),F₅()) . F₇()) - 1 = F₉() . F₈() by C1, Sn, F', 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 C1, F, F', AOFA_000:def 29; :: thesis: verum

end;

suppose C2: 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 S1, Th114;
then s2 nin (Funcs F₂(),INT ) \ F₃(),0 by LemTS;
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 A2, C2, S2, Sn, Z0, AOFA_000:def 31; :: thesis: verum

end;

end;