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
per cases ( InsCode i = 1 or InsCode i = 0 ) by Th6;
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 ;
then x in {1} by ;
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 ;
then x in {2} by ;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum
end;
suppose A4: InsCode i = 0 ; :: thesis: JUMP i is empty
reconsider i = i as Instruction of (STC N) ;
for l being Nat holds NIC (i,l) = {l} by A4, Th2, Th4;
hence JUMP i is empty by Th1; :: thesis: verum
end;
end;