let z be Nat; :: thesis: for N being with_zero set
for l being Nat st l = z holds
SUCC (l,(STC N)) = {z,(z + 1)}
let N be with_zero set ; :: thesis: for l being Nat st l = z holds
SUCC (l,(STC N)) = {z,(z + 1)}
let l be 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 InstructionsF of (STC N) : verum } ;

now :: thesis: for y being object holds
( ( y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } implies y in {{z},{(z + 1)}} ) & ( y in {{z},{(z + 1)}} implies y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } ) )

let y be object ; :: thesis: ( ( y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF 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 InstructionsF 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 InstructionsF of (STC N) : verum } )

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

now :: thesis: y in {{z},{(z + 1)}}

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

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

JUMP ii = {} by Lm5;
then y = {(z + 1)} by A1, A2, A3, Lm4;
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 Lm5;
then y = {z} by A1, A2, A4, Th2, Th4;
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 InstructionsF 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 InstructionsF of (STC N) : verum }

halt (STC N) = [0,{},{}] ;
then reconsider i = [0,0,0] as Instruction of (STC N) ;
( JUMP i = {} & InsCode i = 0 ) by Lm5;
then (NIC (i,l)) \ (JUMP i) = y by A1, A6, Th2, Th4;
hence y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF 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 InstructionsF of (STC N) : verum }

set i = [1,0,0];
[1,0,0] in {[1,{},{}],[0,{},{}]} by TARSKI:def 2;
then reconsider i = [1,0,0] as Instruction of (STC N) by Def7;
( JUMP i = {} & InsCode i = 1 ) by Lm5;
then (NIC (i,l)) \ (JUMP i) = y by A1, A7, Lm4;
hence y in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of (STC N) : verum } ; :: thesis: verum

end;

end;

end;

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