let il be Nat; SUCC (il,SCM) = {il,(il + 1)}
set X = { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } ;
set N = {il,(il + 1)};
now for x being object holds
( ( x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : 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 : verum } ) )let x be
object ;
( ( x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } implies x in {il,(il + 1)} ) & ( x in {il,(il + 1)} implies b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } ) )hereby ( x in {il,(il + 1)} implies b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } )
assume
x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum }
;
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 : verum }
by TARSKI:def 4;
consider i being
Element of the
InstructionsF of
SCM such that A3:
Y = (NIC (i,il)) \ (JUMP i)
by A2;
per cases
( i = [0,{},{}] or ex a, b being Data-Location st i = a := b or ex a, b being Data-Location st i = AddTo (a,b) or ex a, b being Data-Location st i = SubFrom (a,b) or ex a, b being Data-Location st i = MultBy (a,b) or ex a, b being Data-Location st i = Divide (a,b) or ex k being Nat st i = SCM-goto k or ex a being Data-Location ex k being Nat st i = a =0_goto k or ex a being Data-Location ex k being Nat st i = a >0_goto k )
by AMI_3:24;
suppose
ex
a being
Data-Location ex
k being
Nat st
i = a =0_goto k
;
x in {il,(il + 1)}then consider a being
Data-Location,
k being
Nat such that A10:
i = a =0_goto k
;
A11:
NIC (
i,
il)
= {k,(il + 1)}
by A10, Th17;
x in NIC (
i,
il)
by A1, A3, XBOOLE_0:def 5;
then A12:
(
x = k or
x = il + 1 )
by A11, TARSKI:def 2;
x in (NIC (i,il)) \ {k}
by A1, A3, A10, Th18;
then
not
x in {k}
by XBOOLE_0:def 5;
hence
x in {il,(il + 1)}
by A12, TARSKI:def 1, TARSKI:def 2;
verum end; suppose
ex
a being
Data-Location ex
k being
Nat st
i = a >0_goto k
;
x in {il,(il + 1)}then consider a being
Data-Location,
k being
Nat such that A13:
i = a >0_goto k
;
A14:
NIC (
i,
il)
= {k,(il + 1)}
by A13, Th19;
x in NIC (
i,
il)
by A1, A3, XBOOLE_0:def 5;
then A15:
(
x = k or
x = il + 1 )
by A14, TARSKI:def 2;
x in (NIC (i,il)) \ {k}
by A1, A3, A13, Th20;
then
not
x in {k}
by XBOOLE_0:def 5;
hence
x in {il,(il + 1)}
by A15, TARSKI:def 1, TARSKI:def 2;
verum end; end;
end; assume A16:
x in {il,(il + 1)}
;
b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } end;
hence
SUCC (il,SCM) = {il,(il + 1)}
by TARSKI:2; verum