let p1, p2 be Instruction-Sequence of SCM+FSA; for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
let s1, s2 be State of SCM+FSA; for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
let a be read-write Int-Location; for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
let I be really-closed MacroInstruction of SCM+FSA ; ( ProperBodyWhile>0 a,I,s1,p1 & DataPart s1 = DataPart s2 implies for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k) )
assume that
A1:
ProperBodyWhile>0 a,I,s1,p1
and
A2:
DataPart s1 = DataPart s2
; for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
set WH = while>0 (a,I);
set ST2 = StepWhile>0 (a,I,p2,s2);
set PT2 = p2 +* (while>0 (a,I));
set ST1 = StepWhile>0 (a,I,p1,s1);
set PT1 = p1 +* (while>0 (a,I));
defpred S1[ Nat] means DataPart ((StepWhile>0 (a,I,p1,s1)) . $1) = DataPart ((StepWhile>0 (a,I,p2,s2)) . $1);
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
set ST1kI =
Initialize ((StepWhile>0 (a,I,p1,s1)) . k);
set PT1I =
(p1 +* (while>0 (a,I))) +* I;
set ST2kI =
Initialize ((StepWhile>0 (a,I,p2,s2)) . k);
set PT2I =
(p2 +* (while>0 (a,I))) +* I;
A4:
I c= (p1 +* (while>0 (a,I))) +* I
by FUNCT_4:25;
A5:
I c= (p2 +* (while>0 (a,I))) +* I
by FUNCT_4:25;
assume A6:
DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
;
S1[k + 1]
then A7:
((StepWhile>0 (a,I,p1,s1)) . k) . a = ((StepWhile>0 (a,I,p2,s2)) . k) . a
by SCMFSA_M:2;
per cases
( ((StepWhile>0 (a,I,p1,s1)) . k) . a <= 0 or ((StepWhile>0 (a,I,p1,s1)) . k) . a > 0 )
;
suppose A8:
((StepWhile>0 (a,I,p1,s1)) . k) . a <= 0
;
S1[k + 1]hence DataPart ((StepWhile>0 (a,I,p1,s1)) . (k + 1)) =
DataPart ((StepWhile>0 (a,I,p1,s1)) . k)
by Th31
.=
DataPart ((StepWhile>0 (a,I,p2,s2)) . (k + 1))
by A6, A7, A8, Th31
;
verum end; suppose A9:
((StepWhile>0 (a,I,p1,s1)) . k) . a > 0
;
S1[k + 1]A10:
I is_halting_on (StepWhile>0 (a,I,p1,s1)) . k,
p1 +* (while>0 (a,I))
by A1, A9;
then A11:
I is_halting_on (StepWhile>0 (a,I,p2,s2)) . k,
p2 +* (while>0 (a,I))
by A6, SCMFSA8B:5;
A12:
DataPart ((StepWhile>0 (a,I,p1,s1)) . (k + 1)) =
DataPart (Comput (((p1 +* (while>0 (a,I))) +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,p1,s1)) . k)),((LifeSpan (((p1 +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p1,s1)) . k)))) + 2)))
by SCMFSA_9:def 5
.=
DataPart (Comput (((p1 +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p1,s1)) . k)),(LifeSpan (((p1 +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p1,s1)) . k))))))
by A9, A10, Th30
;
A13:
DataPart ((StepWhile>0 (a,I,p2,s2)) . (k + 1)) =
DataPart (Comput (((p2 +* (while>0 (a,I))) +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,p2,s2)) . k)),((LifeSpan (((p2 +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p2,s2)) . k)))) + 2)))
by SCMFSA_9:def 5
.=
DataPart (Comput (((p2 +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p2,s2)) . k)),(LifeSpan (((p2 +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p2,s2)) . k))))))
by A7, A9, A11, Th30
;
A14:
DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart (Initialize ((StepWhile>0 (a,I,p1,s1)) . k))
by MEMSTR_0:79;
A15:
DataPart (Initialize ((StepWhile>0 (a,I,p1,s1)) . k)) =
DataPart ((StepWhile>0 (a,I,p1,s1)) . k)
by MEMSTR_0:79
.=
DataPart (Initialize ((StepWhile>0 (a,I,p2,s2)) . k))
by A6, MEMSTR_0:79
;
I is_halting_on Initialize ((StepWhile>0 (a,I,p1,s1)) . k),
(p1 +* (while>0 (a,I))) +* I
by A10, A14, SCMFSA8B:5;
then
LifeSpan (
((p1 +* (while>0 (a,I))) +* I),
(Initialize ((StepWhile>0 (a,I,p1,s1)) . k)))
= LifeSpan (
((p2 +* (while>0 (a,I))) +* I),
(Initialize ((StepWhile>0 (a,I,p2,s2)) . k)))
by A15, A4, A5, SCMFSA8C:18;
hence
S1[
k + 1]
by A12, A13, A15, A4, A5, SCMFSA8C:17;
verum end;
end;
DataPart ((StepWhile>0 (a,I,p1,s1)) . 0) =
DataPart s1
by SCMFSA_9:def 5
.=
DataPart ((StepWhile>0 (a,I,p2,s2)) . 0)
by A2, SCMFSA_9:def 5
;
then A16:
S1[ 0 ]
;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A16, A3); verum