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

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 } ) )

hence
SUCC (il,SCM) = {il,(il + 1)}
by TARSKI:2; :: thesis: verum( ( 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 b_{1} in union { ((NIC (b_{2},il)) \ (JUMP b_{2})) where I is Element of the InstructionsF of SCM : verum } ) )

_{1} in union { ((NIC (b_{2},il)) \ (JUMP b_{2})) where I is Element of the InstructionsF of SCM : verum }

end;hereby :: thesis: ( x in {il,(il + 1)} implies b_{1} in union { ((NIC (b_{2},il)) \ (JUMP b_{2})) where I is Element of the InstructionsF of SCM : verum } )

assume A16:
x in {il,(il + 1)}
; :: thesis: bassume
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;

end;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;

end;

suppose
i = [0,{},{}]
; :: thesis: x in {il,(il + 1)}

then
x in {il} \ (JUMP (halt SCM))
by A1, A3, AMISTD_1:2;

then x = il by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;then x = il by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

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 A1, A3, A4, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;A4: i = a := b ;

x in {(il + 1)} \ (JUMP (a := b)) by A1, A3, A4, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

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 A1, A3, A5, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;A5: i = AddTo (a,b) ;

x in {(il + 1)} \ (JUMP (AddTo (a,b))) by A1, A3, A5, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

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 A1, A3, A6, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;A6: i = SubFrom (a,b) ;

x in {(il + 1)} \ (JUMP (SubFrom (a,b))) by A1, A3, A6, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

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 A1, A3, A7, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;A7: i = MultBy (a,b) ;

x in {(il + 1)} \ (JUMP (MultBy (a,b))) by A1, A3, A7, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

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 A1, A3, A8, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;A8: i = Divide (a,b) ;

x in {(il + 1)} \ (JUMP (Divide (a,b))) by A1, A3, A8, AMISTD_1:12;

then x = il + 1 by TARSKI:def 1;

hence x in {il,(il + 1)} by TARSKI:def 2; :: thesis: verum

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 A9, Th16;

hence x in {il,(il + 1)} by XBOOLE_1:37; :: thesis: verum

end;A9: i = SCM-goto k ;

x in {k} \ (JUMP i) by A1, A3, A9, Th15;

then x in {k} \ {k} by A9, Th16;

hence x in {il,(il + 1)} by XBOOLE_1:37; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

per cases
( x = il or x = il + 1 )
by A16, TARSKI:def 2;

end;

suppose A17:
x = il
; :: thesis: b_{1} in union { ((NIC (b_{2},il)) \ (JUMP b_{2})) where I is Element of the InstructionsF of SCM : verum }

set i = halt SCM;

(NIC ((halt SCM),il)) \ (JUMP (halt SCM)) = {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 A17, TARSKI:def 1;

hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by A18, TARSKI:def 4; :: thesis: verum

end;(NIC ((halt SCM),il)) \ (JUMP (halt SCM)) = {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 A17, TARSKI:def 1;

hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by A18, TARSKI:def 4; :: thesis: verum

suppose A19:
x = il + 1
; :: thesis: b_{1} in union { ((NIC (b_{2},il)) \ (JUMP b_{2})) 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 A19, TARSKI:def 1;

hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by A20, TARSKI:def 4; :: thesis: verum

end;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 A19, TARSKI:def 1;

hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by A20, TARSKI:def 4; :: thesis: verum