| changeset 18075 | 43000d7a017c |
| parent 17291 | 94f6113fe9ed |
| 18074:a92b7c5133de | 18075:43000d7a017c |
|---|---|
11 by (rtac gix2_def 1); |
11 by (rtac gix2_def 1); |
12 by (rtac (fix_eq RS sym) 1); |
12 by (rtac (fix_eq RS sym) 1); |
13 qed "lemma1"; |
13 qed "lemma1"; |
14 |
14 |
15 |
15 |
16 Goal "gix$F=lub(range(%i. iterate i F UU))"; |
16 Goal "gix$F=lub(range(%i. iterate i$F$UU))"; |
17 by (rtac (lemma1 RS subst) 1); |
17 by (rtac (lemma1 RS subst) 1); |
18 by (rtac fix_def2 1); |
18 by (rtac fix_def2 1); |
19 qed "lemma2"; |
19 qed "lemma2"; |