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

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) and
verum ;
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 }

reconsider i = [0,0,0] as Instruction of (STC N) by Def11;
( JUMP i = {} & InsCode i = 0 ) by Lm6, RECDEF_2:def 1;
then (NIC (i,l)) \ (JUMP i) = y by A1, A6, 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 A7: 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,0];
[1,0,0] in {[1,0,0],[0,0,0]} by TARSKI:def 2;
then reconsider i = [1,0,0] as Instruction of (STC N) by Def11;
( JUMP i = {} & InsCode i = 1 ) by Lm6, RECDEF_2:def 1;
then (NIC (i,l)) \ (JUMP i) = y by A1, A7, 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:1;
hence SUCC (l,(STC N)) = {z,(z + 1)} by ZFMISC_1:26; :: thesis: verum