src/ZF/AC/recfunAC16.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 1204 a4253da68be2
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
lcp@1196
     1
(*  Title: 	ZF/AC/recfunAC16.thy
lcp@1196
     2
    ID:         $Id$
lcp@1204
     3
    Author: 	Krzysztof Grabczewski
lcp@1196
     4
lcp@1196
     5
A recursive definition used in the proof of WO2 ==> AC16
lcp@1196
     6
*)
lcp@1196
     7
lcp@1196
     8
recfunAC16 = Transrec2 + Cardinal +
lcp@1196
     9
lcp@1196
    10
consts
lcp@1196
    11
clasohm@1401
    12
  recfunAC16              :: [i, i, i, i] => i
lcp@1196
    13
lcp@1196
    14
defs
lcp@1196
    15
lcp@1196
    16
  recfunAC16_def
lcp@1196
    17
    "recfunAC16(f,fa,i,a) == 
lcp@1196
    18
	 transrec2(i, 0, 
lcp@1196
    19
	      %g r. if(EX y:r. fa`g <= y, r, 
lcp@1196
    20
		       r Un {f`(LEAST i. fa`g <= f`i & 
lcp@1196
    21
		       (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
lcp@1196
    22
lcp@1196
    23
end