set : α setEXPi : α itself # β itself -> γ itselfFCPi : (num -> α) # β itself -> α ** βIS_EMPTY : (α -> bool) -> boolITSELF : num -> α itselfMULi : α itself # β itself -> γ itselfSUMi : α itself # β itself -> γ itselfi2w_itself : int # α itself -> α wordmk_fcp : (num -> α) # β itself -> α ** βneg_int_of_num : num -> intEXPi[oracles: ] [axioms: EXPi] [] ⊢ EXPi (ITSELF a,ITSELF b) = ITSELF (a ** b)
MULi[oracles: ] [axioms: MULi] [] ⊢ MULi (ITSELF a,ITSELF b) = ITSELF (a * b)
SUMi[oracles: ] [axioms: SUMi] [] ⊢ SUMi (ITSELF a,ITSELF b) = ITSELF (a + b)
dimindexi[oracles: ] [axioms: dimindexi] [] ⊢ dimindex (ITSELF a) = a
FCPi_def_primitive⊢ FCPi = WFREC (@R. WF R) (λFCPi a. case a of (v,v1) => I ($FCP v))
⊢ ∀s. IS_EMPTY s ⇔ if s = ∅ then T else F
i2w_itself_def_primitive⊢ i2w_itself = WFREC (@R. WF R) (λi2w_itself a. case a of (v,v1) => I (i2w v))
⊢ mk_fcp = FCPi
⊢ ∀n. neg_int_of_num n = -int_of_num (n + 1)
⊢ FCPi (f,(:β)) = $FCP f
⊢ ∀P. (∀f. P (f,(:β))) ⇒ ∀v v1. P (v,v1)
⊢ (s = ∅ ⇔ IS_EMPTY s) ∧ (∅ = s ⇔ IS_EMPTY s)
⊢ i2w_itself (i,(:α)) = i2w i
⊢ ∀P. (∀i. P (i,(:α))) ⇒ ∀v v1. P (v,v1)