let loc be Instruction-Location of SCM ; :: 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 hachi = 8 as Element of Segm 9 by GR_CY_1:10;
reconsider mk = loc as Element of NAT by AMI_1:def 4;
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