let n be 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 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 ; :: 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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: for m being Nat st m <= n holds

Comput (P1,s1,m) = Comput (P2,s2,m)

defpred S_{1}[ Nat] means ( $1 <= n implies Comput (P1,s1,$1) = Comput (P2,s2,$1) );

A5: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]

then A11: S_{1}[ 0 ]
;

thus for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A11, A5); :: thesis: verum

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 ; :: 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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: for m being Nat st m <= n holds

Comput (P1,s1,m) = Comput (P2,s2,m)

defpred S

A5: for m being Nat st S

S

proof

Comput (P1,s1,0) = Comput (P2,s2,0)
by A1;
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A6: ( m <= n implies Comput (P1,s1,m) = Comput (P2,s2,m) ) ; :: thesis: S_{1}[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))

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; :: thesis: verum

end;assume A6: ( m <= n implies Comput (P1,s1,m) = Comput (P2,s2,m) ) ; :: thesis: S

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))

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; :: thesis: verum

then A11: S

thus for m being Nat holds S