-definition pic: predicate path ā
- Ī»p. āq,k. qāš±k = p ā ā„
+inductive pic: predicate path ā
+| pic_empty: (š) Ļµ pic
+| pic_m_dx (p): pāšŗ Ļµ pic
+| pic_L_dx (p): pāš Ļµ pic
+| pic_A_dx (p): pāš Ļµ pic
+| pic_S_dx (p): pāš¦ Ļµ pic