let it1, it2 be Element of Fin Int-Locations ; :: thesis:

hereby :: thesis:

assume InsCode i in {1,2,3,4,5} ; :: thesis:
given a1, b1 being Int-Location such that A5: ( ( i = a1 := b1 or i = AddTo a1,b1 or i = SubFrom a1,b1 or i = MultBy a1,b1 or i = Divide a1,b1 ) & it1 = {a1,b1} ) ; :: thesis:
given a2, b2 being Int-Location such that A6: ( ( i = a2 := b2 or i = AddTo a2,b2 or i = SubFrom a2,b2 or i = MultBy a2,b2 or i = Divide a2,b2 ) & it2 = {a2,b2} ) ; :: thesis:
A7: ( ( i = AddTo a1,b1 or i = AddTo a2,b2 ) implies InsCode i = 2 ) by SCMFSA_2:43;
A8: ( ( i = SubFrom a1,b1 or i = SubFrom a2,b2 ) implies InsCode i = 3 ) by SCMFSA_2:44;
A9: ( ( i = MultBy a1,b1 or i = MultBy a2,b2 ) implies InsCode i = 4 ) by SCMFSA_2:45;
A10: ( ( i = Divide a1,b1 or i = Divide a2,b2 ) implies InsCode i = 5 ) by SCMFSA_2:46;

per cases by A5, A6, A7, A8, A9, A10, SCMFSA_2:42;

suppose ( i = a1 := b1 & i = a2 := b2 ) ; :: thesis:

then ( a1 = a2 & b1 = b2 ) by Th5;
hence it1 = it2 by A5, A6; :: thesis:

end;

suppose ( i = AddTo a1,b1 & i = AddTo a2,b2 ) ; :: thesis:

then ( a1 = a2 & b1 = b2 ) by Th6;
hence it1 = it2 by A5, A6; :: thesis:

end;

suppose ( i = SubFrom a1,b1 & i = SubFrom a2,b2 ) ; :: thesis:

then ( a1 = a2 & b1 = b2 ) by Th7;
hence it1 = it2 by A5, A6; :: thesis:

end;

suppose ( i = MultBy a1,b1 & i = MultBy a2,b2 ) ; :: thesis:

then ( a1 = a2 & b1 = b2 ) by Th8;
hence it1 = it2 by A5, A6; :: thesis:

end;

suppose ( i = Divide a1,b1 & i = Divide a2,b2 ) ; :: thesis:

then ( a1 = a2 & b1 = b2 ) by Th9;
hence it1 = it2 by A5, A6; :: thesis:

end;

hereby :: thesis:

assume ( InsCode i = 7 or InsCode i = 8 ) ; :: thesis:
given a1 being Int-Location , l1 being Instruction-Location of SCM+FSA such that A11: ( ( i = a1 =0_goto l1 or i = a1 >0_goto l1 ) & it1 = {a1} ) ; :: thesis:
given a2 being Int-Location , l2 being Instruction-Location of SCM+FSA such that A12: ( ( i = a2 =0_goto l2 or i = a2 >0_goto l2 ) & it2 = {a2} ) ; :: thesis:
A13: ( ( i = a1 >0_goto l1 or i = a2 >0_goto l2 ) implies InsCode i = 8 ) by SCMFSA_2:49;

per cases by A11, A12, A13, SCMFSA_2:48;

suppose ( i = a1 =0_goto l1 & i = a2 =0_goto l2 ) ; :: thesis:

hence it1 = it2 by A11, A12, Th11; :: thesis:

end;

suppose ( i = a1 >0_goto l1 & i = a2 >0_goto l2 ) ; :: thesis:

hence it1 = it2 by A11, A12, Th12; :: thesis:

end;

hereby :: thesis:

assume ( InsCode i = 9 or InsCode i = 10 ) ; :: thesis:
given a1, b1 being Int-Location , f1 being FinSeq-Location such that A14: ( ( i = b1 := f1,a1 or i = f1,a1 := b1 ) & it1 = {a1,b1} ) ; :: thesis:
given a2, b2 being Int-Location , f2 being FinSeq-Location such that A15: ( ( i = b2 := f2,a2 or i = f2,a2 := b2 ) & it2 = {a2,b2} ) ; :: thesis:
A16: ( ( i = f1,a1 := b1 or i = f2,a2 := b2 ) implies InsCode i = 10 ) by SCMFSA_2:51;

per cases by A14, A15, A16, SCMFSA_2:50;

suppose ( i = b1 := f1,a1 & i = b2 := f2,a2 ) ; :: thesis:

then ( a1 = a2 & b1 = b2 ) by Th13;
hence it1 = it2 by A14, A15; :: thesis:

end;

suppose ( i = f1,a1 := b1 & i = f2,a2 := b2 ) ; :: thesis:

then ( a1 = a2 & b1 = b2 ) by Th14;
hence it1 = it2 by A14, A15; :: thesis:

end;

hereby :: thesis:

assume ( InsCode i = 11 or InsCode i = 12 ) ; :: thesis:
given a1 being Int-Location , f1 being FinSeq-Location such that A17: ( ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) & it1 = {a1} ) ; :: thesis:
given a2 being Int-Location , f2 being FinSeq-Location such that A18: ( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {a2} ) ; :: thesis:
A19: ( ( i = f1 :=<0,...,0> a1 or i = f2 :=<0,...,0> a2 ) implies InsCode i = 12 ) by SCMFSA_2:53;

per cases by A17, A18, A19, SCMFSA_2:52;

suppose ( i = a1 :=len f1 & i = a2 :=len f2 ) ; :: thesis:

hence it1 = it2 by A17, A18, Th15; :: thesis:

end;

suppose ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ; :: thesis:

hence it1 = it2 by A17, A18, Th16; :: thesis:

end;

thus ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ; :: thesis: