let it1, it2 be Element of Fin Int-Locations; :: thesis: ( ( InsCode i in {1,2,3,4,5} & ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & it1 = {a,b} ) & ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ex a being Int-Location ex l being Nat st
( ( i = a =0_goto l or i = a >0_goto l ) & it1 = {a} ) & ex a being Int-Location ex l being Nat st
( ( i = a =0_goto l or i = a >0_goto l ) & it2 = {a} ) implies it1 = it2 ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & it1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( 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 ) )

hereby :: thesis: ( ( ( InsCode i = 7 or InsCode i = 8 ) & ex a being Int-Location ex l being Nat st
( ( i = a =0_goto l or i = a >0_goto l ) & it1 = {a} ) & ex a being Int-Location ex l being Nat st
( ( i = a =0_goto l or i = a >0_goto l ) & it2 = {a} ) implies it1 = it2 ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & it1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( 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 ) )
assume InsCode i in {1,2,3,4,5} ; :: thesis: ( ex a1, b1 being Int-Location st
( ( 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} ) & ex a2, b2 being Int-Location st
( ( 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} ) implies it1 = it2 )

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: ( ex a2, b2 being Int-Location st
( ( 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} ) implies it1 = it2 )

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: it1 = it2
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 ( ( i = a1 := b1 & i = a2 := b2 ) or ( i = AddTo (a1,b1) & i = AddTo (a2,b2) ) or ( i = SubFrom (a1,b1) & i = SubFrom (a2,b2) ) or ( i = MultBy (a1,b1) & i = MultBy (a2,b2) ) or ( i = Divide (a1,b1) & i = Divide (a2,b2) ) ) by ;
suppose A13: ( i = a1 := b1 & i = a2 := b2 ) ; :: thesis: it1 = it2
then a1 = a2 by Th1;
hence it1 = it2 by A6, A8, A13, Th1; :: thesis: verum
end;
suppose A14: ( i = AddTo (a1,b1) & i = AddTo (a2,b2) ) ; :: thesis: it1 = it2
then a1 = a2 by Th2;
hence it1 = it2 by A6, A8, A14, Th2; :: thesis: verum
end;
suppose A15: ( i = SubFrom (a1,b1) & i = SubFrom (a2,b2) ) ; :: thesis: it1 = it2
then a1 = a2 by Th3;
hence it1 = it2 by A6, A8, A15, Th3; :: thesis: verum
end;
suppose A16: ( i = MultBy (a1,b1) & i = MultBy (a2,b2) ) ; :: thesis: it1 = it2
then a1 = a2 by Th4;
hence it1 = it2 by A6, A8, A16, Th4; :: thesis: verum
end;
suppose A17: ( i = Divide (a1,b1) & i = Divide (a2,b2) ) ; :: thesis: it1 = it2
then a1 = a2 by Th5;
hence it1 = it2 by A6, A8, A17, Th5; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & it1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( 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 ) )
assume ( InsCode i = 7 or InsCode i = 8 ) ; :: thesis: ( ex a1 being Int-Location ex l1 being Nat st
( ( i = a1 =0_goto l1 or i = a1 >0_goto l1 ) & it1 = {a1} ) & ex a2 being Int-Location ex l2 being Nat st
( ( i = a2 =0_goto l2 or i = a2 >0_goto l2 ) & it2 = {a2} ) implies it1 = it2 )

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: ( ex a2 being Int-Location ex l2 being Nat st
( ( i = a2 =0_goto l2 or i = a2 >0_goto l2 ) & it2 = {a2} ) implies it1 = it2 )

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: it1 = it2
A22: ( ( i = a1 >0_goto l1 or i = a2 >0_goto l2 ) implies InsCode i = 8 ) by SCMFSA_2:25;
per cases ( ( i = a1 =0_goto l1 & i = a2 =0_goto l2 ) or ( i = a1 >0_goto l1 & i = a2 >0_goto l2 ) ) by ;
suppose ( i = a1 =0_goto l1 & i = a2 =0_goto l2 ) ; :: thesis: it1 = it2
hence it1 = it2 by ; :: thesis: verum
end;
suppose ( i = a1 >0_goto l1 & i = a2 >0_goto l2 ) ; :: thesis: it1 = it2
hence it1 = it2 by ; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( 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 ) )
assume ( InsCode i = 9 or InsCode i = 10 ) ; :: thesis: ( ex a1, b1 being Int-Location ex f1 being FinSeq-Location st
( ( i = b1 := (f1,a1) or i = (f1,a1) := b1 ) & it1 = {a1,b1} ) & ex a2, b2 being Int-Location ex f2 being FinSeq-Location st
( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {a2,b2} ) implies it1 = it2 )

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: ( ex a2, b2 being Int-Location ex f2 being FinSeq-Location st
( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {a2,b2} ) implies it1 = it2 )

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: it1 = it2
A27: ( ( i = (f1,a1) := b1 or i = (f2,a2) := b2 ) implies InsCode i = 10 ) by SCMFSA_2:27;
per cases ( ( i = b1 := (f1,a1) & i = b2 := (f2,a2) ) or ( i = (f1,a1) := b1 & i = (f2,a2) := b2 ) ) by ;
suppose A28: ( i = b1 := (f1,a1) & i = b2 := (f2,a2) ) ; :: thesis: it1 = it2
then a1 = a2 by Th9;
hence it1 = it2 by A24, A26, A28, Th9; :: thesis: verum
end;
suppose A29: ( i = (f1,a1) := b1 & i = (f2,a2) := b2 ) ; :: thesis: it1 = it2
then a1 = a2 by Th10;
hence it1 = it2 by ; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( 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 )
assume ( InsCode i = 11 or InsCode i = 12 ) ; :: thesis: ( ex a1 being Int-Location ex f1 being FinSeq-Location st
( ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) & it1 = {a1} ) & ex a2 being Int-Location ex f2 being FinSeq-Location st
( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {a2} ) implies it1 = it2 )

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: ( ex a2 being Int-Location ex f2 being FinSeq-Location st
( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {a2} ) implies it1 = it2 )

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: it1 = it2
A34: ( ( i = f1 :=<0,...,0> a1 or i = f2 :=<0,...,0> a2 ) implies InsCode i = 12 ) by SCMFSA_2:29;
per cases ( ( i = a1 :=len f1 & i = a2 :=len f2 ) or ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ) by ;
suppose ( i = a1 :=len f1 & i = a2 :=len f2 ) ; :: thesis: it1 = it2
hence it1 = it2 by ; :: thesis: verum
end;
suppose ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ; :: thesis: it1 = it2
hence it1 = it2 by ; :: thesis: verum
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: verum