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 ) and
A6: it1 = {a1,b1} ; :: thesis:
given a2, b2 being Int-Location such that A7: ( i = a2 := b2 or i = AddTo a2,b2 or i = SubFrom a2,b2 or i = MultBy a2,b2 or i = Divide a2,b2 ) and
A8: it2 = {a2,b2} ; :: thesis:
A9: ( ( i = AddTo a1,b1 or i = AddTo a2,b2 ) implies InsCode i = 2 ) by SCMFSA_2:43;
A10: ( ( i = Divide a1,b1 or i = Divide a2,b2 ) implies InsCode i = 5 ) by SCMFSA_2:46;
A11: ( ( i = MultBy a1,b1 or i = MultBy a2,b2 ) implies InsCode i = 4 ) by SCMFSA_2:45;
A12: ( ( i = SubFrom a1,b1 or i = SubFrom a2,b2 ) implies InsCode i = 3 ) by SCMFSA_2:44;

per cases by A5, A7, A9, A12, A11, A10, SCMFSA_2:42;

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

then a1 = a2 by Th5;
hence it1 = it2 by A6, A8, A13, Th5; :: thesis:

end;

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

then a1 = a2 by Th6;
hence it1 = it2 by A6, A8, A14, Th6; :: thesis:

end;

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

then a1 = a2 by Th7;
hence it1 = it2 by A6, A8, A15, Th7; :: thesis:

end;

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

then a1 = a2 by Th8;
hence it1 = it2 by A6, A8, A16, Th8; :: thesis:

end;

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

then a1 = a2 by Th9;
hence it1 = it2 by A6, A8, A17, Th9; :: thesis:

end;

end;

end;

hereby :: thesis:

assume ( InsCode i = 7 or InsCode i = 8 ) ; :: thesis:
given a1 being Int-Location , l1 being Element of NAT such that A18: ( i = a1 =0_goto l1 or i = a1 >0_goto l1 ) and
A19: it1 = {a1} ; :: thesis:
given a2 being Int-Location , l2 being Element of NAT such that A20: ( i = a2 =0_goto l2 or i = a2 >0_goto l2 ) and
A21: it2 = {a2} ; :: thesis:
A22: ( ( i = a1 >0_goto l1 or i = a2 >0_goto l2 ) implies InsCode i = 8 ) by SCMFSA_2:49;

per cases by A18, A20, A22, SCMFSA_2:48;

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

hence it1 = it2 by A19, A21, Th11; :: thesis:

end;

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

hence it1 = it2 by A19, A21, Th12; :: thesis:

end;

end;

end;

hereby :: thesis:

assume ( InsCode i = 9 or InsCode i = 10 ) ; :: thesis:
given a1, b1 being Int-Location , f1 being FinSeq-Location such that A23: ( i = b1 := f1,a1 or i = f1,a1 := b1 ) and
A24: it1 = {a1,b1} ; :: thesis:
given a2, b2 being Int-Location , f2 being FinSeq-Location such that A25: ( i = b2 := f2,a2 or i = f2,a2 := b2 ) and
A26: it2 = {a2,b2} ; :: thesis:
A27: ( ( i = f1,a1 := b1 or i = f2,a2 := b2 ) implies InsCode i = 10 ) by SCMFSA_2:51;

per cases by A23, A25, A27, SCMFSA_2:50;

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

then a1 = a2 by Th13;
hence it1 = it2 by A24, A26, A28, Th13; :: thesis:

end;

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

then a1 = a2 by Th14;
hence it1 = it2 by A24, A26, A29, Th14; :: thesis:

end;

end;

end;

hereby :: thesis:

assume ( InsCode i = 11 or InsCode i = 12 ) ; :: thesis:
given a1 being Int-Location , f1 being FinSeq-Location such that A30: ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) and
A31: it1 = {a1} ; :: thesis:
given a2 being Int-Location , f2 being FinSeq-Location such that A32: ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) and
A33: it2 = {a2} ; :: thesis:
A34: ( ( i = f1 :=<0,...,0> a1 or i = f2 :=<0,...,0> a2 ) implies InsCode i = 12 ) by SCMFSA_2:53;

per cases by A30, A32, A34, SCMFSA_2:52;

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

hence it1 = it2 by A31, A33, Th15; :: thesis:

end;

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

hence it1 = it2 by A31, A33, Th16; :: thesis:

end;

end;

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: