Lines Matching defs:gv
70 val gv = genvar int_ty
75 val eq1 = MP (INST [cvar |-> varpart, xvar |-> numpart, yvar |-> gv]
78 yvar |-> gv]
91 | POSITIVE => (K (INST [gv |-> rand (rand t)] eq1) THENC
93 | NEGATED => (K (INST [gv |-> rand (rand t)] eq2) THENC
103 yvar |-> gv] le_context_rwt1) ltthm
105 yvar |-> gv] le_context_rwt2) ltthm)
107 yvar |-> gv] le_context_rwt3) ltthm
109 yvar |-> gv] le_context_rwt4) ltthm)
124 (INST [gv |-> tnumpart] rwt3)) TRUTH
131 (INST [gv |-> tnumpart] rwt4)) TRUTH
141 (INST [gv |-> tnumpart] rwt1)) TRUTH
151 (INST [gv |-> tnumpart] rwt2))