isabelle: src/ZF/AC/Transrec2.thy@a39bec971684 (annotated)

992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	1	(* Title: ZF/AC/Transrec2.thy
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	2	ID: $Id$
1203 a39bec971684 Ran expandshort and changed spelling of Grabczewski lcp parents: 1155 diff changeset	3	Author: Krzysztof Grabczewski
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	4
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	5	Transfinite recursion introduced to handle definitions based on the three
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	6	cases of ordinals.
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	7	*)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	8
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	9	Transrec2 = OrdQuant + Epsilon +
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	10
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	11	consts
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	12
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	13	transrec2 :: "[i, i, [i,i]=>i] =>i"
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	14
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	15	defs
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	16
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 992 diff changeset	17	transrec2_def "transrec2(alpha, a, b) ==
928a16e02f9f removed \...\ inside strings clasohm parents: 992 diff changeset	18	transrec(alpha, %i r. if(i=0,
928a16e02f9f removed \...\ inside strings clasohm parents: 992 diff changeset	19	a, if(EX j. i=succ(j),
928a16e02f9f removed \...\ inside strings clasohm parents: 992 diff changeset	20	b(THE j. i=succ(j), r`(THE j. i=succ(j))),
928a16e02f9f removed \...\ inside strings clasohm parents: 992 diff changeset	21	UN j<i. r`j)))"
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	22
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	23	end

author	lcp
	Fri, 28 Jul 1995 11:02:22 +0200
changeset 1203	a39bec971684
parent 1155	928a16e02f9f
child 1401	0c439768f45c
permissions	-rw-r--r--