let n be Nat; for I being Program of
for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Nat st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Nat st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let I be Program of ; for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Nat st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Nat st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let s1, s2 be State of SCMPDS; for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Nat st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Nat st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let P1, P2 be Instruction-Sequence of SCMPDS; ( s1 = s2 & I c= P1 & I c= P2 & ( for m being Nat st m < n holds
IC (Comput (P2,s2,m)) in dom I ) implies for m being Nat st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m) )
assume that
A1:
s1 = s2
and
A2:
I c= P1
and
A3:
I c= P2
and
A4:
for m being Nat st m < n holds
IC (Comput (P2,s2,m)) in dom I
; for m being Nat st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
defpred S1[ Nat] means ( $1 <= n implies Comput (P1,s1,$1) = Comput (P2,s2,$1) );
A5:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A6:
(
m <= n implies
Comput (
P1,
s1,
m)
= Comput (
P2,
s2,
m) )
;
S1[m + 1]
A7:
Comput (
P2,
s2,
(m + 1)) =
Following (
P2,
(Comput (P2,s2,m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (P2,(Comput (P2,s2,m)))),
(Comput (P2,s2,m)))
;
A8:
Comput (
P1,
s1,
(m + 1)) =
Following (
P1,
(Comput (P1,s1,m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (P1,(Comput (P1,s1,m)))),
(Comput (P1,s1,m)))
;
assume A9:
m + 1
<= n
;
Comput (P1,s1,(m + 1)) = Comput (P2,s2,(m + 1))
A10:
IC (Comput (P2,s2,m)) in dom I
by A4, A9, NAT_1:13;
CurInstr (
P1,
(Comput (P1,s1,m))) =
P1 . (IC (Comput (P1,s1,m)))
by PBOOLE:143
.=
I . (IC (Comput (P1,s1,m)))
by A2, A10, A9, A6, GRFUNC_1:2, NAT_1:13
.=
P2 . (IC (Comput (P2,s2,m)))
by A3, A10, A9, A6, GRFUNC_1:2, NAT_1:13
.=
CurInstr (
P2,
(Comput (P2,s2,m)))
by PBOOLE:143
;
hence
Comput (
P1,
s1,
(m + 1))
= Comput (
P2,
s2,
(m + 1))
by A6, A8, A7, A9, NAT_1:13;
verum
end;
Comput (P1,s1,0) = Comput (P2,s2,0)
by A1;
then A11:
S1[ 0 ]
;
thus
for m being Nat holds S1[m]
from NAT_1:sch 2(A11, A5); verum