Welcome to SWI-Prolog (threaded, 64 bits, version 8.4.2) SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software. Please run ?- license. for legal details. For online help and background, visit https://www.swi-prolog.org For built-in help, use ?- help(Topic). or ?- apropos(Word). ?- true. ?- ti(TI), ⊢ I : TI. TI = α⇒α, I = λ(_A, _A) ; TI = α⇒α, I = λ(_A, λ(_B, _B)@_A) ; TI = α⇒α, I = λ(_A, λ(_B, _B)@(λ(_C, _C)@_A)) ; TI = α⇒α, I = λ(_A, λ(_B, _B)@(λ(_C, _C)@(λ(_D, _D)@_A))) ; TI = α⇒α, I = λ(_A, λ(_B, _B)@(λ(_C, _C)@(λ(_D, _D)@(λ(_E, _E)@_A)))) ; TI = α⇒α, I = λ(_A, λ(_B, _B)@(λ(_C, _C)@(λ(_D, _D)@(λ(_E, _E)@(λ(_F, _F)@_A))))) ; TI = α⇒α, I = λ(_A, λ(_B, _B)@(λ(_C, _C)@(λ(_D, _D)@(λ(_E, _E)@(λ(_F, _F)@(λ(_G, _G)@_A)))))) ; TI = α⇒α, I = λ(_A, λ(_B, _B)@(λ(_C, _C)@(λ(_D, _D)@(λ(_E, _E)@(λ(_F, _F)@(λ(_G, _G)@(λ(_H, _H)@_A))))))) ?- tk(TK), ⊢ K : TK. TK = α⇒β⇒α, K = λ(_A, λ(_, _A)) ; TK = α⇒β⇒α, K = λ(_A, λ(_, λ(_B, _B)@_A)) ; TK = α⇒β⇒α, K = λ(_A, λ(_, λ(_B, _B)@(λ(_C, _C)@_A))) ; TK = α⇒β⇒α, K = λ(_A, λ(_, λ(_B, _B)@(λ(_C, _C)@(λ(_D, _D)@_A)))) a ?- ts(TS), ⊢ S : TS. C-c C-cAction (h for help) ? a abort % Execution Aborted ?- trace. true. [trace] ?- ts(TS), ⊢ S : TS. Call: (11) ts(_2728) ? Exit: (11) ts((α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ) ? Call: (11) ⊢_2732:(α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ ? Call: (12) []⊢_2732:(α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ ? Call: (13) _2732:(α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ∈[] ? Call: (14) lists:member(_2732:(α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ, []) ? Fail: (14) lists:member(_2732:(α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ, []) ? Fail: (13) _2732:(α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ∈[] ? Redo: (12) []⊢_2732:(α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ ? Call: (13) [_8672:α⇒β⇒γ]⊢_8674:(α⇒β)⇒α⇒γ ? Call: (14) _8674:(α⇒β)⇒α⇒γ∈[_8672:α⇒β⇒γ] ? Call: (15) lists:member(_8674:(α⇒β)⇒α⇒γ, [_8672:α⇒β⇒γ]) ? Fail: (15) lists:member(_8674:(α⇒β)⇒α⇒γ, [_8672:α⇒β⇒γ]) ? Fail: (14) _8674:(α⇒β)⇒α⇒γ∈[_8672:α⇒β⇒γ] ? Redo: (13) [_8672:α⇒β⇒γ]⊢_8674:(α⇒β)⇒α⇒γ ? Call: (14) [_12218:α⇒β, _8672:α⇒β⇒γ]⊢_12220:α⇒γ ? Call: (15) _12220:α⇒γ∈[_12218:α⇒β, _8672:α⇒β⇒γ] ? Call: (16) lists:member(_12220:α⇒γ, [_12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (16) lists:member(_12220:α⇒γ, [_12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (15) _12220:α⇒γ∈[_12218:α⇒β, _8672:α⇒β⇒γ] ? Redo: (14) [_12218:α⇒β, _8672:α⇒β⇒γ]⊢_12220:α⇒γ ? Call: (15) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_15766:γ ? Call: (16) _15766:γ∈[_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Call: (17) lists:member(_15766:γ, [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (17) lists:member(_15766:γ, [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (16) _15766:γ∈[_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Redo: (15) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_15766:γ ? Call: (16) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_19310:_19322⇒γ ? Call: (17) _19310:_19322⇒γ∈[_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Call: (18) lists:member(_19310:_19322⇒γ, [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (18) lists:member(_19310:_19322⇒γ, [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (17) _19310:_19322⇒γ∈[_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Redo: (16) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_19310:_19322⇒γ ? Call: (17) [_22850:_19322, _15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_22852:γ ? Call: (18) _22852:γ∈[_22850:_19322, _15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Call: (19) lists:member(_22852:γ, [_22850:_19322, _15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Exit: (19) lists:member(_22850:γ, [_22850:γ, _15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Exit: (18) _22850:γ∈[_22850:γ, _15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Exit: (17) [_22850:γ, _15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_22850:γ ? Exit: (16) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢λ(_22850, _22850):γ⇒γ ? Call: (16) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_19312:γ ? Call: (17) _19312:γ∈[_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Call: (18) lists:member(_19312:γ, [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (18) lists:member(_19312:γ, [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (17) _19312:γ∈[_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Redo: (16) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_19312:γ ? Call: (17) [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]⊢_30506:_30518⇒γ ? Call: (18) _30506:_30518⇒γ∈[_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ] ? Call: (19) lists:member(_30506:_30518⇒γ, [_15764:α, _12218:α⇒β, _8672:α⇒β⇒γ]) ? Fail: (19) lists:member(_270:_282⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (18) _270:_282⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (17) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_270:_282⇒γ ? Call: (18) [_1864:_282, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_1866:γ ? Call: (19) _1866:γ∈[_1864:_282, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (20) lists:member(_1866:γ, [_1864:_282, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (20) lists:member(_1864:γ, [_1864:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (19) _1864:γ∈[_1864:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (18) [_1864:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_1864:γ ? Exit: (17) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_1864, _1864):γ⇒γ ? Call: (17) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_272:γ ? Call: (18) _272:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (19) lists:member(_272:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (19) lists:member(_272:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (18) _272:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (17) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_272:γ ? Call: (18) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_9520:_9532⇒γ ? Call: (19) _9520:_9532⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (20) lists:member(_9520:_9532⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (20) lists:member(_9520:_9532⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (19) _9520:_9532⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (18) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_9520:_9532⇒γ ? Call: (19) [_13060:_9532, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_13062:γ ? Call: (20) _13062:γ∈[_13060:_9532, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (21) lists:member(_13062:γ, [_13060:_9532, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (21) lists:member(_13060:γ, [_13060:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (20) _13060:γ∈[_13060:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (19) [_13060:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_13060:γ ? Exit: (18) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_13060, _13060):γ⇒γ ? Call: (18) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_9522:γ ? Call: (19) _9522:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (20) lists:member(_9522:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (20) lists:member(_9522:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (19) _9522:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (18) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_9522:γ ? Call: (19) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_20716:_20728⇒γ ? Call: (20) _20716:_20728⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (21) lists:member(_20716:_20728⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (21) lists:member(_20716:_20728⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (20) _20716:_20728⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (19) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_20716:_20728⇒γ ? Call: (20) [_24256:_20728, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_24258:γ ? Call: (21) _24258:γ∈[_24256:_20728, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (22) lists:member(_24258:γ, [_24256:_20728, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (22) lists:member(_24256:γ, [_24256:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (21) _24256:γ∈[_24256:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (20) [_24256:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_24256:γ ? Exit: (19) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_24256, _24256):γ⇒γ ? Call: (19) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_20718:γ ? Call: (20) _20718:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (21) lists:member(_20718:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (21) lists:member(_20718:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (20) _20718:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (19) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_20718:γ ? Call: (20) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_31912:_31924⇒γ ? Call: (21) _432:_444⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (22) lists:member(_432:_444⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (22) lists:member(_432:_444⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (21) _432:_444⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (20) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_432:_444⇒γ ? Call: (21) [_3360:_444, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_3362:γ ? Call: (22) _3362:γ∈[_3360:_444, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (23) lists:member(_3362:γ, [_3360:_444, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (23) lists:member(_3360:γ, [_3360:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (22) _3360:γ∈[_3360:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (21) [_3360:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_3360:γ ? Exit: (20) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_3360, _3360):γ⇒γ ? Call: (20) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_434:γ ? Call: (21) _434:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (22) lists:member(_434:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (22) lists:member(_434:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (21) _434:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (20) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_434:γ ? Call: (21) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_11016:_11028⇒γ ? Call: (22) _11016:_11028⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (23) lists:member(_11016:_11028⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (23) lists:member(_11016:_11028⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (22) _11016:_11028⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (21) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_11016:_11028⇒γ ? Call: (22) [_14556:_11028, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_14558:γ ? Call: (23) _14558:γ∈[_14556:_11028, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (24) lists:member(_14558:γ, [_14556:_11028, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (24) lists:member(_14556:γ, [_14556:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (23) _14556:γ∈[_14556:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (22) [_14556:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_14556:γ ? Exit: (21) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_14556, _14556):γ⇒γ ? Call: (21) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_11018:γ ? Call: (22) _11018:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (23) lists:member(_11018:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (23) lists:member(_11018:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (22) _11018:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (21) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_11018:γ ? Call: (22) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_22212:_22224⇒γ ? Call: (23) _22212:_22224⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (24) lists:member(_22212:_22224⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (24) lists:member(_22212:_22224⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (23) _22212:_22224⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (22) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_22212:_22224⇒γ ? Call: (23) [_25752:_22224, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_25754:γ ? Call: (24) _25754:γ∈[_25752:_22224, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (25) lists:member(_25754:γ, [_25752:_22224, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (25) lists:member(_25752:γ, [_25752:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (24) _25752:γ∈[_25752:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (23) [_25752:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_25752:γ ? Exit: (22) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_25752, _25752):γ⇒γ ? Call: (22) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_22214:γ ? Call: (23) _22214:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (24) lists:member(_22214:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (24) lists:member(_22214:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (23) _542:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (22) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_542:γ ? Call: (23) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_1506:_1518⇒γ ? Call: (24) _1506:_1518⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (25) lists:member(_1506:_1518⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (25) lists:member(_1506:_1518⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (24) _1506:_1518⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (23) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_1506:_1518⇒γ ? Call: (24) [_5046:_1518, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_5048:γ ? Call: (25) _5048:γ∈[_5046:_1518, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (26) lists:member(_5048:γ, [_5046:_1518, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (26) lists:member(_5046:γ, [_5046:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (25) _5046:γ∈[_5046:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (24) [_5046:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_5046:γ ? Exit: (23) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_5046, _5046):γ⇒γ ? Call: (23) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_1508:γ ? Call: (24) _1508:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (25) lists:member(_1508:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (25) lists:member(_1508:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (24) _1508:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (23) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_1508:γ ? Call: (24) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_12702:_12714⇒γ ? Call: (25) _12702:_12714⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (26) lists:member(_12702:_12714⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (26) lists:member(_12702:_12714⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (25) _12702:_12714⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (24) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_12702:_12714⇒γ ? Call: (25) [_16242:_12714, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_16244:γ ? Call: (26) _16244:γ∈[_16242:_12714, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (27) lists:member(_16244:γ, [_16242:_12714, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (27) lists:member(_16242:γ, [_16242:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (26) _16242:γ∈[_16242:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (25) [_16242:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_16242:γ ? Exit: (24) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_16242, _16242):γ⇒γ ? Call: (24) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_12704:γ ? Call: (25) _12704:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (26) lists:member(_12704:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (26) lists:member(_12704:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (25) _12704:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (24) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_12704:γ ? Call: (25) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_23898:_23910⇒γ ? Call: (26) _23898:_23910⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (27) lists:member(_23898:_23910⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (27) lists:member(_23898:_23910⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (26) _23898:_23910⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (25) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_23898:_23910⇒γ ? Call: (26) [_27438:_23910, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_27440:γ ? Call: (27) _27440:γ∈[_27438:_23910, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (28) lists:member(_27440:γ, [_27438:_23910, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (28) lists:member(_27438:γ, [_27438:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (27) _27438:γ∈[_27438:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (26) [_27438:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_27438:γ ? Exit: (25) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_27438, _27438):γ⇒γ ? Call: (25) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_23900:γ ? Call: (26) _23900:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (27) lists:member(_704:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (27) lists:member(_704:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (26) _704:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (25) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_704:γ ? Call: (26) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_3116:_3128⇒γ ? Call: (27) _3116:_3128⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (28) lists:member(_3116:_3128⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (28) lists:member(_3116:_3128⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (27) _3116:_3128⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (26) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_3116:_3128⇒γ ? Call: (27) [_6656:_3128, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_6658:γ ? Call: (28) _6658:γ∈[_6656:_3128, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (29) lists:member(_6658:γ, [_6656:_3128, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (29) lists:member(_6656:γ, [_6656:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (28) _6656:γ∈[_6656:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (27) [_6656:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_6656:γ ? Exit: (26) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_6656, _6656):γ⇒γ ? Call: (26) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_3118:γ ? Call: (27) _3118:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (28) lists:member(_3118:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (28) lists:member(_3118:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (27) _3118:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (26) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_3118:γ ? Call: (27) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_14312:_14324⇒γ ? Call: (28) _14312:_14324⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (29) lists:member(_14312:_14324⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (29) lists:member(_14312:_14324⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (28) _14312:_14324⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (27) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_14312:_14324⇒γ ? Call: (28) [_17852:_14324, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_17854:γ ? Call: (29) _17854:γ∈[_17852:_14324, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (30) lists:member(_17854:γ, [_17852:_14324, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (30) lists:member(_17852:γ, [_17852:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Exit: (29) _17852:γ∈[_17852:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Exit: (28) [_17852:γ, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_17852:γ ? Exit: (27) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢λ(_17852, _17852):γ⇒γ ? Call: (27) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_14314:γ ? Call: (28) _14314:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (29) lists:member(_14314:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (29) lists:member(_14314:γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (28) _14314:γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (27) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_14314:γ ? Call: (28) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_25508:_25520⇒γ ? Call: (29) _25508:_25520⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (30) lists:member(_25508:_25520⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (30) lists:member(_25508:_25520⇒γ, [_192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? Fail: (29) _25508:_25520⇒γ∈[_192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Redo: (28) [_192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_25508:_25520⇒γ ? Call: (29) [_29048:_25520, _192:α, _168:α⇒β, _144:α⇒β⇒γ]⊢_29050:γ ? Call: (30) _29050:γ∈[_29048:_25520, _192:α, _168:α⇒β, _144:α⇒β⇒γ] ? Call: (31) lists:member(_29050:γ, [_29048:_25520, _192:α, _168:α⇒β, _144:α⇒β⇒γ]) ? a % Execution Aborted [trace] ?- Call: (19) prolog_load_file(user:'/home/trifon/fmisync/Courses/2022_23/LCPT_2022_23/sandbox/typeinh.pro', [expand(false), expand(true)]) ? a % Execution Aborted [trace] ?- notrace. true. [debug] ?- nodebug. true. ?- Welcome to SWI-Prolog (threaded, 64 bits, version 8.4.2) SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software. Please run ?- license. for legal details. For online help and background, visit https://www.swi-prolog.org For built-in help, use ?- help(Topic). or ?- apropos(Word). ?- true. ?- ti(TI), ⊢ I : TI. ERROR: Unknown procedure: (⊢)/1 ERROR: However, there are definitions for: ERROR: (⊢)/2 false. ?- true. ?- ti(TI), ⊢ I : TI. TI = α⇒α, I = λ(_A, _A) ; false. ?- tk(TK), ⊢ K : TK. TK = α⇒β⇒α, K = λ(_A, λ(_, _A)) ; false. ?- ts(TS), ⊢ S : TS. TS = (α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ, S = λ(_A, λ(_B, λ(_C, _A@_C@(_B@_C)))) ?- tn(TN), ⊢ N : TN. TN = (α⇒α)⇒α⇒α, N = λ(_, λ(_A, _A)) ; TN = (α⇒α)⇒α⇒α, N = λ(_A, λ(_B, _A@_B)) ; TN = (α⇒α)⇒α⇒α, N = λ(_A, λ(_B, _A@(_A@_B))) ; TN = (α⇒α)⇒α⇒α, N = λ(_A, λ(_B, _A@(_A@(_A@_B)))) ; TN = (α⇒α)⇒α⇒α, N = λ(_A, λ(_B, _A@(_A@(_A@(_A@_B))))) ; TN = (α⇒α)⇒α⇒α, N = λ(_A, λ(_B, _A@(_A@(_A@(_A@(_A@_B)))))) ; TN = (α⇒α)⇒α⇒α, N = λ(_A, λ(_B, _A@(_A@(_A@(_A@(_A@(_A@_B))))))) ?- ⊢ M : α. false. ?- ⊢ M : (α ⇒ α) ⇒ α. C-c C-cAction (h for help) ? a abort % Execution Aborted ?- ⊢ M : α ⇒ (β ⇒ α) ⇒ (α ⇒ β) ⇒ α. C-c C-cAction (h for help) ? a abort % Execution Aborted ?- ⊢ M : (β ⇒ α) ⇒ (α ⇒ β) ⇒ α ⇒ α. M = λ(_, λ(_, λ(_A, _A))) ; M = λ(_A, λ(_B, λ(_C, _A@(_B@_C)))) ; M = λ(_A, λ(_B, λ(_C, _A@(_B@(_A@(_B@_C)))))) ; M = λ(_A, λ(_B, λ(_C, _A@(_B@(_A@(_B@(_A@(_B@_C)))))))) ; M = λ(_A, λ(_B, λ(_C, _A@(_B@(_A@(_B@(_A@(_B@(... @ ...))))))))) ?- ⊢ M : α ⇒ (β ⇒ α) ⇒ (α ⇒ β) ⇒ α. C-c C-cAction (h for help) ? a abort % Execution Aborted ?-