_proof_ex

• (1) G |- a: int{a>=0} -> Tot int : Type
• (2) G |- d : Tot (x:int -> Tot t')
• (3) G |- a: int{a>=0} -> Tot int = y:int -> PURE int (fun p -> forall (x:int). p x)
• (4) G, x:int, simple: (y:int -> PURE t'' (up_PURE (precedes (d y) (d x)) /_PURE (fun p -> forall (x:t). p x))) |- if x = 0 the 1 else x + simple (x-1) : (PURE int (fun p -> forall (x:int). p x)[x/y])

(Theorem)-------------------------------------------- [T-Fix]

G |- let rec (simple^d: a: int{a>=0} -> Tot int) x = (if x = 0 the 1 else x + simple (x-1)) : Tot (a: int{a>=0} -> Tot int)

where Tot t = PURE t (fun p -> forall (x:t). p x)

• (5) G |- int{a>=0} : Type_i
• (6) G, a: int{a>=0} |- Tot int : Type_i'

(1)---------------- [T-Arr]

G |- a: int{a>=0} -> Tot int : Type

Premises Missing

(2)------------------

G |- d : Tot (x:int -> Tot t')

Premises Missing

(3)--------------------

G |- a: int{a>=0} -> Tot int = y:int -> PURE t'' wp

Premises Missing

(4)-----------------------------------------

G, x:int, simple: (y:int -> PURE t'' (up_PURE (precedes (d y) (d x)) /_PURE wp)) |- if x = 0 the 1 else x + simple (x-1) : (PURE t'' wp[x/y])

• (-) G |- int : Type_0 (G contains int : Type_0)
• (7) G, a:int |- a>-0 : Type_j

(5)-------------------------- [T-Refine]

G |- int{a>=0} : Type_0

Premises Missing

(6)-------------------------

G, a: int{a>=0} |- Tot int : Type_i'

Premises Missing

(7)------------------------

G, a:int |- a>-0 : Type_j