##
##  Wrong Type Instantiation of the Axiom of Choice (Creating a Scope Violation)
##
##
##  Source: [Kubota 2018 (new)]
##
##  Copyright (c) 2018 Owl of Minerva Press GmbH. All rights reserved.
##  Written by Ken Kubota (<mail@kenkubota.de>).
##
##  This file is part of the publication of the mathematical logic R0.
##  For more information, visit: <http://doi.org/10.4444/100.10>
##

<< definitions1.r0.txt
<< K8005.r0.txt


##
##  Axiom of Choice
##
##  Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 236]
##

:= AC ((E{{{o,{o,\3{^}}},^}}_{t{^},{o,t{^}}}{^}){{o,{o,{t{^},{o,t{^}}}}}}_[\j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}.((A{{{o,{o,\3{^}}},^}}_{o,t{^}}{^}){{o,{o,{o,t{^}}}}}_[\p{{o,t{^}}}{{o,t{^}}}.((=>{{{o,o},o}}_((E{{{o,{o,\3{^}}},^}}_t{^}{^}){{o,{o,t{^}}}}_[\x{t{^}}{t{^}}.(p{{o,t{^}}}{{o,t{^}}}_x{t{^}}{t{^}}){o}]{{o,t{^}}}){o}){{o,o}}_(p{{o,t{^}}}{{o,t{^}}}_(j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){t{^}}){o}){o}]{{o,{o,t{^}}}}){o}]{{o,{t{^},{o,t{^}}}}})


## .1

%K8005

## use Proof Template A5221 (Sub):  B  -->  B [x/A]
:= $B5221 %0
:= $T5221 o
:= $X5221 x{$T5221}
:= $A5221 AC
<< A5221.r0t.txt
:= $B5221; := $T5221; := $X5221; := $A5221
%0


## .2

## use Proof Template A5221H (Sub):  H => B  -->  H => B [x/A in B]
:= $B5221H %0
:= $T5221H ^
:= $X5221H t{$T5221H}
:= $A5221H o
<< A5221H.r0t.txt
:= $B5221H; := $T5221H; := $X5221H; := $A5221H
%0