let il be Nat; :: thesis: SUCC (il,SCM+FSA) = {il,(il + 1)}
set X = { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } ;
set N = {il,(il + 1)};

now :: thesis: for x being object holds
( ( x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } implies x in {il,(il + 1)} ) & ( x in {il,(il + 1)} implies x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } ) )

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

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

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

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 Nat st i = goto i1 or ex i1 being Nat ex a being Int-Location st i = a =0_goto i1 or ex i1 being Nat 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:93;

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

then x in {il} \ (JUMP (halt SCM+FSA)) by A1, A3, AMISTD_1:2;
then x = il by TARSKI:def 1;
hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

suppose ex i1 being Nat st i = goto i1 ; :: thesis: x in {il,(il + 1)}

then consider i1 being Nat such that
A9: i = goto i1 ;
x in {i1} \ (JUMP i) by A1, A3, A9, Th33;
then x in {i1} \ {i1} by A9, Th34;
hence x in {il,(il + 1)} by XBOOLE_1:37; :: thesis: verum

end;

suppose ex i1 being Nat ex a being Int-Location st i = a =0_goto i1 ; :: thesis: x in {il,(il + 1)}

then consider i1 being Nat, a being Int-Location such that
A10: i = a =0_goto i1 ;
A11: NIC (i,il) = {i1,(il + 1)} by A10, Th35;
x in NIC (i,il) by A1, A3, XBOOLE_0:def 5;
then A12: ( x = i1 or x = il + 1 ) by A11, TARSKI:def 2;
x in (NIC (i,il)) \ {i1} by A1, A3, A10, Th36;
then not x in {i1} by XBOOLE_0:def 5;
hence x in {il,(il + 1)} by A12, TARSKI:def 1, TARSKI:def 2; :: thesis: verum

end;

suppose ex i1 being Nat ex a being Int-Location st i = a >0_goto i1 ; :: thesis: x in {il,(il + 1)}

then consider i1 being Nat, a being Int-Location such that
A13: i = a >0_goto i1 ;
A14: NIC (i,il) = {i1,(il + 1)} by A13, Th37;
x in NIC (i,il) by A1, A3, XBOOLE_0:def 5;
then A15: ( x = i1 or x = il + 1 ) by A14, TARSKI:def 2;
x in (NIC (i,il)) \ {i1} by A1, A3, A13, Th38;
then not x in {i1} by XBOOLE_0:def 5;
hence x in {il,(il + 1)} by A15, 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,(il + 1)}

then consider a, b being Int-Location, f being FinSeq-Location such that
A16: i = b := (f,a) ;
x in {(il + 1)} \ (JUMP (b := (f,a))) by A1, A3, A16, AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} 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,(il + 1)}

then consider a, b being Int-Location, f being FinSeq-Location such that
A17: i = (f,a) := b ;
x in {(il + 1)} \ (JUMP ((f,a) := b)) by A1, A3, A17, AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} 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,(il + 1)}

then consider a being Int-Location, f being FinSeq-Location such that
A18: i = a :=len f ;
x in {(il + 1)} \ (JUMP (a :=len f)) by A1, A3, A18, AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} 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,(il + 1)}

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

end;

end;

end;

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

per cases ( x = il or x = il + 1 ) by A20, TARSKI:def 2;

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

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

end;

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

set a = the Int-Location;
set i = AddTo ( the Int-Location, the Int-Location);
(NIC ((AddTo ( the Int-Location, the Int-Location)),il)) \ (JUMP (AddTo ( the Int-Location, the Int-Location))) = {(il + 1)} by AMISTD_1:12;
then A24: {(il + 1)} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } ;
x in {(il + 1)} by A23, TARSKI:def 1;
hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } by A24, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence SUCC (il,SCM+FSA) = {il,(il + 1)} by TARSKI:2; :: thesis: verum