let I be Program of ; :: thesis: for a being Int-Location holds card (if<0 (a,I)) = (card I) + 5
let a be Int-Location; :: thesis: card (if<0 (a,I)) = (card I) + 5
thus card (if<0 (a,I)) = (card ((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I))) + 1 by Lm1, SCMFSA6A:21
.= (2 + (card ((a >0_goto ((card I) + 2)) ";" I))) + 1 by SCMFSA6A:33
.= (2 + ((card I) + 2)) + 1 by SCMFSA6A:33
.= (card I) + 5 ; :: thesis: verum