let il be Instruction-Location of SCM+FSA ; :: thesis: SUCC il = {il,(Next il)}
set X = { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } ;
set N = {il,(Next il)};

now

let x be set ; :: thesis: ( ( x in union { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } implies x in {il,(Next il)} ) & ( x in {il,(Next il)} implies b₁ in union { ((NIC b₂,il) \ (JUMP b₂)) where I is Element of the Instructions of SCM+FSA : verum } ) )

hereby :: thesis: ( x in {il,(Next il)} implies b₁ in union { ((NIC b₂,il) \ (JUMP b₂)) where I is Element of the Instructions of SCM+FSA : verum } )

assume x in union { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } ; :: thesis: x in {il,(Next il)}
then consider Y being set such that
A1: ( x in Y & Y in { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } ) by TARSKI:def 4;
consider i being Element of the Instructions of SCM+FSA such that
A2: Y = (NIC i,il) \ (JUMP i) by A1;

per cases ( i = [0 ,{} ] or ex a, b being Int-Location st i = a := b or ex a, b being Int-Location st i = AddTo a,b or ex a, b being Int-Location st i = SubFrom a,b or ex a, b being Int-Location st i = MultBy a,b or ex a, b being Int-Location st i = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st i = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st i = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st i = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st i = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st i = f,a := b or ex a being Int-Location ex f being FinSeq-Location st i = a :=len f or ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose i = [0 ,{} ] ; :: thesis: x in {il,(Next il)}

then x in {il} \ (JUMP (halt SCM+FSA )) by A1, A2, Th68, AMI_3:71, SCMFSA_2:123;
then x = il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Int-Location st i = a := b ; :: thesis: x in {il,(Next il)}

then consider a, b being Int-Location such that
A3: i = a := b ;
x in {(Next il)} \ (JUMP (a := b)) by A1, A2, A3, Th69;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Int-Location st i = AddTo a,b ; :: thesis: x in {il,(Next il)}

then consider a, b being Int-Location such that
A4: i = AddTo a,b ;
x in {(Next il)} \ (JUMP (AddTo a,b)) by A1, A2, A4, Th70;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Int-Location st i = SubFrom a,b ; :: thesis: x in {il,(Next il)}

then consider a, b being Int-Location such that
A5: i = SubFrom a,b ;
x in {(Next il)} \ (JUMP (SubFrom a,b)) by A1, A2, A5, Th71;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Int-Location st i = MultBy a,b ; :: thesis: x in {il,(Next il)}

then consider a, b being Int-Location such that
A6: i = MultBy a,b ;
x in {(Next il)} \ (JUMP (MultBy a,b)) by A1, A2, A6, Th72;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Int-Location st i = Divide a,b ; :: thesis: x in {il,(Next il)}

then consider a, b being Int-Location such that
A7: i = Divide a,b ;
x in {(Next il)} \ (JUMP (Divide a,b)) by A1, A2, A7, Th73;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA st i = goto i1 ; :: thesis: x in {il,(Next il)}

then consider i1 being Instruction-Location of SCM+FSA such that
A8: i = goto i1 ;
x in {i1} \ (JUMP i) by A1, A2, A8, Th74;
then x in {i1} \ {i1} by A8, Th75;
hence x in {il,(Next il)} by XBOOLE_1:37; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st i = a =0_goto i1 ; :: thesis: x in {il,(Next il)}

then consider i1 being Instruction-Location of SCM+FSA , a being Int-Location such that
A9: i = a =0_goto i1 ;
x in (NIC i,il) \ {i1} by A1, A2, A9, Th77;
then A10: ( x in NIC i,il & not x in {i1} ) by XBOOLE_0:def 5;
NIC i,il = {i1,(Next il)} by A9, Th76;
then ( x = i1 or x = Next il ) by A10, TARSKI:def 2;
hence x in {il,(Next il)} by A10, TARSKI:def 1, TARSKI:def 2; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st i = a >0_goto i1 ; :: thesis: x in {il,(Next il)}

then consider i1 being Instruction-Location of SCM+FSA , a being Int-Location such that
A11: i = a >0_goto i1 ;
x in (NIC i,il) \ {i1} by A1, A2, A11, Th79;
then A12: ( x in NIC i,il & not x in {i1} ) by XBOOLE_0:def 5;
NIC i,il = {i1,(Next il)} by A11, Th78;
then ( x = i1 or x = Next il ) by A12, TARSKI:def 2;
hence x in {il,(Next il)} by A12, TARSKI:def 1, TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st i = b := f,a ; :: thesis: x in {il,(Next il)}

then consider a, b being Int-Location , f being FinSeq-Location such that
A13: i = b := f,a ;
x in {(Next il)} \ (JUMP (b := f,a)) by A1, A2, A13, Th80;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st i = f,a := b ; :: thesis: x in {il,(Next il)}

then consider a, b being Int-Location , f being FinSeq-Location such that
A14: i = f,a := b ;
x in {(Next il)} \ (JUMP (f,a := b)) by A1, A2, A14, Th81;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st i = a :=len f ; :: thesis: x in {il,(Next il)}

then consider a being Int-Location , f being FinSeq-Location such that
A15: i = a :=len f ;
x in {(Next il)} \ (JUMP (a :=len f)) by A1, A2, A15, Th82;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a ; :: thesis: x in {il,(Next il)}

then consider a being Int-Location , f being FinSeq-Location such that
A16: i = f :=<0,...,0> a ;
x in {(Next il)} \ (JUMP (f :=<0,...,0> a)) by A1, A2, A16, Th83;
then x = Next il by TARSKI:def 1;
hence x in {il,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

assume A17: x in {il,(Next il)} ; :: thesis: b₁ in union { ((NIC b₂,il) \ (JUMP b₂)) where I is Element of the Instructions of SCM+FSA : verum }

per cases ( x = il or x = Next il ) by A17, TARSKI:def 2;

suppose A18: x = il ; :: thesis: b₁ in union { ((NIC b₂,il) \ (JUMP b₂)) where I is Element of the Instructions of SCM+FSA : verum }

set i = halt SCM+FSA ;
(NIC (halt SCM+FSA ),il) \ (JUMP (halt SCM+FSA )) = {il} by Th68;
then ( x in {il} & {il} in { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } ) by A18, TARSKI:def 1;
hence x in union { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } by TARSKI:def 4; :: thesis: verum

end;

suppose A19: x = Next il ; :: thesis: b₁ in union { ((NIC b₂,il) \ (JUMP b₂)) where I is Element of the Instructions of SCM+FSA : verum }

consider a, b being Int-Location ;
set i = AddTo a,b;
(NIC (AddTo a,b),il) \ (JUMP (AddTo a,b)) = {(Next il)} by Th70;
then ( x in {(Next il)} & {(Next il)} in { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } ) by A19, TARSKI:def 1;
hence x in union { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of SCM+FSA : verum } by TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence SUCC il = {il,(Next il)} by TARSKI:2; :: thesis: verum