Go backward to S Rule Go up to Top Go forward to Simplification

Simplification

P[[ON 2+1 TOTAL IF LA , 2 , 0 TOTAL OFF]]
= S[[2+1 TOTAL IF LA, 2, 0 TOTAL OFF]](zero)
= let n' = E[[2+1]](zero)
     in n' cons S[[IF LA , 2 , 0 TOTAL OFF]](n')
= let n' = three
     in n' cons S[[IF LA , 2 , 0 TOTAL OFF]](n')
= three cons S[[IF LA , 2 , 0 TOTAL OFF]](three)
= three cons (E[[IF LA , 2 , 0]](three) cons nil)
= three cons (zero cons nil)

E[[IF LA , 2 , 0]](three)
= E[[LA]](three) equals zero ->
    E[[2]](three) [] E[[0]](three)
= three equals zero -> two [] zero
= false -> two [] zero
= zero