let n be Element of NAT ; :: thesis: 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 Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let I be Program of ; :: thesis: 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 Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let s1, s2 be State of SCMPDS; :: thesis: for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: ( s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) implies for m being Element of 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 Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ; :: thesis: for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
defpred S₁[ Nat] means ( $1 <= n implies Comput (P1,s1,$1) = Comput (P2,s2,$1) );
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 (P1,s1,m) = Comput (P2,s2,m) ) ; :: thesis: S₁[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 ; :: thesis: Comput (P1,s1,(m + 1)) = Comput (P2,s2,(m + 1))
then A10: IC (Comput (P1,s1,m)) = IC (Comput (P2,s2,m)) by A6, NAT_1:13;
m < n by A9, NAT_1:13;
then A11: IC (Comput (P2,s2,m)) in dom I by A4;
A12: P1 /. (IC (Comput (P1,s1,m))) = P1 . (IC (Comput (P1,s1,m))) by PBOOLE:143;
A13: P2 /. (IC (Comput (P2,s2,m))) = P2 . (IC (Comput (P2,s2,m))) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,m))) = P1 . (IC (Comput (P1,s1,m))) by A12
.= I . (IC (Comput (P1,s1,m))) by A2, A11, A10, GRFUNC_1:2
.= P2 . (IC (Comput (P2,s2,m))) by A3, A11, A10, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,m))) by A13 ;
hence Comput (P1,s1,(m + 1)) = Comput (P2,s2,(m + 1)) by A6, A8, A7, A9, NAT_1:13; :: thesis: verum

end;

Comput (P1,s1,0) = s1 by EXTPRO_1:2;
then A14: S₁[ 0 ] by A1, EXTPRO_1:2;
thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A14, A5); :: thesis: verum