let a be Int_position ; :: thesis: for i being Integer
for n, m being Element of NAT
for I being Program of SCMPDS holds
( m < (card I) + 3 iff inspos m in dom (for-down a,i,n,I) )
let i be Integer; :: thesis: for n, m being Element of NAT
for I being Program of SCMPDS holds
( m < (card I) + 3 iff inspos m in dom (for-down a,i,n,I) )
let n, m be Element of NAT ; :: thesis: for I being Program of SCMPDS holds
( m < (card I) + 3 iff inspos m in dom (for-down a,i,n,I) )
let I be Program of SCMPDS ; :: thesis: ( m < (card I) + 3 iff inspos m in dom (for-down a,i,n,I) )
card (for-down a,i,n,I) = (card I) + 3 by Th60;
hence ( m < (card I) + 3 iff inspos m in dom (for-down a,i,n,I) ) by SCMPDS_4:1; :: thesis: verum