Welcome to SWI-Prolog (threaded, 64 bits, version 8.2.4)
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).

?- ERROR: /home/trifon/fmisync/Courses/2021_22/LCPT_2021_22/sandbox/typeinh.pro:31:2: Syntax error: Operator expected
ERROR: /home/trifon/fmisync/Courses/2021_22/LCPT_2021_22/sandbox/typeinh.pro:32:3: Syntax error: Operator expected
ERROR: /home/trifon/fmisync/Courses/2021_22/LCPT_2021_22/sandbox/typeinh.pro:51:18: Syntax error: Operator expected
true.

?- Warning: /home/trifon/fmisync/Courses/2021_22/LCPT_2021_22/sandbox/typeinh.pro:48:
Warning:    Singleton variables: [Σ]
true.

?- true.

?- ts(TS), ⊢ S : TS.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- ti(TI), ⊢ I : TI.
  C-c C-cAction (h for help) ? 
Unknown option (h for help)
Action (h for help) ? a
abort
% Execution Aborted
?- trace.
true.

[trace]  ?- ti(TI), ⊢ I : TI.
   Call: (11) ti(_1776) ? 
   Exit: (11) ti(α⇒α) ? 
   Call: (11) ⊢_1780:α⇒α ? 
   Call: (12) []⊢_1780:α⇒α ? 
   Call: (13) functional(α⇒α) ? 
   Exit: (13) functional(α⇒α) ? 
   Call: (13) deconstruct(_2592, _2594, α⇒α) ? 
   Exit: (13) deconstruct([], α⇒α, α⇒α) ? 
   Call: (13) extendContext([], _2682, [], _2686) ? 
   Exit: (13) extendContext([], [], [], []) ? 
   Call: (13) []⊢_2716:α⇒α ? 
   Call: (14) functional(α⇒α) ? 
   Exit: (14) functional(α⇒α) ? 
   Call: (14) deconstruct(_2906, _2908, α⇒α) ? 
   Exit: (14) deconstruct([], α⇒α, α⇒α) ? 
   Call: (14) extendContext([], _2996, [], _3000) ? 
   Exit: (14) extendContext([], [], [], []) ? 
   Call: (14) []⊢_3030:α⇒α ? 
   Call: (15) functional(α⇒α) ? 
   Exit: (15) functional(α⇒α) ? 
   Call: (15) deconstruct(_3220, _3222, α⇒α) ? 
   Exit: (15) deconstruct([], α⇒α, α⇒α) ? 
   Call: (15) extendContext([], _3310, [], _3314) ? 
   Exit: (15) extendContext([], [], [], []) ? 
   Call: (15) []⊢_3344:α⇒α ? 
   Call: (16) functional(α⇒α) ? 
   Exit: (16) functional(α⇒α) ? 
   Call: (16) deconstruct(_3534, _3536, α⇒α) ? 
   Exit: (16) deconstruct([], α⇒α, α⇒α) ? 
   Call: (16) extendContext([], _3624, [], _3628) ? 
   Exit: (16) extendContext([], [], [], []) ?   C-c C-c
Action (h for help) ? a
EOF: exit (status 4)

Process prolog exited abnormally with code 4
Welcome to SWI-Prolog (threaded, 64 bits, version 8.2.4)
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 = λ(_3444, _3444) ;
false.

?- tk(TK), ⊢ K : TK.
TK = α⇒β⇒α,
K = λ(_6518, λ(_6536, _6518)) ;
false.

?- ts(TS), ⊢ S : TS.
TS =  (α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ,
S = λ(_8632, λ(_8650, λ(_8668, _8632@_8668@(_8650@_8668)))) ;
false.

?- tc(TC), ⊢ C : TC.
ERROR: Unknown procedure: tc/1 (DWIM could not correct goal)
?- true.

?- tc(TC), ⊢ C : TC.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- trace.
true.

[trace]  ?- tc(TC), ⊢ C : TC.
   Call: (11) tc(_1776) ? 
   Exit: (11) tc((α⇒α)⇒α⇒α) ? 
   Call: (11) ⊢_1780:(α⇒α)⇒α⇒α ? 
   Call: (12) []⊢_1780:(α⇒α)⇒α⇒α ? 
   Call: (13) functional((α⇒α)⇒α⇒α) ? 
   Exit: (13) functional((α⇒α)⇒α⇒α) ? 
   Call: (13) deconstruct(_2604, _2606,  (α⇒α)⇒α⇒α) ? 
   Call: (14) deconstruct(_2598, _2656, α⇒α) ? 
   Call: (15) deconstruct(_2648, _2706, α) ? 
   Exit: (15) deconstruct([], α, α) ? 
   Exit: (14) deconstruct([α], α, α⇒α) ? 
   Exit: (13) deconstruct([α⇒α, α], α,  (α⇒α)⇒α⇒α) ? 
   Call: (13) extendContext([], _2882, [α⇒α, α], _2886) ? 
   Call: (14) extendContext([], _2874, [α], _2880) ? 
   Call: (15) extendContext([], _2936, [], _2942) ? 
   Exit: (15) extendContext([], [], [], []) ? 
   Exit: (14) extendContext([], [_2934], [α], [_2934:α]) ? 
   Exit: (13) extendContext([], [_2872, _2934], [α⇒α, α], [_2872:α⇒α, _2934:α]) ? 
   Call: (13) [_2872:α⇒α, _2934:α]⊢_3128:α ? 
   Call: (14) lists:member(_3178:_3180, [_2872:α⇒α, _2934:α]) ? 
   Exit: (14) lists:member(_2872:α⇒α, [_2872:α⇒α, _2934:α]) ? 
   Call: (14) deconstruct(_3324, α, α⇒α) ? 
   Call: (15) deconstruct(_3318, α, α) ? 
   Exit: (15) deconstruct([], α, α) ? 
   Exit: (14) deconstruct([α], α, α⇒α) ? 
   Call: (14) [_2872:α⇒α, _2934:α]⊩_3454:[α] ? 
   Call: (15) [_2872:α⇒α, _2934:α]⊢_3504:α ? 
   Call: (16) lists:member(_3560:_3562, [_2872:α⇒α, _2934:α]) ?   C-c C-c
Action (h for help) ? a
EOF: exit (status 4)

Process prolog exited abnormally with code 4
Welcome to SWI-Prolog (threaded, 64 bits, version 8.2.4)
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).

?- tc(TC), ⊢ C : TC.
TC =  (α⇒α)⇒α⇒α,
C = λ(_8666, λ(_8684, _8684)) 

?- ti(TI), ⊢ I : TI.
TI = α⇒α,
I = λ(_534, _534) ;
TI = α⇒α,
I = λ(_534, _534) ;
false.

?- ti(TI), ⊢ I : TI.
TI = α⇒α,
I = λ(_3630, _3630) 

?- ti(TI), ⊢ I : TI.
TI = α⇒α,
I = λ(_5662, _5662) ;
TI = α⇒α,
I = λ(_5662, _5662) ;
false.

?- true.

?- ti(TI), ⊢ I : TI.
TI = α⇒α,
I = λ(_536, _536) ;
false.

?- tk(TK), ⊢ K : TK.
TK = α⇒β⇒α,
K = λ(_2590, λ(_2608, _2590)) ;
false.

?- ts(TS), ⊢ S : TS.
TS =  (α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ,
S = λ(_4698, λ(_4716, λ(_4734, _4698@_4734@(_4716@_4734)))) ;
false.

?- ⊢ M : α.
false.

?- ⊢ M : (β ⇒ β) ⇒ α.
false.

?- ⊢ M : (α ⇒ α) ⇒ α.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- ⊢ M : ((α ⇒ α) ⇒ α) ⇒ α.
M = λ(_898, _898@λ(_958, _958)) ;
false.

?- ⊢ M : (α ⇒ β) ⇒ (β ⇒ α) ⇒ α.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- true.

?- ⊢ M : (α ⇒ β) ⇒ (β ⇒ α) ⇒ α.
false.

?- ⊢ M : (α ⇒ α) ⇒ α.
false.

?- ti(TI), ⊢ I : TI.
TI = α⇒α,
I = λ(_4454, _4454) ;
false.

?- tk(TK), ⊢ K : TK.
TK = α⇒β⇒α,
K = λ(_6550, λ(_6568, _6550)) ;
false.

?- ts(TS), ⊢ S : TS.
TS =  (α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ,
S = λ(_8700, λ(_8718, λ(_8736, _8700@_8736@(_8718@_8736)))) ;
false.