src/ZF/AC/recfunAC16.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2469 b50b8c0eec01
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      ZF/AC/recfunAC16.thy
lcp@1196
     2
    ID:         $Id$
clasohm@1478
     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) == 
clasohm@1478
    18
         transrec2(i, 0, 
clasohm@1478
    19
              %g r. if(EX y:r. fa`g <= y, r, 
clasohm@1478
    20
                       r Un {f`(LEAST i. fa`g <= f`i & 
clasohm@1478
    21
                       (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
lcp@1196
    22
lcp@1196
    23
end