let it1, it2 be Element of Fin FinSeq-Locations; :: 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 = {f} ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {f} ) 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 = {f} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {f} ) implies it1 = it2 ) & ( 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 = 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 = {f} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {f} ) implies it1 = it2 ) & ( 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 = {f1} ) & ex a2, b2 being Int-Location ex f2 being FinSeq-Location st
( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {f2} ) implies it1 = it2 )
given a1, b1 being Int-Location, f1 being FinSeq-Location such that A3: ( i = b1 := (f1,a1) or i = (f1,a1) := b1 ) and
A4: it1 = {f1} ; :: thesis: ( ex a2, b2 being Int-Location ex f2 being FinSeq-Location st
( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {f2} ) implies it1 = it2 )
given a2, b2 being Int-Location, f2 being FinSeq-Location such that A5: ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) and
A6: it2 = {f2} ; :: thesis: it1 = it2
A7: ( ( 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 A3, A5, A7, SCMFSA_2:26;
suppose ( i = b1 := (f1,a1) & i = b2 := (f2,a2) ) ; :: thesis: it1 = it2
hence it1 = it2 by A4, A6, Th9; :: thesis: verum
end;
suppose ( i = (f1,a1) := b1 & i = (f2,a2) := b2 ) ; :: thesis: it1 = it2
hence it1 = it2 by A4, A6, Th10; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( 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 = {f1} ) & ex a2 being Int-Location ex f2 being FinSeq-Location st
( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {f2} ) implies it1 = it2 )
given a1 being Int-Location, f1 being FinSeq-Location such that A8: ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) and
A9: it1 = {f1} ; :: thesis: ( ex a2 being Int-Location ex f2 being FinSeq-Location st
( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {f2} ) implies it1 = it2 )
given a2 being Int-Location, f2 being FinSeq-Location such that A10: ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) and
A11: it2 = {f2} ; :: thesis: it1 = it2
A12: ( ( 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 A8, A10, A12, SCMFSA_2:28;
suppose ( i = a1 :=len f1 & i = a2 :=len f2 ) ; :: thesis: it1 = it2
hence it1 = it2 by A9, A11, Th11; :: thesis: verum
end;
suppose ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ; :: thesis: it1 = it2
hence it1 = it2 by A9, A11, Th12; :: thesis: verum
end;
end;
end;
thus ( 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