isabelle: src/ZF/AC/Transrec2.thy@0140ff702b23 (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$
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	3	Author: Krzysztof Gr`abczewski
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
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	17	transrec2_def "transrec2(alpha, a, b) == \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	18	\ transrec(alpha, %i r. if(i=0, \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	19	\ a, if(EX j. i=succ(j), \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	20	\ b(THE j. i=succ(j), r`(THE j. i=succ(j))), \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	21	\ UN j<i. r`j)))"
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
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 992	4ef4f7ff2aeb
child 1155	928a16e02f9f
permissions	-rw-r--r--