let n be Element of NAT ; :: thesis: for I being Program of SCMPDS
for s1, s2 being State of SCMPDS st s1,s2 equal_outside NAT & I c= s1 & I c= s2 & ( for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s2),s2,m) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (ProgramPart s1),s1,m, Comput (ProgramPart s2),s2,m equal_outside NAT
let I be Program of SCMPDS ; :: thesis: for s1, s2 being State of SCMPDS st s1,s2 equal_outside NAT & I c= s1 & I c= s2 & ( for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s2),s2,m) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (ProgramPart s1),s1,m, Comput (ProgramPart s2),s2,m equal_outside NAT
let s1, s2 be State of SCMPDS ; :: thesis: ( s1,s2 equal_outside NAT & I c= s1 & I c= s2 & ( for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s2),s2,m) in dom I ) implies for m being Element of NAT st m <= n holds
Comput (ProgramPart s1),s1,m, Comput (ProgramPart s2),s2,m equal_outside NAT )
assume that
A1: s1,s2 equal_outside NAT and
A2: I c= s1 and
A3: I c= s2 and
A4: for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s2),s2,m) in dom I ; :: thesis: for m being Element of NAT st m <= n holds
Comput (ProgramPart s1),s1,m, Comput (ProgramPart s2),s2,m equal_outside NAT
defpred S₁[ Nat] means ( $1 <= n implies Comput (ProgramPart s1),s1,$1, Comput (ProgramPart s2),s2,$1 equal_outside NAT );
A5: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A6: ( m <= n implies Comput (ProgramPart s1),s1,m, Comput (ProgramPart s2),s2,m equal_outside NAT ) ; :: thesis: S₁[m + 1]
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,m) by AMI_1:123;
A7: Comput (ProgramPart s2),s2,(m + 1) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,m) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,m)),(Comput (ProgramPart s2),s2,m)),(Comput (ProgramPart s2),s2,m) by T ;
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,m) by AMI_1:123;
A8: Comput (ProgramPart s1),s1,(m + 1) = Following (ProgramPart s1),(Comput (ProgramPart s1),s1,m) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,m)),(Comput (ProgramPart s1),s1,m)),(Comput (ProgramPart s1),s1,m) by T ;
assume A9: m + 1 <= n ; :: thesis: Comput (ProgramPart s1),s1,(m + 1), Comput (ProgramPart s2),s2,(m + 1) equal_outside NAT
then A10: IC (Comput (ProgramPart s1),s1,m) = IC (Comput (ProgramPart s2),s2,m) by A6, COMPOS_1:24, NAT_1:13;
m < n by A9, NAT_1:13;
then A11: IC (Comput (ProgramPart s2),s2,m) in dom I by A4;
Y: (ProgramPart (Comput (ProgramPart s1),s1,m)) /. (IC (Comput (ProgramPart s1),s1,m)) = (Comput (ProgramPart s1),s1,m) . (IC (Comput (ProgramPart s1),s1,m)) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart s2),s2,m)) /. (IC (Comput (ProgramPart s2),s2,m)) = (Comput (ProgramPart s2),s2,m) . (IC (Comput (ProgramPart s2),s2,m)) by COMPOS_1:38;
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,m)),(Comput (ProgramPart s1),s1,m) = s1 . (IC (Comput (ProgramPart s1),s1,m)) by Y, AMI_1:54
.= I . (IC (Comput (ProgramPart s1),s1,m)) by A2, A11, A10, GRFUNC_1:8
.= s2 . (IC (Comput (ProgramPart s2),s2,m)) by A3, A11, A10, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart s2),s2,m)),(Comput (ProgramPart s2),s2,m) by Z, AMI_1:54 ;
hence Comput (ProgramPart s1),s1,(m + 1), Comput (ProgramPart s2),s2,(m + 1) equal_outside NAT by A6, A8, A7, A9, Th15, NAT_1:13; :: thesis: verum

end;

Comput (ProgramPart s1),s1,0 = s1 by AMI_1:13;
then A12: S₁[ 0 ] by A1, AMI_1:13;
thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A12, A5); :: thesis: verum