let z be natural number ; :: thesis: for N being with_non-empty_elements set
for l being Instruction-Location of STC N st l = z holds
SUCC l = {z,(z + 1)}
let N be with_non-empty_elements set ; :: thesis: for l being Instruction-Location of STC N st l = z holds
SUCC l = {z,(z + 1)}
let l be Instruction-Location of STC N; :: thesis: ( l = z implies SUCC l = {z,(z + 1)} )
assume A1: l = z ; :: thesis: SUCC l = {z,(z + 1)}
set K = { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of (STC N) : verum } ;
set M = STC N;

now

let y be set ; :: thesis: ( ( y in { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of (STC N) : verum } implies y in {{z},{(z + 1)}} ) & ( y in {{z},{(z + 1)}} implies b₁ in { ((NIC b₂,l) \ (JUMP b₂)) where i is Element of the Instructions of (STC N) : verum } ) )

hereby :: thesis: ( y in {{z},{(z + 1)}} implies b₁ in { ((NIC b₂,l) \ (JUMP b₂)) where i is Element of the Instructions of (STC N) : verum } )

assume y in { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of (STC N) : verum } ; :: thesis: y in {{z},{(z + 1)}}
then consider ii being Element of the Instructions of (STC N) such that
A2: y = (NIC ii,l) \ (JUMP ii) ;
reconsider ii = ii as Instruction of (STC N) ;

now

per cases ( InsCode ii = 1 or InsCode ii = 0 ) by Th22;

suppose A3: InsCode ii = 1 ; :: thesis: y in {{z},{(z + 1)}}

JUMP ii = {} by Lm6;
then y = {(z + 1)} by A1, A2, A3, Lm5;
hence y in {{z},{(z + 1)}} by TARSKI:def 2; :: thesis: verum

end;

suppose A4: InsCode ii = 0 ; :: thesis: y in {{z},{(z + 1)}}

JUMP ii = {} by Lm6;
then y = {z} by A1, A2, A4, Th15, Th20;
hence y in {{z},{(z + 1)}} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence y in {{z},{(z + 1)}} ; :: thesis: verum

end;

assume A5: y in {{z},{(z + 1)}} ; :: thesis: b₁ in { ((NIC b₂,l) \ (JUMP b₂)) where i is Element of the Instructions of (STC N) : verum }

per cases ( y = {z} or y = {(z + 1)} ) by A5, TARSKI:def 2;

suppose A6: y = {z} ; :: thesis: b₁ in { ((NIC b₂,l) \ (JUMP b₂)) where i is Element of the Instructions of (STC N) : verum }

set i = [0 ,0 ];
[0 ,0 ] in {[1,0 ],[0 ,0 ]} by TARSKI:def 2;
then reconsider i = [0 ,0 ] as Instruction of (STC N) by Def11;
A7: JUMP i = {} by Lm6;
InsCode i = 0 by MCART_1:def 1;
then (NIC i,l) \ (JUMP i) = y by A1, A6, A7, Th15, Th20;
hence y in { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of (STC N) : verum } ; :: thesis: verum

end;

suppose A8: y = {(z + 1)} ; :: thesis: b₁ in { ((NIC b₂,l) \ (JUMP b₂)) where i is Element of the Instructions of (STC N) : verum }

set i = [1,0 ];
[1,0 ] in {[1,0 ],[0 ,0 ]} by TARSKI:def 2;
then reconsider i = [1,0 ] as Instruction of (STC N) by Def11;
A9: JUMP i = {} by Lm6;
InsCode i = 1 by MCART_1:def 1;
then (NIC i,l) \ (JUMP i) = y by A1, A8, A9, Lm5;
hence y in { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of (STC N) : verum } ; :: thesis: verum

end;

end;

end;

then { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of (STC N) : verum } = {{z},{(z + 1)}} by TARSKI:2;
hence SUCC l = {z,(z + 1)} by ZFMISC_1:32; :: thesis: verum