let il be Nat; SUCC (il,SCM+FSA) = {il,(il + 1)}
set X = { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : 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+FSA : 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+FSA : verum } ) )let x be
object ;
( ( x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : 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+FSA : 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+FSA : verum } )
assume
x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : 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+FSA : verum }
by TARSKI:def 4;
consider i being
Element of the
InstructionsF of
SCM+FSA such that A3:
Y = (NIC (i,il)) \ (JUMP i)
by A2;
per cases
( i = [0,{},{}] or ex a, b being Int-Location st i = a := b or ex a, b being Int-Location st i = AddTo (a,b) or ex a, b being Int-Location st i = SubFrom (a,b) or ex a, b being Int-Location st i = MultBy (a,b) or ex a, b being Int-Location st i = Divide (a,b) or ex i1 being Nat st i = goto i1 or ex i1 being Nat ex a being Int-Location st i = a =0_goto i1 or ex i1 being Nat ex a being Int-Location st i = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) or ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b or ex a being Int-Location ex f being FinSeq-Location st i = a :=len f or ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a )
by SCMFSA_2:93;
suppose
ex
i1 being
Nat ex
a being
Int-Location st
i = a =0_goto i1
;
x in {il,(il + 1)}then consider i1 being
Nat,
a being
Int-Location such that A10:
i = a =0_goto i1
;
A11:
NIC (
i,
il)
= {i1,(il + 1)}
by A10, Th35;
x in NIC (
i,
il)
by A1, A3, XBOOLE_0:def 5;
then A12:
(
x = i1 or
x = il + 1 )
by A11, TARSKI:def 2;
x in (NIC (i,il)) \ {i1}
by A1, A3, A10, Th36;
then
not
x in {i1}
by XBOOLE_0:def 5;
hence
x in {il,(il + 1)}
by A12, TARSKI:def 1, TARSKI:def 2;
verum end; suppose
ex
i1 being
Nat ex
a being
Int-Location st
i = a >0_goto i1
;
x in {il,(il + 1)}then consider i1 being
Nat,
a being
Int-Location such that A13:
i = a >0_goto i1
;
A14:
NIC (
i,
il)
= {i1,(il + 1)}
by A13, Th37;
x in NIC (
i,
il)
by A1, A3, XBOOLE_0:def 5;
then A15:
(
x = i1 or
x = il + 1 )
by A14, TARSKI:def 2;
x in (NIC (i,il)) \ {i1}
by A1, A3, A13, Th38;
then
not
x in {i1}
by XBOOLE_0:def 5;
hence
x in {il,(il + 1)}
by A15, TARSKI:def 1, TARSKI:def 2;
verum end; end;
end; assume A20:
x in {il,(il + 1)}
;
b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM+FSA : verum } end;
hence
SUCC (il,SCM+FSA) = {il,(il + 1)}
by TARSKI:2; verum