isabelle: src/ZF/AC/recfunAC16.thy@a4253da68be2 (annotated)

1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	1	(* Title: ZF/AC/recfunAC16.thy
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	2	ID: $Id$
1204 a4253da68be2 Ran expandshort and changed spelling of Grabczewski lcp parents: 1196 diff changeset	3	Author: Krzysztof Grabczewski
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	4
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	5	A recursive definition used in the proof of WO2 ==> AC16
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	6	*)
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	7
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	8	recfunAC16 = Transrec2 + Cardinal +
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	9
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	10	consts
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	11
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	12	recfunAC16 :: "[i, i, i, i] => i"
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	13
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	14	defs
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	15
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	16	recfunAC16_def
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	17	"recfunAC16(f,fa,i,a) ==
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	18	transrec2(i, 0,
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	19	%g r. if(EX y:r. fa`g <= y, r,
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	20	r Un {f`(LEAST i. fa`g <= f`i &
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	21	(ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	22
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	23	end

author	lcp
	Fri, 28 Jul 1995 11:20:22 +0200
changeset 1204	a4253da68be2
parent 1196	d43c1f7a53fe
child 1401	0c439768f45c
permissions	-rw-r--r--