let N be with_zero set ; :: thesis: for i being Element of the InstructionsF of (STC N) holds JUMP i is empty

let i be Element of the InstructionsF of (STC N); :: thesis: JUMP i is empty

let i be Element of the InstructionsF of (STC N); :: thesis: JUMP i is empty

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

end;

suppose A1:
InsCode i = 1
; :: thesis: JUMP i is empty

reconsider l1 = 0 , l2 = 1 as Nat ;

set X = { (NIC (i,l)) where l is Nat : verum } ;

assume not JUMP i is empty ; :: thesis: contradiction

then consider x being object such that

A2: x in meet { (NIC (i,l)) where l is Nat : verum } ;

NIC (i,l1) in { (NIC (i,l)) where l is Nat : verum } ;

then {(0 + 1)} in { (NIC (i,l)) where l is Nat : verum } by A1, Lm4;

then x in {1} by A2, SETFAM_1:def 1;

then A3: x = 1 by TARSKI:def 1;

NIC (i,l2) in { (NIC (i,l)) where l is Nat : verum } ;

then {(1 + 1)} in { (NIC (i,l)) where l is Nat : verum } by A1, Lm4;

then x in {2} by A2, SETFAM_1:def 1;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;set X = { (NIC (i,l)) where l is Nat : verum } ;

assume not JUMP i is empty ; :: thesis: contradiction

then consider x being object such that

A2: x in meet { (NIC (i,l)) where l is Nat : verum } ;

NIC (i,l1) in { (NIC (i,l)) where l is Nat : verum } ;

then {(0 + 1)} in { (NIC (i,l)) where l is Nat : verum } by A1, Lm4;

then x in {1} by A2, SETFAM_1:def 1;

then A3: x = 1 by TARSKI:def 1;

NIC (i,l2) in { (NIC (i,l)) where l is Nat : verum } ;

then {(1 + 1)} in { (NIC (i,l)) where l is Nat : verum } by A1, Lm4;

then x in {2} by A2, SETFAM_1:def 1;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum