let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N

for q being NAT -defined the InstructionsF of b_{1} -valued finite non halt-free Function

for p being non empty b_{2} -autonomic FinPartState of S

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let S be non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of S

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of S

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let p be non empty q -autonomic FinPartState of S; :: thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let s1, s2 be State of S; :: thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume that

A1: p c= s1 and

A2: p c= s2 ; :: thesis: for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let P1, P2 be Instruction-Sequence of S; :: thesis: ( q c= P1 & q c= P2 implies for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume that

A3: q c= P1 and

A4: q c= P2 ; :: thesis: for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

A5: dom q c= dom P1 by A3, RELAT_1:11;

A6: dom q c= dom P2 by A4, RELAT_1:11;

let i be Nat; :: thesis: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

set Cs2i = Comput (P2,s2,i);

set Cs1i = Comput (P1,s1,i);

A7: IC (Comput (P1,s1,i)) in dom q by A3, Def4, A1;

A8: IC (Comput (P2,s2,i)) in dom q by A4, Def4, A2;

thus A9: IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) :: thesis: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i)))

.= q . (IC (Comput (P1,s1,i))) by A7, A3, GRFUNC_1:2

.= P2 . (IC (Comput (P2,s2,i))) by A8, A4, A9, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s2,i))) by A8, A6, PARTFUN1:def 6 ; :: thesis: verum

for q being NAT -defined the InstructionsF of b

for p being non empty b

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let S be non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of S

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let p be non empty q -autonomic FinPartState of S; :: thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let s1, s2 be State of S; :: thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume that

A1: p c= s1 and

A2: p c= s2 ; :: thesis: for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

let P1, P2 be Instruction-Sequence of S; :: thesis: ( q c= P1 & q c= P2 implies for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume that

A3: q c= P1 and

A4: q c= P2 ; :: thesis: for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

A5: dom q c= dom P1 by A3, RELAT_1:11;

A6: dom q c= dom P2 by A4, RELAT_1:11;

let i be Nat; :: thesis: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

set Cs2i = Comput (P2,s2,i);

set Cs1i = Comput (P1,s1,i);

A7: IC (Comput (P1,s1,i)) in dom q by A3, Def4, A1;

A8: IC (Comput (P2,s2,i)) in dom q by A4, Def4, A2;

thus A9: IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) :: thesis: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i)))

proof

thus CurInstr (P1,(Comput (P1,s1,i))) =
P1 . (IC (Comput (P1,s1,i)))
by A7, A5, PARTFUN1:def 6
assume A10:
IC (Comput (P1,s1,i)) <> IC (Comput (P2,s2,i))
; :: thesis: contradiction

( ((Comput (P1,s1,i)) | (dom p)) . (IC ) = (Comput (P1,s1,i)) . (IC ) & ((Comput (P2,s2,i)) | (dom p)) . (IC ) = (Comput (P2,s2,i)) . (IC ) ) by Th6, FUNCT_1:49;

hence contradiction by A10, A3, A4, A1, A2, EXTPRO_1:def 10; :: thesis: verum

end;( ((Comput (P1,s1,i)) | (dom p)) . (IC ) = (Comput (P1,s1,i)) . (IC ) & ((Comput (P2,s2,i)) | (dom p)) . (IC ) = (Comput (P2,s2,i)) . (IC ) ) by Th6, FUNCT_1:49;

hence contradiction by A10, A3, A4, A1, A2, EXTPRO_1:def 10; :: thesis: verum

.= q . (IC (Comput (P1,s1,i))) by A7, A3, GRFUNC_1:2

.= P2 . (IC (Comput (P2,s2,i))) by A8, A4, A9, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s2,i))) by A8, A6, PARTFUN1:def 6 ; :: thesis: verum