let R be good Ring; :: thesis: for il being Element of NAT holds SUCC il,(SCM R) = {il,(succ il)}
let il be Element of NAT ; :: thesis: SUCC il,(SCM R) = {il,(succ il)}
set X = { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of (SCM R) : verum } ;
set N = {il,(succ il)};

now

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

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

assume x in union { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of (SCM R) : verum } ; :: thesis: x in {il,(succ il)}
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 Instructions of (SCM R) : verum } by TARSKI:def 4;
consider i being Element of the Instructions of (SCM R) such that
A3: Y = (NIC i,il) \ (JUMP i) by A2;

per cases ( i = [0 ,{} ] or ex a, b being Data-Location of R st i = a := b or ex a, b being Data-Location of R st i = AddTo a,b or ex a, b being Data-Location of R st i = SubFrom a,b or ex a, b being Data-Location of R st i = MultBy a,b or ex i1 being Element of NAT st i = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st i = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st i = a := r ) by SCMRING2:8;

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

then i = halt (SCM R) by SCMRING2:30;
then x in {il} \ (JUMP (halt (SCM R))) by A1, A3, Th53;
then x = il by TARSKI:def 1;
hence x in {il,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st i = a := b ; :: thesis: x in {il,(succ il)}

then consider a, b being Data-Location of R such that
A4: i = a := b ;
x in {(succ il)} \ (JUMP (a := b)) by A1, A3, A4, Th54;
then x = succ il by TARSKI:def 1;
hence x in {il,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st i = AddTo a,b ; :: thesis: x in {il,(succ il)}

then consider a, b being Data-Location of R such that
A5: i = AddTo a,b ;
x in {(succ il)} \ (JUMP (AddTo a,b)) by A1, A3, A5, Th55;
then x = succ il by TARSKI:def 1;
hence x in {il,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st i = SubFrom a,b ; :: thesis: x in {il,(succ il)}

then consider a, b being Data-Location of R such that
A6: i = SubFrom a,b ;
x in {(succ il)} \ (JUMP (SubFrom a,b)) by A1, A3, A6, Th56;
then x = succ il by TARSKI:def 1;
hence x in {il,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st i = MultBy a,b ; :: thesis: x in {il,(succ il)}

then consider a, b being Data-Location of R such that
A7: i = MultBy a,b ;
x in {(succ il)} \ (JUMP (MultBy a,b)) by A1, A3, A7, Th57;
then x = succ il by TARSKI:def 1;
hence x in {il,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

suppose ex i1 being Element of NAT st i = goto i1,R ; :: thesis: x in {il,(succ il)}

then consider i1 being Element of NAT such that
A8: i = goto i1,R ;
x in {i1} \ (JUMP i) by A1, A3, A8, Th59;
then x in {i1} \ {i1} by A8, Th60;
hence x in {il,(succ il)} by XBOOLE_1:37; :: thesis: verum

end;

suppose ex a being Data-Location of R ex i1 being Element of NAT st i = a =0_goto i1 ; :: thesis: x in {il,(succ il)}

then consider a being Data-Location of R, i1 being Element of NAT such that
A9: i = a =0_goto i1 ;
A10: NIC i,il c= {i1,(succ il)} by A9, Th61;
x in NIC i,il by A1, A3, XBOOLE_0:def 5;
then A11: ( x = i1 or x = succ il ) by A10, TARSKI:def 2;
x in (NIC i,il) \ {i1} by A1, A3, A9, Th63;
then not x in {i1} by XBOOLE_0:def 5;
hence x in {il,(succ il)} by A11, TARSKI:def 1, TARSKI:def 2; :: thesis: verum

end;

suppose ex a being Data-Location of R ex r being Element of R st i = a := r ; :: thesis: x in {il,(succ il)}

then consider a being Data-Location of R, r being Element of R such that
A12: i = a := r ;
x in {(succ il)} \ (JUMP (a := r)) by A1, A3, A12, Th58;
then x = succ il by TARSKI:def 1;
hence x in {il,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

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

per cases ( x = il or x = succ il ) by A13, TARSKI:def 2;

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

set i = halt (SCM R);
(NIC (halt (SCM R)),il) \ (JUMP (halt (SCM R))) = {il} by Th53;
then A15: {il} in { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of (SCM R) : verum } ;
x in {il} by A14, TARSKI:def 1;
hence x in union { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of (SCM R) : verum } by A15, TARSKI:def 4; :: thesis: verum

end;

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

consider a, b being Data-Location of R;
set i = AddTo a,b;
(NIC (AddTo a,b),il) \ (JUMP (AddTo a,b)) = {(succ il)} by Th55;
then A17: {(succ il)} in { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of (SCM R) : verum } ;
x in {(succ il)} by A16, TARSKI:def 1;
hence x in union { ((NIC I,il) \ (JUMP I)) where I is Element of the Instructions of (SCM R) : verum } by A17, TARSKI:def 4; :: thesis: verum

end;

end;

end;

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