set b = DataLoc ((F1() . F4()),F5());
set FR = for-down (F4(),F5(),F6(),F2());
defpred S1[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . (DataLoc ((F1() . F4()),F5())) <= $1 & t . F4() = F1() . F4() & P1[t] holds
( (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t))] );
A4:
S1[ 0 ]
proof
let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st t . (DataLoc ((F1() . F4()),F5())) <= 0 & t . F4() = F1() . F4() & P1[t] holds
( (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t))] )let Q be
Instruction-Sequence of
SCMPDS;
( t . (DataLoc ((F1() . F4()),F5())) <= 0 & t . F4() = F1() . F4() & P1[t] implies ( (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t))] ) )
assume that A5:
(
t . (DataLoc ((F1() . F4()),F5())) <= 0 &
t . F4()
= F1()
. F4() )
and A6:
P1[
t]
;
( (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t))] )
A7:
Initialize t = t
by MEMSTR_0:44;
hence
(IExec ((for-down (F4(),F5(),F6(),F2())),Q,t)) . (DataLoc ((F1() . F4()),F5())) <= 0
by A5, SCMPDS_7:47;
P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t))]
for
x being
Int_position holds
(IExec ((for-down (F4(),F5(),F6(),F2())),Q,t)) . x = t . x
by A5, A7, SCMPDS_7:47;
hence
P1[
Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),Q,t))]
by A6, Th4, A7;
verum
end;
A8:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A9:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
let u be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st u . (DataLoc ((F1() . F4()),F5())) <= k + 1 & u . F4() = F1() . F4() & P1[u] holds
( (IExec ((for-down (F4(),F5(),F6(),F2())),Q,u)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),Q,u))] )let U be
Instruction-Sequence of
SCMPDS;
( u . (DataLoc ((F1() . F4()),F5())) <= k + 1 & u . F4() = F1() . F4() & P1[u] implies ( (IExec ((for-down (F4(),F5(),F6(),F2())),U,u)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),U,u))] ) )
assume that A10:
u . (DataLoc ((F1() . F4()),F5())) <= k + 1
and A11:
u . F4()
= F1()
. F4()
and A12:
P1[
u]
;
( (IExec ((for-down (F4(),F5(),F6(),F2())),U,u)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),U,u))] )
per cases
( u . (DataLoc ((F1() . F4()),F5())) <= 0 or u . (DataLoc ((F1() . F4()),F5())) > 0 )
;
suppose
u . (DataLoc ((F1() . F4()),F5())) <= 0
;
( (IExec ((for-down (F4(),F5(),F6(),F2())),U,u)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),U,u))] )hence
(
(IExec ((for-down (F4(),F5(),F6(),F2())),U,u)) . (DataLoc ((F1() . F4()),F5())) <= 0 &
P1[
Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),U,u))] )
by A4, A11, A12;
verum end; suppose A13:
u . (DataLoc ((F1() . F4()),F5())) > 0
;
( (IExec ((for-down (F4(),F5(),F6(),F2())),U,u)) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),U,u))] )set Ad =
AddTo (
F4(),
F5(),
(- F6()));
set Iu =
IExec (
(F2() ';' (AddTo (F4(),F5(),(- F6())))),
U,
u);
A14:
(
(IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u)) . F4()
= F1()
. F4() &
P1[
Initialize (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u))] )
by A3, A11, A12, A13;
(IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u)) . (DataLoc ((F1() . F4()),F5())) = (u . (DataLoc ((F1() . F4()),F5()))) - F6()
by A3, A11, A12, A13;
then
((IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u)) . (DataLoc ((F1() . F4()),F5()))) + 1
<= u . (DataLoc ((F1() . F4()),F5()))
by A1, INT_1:7, XREAL_1:44;
then
((IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u)) . (DataLoc ((F1() . F4()),F5()))) + 1
<= k + 1
by A10, XXREAL_0:2;
then A15:
(IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u)) . (DataLoc ((F1() . F4()),F5())) <= k
by XREAL_1:6;
A16:
P1[
u]
by A12;
A17:
for
t being
0 -started State of
SCMPDS for
Q being
Instruction-Sequence of
SCMPDS st
P1[
t] &
t . F4()
= u . F4() &
t . (DataLoc ((u . F4()),F5())) > 0 holds
(
(IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4()
= t . F4() &
(IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((u . F4()),F5())) = (t . (DataLoc ((u . F4()),F5()))) - F6() &
F2()
is_closed_on t,
Q &
F2()
is_halting_on t,
Q &
P1[
Initialize (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
by A3, A11;
A18:
u . (DataLoc ((u . F4()),F5())) > 0
by A11, A13;
A19:
(Initialize (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u))) . (DataLoc ((F1() . F4()),F5())) = (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u)) . (DataLoc ((F1() . F4()),F5()))
by SCMPDS_5:15;
A20:
(Initialize (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u))) . F4()
= (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u)) . F4()
by SCMPDS_5:15;
IExec (
(for-down (F4(),F5(),F6(),F2())),
U,
u)
= IExec (
(for-down (F4(),F5(),F6(),F2())),
U,
(Initialize (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),U,u))))
from SCPISORT:sch 2(A1, A18, A16, A17);
hence
(
(IExec ((for-down (F4(),F5(),F6(),F2())),U,u)) . (DataLoc ((F1() . F4()),F5())) <= 0 &
P1[
Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),U,u))] )
by A9, A15, A14, A19, A20;
verum end; end;
end; end;
A21:
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A8);
per cases
( F1() . (DataLoc ((F1() . F4()),F5())) > 0 or F1() . (DataLoc ((F1() . F4()),F5())) <= 0 )
;
suppose
F1()
. (DataLoc ((F1() . F4()),F5())) > 0
;
( (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1())) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1()))] )then reconsider m =
F1()
. (DataLoc ((F1() . F4()),F5())) as
Element of
NAT by INT_1:3;
S1[
m]
by A21;
hence
(
(IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1())) . (DataLoc ((F1() . F4()),F5())) <= 0 &
P1[
Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1()))] )
by A2;
verum end; suppose
F1()
. (DataLoc ((F1() . F4()),F5())) <= 0
;
( (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1())) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1()))] )hence
(
(IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1())) . (DataLoc ((F1() . F4()),F5())) <= 0 &
P1[
Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1()))] )
by A2, A4;
verum end; end;