let il be Nat; :: thesis: 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 :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: ( 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 } ; :: thesis: 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 i = [0,{},{}] ; :: thesis: x in {il,(il + 1)}
then x in {il} \ (JUMP ()) by ;
then x = il by TARSKI:def 1;
hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
suppose ex a, b being Data-Location st i = a := b ; :: thesis: x in {il,(il + 1)}
then consider a, b being Data-Location such that
A4: i = a := b ;
x in {(il + 1)} \ (JUMP (a := b)) by ;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
suppose ex a, b being Data-Location st i = AddTo (a,b) ; :: thesis: x in {il,(il + 1)}
then consider a, b being Data-Location such that
A5: i = AddTo (a,b) ;
x in {(il + 1)} \ (JUMP (AddTo (a,b))) by ;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
suppose ex a, b being Data-Location st i = SubFrom (a,b) ; :: thesis: x in {il,(il + 1)}
then consider a, b being Data-Location such that
A6: i = SubFrom (a,b) ;
x in {(il + 1)} \ (JUMP (SubFrom (a,b))) by ;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
suppose ex a, b being Data-Location st i = MultBy (a,b) ; :: thesis: x in {il,(il + 1)}
then consider a, b being Data-Location such that
A7: i = MultBy (a,b) ;
x in {(il + 1)} \ (JUMP (MultBy (a,b))) by ;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
suppose ex a, b being Data-Location st i = Divide (a,b) ; :: thesis: x in {il,(il + 1)}
then consider a, b being Data-Location such that
A8: i = Divide (a,b) ;
x in {(il + 1)} \ (JUMP (Divide (a,b))) by ;
then x = il + 1 by TARSKI:def 1;
hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
suppose ex k being Nat st i = SCM-goto k ; :: thesis: x in {il,(il + 1)}
then consider k being Nat such that
A9: i = SCM-goto k ;
x in {k} \ (JUMP i) by A1, A3, A9, Th15;
then x in {k} \ {k} by ;
hence x in {il,(il + 1)} by XBOOLE_1:37; :: thesis: verum
end;
suppose ex a being Data-Location ex k being Nat st i = a =0_goto k ; :: thesis: 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 ;
x in NIC (i,il) by ;
then A12: ( x = k or x = il + 1 ) by ;
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 ; :: thesis: verum
end;
suppose ex a being Data-Location ex k being Nat st i = a >0_goto k ; :: thesis: 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 ;
x in NIC (i,il) by ;
then A15: ( x = k or x = il + 1 ) by ;
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 ; :: thesis: verum
end;
end;
end;
assume A16: x in {il,(il + 1)} ; :: thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum }
per cases ( x = il or x = il + 1 ) by ;
suppose A17: x = il ; :: thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum }
set i = halt SCM;
(NIC ((),il)) \ (JUMP ()) = {il} by AMISTD_1:2;
then A18: {il} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } ;
x in {il} by ;
hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by ; :: thesis: verum
end;
suppose A19: x = il + 1 ; :: thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum }
set a = the Data-Location;
set i = AddTo ( the Data-Location, the Data-Location);
(NIC ((AddTo ( the Data-Location, the Data-Location)),il)) \ (JUMP (AddTo ( the Data-Location, the Data-Location))) = {(il + 1)} by AMISTD_1:12;
then A20: {(il + 1)} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } ;
x in {(il + 1)} by ;
hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by ; :: thesis: verum
end;
end;
end;
hence SUCC (il,SCM) = {il,(il + 1)} by TARSKI:2; :: thesis: verum