reconsider hachi = 8 as Element of Segm 9 by NAT_1:45;
let loc be Element of NAT ; :: thesis: for a being Data-Location holds
( (@ (a >0_goto loc)) cjump_address = loc & (@ (a >0_goto loc)) cond_address = a )
let a be Data-Location ; :: thesis: ( (@ (a >0_goto loc)) cjump_address = loc & (@ (a >0_goto loc)) cond_address = a )
reconsider mk = loc as Element of NAT ;
reconsider aa = a as Element of SCM-Data-Loc by AMI_3:def 2;
@ (a >0_goto loc) = [hachi,<*mk,aa*>] ;
hence ( (@ (a >0_goto loc)) cjump_address = loc & (@ (a >0_goto loc)) cond_address = a ) by AMI_2:25; :: thesis: verum