Type Systems : Sample Typing Proof
Show ? |- ((? f :bool?bool . (? x:bool . (f (f x)))) (? x:bool . x)) : bool?bool
Tree1: f :bool?bool, x:bool |- f :bool?bool, f :bool?bool, x:bool |- x :bool
f :bool?bool, x:bool |- (f x): bool
Tree2: f :bool?bool, x:bool |- f :bool?bool, Tree1
f :bool?bool, x:bool | (f (f x)): bool
f :bool?bool |- (? x:bool . (f (f x))): bool?bool
? | ((? f :bool?bool . (? x:bool . (f (f x)))) : (bool?bool) ? (bool?bool)
? |- (? x:bool . x)) : bool?bool
? |- ((? f :bool?bool . (? x:bool . (f (f x)))) (? x:bool . x)) : bool?bool