We want to prove the following lemma: ! n. ! t. ~ ( varoccursinterm n t ) ==> ! sys. ( CARD ( systemvarset ( applsystem ( substsingle n t ) sys ))) < ( CARD ( systemvarset ( Addequation sys ( Variable n ) t ))) We do this using pre-proved HOL theorem CARD_PSUBSET, which says that |- !a b. a PSUBSET b /\ FINITE b ==> CARD a < CARD b. Thus, we need to prove that systemvarset ( applsystem ( substsingle n t ) sys ) is a proper subset of systemvarset ( Addequation sys ( Variable n ) t ) (we do this in the 2nd part) and that those sets are not equal (the 1st part). PART 0 xcLemma0: ! t. ( FINITE ( termvarset t )) xcLemma1: ! sys. ( FINITE ( systemvarset sys )) PART I xLemma01: !a t n. (\m. if n = m then t else Variable m) a = (if n = a then t else Variable a) xLemma03: !n:num t:term. n IN termvarset t <=> varoccursinterm n t xLemma04: !n t. !ter. (n IN termvarset (applterm (substsingle n t) ter)) ==> varoccursinterm n t xLemma06: !P:bool n:num A B C. (n IN {x | x IN A \/ x IN {x | x IN B \/ x IN C}} ==> P) = (n IN A \/ n IN B \/ n IN C ==> P) xLemma07: ! n. ! t. ! sys. ( n IN systemvarset ( applsystem ( substsingle n t ) sys )) ==> ( varoccursinterm n t ) xLemma08: ! n. ! t. ~(varoccursinterm n t) ==> ! sys. ~(n IN systemvarset ( applsystem ( substsingle n t ) sys)) xLemma09: ! n. ! t. ~(varoccursinterm n t) ==> ! sys. n IN (systemvarset ( Addequation sys ( Variable n ) t )) xLemma10: ! n. ! t. ~(varoccursinterm n t) ==> ~( (systemvarset ( Addequation sys ( Variable n ) t )) = (systemvarset ( applsystem ( substsingle n t ) sys)) ) PART II xLemma11: !n:num. !t:term. !m:num. !x:term. ~(m = n) ==> (varoccursinterm m x) ==> (varoccursinterm m (applterm (substsingle n t) x)) xLemma12: !ter:term n:num t:term. ~(varoccursinterm n t) ==> !x:num. ~(x = n) ==> (x IN (termvarset ter)) ==> (x IN (termvarset (applterm (substsingle n t) ter))) xLemma13: ! n. ! t. ~ ( varoccursinterm n t ) ==> ! sys. !v. (v = n) ==> v IN ( systemvarset ( applsystem ( substsingle n t ) sys )) ==> v IN ( systemvarset ( Addequation sys ( Variable n ) t )) xLemma14: !term v n t. varoccursinterm v (applterm (substsingle n t) term) ==> varoccursinterm v term \/ varoccursinterm v t xLemma15: !term v n t. v IN termvarset (applterm (substsingle n t) term) ==> v IN termvarset term \/ v IN termvarset t xLemma16: !v t n term. ~(v IN termvarset t) ==> v IN termvarset (applterm (substsingle n t) term) ==> v IN termvarset term xLemma17: !v n t sys. v IN systemvarset (applsystem (substsingle n t) sys) ==> (v IN systemvarset sys) \/ v IN termvarset t xLemma18: ! n. ! t. ~ ( varoccursinterm n t ) ==> ! sys. !v. ~(v = n) ==> v IN ( systemvarset ( applsystem ( substsingle n t ) sys )) ==> v IN ( systemvarset ( Addequation sys ( Variable n ) t ))`;; xLemma19: ! n. ! t. ~ ( varoccursinterm n t ) ==> ! sys. !v. v IN ( systemvarset ( applsystem ( substsingle n t ) sys )) ==> v IN ( systemvarset ( Addequation sys ( Variable n ) t )) xLemma20: ! n. ! t. ~ ( varoccursinterm n t ) ==> ! sys. (systemvarset ( applsystem ( substsingle n t ) sys)) SUBSET (systemvarset ( Addequation sys ( Variable n ) t)) PART III finalLemma: ! n. ! t. ~ ( varoccursinterm n t ) ==> ! sys. ( CARD ( systemvarset ( applsystem ( substsingle n t ) sys ))) < ( CARD ( systemvarset ( Addequation sys ( Variable n ) t )))