hereby :: thesis: ( ( ( InsCode i = 7 or InsCode i = 8 ) implies ex b_{1} being Element of Fin Int-Locations ex a being Int-Location ex l being Nat st

( ( i = a =0_goto l or i = a >0_goto l ) & b_{1} = {a} ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b_{1} being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b_{1} = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b_{1} being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{1} = {a} ) ) & ( 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 ex b_{1} being Element of Fin Int-Locations st b_{1} = {} ) )

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

assume
InsCode i in {1,2,3,4,5}
; :: thesis: ex IT being Element of Fin Int-Locations 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) ) & IT = {a,b} )

then not not InsCode i = 1 & ... & not InsCode i = 5 by ENUMSET1:def 3;

then consider a, b being Int-Location such that

A1: ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) by SCMFSA_2:30, SCMFSA_2:31, SCMFSA_2:32, SCMFSA_2:33, SCMFSA_2:34;

reconsider a9 = a, b9 = b as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9,b9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: 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) ) & IT = {a,b} )

take a = a; :: thesis: ex 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) ) & IT = {a,b} )

take b = b; :: thesis: ( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & IT = {a,b} )

thus ( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & IT = {a,b} ) by A1; :: thesis: verum

end;( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & IT = {a,b} )

then not not InsCode i = 1 & ... & not InsCode i = 5 by ENUMSET1:def 3;

then consider a, b being Int-Location such that

A1: ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) by SCMFSA_2:30, SCMFSA_2:31, SCMFSA_2:32, SCMFSA_2:33, SCMFSA_2:34;

reconsider a9 = a, b9 = b as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9,b9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: 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) ) & IT = {a,b} )

take a = a; :: thesis: ex 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) ) & IT = {a,b} )

take b = b; :: thesis: ( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & IT = {a,b} )

thus ( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & IT = {a,b} ) by A1; :: thesis: verum

hereby :: thesis: ( ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b_{1} being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b_{1} = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b_{1} being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{1} = {a} ) ) & ( 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 ex b_{1} being Element of Fin Int-Locations st b_{1} = {} ) )

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

assume
( InsCode i = 7 or InsCode i = 8 )
; :: thesis: ex IT being Element of Fin Int-Locations ex a being Int-Location ex l being Nat st

( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

then consider l being Nat, a being Int-Location such that

A2: ( i = a =0_goto l or i = a >0_goto l ) by SCMFSA_2:36, SCMFSA_2:37;

reconsider a9 = a as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: ex a being Int-Location ex l being Nat st

( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

take a = a; :: thesis: ex l being Nat st

( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

take l = l; :: thesis: ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

thus ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} ) by A2; :: thesis: verum

end;( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

then consider l being Nat, a being Int-Location such that

A2: ( i = a =0_goto l or i = a >0_goto l ) by SCMFSA_2:36, SCMFSA_2:37;

reconsider a9 = a as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: ex a being Int-Location ex l being Nat st

( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

take a = a; :: thesis: ex l being Nat st

( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

take l = l; :: thesis: ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )

thus ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} ) by A2; :: thesis: verum

hereby :: thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b_{1} being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{1} = {a} ) ) & ( 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 ex b_{1} being Element of Fin Int-Locations st b_{1} = {} ) )

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

assume
( InsCode i = 9 or InsCode i = 10 )
; :: thesis: ex IT being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

then consider a, b being Int-Location, f being FinSeq-Location such that

A3: ( i = b := (f,a) or i = (f,a) := b ) by SCMFSA_2:38, SCMFSA_2:39;

reconsider a9 = a, b9 = b as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9,b9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

take a = a; :: thesis: ex b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

take b = b; :: thesis: ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

take f = f; :: thesis: ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

thus ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) by A3; :: thesis: verum

end;( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

then consider a, b being Int-Location, f being FinSeq-Location such that

A3: ( i = b := (f,a) or i = (f,a) := b ) by SCMFSA_2:38, SCMFSA_2:39;

reconsider a9 = a, b9 = b as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9,b9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

take a = a; :: thesis: ex b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

take b = b; :: thesis: ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

take f = f; :: thesis: ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} )

thus ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) by A3; :: thesis: verum

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 ex b_{1} being Element of Fin Int-Locations st b_{1} = {} )

{} in Fin Int-Locations
by FINSUB_1:7;assume
( InsCode i = 11 or InsCode i = 12 )
; :: thesis: ex IT being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

then consider a being Int-Location, f being FinSeq-Location such that

A4: ( i = a :=len f or i = f :=<0,...,0> a ) by SCMFSA_2:40, SCMFSA_2:41;

reconsider a9 = a as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

take a = a; :: thesis: ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

take f = f; :: thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

thus ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} ) by A4; :: thesis: verum

end;( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

then consider a being Int-Location, f being FinSeq-Location such that

A4: ( i = a :=len f or i = f :=<0,...,0> a ) by SCMFSA_2:40, SCMFSA_2:41;

reconsider a9 = a as Element of Int-Locations by AMI_2:def 16;

reconsider IT = {.a9.} as Element of Fin Int-Locations ;

take IT = IT; :: thesis: ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

take a = a; :: thesis: ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

take f = f; :: thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} )

thus ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} ) by A4; :: thesis: verum

hence ( 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 ex b