let N be with_zero set ; :: thesis: for n being Nat

for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for s being State of S

for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let n be Nat; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for s being State of S

for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for s being State of S

for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let s be State of S; :: thesis: for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let I be Program of ; :: thesis: for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let P1, P2 be Instruction-Sequence of S; :: thesis: ( I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) implies for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m) )

assume A1: ( I c= P1 & I c= P2 ) ; :: thesis: ( ex m being Nat st

( m < n & not IC (Comput (P2,s,m)) in dom I ) or for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m) )

assume A2: for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ; :: thesis: for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

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

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

S_{1}[m + 1]
_{1}[ 0 ]
;

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

for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for s being State of S

for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let n be Nat; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for s being State of S

for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for s being State of S

for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let s be State of S; :: thesis: for I being Program of

for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let I be Program of ; :: thesis: for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

let P1, P2 be Instruction-Sequence of S; :: thesis: ( I c= P1 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) implies for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m) )

assume A1: ( I c= P1 & I c= P2 ) ; :: thesis: ( ex m being Nat st

( m < n & not IC (Comput (P2,s,m)) in dom I ) or for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m) )

assume A2: for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ; :: thesis: for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

defpred S

A3: for m being Nat st S

S

proof

A11:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A4: S_{1}[m]
; :: thesis: S_{1}[m + 1]

A5: Comput (P2,s,(m + 1)) = Following (P2,(Comput (P2,s,m))) by EXTPRO_1:3

.= Exec ((CurInstr (P2,(Comput (P2,s,m)))),(Comput (P2,s,m))) ;

A6: Comput (P1,s,(m + 1)) = Following (P1,(Comput (P1,s,m))) by EXTPRO_1:3

.= Exec ((CurInstr (P1,(Comput (P1,s,m)))),(Comput (P1,s,m))) ;

assume A7: m + 1 <= n ; :: thesis: Comput (P1,s,(m + 1)) = Comput (P2,s,(m + 1))

then m < n by NAT_1:13;

then A8: IC (Comput (P1,s,m)) = IC (Comput (P2,s,m)) by A4;

m < n by A7, NAT_1:13;

then A9: IC (Comput (P2,s,m)) in dom I by A2;

dom P2 = NAT by PARTFUN1:def 2;

then A10: IC (Comput (P2,s,m)) in dom P2 ;

dom P1 = NAT by PARTFUN1:def 2;

then IC (Comput (P1,s,m)) in dom P1 ;

then CurInstr (P1,(Comput (P1,s,m))) = P1 . (IC (Comput (P1,s,m))) by PARTFUN1:def 6

.= I . (IC (Comput (P1,s,m))) by A9, A8, A1, GRFUNC_1:2

.= P2 . (IC (Comput (P2,s,m))) by A9, A8, A1, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s,m))) by A10, PARTFUN1:def 6 ;

hence Comput (P1,s,(m + 1)) = Comput (P2,s,(m + 1)) by A4, A6, A5, A7, NAT_1:13; :: thesis: verum

end;assume A4: S

A5: Comput (P2,s,(m + 1)) = Following (P2,(Comput (P2,s,m))) by EXTPRO_1:3

.= Exec ((CurInstr (P2,(Comput (P2,s,m)))),(Comput (P2,s,m))) ;

A6: Comput (P1,s,(m + 1)) = Following (P1,(Comput (P1,s,m))) by EXTPRO_1:3

.= Exec ((CurInstr (P1,(Comput (P1,s,m)))),(Comput (P1,s,m))) ;

assume A7: m + 1 <= n ; :: thesis: Comput (P1,s,(m + 1)) = Comput (P2,s,(m + 1))

then m < n by NAT_1:13;

then A8: IC (Comput (P1,s,m)) = IC (Comput (P2,s,m)) by A4;

m < n by A7, NAT_1:13;

then A9: IC (Comput (P2,s,m)) in dom I by A2;

dom P2 = NAT by PARTFUN1:def 2;

then A10: IC (Comput (P2,s,m)) in dom P2 ;

dom P1 = NAT by PARTFUN1:def 2;

then IC (Comput (P1,s,m)) in dom P1 ;

then CurInstr (P1,(Comput (P1,s,m))) = P1 . (IC (Comput (P1,s,m))) by PARTFUN1:def 6

.= I . (IC (Comput (P1,s,m))) by A9, A8, A1, GRFUNC_1:2

.= P2 . (IC (Comput (P2,s,m))) by A9, A8, A1, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s,m))) by A10, PARTFUN1:def 6 ;

hence Comput (P1,s,(m + 1)) = Comput (P2,s,(m + 1)) by A4, A6, A5, A7, NAT_1:13; :: thesis: verum

thus for m being Nat holds S