let N be non empty with_non-empty_elements set ; :: thesis: for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic Exec-preserving AMI-Struct of N
for s1, s2 being State of S
for I being Program of N
for P1, P2 being the Instructions of b₂ -valued ManySortedSet of NAT st I c= P1 & I c= P2 & NPP s1 = NPP s2 & ( 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
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))
let n be Element of NAT ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic Exec-preserving AMI-Struct of N
for s1, s2 being State of S
for I being Program of N
for P1, P2 being the Instructions of b₁ -valued ManySortedSet of NAT st I c= P1 & I c= P2 & NPP s1 = NPP s2 & ( 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
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))
let S be non empty stored-program IC-Ins-separated definite realistic Exec-preserving AMI-Struct of N; :: thesis: for s1, s2 being State of S
for I being Program of N
for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st I c= P1 & I c= P2 & NPP s1 = NPP s2 & ( 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
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))
let s1, s2 be State of S; :: thesis: for I being Program of N
for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st I c= P1 & I c= P2 & NPP s1 = NPP s2 & ( 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
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))
let I be Program of N; :: thesis: for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st I c= P1 & I c= P2 & NPP s1 = NPP s2 & ( 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
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))
let P1, P2 be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( I c= P1 & I c= P2 & NPP s1 = NPP s2 & ( 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
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m)) )
assume A1: ( I c= P1 & I c= P2 ) ; :: thesis: ( not NPP s1 = NPP s2 or ex m being Element of NAT st
( m < n & not IC (Comput (P2,s2,m)) in dom I ) or for m being Element of NAT st m <= n holds
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m)) )
assume that
A2: NPP s1 = NPP s2 and
A3: 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
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))
defpred S₁[ Nat] means ( $1 <= n implies NPP (Comput (P1,s1,$1)) = NPP (Comput (P2,s2,$1)) );
A4: 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 A5: S₁[m] ; :: thesis: S₁[m + 1]
A6: Comput (P2,s2,(m + 1)) = Following (P2,(Comput (P2,s2,m))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s2,m)))),(Comput (P2,s2,m))) ;
A7: Comput (P1,s1,(m + 1)) = Following (P1,(Comput (P1,s1,m))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,m)))),(Comput (P1,s1,m))) ;
assume A8: m + 1 <= n ; :: thesis: NPP (Comput (P1,s1,(m + 1))) = NPP (Comput (P2,s2,(m + 1)))
then m < n by NAT_1:13;
then A9: IC (Comput (P1,s1,m)) = IC (Comput (P2,s2,m)) by A5, COMPOS_1:230;
m < n by A8, NAT_1:13;
then A10: IC (Comput (P2,s2,m)) in dom I by A3;
dom P2 = NAT by PARTFUN1:def 4;
then A11: IC (Comput (P2,s2,m)) in dom P2 ;
dom P1 = NAT by PARTFUN1:def 4;
then IC (Comput (P1,s1,m)) in dom P1 ;
then CurInstr (P1,(Comput (P1,s1,m))) = P1 . (IC (Comput (P1,s1,m))) by PARTFUN1:def 8
.= I . (IC (Comput (P1,s1,m))) by A10, A9, GRFUNC_1:8, A1
.= P2 . (IC (Comput (P2,s2,m))) by A10, A9, GRFUNC_1:8, A1
.= CurInstr (P2,(Comput (P2,s2,m))) by A11, PARTFUN1:def 8 ;
hence NPP (Comput (P1,s1,(m + 1))) = NPP (Comput (P2,s2,(m + 1))) by A5, A7, A6, A8, NAT_1:13, Def20; :: thesis: verum

end;

Comput (P1,s1,0) = s1 by EXTPRO_1:3;
then A12: S₁[ 0 ] by A2, EXTPRO_1:3;
thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A12, A4); :: thesis: verum