]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/reduction_new.ma
init_copy init_match
[helm.git] / matita / matita / tests / reduction_new.ma
1 include "reduction_new_preamble.ma".
2
3 ndefinition test:
4  〈〈x0,x0〉:〈x0,xF〉〉 =
5     ((succ_w16(succ_w16(succ_w16
6     (succ_w16(succ_w16(succ_w16(succ_w16
7     (succ_w16(succ_w16(succ_w16(succ_w16
8     (succ_w16(succ_w16(succ_w16(succ_w16
9      〈〈x0,x0〉:〈x0,x0〉〉)))))))))))))))).
10 napply (refl_eq word16 〈〈x0,x0〉:〈x0,xF〉〉); 
11 nqed.