hereby :: thesis: ( ( ( InsCode i = 7 or InsCode i = 8 ) implies ex b₁ being Element of Fin Int-Locations ex a being Int-Location ex l being Instruction-Location of SCM+FSA st
( ( i = a =0_goto l or i = a >0_goto l ) & b₁ = {a} ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b₁ 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₁ = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b₁ 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₁ = {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₁ being Element of Fin Int-Locations st 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 ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or 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:54, SCMFSA_2:55, SCMFSA_2:56, SCMFSA_2:57, SCMFSA_2:58;
reconsider a' = a, b' = b as Element of Int-Locations by SCMFSA_2:9;
reconsider IT = {.a',b'.} 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;

hereby :: thesis: ( ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b₁ 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₁ = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b₁ 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₁ = {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₁ being Element of Fin Int-Locations st 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 Instruction-Location of SCM+FSA st
( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )
then consider l being Instruction-Location of SCM+FSA , a being Int-Location such that
A2: ( i = a =0_goto l or i = a >0_goto l ) by SCMFSA_2:60, SCMFSA_2:61;
reconsider a' = a as Element of Int-Locations by SCMFSA_2:9;
reconsider IT = {.a'.} as Element of Fin Int-Locations ;
take IT = IT; :: thesis: ex a being Int-Location ex l being Instruction-Location of SCM+FSA st
( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} )
take a = a; :: thesis: ex l being Instruction-Location of SCM+FSA 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;

hereby :: thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b₁ 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₁ = {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₁ being Element of Fin Int-Locations st 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:62, SCMFSA_2:63;
reconsider a' = a, b' = b as Element of Int-Locations by SCMFSA_2:9;
reconsider IT = {.a',b'.} 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;

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₁ being Element of Fin Int-Locations st b₁ = {} )

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:64, SCMFSA_2:65;
reconsider a' = a as Element of Int-Locations by SCMFSA_2:9;
reconsider IT = {.a'.} 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;

{} in Fin Int-Locations by FINSUB_1:18;
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₁ being Element of Fin Int-Locations st b₁ = {} ) ; :: thesis: verum