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:19;
A10: ( ( i = Divide (a1,b1) or i = Divide (a2,b2) ) implies InsCode i = 5 ) by SCMFSA_2:22;
A11: ( ( i = MultBy (a1,b1) or i = MultBy (a2,b2) ) implies InsCode i = 4 ) by SCMFSA_2:21;
A12: ( ( i = SubFrom (a1,b1) or i = SubFrom (a2,b2) ) implies InsCode i = 3 ) by SCMFSA_2:20;

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

hereby :: thesis:

assume ( InsCode i = 7 or InsCode i = 8 ) ; :: thesis:
given a1 being Int-Location, l1 being 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 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:25;

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

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

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

end;

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

hence it1 = it2 by A19, A21, Th8; :: 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:27;

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

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

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

end;

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

then a1 = a2 by Th10;
hence it1 = it2 by A24, A26, A29, Th10; :: 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:29;

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

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

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

end;

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

hence it1 = it2 by A31, A33, Th12; :: 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: