NuITP (alpha 30) ProofProved


Goal

False = alter($2:List $1:Card $1:Card $3:List)

Script

set goal alter(L1:List C1:Card C1:Card L2:List) = False .
apply gsi* to 0 on $2 .
apply gsi! to 0.1.1 on $4 .
apply cas! to 0.1.1.3 on $5 .
apply cas! to 0.1.1.4 on $5 .
apply gsi! to 0.1.2 on $4 .
apply cas! to 0.1.2.3 on $5 .
apply cas! to 0.1.2.4 on $5 .

Rewriting Theory

fmod GILBREATH-ACU is
sorts Boolean Card List NeList .
subsort Card < NeList .
subsort NeList < List .
op False : -> Boolean [ ctor metadata "1" ] .
op True : -> Boolean [ ctor metadata "0" ] .
op __ : List List -> List [ assoc id: nil metadata "5" ] .
op __ : NeList NeList -> NeList [ assoc ctor id: nil metadata "5" ] .
op alter : List -> Boolean [ metadata "8" ] .
op black : -> Card [ ctor metadata "3" ] .
op even : List -> Boolean [ metadata "11" ] .
op neg : Card -> Card [ metadata "12" ] .
op nil : -> List [ ctor metadata "2" ] .
op opposite : List List -> Boolean [ metadata "7" ] .
op paired : Card Card -> Boolean [ metadata "6" ] .
op pairedList : List -> Boolean [ metadata "9" ] .
op red : -> Card [ ctor metadata "4" ] .
op rotate : List -> List [ metadata "13" ] .
op shuffle : List List List -> Boolean [ metadata "10" ] .
eq alter(C:Card) = True .
eq alter(nil) = True .
eq even(C:Card) = False .
eq even(nil) = True .
eq even(L1:List C1:Card L2:List C2:Card L3:List) = even(L1:List L2:List L3:List) .
eq neg(black) = red [ variant ] .
eq neg(red) = black [ variant ] .
eq opposite(L:List, nil) = False [ variant ] .
eq opposite(nil, L:List) = False [ variant ] .
eq opposite(C1:Card L1:List, C2:Card L2:List) = paired(C1:Card, C2:Card) [ variant ] .
eq paired(C:Card, C:Card) = False [ variant ] .
eq paired(black, red) = True [ variant ] .
eq paired(red, black) = True [ variant ] .
eq pairedList(C:Card) = False .
eq pairedList(nil) = True .
eq pairedList(C:Card C:Card L:List) = False .
eq rotate(nil) = nil [ variant ] .
eq rotate(C:Card L:List) = L:List C:Card [ variant ] .
eq shuffle(L1:List, C2:Card L2:List, nil) = False .
eq shuffle(nil, nil, nil) = True .
eq shuffle(nil, nil, C3:Card L3:List) = False .
eq shuffle(C1:Card L1:List, L2:List, nil) = False .
ceq alter(C1:Card C2:Card L:List) = False if paired(C1:Card, C2:Card) = False .
ceq alter(C1:Card C2:Card L:List) = alter(C2:Card L:List) if paired(C1:Card, C2:Card) = True .
ceq pairedList(C1:Card C2:Card L:List) = pairedList(L:List) if paired(C1:Card, C2:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = shuffle(nil, L2:List, L3:List) if paired(C2:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = shuffle(L1:List, nil, L3:List) if paired(C1:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ paired(C2:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True /\ shuffle(L1:List, C2:Card L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if shuffle(L1:List, C2:Card L2:List, L3:List) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C1:Card, C3:Card) = False /\ shuffle(L1:List, C2:Card L2:List, L3:List) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C2:Card, C3:Card) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = True .
endfm

Goals

Goal Id:  0
Generated By:  init
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter($2:List $1:Card $1:Card $3:List)
Goal Id:  0.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter($4:NeList $1:Card $1:Card $3:List)
Goal Id:  0.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter($1:Card $1:Card $3:List)
Goal Id:  0.1.1
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter($4:NeList black black $3:List)
Goal Id:  0.1.2
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter($4:NeList red red $3:List)
Goal Id:  0.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter(black black black $3:List)
Goal Id:  0.1.1.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter(red black black $3:List)
Goal Id:  0.1.1.3
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
alter($5 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(black $5 black black $3:List)
Goal Id:  0.1.1.4
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
alter($5 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(red $5 black black $3:List)
Goal Id:  0.1.2.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter(black red red $3:List)
Goal Id:  0.1.2.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = alter(red red red $3:List)
Goal Id:  0.1.2.3
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
alter($5 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(black $5 red red $3:List)
Goal Id:  0.1.2.4
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
alter($5 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(red $5 red red $3:List)
Goal Id:  0.1.1.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.3.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
False = alter(black black black black $3:List)
Goal Id:  0.1.1.3.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
False = alter(black red black black $3:List)
Goal Id:  0.1.1.3.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(black black $6 black black $3:List)
Goal Id:  0.1.1.3.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(black red $6 black black $3:List)
Goal Id:  0.1.1.4.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
False = alter(red black black black $3:List)
Goal Id:  0.1.1.4.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
False = alter(red red black black $3:List)
Goal Id:  0.1.1.4.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(red black $6 black black $3:List)
Goal Id:  0.1.1.4.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(red red $6 black black $3:List)
Goal Id:  0.1.2.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.3.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
False = alter(black black red red $3:List)
Goal Id:  0.1.2.3.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
False = alter(black red red red $3:List)
Goal Id:  0.1.2.3.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(black black $6 red red $3:List)
Goal Id:  0.1.2.3.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(black red $6 red red $3:List)
Goal Id:  0.1.2.4.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
False = alter(red black red red $3:List)
Goal Id:  0.1.2.4.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
False = alter(red red red red $3:List)
Goal Id:  0.1.2.4.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(red black $6 red red $3:List)
Goal Id:  0.1.2.4.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
False = alter(red red $6 red red $3:List)
Goal Id:  0.1.1.3.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.3.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.3.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.3.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.4.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.4.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.4.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.1.4.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 black black $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.3.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.3.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.3.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.3.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.4.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.4.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.4.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
alter(black $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.4.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
alter(red $6 red red $3:List) ⇒ False
Non-Executable Hypotheses:
None
Goal:
true

Proof Tree