Lines Matching refs:SPEC
74 (SPECL [(tm i);(tm n)] (SPEC "ready:num->bool" NEXT_INC_INTERVAL_LEMMA))
79 (SPECL [(tm 0);(tm n);"t2:num"] (SPEC "ready:num->bool" NEXT_IDENTITY_LEMMA))
85 (SPEC (tm (n - 1))(SPEC "ready:num->bool" NEXT_INC_LEMMA))
92 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in
93 let th2 = (SUBS [SPEC (tm 1) ADD1] (SPEC (tm 1) LESS_SUC_REFL)) in
97 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in
98 let th2 = (SUBS [SPEC (tm 1) ADD1] (SPEC (tm 1) LESS_SUC_REFL)) in
100 let th4 = (SUBS [SPEC (tm 2) ADD1] th3) in
104 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in
105 let th2 = (SUBS [SPEC (tm 1) ADD1] (SPEC (tm 1) LESS_SUC_REFL)) in
107 let th4 = (SUBS [SPEC (tm 2) ADD1] th3) in
109 let th6 = (SUBS [SPEC (tm 3) ADD1] th5) in
134 DISJ_CASES (SPEC "(knob ((t1:num) + 1)):word2" VAL_word2_CASES)
140 let th3 = (SPEC (tm 1) th2) in
144 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in
146 let th3 = (SUBS [SPEC (tm 1) ADD1] th2) in
147 let th4 = (SUBS [SPEC (tm 2) ADD1] (SPEC (tm 2) LESS_SUC_REFL)) in
154 let th4 = (SPEC (tm 2) th3) in