set b = DataLoc ((F2() . F5()),F6());
set WHL = while<>0 (F5(),F6(),F4());
defpred S1[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st F1(t) <= $1 & t . F5() = F2() . F5() & P1[t] holds
( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t))] );
A4: S1[ 0 ]
proof
let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st F1(t) <= 0 & t . F5() = F2() . F5() & P1[t] holds
( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t))] )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( F1(t) <= 0 & t . F5() = F2() . F5() & P1[t] implies ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t))] ) )
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: F1(t) <= 0 and
A7: t . F5() = F2() . F5() and
A8: P1[t] ; :: thesis: ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t))] )
A9: F1(t) = 0 by A6;
then t . (DataLoc ((t . F5()),F6())) = 0 by A1, A7, A8;
then for b being Int_position holds (IExec ((while<>0 (F5(),F6(),F4())),Q,t)) . b = t . b by Th15, A5;
hence ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),Q,t))] ) by A8, A9, A5, SCPISORT:4; :: thesis: verum
end;
A10: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for u being 0 -started State of SCMPDS
for U being Instruction-Sequence of SCMPDS st F1(u) <= k + 1 & u . F5() = F2() . F5() & P1[u] holds
( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),U,u)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),U,u))] )
let u be 0 -started State of SCMPDS; :: thesis: for U being Instruction-Sequence of SCMPDS st F1(u) <= k + 1 & u . F5() = F2() . F5() & P1[u] holds
( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),b3,b2)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),b3,b2))] )
let U be Instruction-Sequence of SCMPDS; :: thesis: ( F1(u) <= k + 1 & u . F5() = F2() . F5() & P1[u] implies ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1))] ) )
assume that
A12: F1(u) <= k + 1 and
A13: u . F5() = F2() . F5() and
A14: P1[u] ; :: thesis: ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1))] )
per cases ( F1(u) = 0 or F1(u) <> 0 ) ;
suppose F1(u) = 0 ; :: thesis: ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1))] )
hence ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),U,u)))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),U,u))] ) by A4, A13, A14; :: thesis: verum
end;
suppose A15: F1(u) <> 0 ; :: thesis: ( H1( Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),b2,b1))] )
set Iu = IExec (F4(),U,u);
A16: u . (DataLoc ((F2() . F5()),F6())) <> 0 by A1, A14, A15;
then A17: ( (IExec (F4(),U,u)) . F5() = F2() . F5() & P1[ Initialize (IExec (F4(),U,u))] ) by A3, A13, A14;
deffunc H1( State of SCMPDS) -> Element of NAT = F1($1);
A18: P1[u] by A14;
A19: for t being 0 -started State of SCMPDS st P1[t] & H1(t) = 0 holds
t . (DataLoc ((u . F5()),F6())) = 0 by A1, A13;
H1( Initialize (IExec (F4(),U,u))) < H1(u) by A3, A13, A14, A16;
then H1( Initialize (IExec (F4(),U,u))) + 1 <= H1(u) by INT_1:7;
then H1( Initialize (IExec (F4(),U,u))) + 1 <= k + 1 by A12, XXREAL_0:2;
then A20: H1( Initialize (IExec (F4(),U,u))) <= k by XREAL_1:6;
A21: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = u . F5() & t . (DataLoc ((u . F5()),F6())) <> 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & H1( Initialize (IExec (F4(),Q,t))) < H1(t) & P1[ Initialize (IExec (F4(),Q,t))] ) by A3, A13;
A22: u . (DataLoc ((u . F5()),F6())) <> 0 by A1, A13, A14, A15;
A23: IExec ((while<>0 (F5(),F6(),F4())),U,u) = IExec ((while<>0 (F5(),F6(),F4())),U,(Initialize (IExec (F4(),U,u)))) from SCPINVAR:sch 4(A22, A19, A18, A21);
 (Initialize (IExec (F4(),U,u))) . F5() = (IExec (F4(),U,u)) . F5() by SCMPDS_5:15;
hence ( H1( Initialize (IExec ((while<>0 (F5(),F6(),F4())),U,u))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),U,u))] ) by A11, A20, A17, A23; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A10);
 then S1[F1(F2())] ;
hence ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),F3(),F2())))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),F3(),F2()))] ) by A2; :: thesis: verum