Lines Matching refs:lookup
31 (IMAGE (\n. lookup n graph.nodeInfo) (domain graph.nodeInfo))}`;
38 MEM x (CAT_OPTIONS (MAP (\n. lookup n graph.nodeInfo) l)) })
44 (IMAGE (\n. lookup n graph.nodeInfo) (domain graph.nodeInfo))
520 lookup nId graph.followers
533 ��� SOME suc = lookup sucId graph.nodeInfo
667 ``!g id node f. unique_node_formula g ��� (lookup id g.nodeInfo = SOME node)
694 (lookup id g.nodeInfo = SOME q)
695 ��� (lookup id g.followers = SOME fls)
696 ��� (lookup sucId g.nodeInfo = SOME suc)
713 lookup nId g.followers
714 od) ��� SOME suc = lookup sucId g.nodeInfo}`
858 oldSucPairs <- lookup nodeId g.followers ;
874 !id node. (lookup id g.nodeInfo = SOME node
876 ==> (lookup id g.followers = SOME []
904 >> `lookup q (g.nodeInfo) = SOME r ��� (��(n,l). l.frml = f) (q,r)`
914 >> `lookup q (g.nodeInfo) = SOME r ��� (��(n,l). l.frml = f) (q,r)`
929 ��� (lookup x_id g.followers = SOME fls)
944 ��� (lookup x_id g.followers = SOME (fl::fls))
993 >> `lookup x_id g.followers = SOME (h::t)
1006 !id node. (lookup id g.nodeInfo = SOME node)
1013 ��� (!id. IS_SOME (lookup id g.nodeInfo)
1014 ==> ((lookup id g.nodeInfo
1015 = lookup id (addFrmlToGraph g f).nodeInfo)
1016 ��� (lookup id g.followers
1017 = lookup id (addFrmlToGraph g f).followers))
1047 >> (`lookup q g.nodeInfo = NONE` by metis_tac[lookup_NONE_domain]
1055 >> `?node. lookup id g.nodeInfo = SOME node` by fs[IS_SOME_EXISTS]
1064 >> `?node. lookup id g.nodeInfo = SOME node` by fs[IS_SOME_EXISTS]
1098 ==> (lookup i (addFrmlToGraph g f).nodeInfo
1099 = lookup i g.nodeInfo)` by (
1138 >- (`~(lookup oId g.nodeInfo = SOME r')`
1181 >- (`lookup oId (addFrmlToGraph g f).nodeInfo = SOME r` by (
1214 >> `!id. (IS_SOME (lookup id g1.nodeInfo))
1215 ==> (lookup id g2.followers = lookup id g1.followers)` by (
1222 >> `!v. ~(lookup g1.next g1.nodeInfo = SOME v)` by fs[]
1284 >> `lookup q (addFrmlToGraph g1 f).followers = SOME []` by (
1309 >> `lookup q' g1.nodeInfo = SOME r'` by (
1334 >> `lookup id g1.nodeInfo = SOME node` by (
1356 IS_SOME (lookup id g1.nodeInfo) ���
1357 lookup id g1.nodeInfo = lookup id (addFrmlToGraph g1 f).nodeInfo`
1361 >> `lookup q (addFrmlToGraph g1 f).followers =
1362 lookup q g1.followers` by metis_tac[IS_SOME_DEF]
1438 ��� (!id. IS_SOME (lookup id g.nodeInfo)
1439 ==> ((lookup id g.nodeInfo
1440 = lookup id
1442 ��� (lookup id g.followers
1443 = lookup id
1510 ��� (lookup i (FOLDR (��f g. addFrmlToGraph g f) g ks).nodeInfo
1512 ==> (lookup i g.nodeInfo = SOME n)
1513 ��� (lookup i g.followers =
1514 lookup i (FOLDR (��f g. addFrmlToGraph g f) g ks).followers)`
1554 >> `lookup id G0.nodeInfo = SOME node` by (
1609 >> `lookup id G0.followers =
1610 lookup id (addFrmlToGraph G0 h).followers` by (
1617 >> `lookup id G0.nodeInfo = SOME node` by (
1626 >- (`lookup id G0.nodeInfo = SOME node` by (
1647 (lookup nId g.nodeInfo = SOME lab)
1660 >> `(lookup id nodeInfo2 = SOME r) ��� (lookup oId nodeInfo2 = SOME r')`
1662 >> `?z1. (lookup id g.nodeInfo = SOME z1) ��� (z1.frml = r.frml)` by (
1666 >> `?z2. (lookup oId g.nodeInfo = SOME z2) ��� (z2.frml = r.frml)` by (
1702 >> `(lookup x_id g.followers = SOME fls)
1732 ��� (!fl fls. lookup q m.followers = SOME (fl::fls)
1739 ==> (lookup id m.followers = lookup id g.followers))
1796 >> `���j. lookup q m.followers = SOME j` by (
1818 >- (`lookup x_id m.followers = SOME fls`
1848 >- (`lookup x_id m.followers = SOME fls`
1864 >- (`lookup x_id m.followers = SOME fls`
1915 >> `lookup q g.nodeInfo = SOME r`
1923 >- (`lookup id g.nodeInfo = SOME node`
1988 >> `lookup nId g.nodeInfo = SOME frml` by (
2006 >> `lookup nId g.nodeInfo = SOME r'` by metis_tac[MEM_toAList]
2007 >> `lookup nId g.nodeInfo = SOME frml` by metis_tac[MEM_toAList]
2019 >> `lookup nId g.nodeInfo = SOME frml` by metis_tac[MEM_toAList]
2021 >> `lookup nId (insert nId NEW_LAB g.nodeInfo) = SOME r'`
2055 >> `lookup q (insert q NEW_LAB g.nodeInfo) = SOME r` by metis_tac[]
2069 (OPTION_TO_LIST (lookup nId x.followers))
2070 ��� SOME suc = lookup sucId x.nodeInfo}`
2080 (���l. lookup nId x.followers = SOME l
2082 ��� SOME suc = lookup sucId g.nodeInfo}` by (
2135 >> `���l. lookup nId g.followers = SOME l ��� MEM (label,sucId) l`
2270 >> `lookup q x.nodeInfo = SOME r ��� (��(n,l). l.frml = h) (q,r)
2271 ��� lookup q' g.nodeInfo = SOME r'
2334 >> `lookup sucId x.nodeInfo = lookup sucId g.nodeInfo` by (
2493 ��� (lookup q m.followers = SOME fls)
2497 ==> (lookup o_id m.nodeInfo
2498 = lookup o_id g.nodeInfo)))` by (
2520 ��� lookup q k.followers = SOME fls
2523 ��� lookup o_id k.nodeInfo = lookup o_id g.nodeInfo)`
2548 >> `!id. lookup id k.followers =
2550 else lookup id g.followers` by (
2630 ��� SOME suc = lookup sucId k.nodeInfo}`
2718 >> `lookup q k.followers = lookup q g.followers` by (
2736 ��� (lookup id x1.followers = lookup id x2.followers)
2804 ��� lookup q m.followers = SOME fls
2807 ��� lookup o_id m.nodeInfo = lookup o_id g.nodeInfo)))`
2814 ��� lookup q m1.followers = SOME fls
2817 ��� lookup o_id m1.nodeInfo = lookup o_id g.nodeInfo)))`
2835 lookup nId m.followers = SOME followers_old ���
2836 lookup id m.preds = SOME preds_old`
2893 >> `lookup nId m.nodeInfo = SOME r` by (
2912 `lookup q m.followers = SOME l'`
2918 >> `lookup q m.nodeInfo = SOME r` by (
2957 >> `lookup nId m.nodeInfo = SOME frml`
3116 >> `?suc. lookup id m1.nodeInfo = SOME suc`
3124 >> `lookup nId m1.followers = SOME ((LABEL,id)::followers_old)`
3126 >> `?suc. lookup id m1.nodeInfo = SOME suc`
3128 >> `lookup nId m1.nodeInfo = SOME frml`
3166 >> `lookup q m1.followers = lookup q m.followers` by (
3184 ��� (lookup id x1.followers = lookup id x2.followers)