Lines Matching refs:source
12 `!subst source z.
13 (((FINITE (source z)) /\
15 (!n. DISJOINT (FDOM (subst n)) (source n)) /\
16 (!n. z < n ==> (FDOM (subst n) UNION (source n) = FDOM (subst z) UNION (source z))))
20 `!m. z <= m ==> ?n.m < n /\ CARD(source n) < CARD(source m)`
25 by (Q.EXISTS_TAC `\n.CARD(source(FUNPOW f n z))` THEN
35 `(FDOM (subst n) UNION source n = FDOM (subst m) UNION source m) /\
36 FINITE (source m) /\ FINITE (source n)`
40 `(CARD (FDOM (subst n) UNION source n) = CARD (FDOM (subst n)) + CARD (source n)) /\
41 (CARD (FDOM (subst m) UNION source m) = CARD (FDOM (subst m)) + CARD (source m)) /\
42 (CARD (FDOM (subst m) UNION source m) = CARD (FDOM (subst n) UNION source n))` by